proposition: Fact mma_decs_length k i : length (mma_decs k i) = 2+3*k.
proof: Proof. revert i; induction k as [ | ? IHk ]; intros i; simpl; auto. rewrite IHk; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)