proposition: Theorem FRACTRAN_computable_to_Diophantine {k} (R : Vector.t nat k -> nat -> Prop) : FRACTRAN_computable R -> Diophantine' R.
proof: Proof. intros (P & regP & HP). enough (dio_rec_single_n (fun v : vec _ (S k) => R (vec_tail v) (vec_head v))) as (n & P1 & P2 & H). - exists n, P1, P2. intros v. eapply (Vector.caseS' v). clear v. intros x v ρ. specialize (H (x ## v)). cbn [vec_head vec_tail] in H. rewrite H. split. + intros [w Hw]. exists (vec_pos w). subst ρ. erewrite dio_single.dp_eval_ext. 1: rewrite Hw. 1:eapply dio_single.dp_eval_ext. all: intros; now rewrite ?vec_pos_set, ?vec_pos_spec. + intros [ν Hν]. subst ρ. exists (vec_set_pos ν). erewrite dio_single.dp_eval_ext. 1: rewrite Hν. 1:eapply dio_single.dp_eval_ext. all: intros; now rewrite ?vec_pos_set, ?vec_pos_spec. - eapply DPRM_n, DPRM_n. edestruct (fractran_computable_diophantine) with (l := P) (n := k) as (A & HA). exists A. intros v. eapply (Vector.caseS' v). clear v. intros m v. cbn [vec_tail vec_head]. specialize (HP v) as HP1. rewrite HP1, HA, fun2vec_plus, (fun2vec_ext _ (vec2fun v 0)), fun2vec_vec2fun. 1: reflexivity. intros x. unfold vec2fun. do 2 destruct Compare_dec.le_lt_dec. 1,2,3: lia. enough (pos.nat2pos l = Fin.FS (pos.nat2pos l0)) as -> by reflexivity. destruct k, x; cbn; try lia; do 2 f_equal; eapply nat2pos_ext. Qed.
imports: Lia Nat Fin Undecidability.H10.Util.Diophantine Undecidability.FRACTRAN(FRACTRAN_computable prime_seq) Undecidability.H10(fractran_dio DPRM dio_logic) Undecidability.Shared.Libs.DLW(vec)