Theorems · Definition · logic and foundations

Turing.TM0.Reaches

{Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Λ] →
      [inst_1 : Inhabited Γ] → Turing.TM0.Machine Γ Λ → Turing.TM0.Cfg Γ Λ → Turing.TM0.Cfg Γ Λ → Prop

The statement Reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps.

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

InhabitedInhabited