# Definition of Recursive Enumerability

Definition RE P := (f : term), closed f ( n, f(enc n) == none s, f (enc n) == some (tenc s) P s) s, P s n, f (enc n) == some (tenc s).

# The Enumeration combinator and its properties

Section Fix_f.

Variable f : term.
Hypothesis cls_f : closed f.
Hypothesis total_f : n, f (enc n) == none s, f (enc n) == some (tenc s).

Definition Re := R (.\ "Re", "n", "s"; (!f "n") (.\"t"; ( !(lam(Eq #0)) "t" "s" !I (.\ "", ""; "Re" (!Succ "n") "s") !I))
(.\ ""; "Re" (!Succ "n") "s") !I).

Lemma Re_rec_s n t : Re (enc n) (tenc t) >* (f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc t) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc t)))) I))
(lam ((lam(Re #0)) (Succ (enc n)) (tenc t))) I.

Lemma Re_rec n t : Re (enc n) (tenc t) == (f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc t) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc t)))) I))
(lam ((lam(Re #0)) (Succ (enc n)) (tenc t))) I.

Lemma Re_S n s : converges (Re (enc (S n)) (tenc s)) → converges (Re (enc n) (tenc s)).

Lemma Re_ge n m s : n mconverges (Re (enc n) (tenc s)) → converges (Re (enc m) (tenc s)).

Lemma Re_converges n s : converges (Re (enc n) (tenc s)) → n, f (enc n) == oenc (Some s).

End Fix_f.

# Recursive Enumerability implies semi decidability

Lemma RE_Acc P : RE Placc P.

# Semi decidability implies recursive enumerability

Lemma pi_eval u s : pi u s v, eval (u (tenc s)) v.

Theorem Acc_RE P : lacc PRE P.