proposition: Lemma DoWrite_Realise (d : option move) (s : sig) : DoWrite d s ⊨ DoWrite_Rel d s.
proof: Proof. unfold DoWrite. destruct d as [ [ | | ] | ]. { eapply Realise_monotone. { now auto with nocore TMdb. } intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; [discriminate| |discriminate|discriminate]. unfold atCons_current in *. TMSimp. simpl_tape. unfold atCons_current_leftof in HCons. TMSimp. rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_correct_midtape; auto. - hnf. cbn. f_equal. f_equal. rewrite map_id, rev_app_distr; cbn. rewrite rev_app_distr. cbn. rewrite rev_involutive. reflexivity. - intros ?. cbn. rewrite map_rev, rev_involutive. intros [ [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff | [ <- | ] ] % in_app_iff; auto. } { eapply Realise_monotone. { now auto with nocore TMdb. } intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; [discriminate|discriminate| |discriminate]. unfold atCons_current in *. TMSimp. simpl_tape. unfold atCons_current_rightof in HCons. TMSimp. rewrite Shift_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_L_correct_midtape; cbn; auto. - hnf. f_equal. cbn. f_equal. rewrite map_id, rev_app_distr; cbn. now rewrite rev_involutive. - intros ? [ (?&<-&?) % in_rev % in_map_iff | [ <- | ] ] % in_app_iff; auto. } { eapply Realise_monotone. { now auto with nocore TMdb. } intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; [discriminate|discriminate|discriminate|]. unfold atCons_current in *. cbn. unfold atCons_current_midtape in HCons. TMSimp. reflexivity. } { eapply Realise_monotone. { now auto 7 with nocore TMdb. } intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; [|discriminate|discriminate|discriminate]. unfold atCons_current in *. unfold atCons_current_niltape in HCons. TMSimp. rewrite Shift_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_L_correct_midtape; cbn; auto. + rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto; cbn. rewrite map_rev, rev_involutive, !map_id. rewrite MoveToSymbol_correct_midtape; cbn; auto. * rewrite !map_id, !rev_app_distr. hnf. rewrite <- !map_rev. rewrite !rev_involutive. reflexivity. * intros ? [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff; auto. + intros ? [ (?&<-&?) % in_rev % in_map_iff | [ <- | ] ] % in_app_iff; 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)