proposition: Theorem fractran_reg_mma0_reductions Q : fractran_regular Q -> (forall x, Q /F/ x ↓ <-> (1,fractran_mma0 Q) //ₐ (1,x##0##ø) ↓) /\ (forall x, Q /F/ x ↓ <-> (1,fractran_mma0 Q) //ₐ (1,x##0##ø) ~~> (0,(0##0##ø))).
proof: Proof. do 2 (split; intros); repeat (apply fractran_mma0_reduction; 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)