proposition: Fact mv_right_spec t v w : t ~r v -> mv go_right t ~r w -> (i,mv_right) // (i,v) -+> (j,w).
proof: Proof. Proof using Hxy. destruct t as ((l,b),r). intros (H1 & H2) H3. unfold mv_right. destruct b. + bsm sss POP one with y (4+i) (4+i) r. bsm sss PUSH with x One. rew vec; rewrite <- H1. apply subcode_sss_compute_trans with (P := (2+i,jump (5+i))) (st2 := (5+i,v[r/y][(One::l)/x])); auto. apply subcode_sss_compute with (P := (5+i,to_default (5+i) j)); auto. apply to_default_spec. rew vec. symmetry. apply vec_pos_ext; intros z. unfold x, y in *; repeat invert pos z; rew vec. all: destruct r; simpl in *; destruct H3; auto. + bsm sss POP zero with y (4+i) (4+i) r. bsm sss PUSH with x Zero. rew vec; rewrite <- H1. apply subcode_sss_compute with (P := (5+i,to_default (5+i) j)); auto. apply to_default_spec. rew vec. symmetry. apply vec_pos_ext; intros z. unfold x, y in *; repeat invert pos z; rew vec. all: destruct r; simpl in *; destruct H3; auto. Qed.
imports: List Arith Lia Bool Undecidability.Synthetic(ReducibilityFacts) Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.TM(SBTM pctm_defs)