proposition: Theorem fractran_mma_reduction x : Q /F/ x ↓ <-> (1,fractran_mma) //ₐ (1,x##0##ø) ↓.
proof: Proof. Proof using HQ. split; auto. + intros (y & H2 & H3). exists (length fractran_mma+1,y##0##vec_nil); split; simpl; auto; try lia. apply fractran_mma_sound; auto. + apply fractran_mma_complete; auto. 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)