proposition: Fact mma_fractran_one_length : length mma_fractran_one = 29+4*p+7*q.
proof: Proof. unfold mma_fractran_one; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils) Undecidability.FRACTRAN(FRACTRAN fractran_utils)