Theorems · Theorem · logic and foundations

Turing.ToPartrec.stepNormal_then

∀ (c : Turing.ToPartrec.Code) (k k' : Turing.ToPartrec.Cont) (v : List ℕ),
  Turing.ToPartrec.stepNormal c (k.then k') v = (Turing.ToPartrec.stepNormal c k v).then k'

The stepNormal function respects the then k' homomorphism. Note that this is an exact equality, not a simulation; the original and embedded machines move in lock-step until the embedded machine reaches the halt state.

Defined in

Mathlib.Computability.TuringMachine.Config

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound