Theorems · Theorem · logic and foundations

Turing.PartrecToTM2.trNormal.eq_def

∀ (x : Turing.ToPartrec.Code) (x_1 : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trNormal x x_1 =
    match x, x_1 with
    | Turing.ToPartrec.Code.zero', k =>
      Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.main (fun x => some Turing.PartrecToTM2.Γ'.cons)
        (Turing.PartrecToTM2.Λ'.ret k)
    | Turing.ToPartrec.Code.succ, k =>
      Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret k).succ
    | Turing.ToPartrec.Code.tail, k =>
      Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.Λ'.ret k)
    | f.cons fs, k =>
      Turing.PartrecToTM2.Λ'.push Turing.PartrecToTM2.K'.stack (fun x => some Turing.PartrecToTM2.Γ'.consₗ)
        (Turing.PartrecToTM2.Λ'.move (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.rev
          (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.cons₁ fs k)).copy)
    | f.comp g, k => Turing.PartrecToTM2.trNormal g (Turing.PartrecToTM2.Cont'.comp f k)
    | f.case g, k => (Turing.PartrecToTM2.trNormal f k).pred (Turing.PartrecToTM2.trNormal g k)
    | f.fix, k => Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k)

Defined in

Mathlib.Computability.TuringMachine.ToPartrec

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext