proposition: Fact copy_stack_spec l v w : v#>x = l -> v#>z = nil -> w = v[(l++v#>y)/y] -> (i,copy_stack) // (i,v) ->> (16+i,w).
proof: Proof. Proof using Hxy Hyz Hxz. intros H1 H2 H3; subst w. unfold copy_stack. apply sss_compute_trans with (st2 := (7+i,v[nil/x][(rev l)/z])). * apply subcode_sss_compute with (P := (i,move_rev_stack x z i)); auto. apply move_rev_stack_spec with l; auto. rew vec; rewrite H2; solve list eq. * apply subcode_sss_compute with (P := (7+i,copy_rev_stack z x y (7+i))); auto. apply copy_rev_stack_spec with (rev l); rew vec. apply vec_pos_ext; intros k. dest k z; simpl; solve list eq. dest k y; [ | dest k x ]; rewrite rev_involutive; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)