Commit 2026-02-17 15:39 80378d40

View on Github →

refactor(Computability): file for state transition systems (#33291) This PR makes a new file to contain content having to do with state transition systems defined by a function σ → Option σ. This content was previously split over PostTuringMachine.lean and TMComputable.lean, but since these definitions don't only apply to Turing machines in particular, it seems sensible to refactor them and remove them from the Turing namespace and put them in a new StateTransition namespace.

Estimated changes

deleted def Turing.FRespects
deleted theorem Turing.Reaches.to₀
deleted def Turing.Reaches
deleted theorem Turing.Reaches₀.head
deleted theorem Turing.Reaches₀.refl
deleted theorem Turing.Reaches₀.single
deleted theorem Turing.Reaches₀.tail'
deleted theorem Turing.Reaches₀.tail
deleted theorem Turing.Reaches₀.trans
deleted def Turing.Reaches₀
deleted theorem Turing.Reaches₁.to₀
deleted def Turing.Reaches₁
deleted def Turing.Respects
deleted def Turing.eval
deleted theorem Turing.eval_maximal
deleted theorem Turing.eval_maximal₁
deleted theorem Turing.frespects_eq
deleted theorem Turing.fun_respects
deleted theorem Turing.mem_eval
deleted theorem Turing.reaches_eval
deleted theorem Turing.reaches_total
deleted theorem Turing.reaches₀_eq
deleted theorem Turing.reaches₁_eq
deleted theorem Turing.reaches₁_fwd
deleted theorem Turing.tr_eval'
deleted theorem Turing.tr_eval
deleted theorem Turing.tr_eval_dom
deleted theorem Turing.tr_eval_rev
deleted theorem Turing.tr_reaches
deleted theorem Turing.tr_reaches_rev
deleted theorem Turing.tr_reaches₁
added structure StateTransition.EvalsTo