proposition: Theorem mm_fractran_simulation n P v : @mm_no_self_loops n (1, P) -> (1,P) /MM/ (1,v) ↓ <-> encode_mm_instr 1 P /F/ ps 1 * exp 0 v ↓.
proof: Proof. intros HP. change (ps 1* exp 0 v) with (encode_state (1,v)). split. + intros ((j,w) & (k & H1) & H2); simpl fst in *. exists (encode_state (j,w)); 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. + intros (st & (k & H1) & H2). destruct steps_backward with (2 := H1) as (i2 & v2 & H3 & ->); auto. exists (i2,v2); split. * exists k; auto. * simpl fst. destruct (in_out_code_dec i2 (1,P)) as [ H4 | H4 ]; auto; exfalso. destruct in_code_subcode with (1 := H4) as (rho & l & r & G1 & G2). destruct (mm_sss_total rho (i2,v2)) as ((i3,v3) & G3). apply H2 with (encode_state (i3,v3)). apply one_step_forward; auto. subst P; apply in_sss_step; 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)