proposition: Lemma DoMove_Sem (d : option move) (m : move) : DoMove d m ⊨c(DoMove_steps) DoMove_Rel d m.
proof: Proof. unfold DoMove_steps. unfold DoMove. destruct d as [ [ | | ] | ]. { destruct m; cbn. { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_leftof in *. TMSimp. f_equal. } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_leftof, atCons_current_midtape in *. TMSimp. specialize H with (1 := eq_refl); TMSimp; specialize H1 with (1 := eq_refl); TMSimp. f_equal. } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_leftof in *. TMSimp. f_equal. } } { destruct m; cbn. { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_rightof, atCons_current_midtape in *. TMSimp. specialize H with (1 := eq_refl); TMSimp; specialize H1 with (1 := eq_refl); TMSimp. f_equal. } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_rightof in *. TMSimp. f_equal. } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_rightof in *. TMSimp. f_equal. } } { destruct m; cbn. { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_midtape, atCons_current_midtape in *. TMSimp. specialize H with (1 := eq_refl); TMSimp. destruct ls as [ | l' ls']; cbn in *. { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. } { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. } } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_midtape in *. TMSimp. specialize H with (1 := eq_refl); TMSimp. destruct rs as [ | r' rs']; cbn in *. { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. } { specialize H1 with (1 := eq_refl). TMSimp. hnf. f_equal. } } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir; TMSimp. unfold atCons_current_midtape in *. TMSimp. f_equal. } } { eapply RealiseIn_monotone. now auto with nocore TMdb. lia. intros tin ([], tout) H. intros tps1 tps2 tp HDir HCons. destruct tp as [ | r rs | l ls | ls m' rs ]; cbn in *; inv HDir; TMSimp. now simpl_tape in *. } 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)