proposition: Lemma one_step_backward m i P i1 v1 st : @mm_no_self_loops m (i, P) -> encode_mm_instr i P /F/ @encode_state m (i1,v1) → st -> exists i2 v2, st = @encode_state m (i2,v2) /\ (i, P) /MM/ (i1, v1) → (i2,v2).
proof: Proof. intros H1 H2. destruct fractran_step_inv with (1 := H2) as (el & p & q & er & H3 & H4 & H5). unfold encode_state in H5; simpl in H5. destruct encode_mm_instr_in_inv with (1 := H3) as (l & rho & r & -> & G2). assert (i1 = length l+i) as E. { unfold encode_one_instr in G2. destruct rho as [ u | u j ]; unfold encode_inc, encode_dec, encode_dec2 in G2; [ destruct G2 as [ G2 | [] ] | destruct G2 as [ G2 | [ G2 | [] ] ] ]; inversion G2; subst p q; clear G2; repeat rewrite Nat.mul_assoc in H5. * apply divides_from_eq, prime_div_mult4 in H5; auto. destruct H5 as [ H5 | [ H5 | [ H5 | H5 ] ] ]. + apply primestream_divides in H5; lia. + apply ps_qs_div in H5; tauto. + apply primestream_divides in H5; lia. + apply ps_exp in H5; tauto. * rewrite <- Nat.mul_assoc in H5. apply divides_from_eq, prime_div_mult3 in H5; auto. destruct H5 as [ H5 | [ H5 | H5 ] ]. + apply primestream_divides in H5; lia. + apply primestream_divides in H5; lia. + apply ps_exp in H5; tauto. * apply divides_from_eq, prime_div_mult3 in H5; auto. destruct H5 as [ H5 | [ H5 | H5 ] ]. + apply primestream_divides in H5. exfalso; apply (H1 j u); auto. + apply primestream_divides in H5; lia. + apply ps_exp in H5; tauto. } destruct mm_sss_total with (ii := rho) (s := (i1,v1)) as ((i2 & v2) & H7). exists i2, v2. assert ((i, l++rho::r) /MM/ (i1,v1) → (i2,v2)) as H8. { apply in_sss_step; auto; simpl; lia. } split; auto. apply one_step_forward in H8; auto. revert H2 H8; apply fractran_step_fun; 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)