proposition: Lemma GoToNext_Realise : GoToNext ⊨ GoToNext_Rel.
proof: Proof. eapply Realise_monotone. { unfold GoToNext. now auto with nocore TMdb. } { intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons_current in *. TMSimp. TMSimp. rename H1 into H. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp; rename H into HNil, H0 into HCons. { destruct tps2 as [ | tp' tps2']; cbn in *. - specialize (HNil (tps1 ++ [niltape _])). spec_assert HNil as [HNil ->]; auto. do 2 (rewrite MoveToSymbol_Fun_equation; cbn). hnf. cbv [id]. hnf. f_equal. rewrite encode_list_app. rewrite removelast_app by apply encode_list_neq_nil. cbn. rewrite rev_app_distr. cbn. f_equal. - specialize (HCons (tps1 ++ [niltape _]) tps2' tp'). spec_assert HCons as [HCons ->]; auto. do 2 (rewrite MoveToSymbol_Fun_equation; cbn). cbv [id]. hnf. f_equal. + rewrite encode_list_app; cbn. rewrite removelast_app by congruence. cbn. rewrite rev_app_distr. cbn. f_equal. + rewrite !List.map_map. rewrite !map_app, <- !app_assoc. now rewrite !List.map_map. } { destruct tps2 as [ | tp' tps2']; cbn in *. - specialize (HNil (tps1 ++ [leftof r rs])). spec_assert HNil as [HNil ->]; auto. rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))). rewrite MoveToSymbol_correct_midtape; cbn in *; auto. + rewrite !map_id; cbv [id]. hnf. f_equal. simpl_list. cbn. rewrite encode_list_app. cbn. rewrite !map_app. cbn. rewrite !removelast_app by congruence. rewrite !removelast_cons by congruence. rewrite removelast_cons. 2: { intros H. symmetry in H. now apply app_cons_not_nil in H. } rewrite removelast_app by congruence. cbn. rewrite app_nil_r. rewrite rev_app_distr. cbn. rewrite <- !app_assoc. rewrite !rev_app_distr, <- !app_assoc. cbn. rewrite !map_rev. rewrite map_app, <- !app_assoc. cbn. rewrite !map_rev, !List.map_map. f_equal. + intros ? [ <- | [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff ]; cbn; auto. - specialize (HCons (tps1 ++ [leftof r rs]) tps2' tp'). spec_assert HCons as [HCons ->]; auto. rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))). rewrite MoveToSymbol_correct_midtape; cbn in *; auto. + rewrite !map_id; cbv [id]. hnf. f_equal. * simpl_list. cbn. rewrite encode_list_app. cbn. rewrite !map_app. cbn. rewrite !removelast_app by congruence. rewrite !removelast_cons by congruence. rewrite removelast_cons. 2: { intros H. symmetry in H. now apply app_cons_not_nil in H. } rewrite removelast_app by congruence. cbn. rewrite app_nil_r. rewrite rev_app_distr. cbn. rewrite <- !app_assoc. rewrite !rev_app_distr, <- !app_assoc. cbn. rewrite !map_rev. rewrite map_app, <- !app_assoc. cbn. rewrite !map_rev, !List.map_map. f_equal. * now simpl_list. + intros ? [ <- | [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff ]; cbn; auto. } { destruct tps2 as [ | tp' tps2']; cbn in *. - specialize (HNil (tps1 ++ [rightof l ls])). spec_assert HNil as [HNil ->]; auto. do 2 (rewrite MoveToSymbol_Fun_equation; cbn). cbv [id]. hnf. f_equal. rewrite encode_list_app. cbn. rewrite removelast_app by congruence. rewrite !removelast_cons. 3: congruence. 2: { intros H; symmetry in H; now apply app_cons_not_nil in H. } rewrite map_app, !List.map_map, <- !app_assoc. cbn. rewrite removelast_app by congruence. cbn. rewrite rev_app_distr; cbn. rewrite <- !app_assoc. cbn. rewrite !map_app, <- !app_assoc. rewrite !rev_app_distr. cbn. rewrite !map_rev, rev_involutive. rewrite !List.map_map. reflexivity. - specialize (HCons (tps1 ++ [rightof l ls]) tps2' tp'). spec_assert HCons as [HCons ->]; auto. do 2 (rewrite MoveToSymbol_Fun_equation; cbn). cbv [id]. hnf. f_equal. + rewrite encode_list_app. cbn. rewrite removelast_app by congruence. rewrite !removelast_cons. 3: congruence. 2: { intros H; symmetry in H; now apply app_cons_not_nil in H. } rewrite map_app, !List.map_map, <- !app_assoc. cbn. rewrite removelast_app by congruence. cbn. rewrite rev_app_distr; cbn. rewrite <- !app_assoc. cbn. rewrite !map_app, <- !app_assoc. rewrite !rev_app_distr. cbn. rewrite !map_rev, rev_involutive. rewrite !List.map_map. reflexivity. + now simpl_list. } { destruct tps2 as [ | tp' tps2']; cbn in *. - specialize (HNil (tps1 ++ [midtape ls m rs])). spec_assert HNil as [HNil ->]; auto. rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite MoveToSymbol_correct_midtape; cbn; auto. + cbn in *. TMSimp. rewrite map_id; cbv [id]. hnf. f_equal. rewrite encode_list_app. cbn. rewrite !map_app. rewrite removelast_app by congruence. rewrite !removelast_cons. 3: congruence. 2: { intros H; symmetry in H; now apply app_cons_not_nil in H. } rewrite removelast_app by congruence. cbn. rewrite !map_rev. simpl_list. cbn. rewrite <- !app_assoc. cbn. rewrite !map_app. cbn. rewrite !map_rev. repeat first [ progress cbn | rewrite rev_app_distr | rewrite map_app | rewrite <- app_assoc | rewrite rev_involutive | rewrite map_map ]. f_equal. + intros ? [ (?&<-&?) % in_map_iff | [<- | ] ] % in_app_iff; cbn; auto. - specialize (HCons (tps1 ++ [midtape ls m rs]) tps2' tp'). spec_assert HCons as [HCons ->]; auto. rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))). rewrite MoveToSymbol_correct_midtape; cbn; auto. + cbn in *. TMSimp. rewrite map_id; cbv [id]. hnf. f_equal. rewrite encode_list_app. cbn. rewrite !map_app. * rewrite removelast_app by congruence. rewrite !removelast_cons. 3: congruence. 2: { intros H; symmetry in H; now apply app_cons_not_nil in H. } rewrite removelast_app by congruence. cbn. rewrite !map_rev. simpl_list. cbn. rewrite <- !app_assoc. cbn. rewrite !map_app. cbn. rewrite !map_rev. repeat first [ progress cbn | rewrite rev_app_distr | rewrite map_app | rewrite <- app_assoc | rewrite rev_involutive | rewrite map_map ]. f_equal. * now simpl_list. + intros ? [ (?&<-&?) % in_map_iff | [<- | ] ] % in_app_iff; cbn; 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)