proposition: Fact mv_left_spec t v w : t ~r v -> mv go_left t ~r w -> (i,mv_left) // (i,v) -+> (j,w).
proof: Proof. Proof using Hxy. destruct t as ((l,b),r). intros (H1 & H2) H3. unfold mv_left. destruct l as [ | [] l ]. + bsm sss POP empty with x (11+i) (11+i). bsm sss PUSH with y Zero. apply subcode_sss_compute_trans with (P := (12+i,jump j')) (st2 := (j,w)); auto. 2: bsm sss stop. unfold j'; apply jump_spec'. simpl in H3. destruct H3 as (H3 & H5). apply vec_pos_ext; intros z. repeat invert pos z; rew vec. * rewrite <- H1; auto. * unfold y in *; rew vec; rewrite <- H2; auto. + bsm sss POP one with x (11+i) (11+i) l. bsm sss PUSH with y One. apply subcode_sss_compute_trans with (P := (2+i,jump j)) (st2 := (j,w)); auto. 2: bsm sss stop. apply jump_spec'. simpl in H3. destruct H3 as (H3 & H5). apply vec_pos_ext; intros z. unfold x, y in *; repeat invert pos z; rew vec. rewrite <- H2; auto. + bsm sss POP zero with x (11+i) (11+i) l. bsm sss PUSH with y Zero. apply subcode_sss_compute_trans with (P := (12+i,jump j')) (st2 := (j,w)); auto. 2: bsm sss stop. apply jump_spec'. simpl in H3. destruct H3 as (H3 & H5). apply vec_pos_ext; intros z. unfold x, y in *; repeat invert pos z; rew vec. rewrite <- H2; 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)