proposition: Fact mm_null_progress i v st : v#>zero = 0 -> st = (2+i,v[0/src]) -> (i,mm_null i) // (i,v) -+> st.
proof: Proof. Proof using Hsz. intros; subst. apply mm_null_spec with (1 := eq_refl); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)