fact: Definition Step_Rel : pRel sigSim (state (projT1 pM) + F) 1 := fun tin '(yout, tout) => forall (T : tapes sig n), tin[@Fin0] ≃ T -> if halt q then tout[@Fin0] ≃ T /\ yout = inr (projT2 pM q) else let c := {| cstate := q; ctapes := T |} in let (q', T') := step c in tout[@Fin0] ≃ T' /\ yout = inl q'.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)