proposition: Lemma Sim_Terminates {Σ} (L : finType) (M : pTM Σ L 1) T : projT1 M ↓ T -> exists C1 C2, projT1 (Relabel (StateWhile (@Step Σ (projT1 M)) (start (projT1 M))) (projT2 M)) ↓ fun t k => exists t_sig k', t = [| encode_tape' t_sig |] /\ T [| t_sig |] k' /\ k >= C1 * k' + C2.
proof: Proof. intros HM. destruct (WhileStep_Terminates (projT1 M)) as (C1 & C2 & HC). exists C1, C2. eapply TerminatesIn_monotone. { eapply Relabel_Terminates, HC. } intros ? ? ?. TMSimp. eapply HM in H0. TMSimp. destruct ymid1. rewrite (destruct_tape ctapes) in *. repeat eexists; eassumption. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString