Require Import Undecidability.Synthetic.Undecidability.
From Undecidability.Shared.Libs.DLW Require Import pos vec sss.
From Undecidability.FRACTRAN Require Import FRACTRAN.
From Undecidability.MinskyMachines Require Import mma_defs fractran_mma.
Set Implicit Arguments.
Set Default Proof Using "Type".
Local Notation "P /MMA/ s ↓" := (sss_terminates (@mma_sss 2) P s) (at level 70, no associativity).
Theorem fractran_reg_mma2 l :
fractran_regular l
-> { Q : list (mm_instr (pos 2))
| forall x, l /F/ x ↓ <-> (1,Q) /MMA/ (1,x##0##vec_nil) ↓ }.
Proof.
intros Hl.
exists (fractran_reg_mma l).
apply fractran_reg_mma_reduction; auto.
Qed.
Section FRACTRAN_REG_MMA2.
Let f : FRACTRAN_REG_PROBLEM -> MMA2_PROBLEM.
Proof.
intros (l & x & Hl).
destruct (fractran_reg_mma2 Hl) as (Q & HQ).
exact (Q, (x##0##vec_nil)).
Defined.
Theorem FRACTRAN_REG_MMA2_HALTING : FRACTRAN_REG_HALTING ⪯ MMA2_HALTING.
Proof.
exists f.
intros (l & x & Hl); simpl.
destruct (fractran_reg_mma2 Hl) as (Q & HQ); apply HQ.
Qed.
End FRACTRAN_REG_MMA2.
Check FRACTRAN_REG_MMA2_HALTING.