Theorems · Theorem · logic and foundations

Turing.ToPartrec.stepNormal.eq_def

∀ (x : Turing.ToPartrec.Code),
  Turing.ToPartrec.stepNormal x =
    match (motive := Turing.ToPartrec.Code → Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg) x with
    | Turing.ToPartrec.Code.zero' => fun k v => Turing.ToPartrec.Cfg.ret k (0 :: v)
    | Turing.ToPartrec.Code.succ => fun k v => Turing.ToPartrec.Cfg.ret k [v.headI.succ]
    | Turing.ToPartrec.Code.tail => fun k v => Turing.ToPartrec.Cfg.ret k v.tail
    | f.cons fs => fun k v => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.cons₁ fs v k) v
    | f.comp g => fun k v => Turing.ToPartrec.stepNormal g (Turing.ToPartrec.Cont.comp f k) v
    | f.case g => fun k v =>
      Nat.rec (Turing.ToPartrec.stepNormal f k v.tail) (fun y x => Turing.ToPartrec.stepNormal g k (y :: v.tail))
        v.headI
    | f.fix => fun k v => Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms