proposition: Fact mma_null_all_spec v : (i,mma_null_all) // (i,v) ->> (n+i,vec_zero).
proof: Proof. replace (n+i) with (length (pos_list n)+i). + apply mma_null_list_spec. * intros; apply vec_zero_spec. * intros ? []; apply pos_list_prop. + now rewrite pos_list_length. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)