proposition: Theorem mm_mma2 n (P : list (mm_instr (pos n))) : { Q : list (mm_instr (pos 2)) & { f : vec nat n -> vec nat 2 | forall v, (1,P) /MM/ (1,v) ↓ <-> (1,Q) /MMA/ (1,f v) ↓ } }.
proof: Proof. destruct (mm_fractran_not_zero P) as (l & H1 & H2). exists (fractran_mma l), (fun v => ps 1 * exp 1 v ## 0 ## vec_nil). intros v; rewrite H2. apply fractran_mma_reduction; trivial. revert H1; apply Forall_impl; tauto. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Shared.Libs.DLW(Utils.utils Vec.pos Vec.vec) Undecidability.Shared.Libs.DLW.Code(sss) Undecidability.MinskyMachines(MM MM_sss MMA FRACTRAN_to_MMA2) Undecidability.FRACTRAN(FRACTRAN MM_FRACTRAN) Undecidability.MinskyMachines(mm_defs mma_defs fractran_mma) Undecidability.FRACTRAN(fractran_utils prime_seq mm_fractran)