proposition: Fact transfer_ones_spec_2 b k v st : v#>x = list_repeat One k -> st = (q,v[nil/x][(list_repeat b k ++ v#>y)/y]) -> (i,transfer_ones b) // (i,v) ->> st.
proof: Proof. Proof using Hxy. intros H1 E; subst st. revert v H1. induction k as [ | k IHk ]; intros v; intros Hx; simpl list_repeat; simpl app; unfold transfer_ones; simpl in Hx. bsm sss POP empty with x p q. bsm sss stop; f_equal. apply vec_pos_ext; intros z; dest z y; dest z x. bsm sss POP one with x p q (list_repeat One k). bsm sss PUSH with y b. bsm sss PUSH with y Zero. bsm sss POP zero with y i i (b::v#>y); rew vec. specialize (IHk (v [(list_repeat One k) / x] [(b :: v #> y) / y])). spec in IHk. rew vec. eq goal IHk; do 2 f_equal. apply vec_pos_ext; intros z; dest z y. 2: dest z x. change (b :: list_repeat b k ++ v#>y) with (list_repeat b (S k) ++ v#>y). replace (S k) with (k+1) by lia. rewrite list_repeat_plus; solve list eq. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)