proposition: Lemma FRACTRAN_computable_functional {k} (R : Vector.t nat k -> nat -> Prop) : FRACTRAN_computable R -> forall v m1 m2, R v m1 -> R v m2 -> m1 = m2.
proof: Proof. intros (P & Hreg & HP) v m1 m2 (j1 & H1 & Hj1) % HP (j2 & H2 & Hj2) % HP. eapply eval_iff in H1 as [H1 H1'], H2 as [H2 H2']. eapply fractran_compute_fun in H1'; eauto. rewrite Nat.mul_comm in H1' at 1. symmetry in H1'. rewrite Nat.mul_comm in H1' at 1. symmetry in H1'. eapply power_factor_uniq in H1'. - firstorder. - epose proof (nxtprime_spec1 (nxtprime (nxtprime 2))). cbn. lia. - eauto. - eauto. Qed.
imports: Undecidability.FRACTRAN.FRACTRAN Coq(List Vector Nat Arith Lia) Undecidability.FRACTRAN(prime_seq) Undecidability(Utils.gcd Utils.prime FRACTRAN_sss Code.sss fractran_utils)