proposition: Lemma GoToCurrent_Realise : GoToCurrent ⊨ GoToCurrent_Rel.
proof: Proof. eapply Realise_monotone. { unfold GoToCurrent. now auto with nocore TMdb. } { intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons in *. TMSimp. destruct tp as [ | r rs | l ls | ls m rs]; cbn in *; TMSimp. - do 2 ( rewrite MoveToSymbol_Fun_equation in *; cbn in * ). easy. - do 2 ( rewrite MoveToSymbol_Fun_equation in *; cbn in * ). TMSimp. split; [|reflexivity]. hnf. cbn. f_equal. rewrite !List.map_map, !map_app, <- !app_assoc, !List.map_map. reflexivity. - replace (inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true])) ++ map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l]))) ++ inr (sigList_X (RightBlank true)) :: (map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])) by (now simpl_list; cbn; rewrite <- !app_assoc). rewrite MoveToSymbol_correct_midtape; cbn; auto. + split; [|reflexivity]. hnf. f_equal. rewrite !map_id, !List.map_map. rewrite !map_app; cbn. rewrite !List.map_map. rewrite rev_app_distr. cbn. rewrite !map_rev, rev_involutive, <- app_assoc. reflexivity. + rewrite !map_app, !List.map_map. cbn. intros ? [<- | [(?&<-&?)%in_map_iff | [<- | ?]] % in_app_iff ]; cbn; auto. - replace (inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls)))) ++ inr (sigList_X (MarkedSymbol m)) :: (map inr (map sigList_X (map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])). rewrite MoveToSymbol_correct_midtape; cbn; auto. + split; [|reflexivity]. rewrite !map_id, !List.map_map. rewrite !map_app; cbn. rewrite !List.map_map, <- !app_assoc. rewrite map_rev, rev_involutive. reflexivity. + rewrite !List.map_map. intros ? [ <- | (?&<-&?) % in_map_iff]; cbn; auto. + simpl_list. cbn. f_equal. f_equal. f_equal. rewrite !map_app, <- !app_assoc. reflexivity. } 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)