proposition: Theorem WhileStep_Terminates : exists C1 C2, projT1 (StateWhile Step (start M)) ↓ fun t k => exists t_sig, t = [| encode_tape' t_sig |] /\ exists k' t_sig' q', loopM (initc M [| t_sig |]) k' = Some (mk_mconfig q' [| t_sig' |] ) /\ k >= C1 * k' + C2.
proof: Proof. unfold initc. generalize (start M). intros q. destruct (Step_total') as [C HC]. exists (1 + C), (2 + 2 * C). eapply TerminatesIn_monotone. { eapply StateWhile_TerminatesIn. { intros. eapply Step_Realise. } intros. eapply HC. } revert q. eapply StateWhileCoInduction. intros q tin k H. TMSimp. rename ymid0 into steps, ymid into t_sig, ymid1 into t_sig', ymid2 into q'. remember [|t_sig|] as tin. remember [|t_sig'|] as tout. rename H0 into H. rename H1 into H0. induction steps in tin, t_sig, Heqtin, q, H0, H |- *. - cbn in H. unfold haltConf in H. cbn in *. destruct (halt q) eqn:Eq; cbn. + inv H. eexists. split. { apply Nat.le_refl. } intros. rewrite (destruct_tape tmid) in *. specialize (H _ eq_refl) as [-> _]. lia. + inv H. - cbn in H. unfold haltConf in H. cbn in *. destruct (halt q) eqn:Eq; cbn. + inv H. eexists. split. { apply Nat.le_refl. } intros. rewrite (destruct_tape tmid) in *. specialize (H _ eq_refl) as [-> _]. lia. + subst. unfold step in H. cbn in *. unfold current_chars in *. cbn in *. destruct trans as (qnxt, A) eqn:Et. cbn in *. rewrite (destruct_vector_single A) in *. destruct (Vector.hd A) as [c' m]. cbn in *. pose proof (Hrem := H). eapply IHsteps in H. { eexists. split. { apply Nat.le_refl. } intros. specialize (H1 _ eq_refl). rewrite Et in H1. destruct H1. subst. repeat eexists. { rewrite <- Hrem. repeat f_equal. now destruct t_sig, m, c'. } { apply Nat.le_refl. } lia. } { reflexivity. } lia. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString