proposition: Fact copy_rev_stack_spec l v w : v#>x = l -> w = v[nil/x][(rev l++v#>y)/y][(rev l++v#>z)/z] -> (i,copy_rev_stack) // (i,v) ->> (9+i,w).
proof: Proof. Proof using Hxy Hyz Hxz. revert v w; induction l as [ | [] l IHl ]; intros v w Hv Hw; subst w; unfold copy_rev_stack. * bsm sss POP empty with x (5+i) (9+i). bsm sss stop. f_equal. apply vec_pos_ext; intros k; dest k z; dest k y; dest k x. * bsm sss POP one with x (5+i) (9+i) l. bsm sss PUSH with y One. bsm sss PUSH with z One. bsm sss PUSH with y' Zero. bsm sss POP zero with y' i i (One::v#>y); unfold y'; rew vec. apply IHl; rew vec. apply vec_pos_ext; intros k. dest k z; simpl; solve list eq. dest k y; dest k x. * bsm sss POP zero with x (5+i) (9+i) l. bsm sss PUSH with y Zero. bsm sss PUSH with z Zero. bsm sss PUSH with x Zero. bsm sss POP zero with x i i l; rew vec. apply IHl; rew vec. apply vec_pos_ext; intros k. dest k z; simpl; solve list eq. dest k y; dest k x. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)