proposition: Lemma DoActions_Loop_Realise (i : Fin.t n) : DoActions_Loop i ⊨ DoActions_Loop_Rel i.
proof: Proof. eapply Realise_monotone. { unfold DoActions_Loop. now auto with nocore TMdb. } { revert i; apply StateWhileInduction; intros; rename l into i. { split. { intros tps1 tps2 tp HL1 HL2 HCons. TMSimp. rename H into HCaseCons, H0 into HCaseNil. specialize HCaseCons with (3 := HCons). do 2 spec_assert HCaseCons by now rewrite map_vect_list_length. destruct tps2 as [ | tp' tps']; destruct HCaseCons as [HCaseCons1 HCaseCons2]. - apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2; cbn in *. assert (S (fin_to_nat i) = n) by lia. clear HCaseCons2. replace (map_vect_list (doAct (sig:=eqType_X (type sig))) acts (tps1 ++ [tp])) with (map_vect_list (doAct (sig:=eqType_X (type sig))) acts tps1 ++ [doAct tp acts[@i]]); auto. symmetry. apply map_vect_list_app. lia. - apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2; cbn in *. assert (S (fin_to_nat i) < n) by lia. apply finSucc_opt_Some in H as (i'&H). rewrite H in HCaseCons2. inv HCaseCons2. } { intros tps HNil. TMSimp. now specialize H0 with (1 := HNil). } } { split. { intros tps1 tps2 tp HL1 HL2 HCons. TMSimp. rename H1 into HCaseCons1, H2 into HCaseNil1, H into HCaseCons2, H0 into HCaseNil2. specialize HCaseCons1 with (3 := HCons). do 2 spec_assert HCaseCons1 by now rewrite map_vect_list_length. destruct tps2 as [ | tp' tps2']. - destruct HCaseCons1 as [ _ ? ]. inv H. - destruct HCaseCons1 as [ HCaseCons1 ? ]. destruct (finSucc_opt i) as [ i' | ] eqn:E; [|easy]. inv H. apply Nat.eqb_eq in HL1; apply Nat.eqb_eq in HL2; cbn in *. rewrite <- map_vect_list_app in HCaseCons1 by lia. specialize HCaseCons2 with (3 := HCaseCons1). spec_assert HCaseCons2. { apply Nat.eqb_eq. rewrite app_length. cbn. enough (fin_to_nat i' = S (fin_to_nat i)) by lia. now apply finSucc_opt_Some'. } spec_assert HCaseCons2. { apply Nat.eqb_eq. rewrite app_length. cbn. lia. } rewrite <- app_assoc in HCaseCons2. cbn in *. auto. } { intros tps HNil. TMSimp. now specialize H2 with (1 := HNil). } } } 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)