proposition: Theorem mm_fractran_simulation_strong n P v j v' : @mm_no_self_loops n (1, P) -> (1,P) /MM/ (1,v) ▹ (j, v') <-> encode_mm_instr 1 P /F/ ps 1 * exp 0 v ▹ encode_state (j, v').
proof: Proof. intros HP. change (ps 1* exp 0 v) with (encode_state (1,v)). split. - now eapply mm_fractran_simulation_forward. - intros [H1 H2] % eval_iff. edestruct mm_fractran_simulation as [_ [[j' w] Hw]]; [ eauto | eexists; eauto | ]. pose proof (Hw' := Hw). eapply mm_fractran_simulation_forward in Hw as [Hw1 Hw2] % eval_iff; [ | eauto]. eapply fractran_compute_fun in H1; eauto. enough ((j', w) = (j, v')) as <- by eassumption. eapply encode_state_inj in H1; eauto. 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)