proposition: Theorem mm_fractran_simulation_forward 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)). intros ((k & H1) & H2); simpl fst in *. rewrite eval_iff. split. * exists k; apply steps_forward in H1; auto. * intros x Hx. destruct one_step_backward with (2 := Hx) as (i2 & v2 & -> & ?); auto. revert H; apply sss_out_step_stall; auto. 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)