proposition: Theorem mm_fractran_n_strong n (P : list (mm_instr (pos n))) : { l | Forall (fun c => snd c <> 0) l /\ (forall v w, (exists j, (1,P) /MM/ (1,v) ▹ (j,w)) -> (exists j, l /F/ ps 1 * exp 1 v ▹ encode_state (j,0 ## w))) /\ (forall v, (l /F/ ps 1 * exp 1 v ↓) -> (1,P) /MM/ (1,v) ↓) }.
proof: Proof. destruct mm_remove_self_loops_strong with (P := P) as (Q & H1 & H2 & H3 & H4). exists (encode_mm_instr 1 Q); split. + eapply Forall_impl. 2: apply encode_mm_instr_regular. firstorder. + split. - intros v w [j H % mm_fractran_simulation_forward] % H3; eauto. cbn in H. rewrite Nat.add_0_r in H. eauto. - intros v H. eapply H4. eapply mm_fractran_simulation; [ auto | ]. cbn. now rewrite Nat.add_0_r. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs mm_no_self) Undecidability.FRACTRAN(FRACTRAN fractran_utils prime_seq FRACTRAN_sss)