proposition: Fact increment_spec_2 i v k : v#>x = list_repeat One k -> (i,increment i) // (i,v) ->> (15+i,v[(list_repeat Zero (S k))/x]).
proof: Proof. Proof using Hxy. intros Hx. unfold increment. bsm sss PUSH with y Zero. apply subcode_sss_compute_trans with (P := (1+i,transfer_ones x y (1+i) (5+i) (10+i) One)) (st2 := (10+i,v[nil/x][(list_repeat One k ++ Zero:: v#>y)/y])); auto. apply transfer_ones_spec_2 with (k := k); rew vec. f_equal. apply vec_pos_ext; intros z; dest z y; dest z x. bsm sss PUSH with x Zero. apply subcode_sss_compute_trans with (P := (11+i,transfer_ones y x (11+i) (15+i) (15+i) Zero)) (st2 := (15+i,v[(list_repeat Zero (S k))/x])); auto. apply transfer_ones_spec_1 with (k := k) (l := v#>y); rew vec. f_equal. apply vec_pos_ext; intros z; dest z y; dest z x. replace (S k) with (k+1) by lia. rewrite list_repeat_plus; auto. bsm sss stop. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)