proposition: Fact increment_erase_spec v ln mn w : list_bool_succ ln mn -> v#>s = ln -> w = v[mn/s][nil/h][nil/l][nil/a] -> (i,increment_erase) // (i,v) ->> (p,w).
proof: Proof. Proof using Hsa Hal. intros H1 H2 ?; subst w. unfold increment_erase. apply sss_compute_trans with (st2 := (15+i,v[mn/s])). apply subcode_sss_compute with (P := (i,increment s a i )); auto. apply increment_spec with ln; auto. apply sss_compute_trans with (st2 := (18+i,v[mn/s][nil/h])). apply subcode_sss_compute with (P := (15+i,empty_stack h (15+i))); auto. apply empty_stack_spec. apply sss_compute_trans with (st2 := (21+i,v[mn/s][nil/h][nil/l])). apply subcode_sss_compute with (P := (18+i,empty_stack l (18+i))); auto. apply empty_stack_spec. apply sss_compute_trans with (st2 := (24+i,v[mn/s][nil/h][nil/l][nil/a])). apply subcode_sss_compute with (P := (21+i,empty_stack a (21+i))); auto. apply empty_stack_spec. bsm sss PUSH with l Zero. bsm sss POP zero with l p p nil; rew vec. bsm sss stop. f_equal. apply vec_pos_ext; intros x; dest x l. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)