proposition: Theorem fractran_mma0_reduction : (Term1 -> Term2) /\ (Term2 -> Term3) /\ (Term3 -> Term1).
proof: Proof. Proof using HQ. msplit 2; unfold Term1, Term2, Term3. + intros (y & H1 & H2); split; simpl; auto. apply fractran_mma0_sound with (1 := H1); auto. + now exists (0,0##0##ø). + intros H1; apply fractran_mma_reduction; auto. revert H1; apply subcode_sss_terminates. unfold fractran_mma0, P; 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)