proposition: Fact mma_non_empty_progress v st : st = (4+i,v) -> v#>x <> 0 -> (i,EMPTYₐ) // (i,v) -+> st.
proof: Proof. intros -> H. unfold mma_isempty. case_eq (v#>x). + now intros; subst. + clear H; intros u H. mma sss DEC S with x (3+i) u; rew vec. mma sss INC with x; auto. mma sss stop; f_equal. apply vec_pos_ext; intros y; dest y x; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)