proposition: Lemma DoActions_Loop_Terminates (i : Fin.t n) : projT1 (DoActions_Loop i) ↓ DoActions_Loop_T i.
proof: Proof. eapply TerminatesIn_monotone. { unfold DoActions_Loop. now auto with nocore TMdb. } { revert i. apply StateWhileCoInduction; intros i; intros. destruct HT as [ (tps1&tps2&tp&HL1&HL2&HCons&Hk) | (tps&HNil&Hk) ]. { exists (DoActions_Step_steps_cons i tps1 tps2 tp). repeat split. { hnf. left. eauto 7. } intros ymid mmid (HStep_cons&HStep_nil). destruct ymid as [ i' | [] ]. { specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons). destruct tps2 as [ | tp' tps2']; cbn in *. - destruct HStep_cons as (?&?); congruence. - destruct HStep_cons as [HStep_cons HStep_cons']. destruct (finSucc_opt i) as [ iSucc | ] eqn:Ei; [|easy]. inv HStep_cons'. rename iSucc into i'. eexists. split; [| now eauto]. { hnf. left. exists (tps1 ++ [doAct tp acts[@i]]), tps2', tp'. simpl_list. cbn. apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. apply finSucc_opt_Some' in Ei. repeat split; auto; apply Nat.eqb_eq; lia. } } { specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons). destruct tps2 as [ | tp' tps2']; cbn in *. - destruct HStep_cons as (HStep_cons&_). auto. - destruct HStep_cons as (?&?). destruct (finSucc_opt i); easy. } } { exists (DoActions_Step_steps_nil). repeat split. { hnf. right. eauto. } intros ymid tmid (HStep_cons&HStep_nil). destruct ymid as [ i' | ]; cbn in *. - specialize HStep_nil with (1 := HNil) as (HStep_nil&HStep_nil'); inv HStep_nil'. - specialize HStep_nil with (1 := HNil) as (HStep_nil&HStep_nil'); inv HStep_nil'. 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)