Require Import List Arith.

From Undecidability.Shared.Libs.DLW
  Require Import gcd rel_iter pos vec.

From Undecidability.FRACTRAN.Utils
  Require Import prime_seq.

Reserved Notation "l '/F/' x → y" (at level 70, no associativity).

Implicit Type l : list (*).

Inductive fractran_step : list (*) Prop :=
  | in_fractran_0 : p q l x y, q*y = p*x (p,q)::l /F/ x y
  | in_fractran_1 : p q l x y, divides q (p*x) l /F/ x y (p,q)::l /F/ x y
where "l /F/ x → y" := (fractran_step l x y).

Definition fractran_stop l x := z, l /F/ x z.

Definition fractran_steps l := rel_iter (fractran_step l).
Definition fractran_compute l x y := n, fractran_steps l n x y.
Definition fractran_terminates l x := y, fractran_compute l x y fractran_stop l y.

Notation "l '/F/' x ↓ " := (fractran_terminates l x) (at level 70, no associativity).


Definition FRACTRAN_PROBLEM := (list (*) * )%type.
Definition FRACTRAN_HALTING (P : FRACTRAN_PROBLEM) := let (l,x) := P in l /F/ x .

Definition fractran_regular l := Forall ( c snd c 0) l.

Definition FRACTRAN_REG_PROBLEM :=
  { l : list (*) & { _ : | fractran_regular l } }.
Definition FRACTRAN_REG_HALTING (P : FRACTRAN_REG_PROBLEM) : Prop.
Proof.
  destruct P as (l & x & _).
  exact (l /F/ x ).
Defined.



Definition FRACTRAN_ALT_PROBLEM := (list (*) * { n : & vec n })%type.

Definition FRACTRAN_ALT_HALTING : FRACTRAN_ALT_PROBLEM Prop.
Proof.
  intros (l & n & v).
  exact (l /F/ ps 1 * exp 1 v ).
Defined.