Theorems · Theorem · logic and foundations

Turing.ToPartrec.Cont.then.eq_def

∀ (x : Turing.ToPartrec.Cont),
  x.then =
    match (motive := Turing.ToPartrec.Cont → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont) x with
    | Turing.ToPartrec.Cont.halt => fun k' => k'
    | Turing.ToPartrec.Cont.cons₁ fs as k => fun k' => Turing.ToPartrec.Cont.cons₁ fs as (k.then k')
    | Turing.ToPartrec.Cont.cons₂ ns k => fun k' => Turing.ToPartrec.Cont.cons₂ ns (k.then k')
    | Turing.ToPartrec.Cont.comp f k => fun k' => Turing.ToPartrec.Cont.comp f (k.then k')
    | Turing.ToPartrec.Cont.fix f k => fun k' => Turing.ToPartrec.Cont.fix f (k.then k')

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms