proposition: Fact mma_mult_cst_with_zero_length :length mma_mult_cst_with_zero = 8+k.
proof: Proof. unfold mma_mult_cst_with_zero; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)