proposition: Lemma Loop_steps_eq q T k : Loop_steps q T k = if halt q then 0 else match k with | 0 => 0 | S k' => let (q', acts) := trans (m := projT1 pM) (q, current_chars T) in 1 + Step_steps q T + Loop_steps q' (doAct_multi T acts) k' end.
proof: Proof. destruct k; auto. Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)