Library Partial

Section PartialFunctions.

Variable F : term.
Hypothesis proc_F : proc F.

Hypothesis total_F : ∀ t n, (∃ v, F (enc n) (tenc t) == some v ∧ proc v) ∨ F (enc n) (tenc t) == none.

Definition S' := R (.\"S'", "n", "F", "t"; ("F" "n" "t") !K (.\"x"; "S'" (!Succ "n") "F" "t") !I).


Lemma S'_rec n t : S' (enc n) F (tenc t) == (F (enc n) (tenc t)) K (lam ( (lam (S' #0)) (Succ (enc n)) F (tenc t))) I.

Hypothesis mono_F : ∀ n t v, F (enc n) (tenc t) == some v → F (enc (S n)) (tenc t) == some v.

Lemma S'_n_Sn n t : S' (enc n) F (tenc t) == S' (enc (S n)) F (tenc t).

Definition Se := S' (enc 0).

Lemma S'_0_n n t : Se F (tenc t) == S' (enc n) F (tenc t).

Lemma Se_converges t v : Se F (tenc t) == lam v → closed (lam v).

Lemma Se_correct' (t v : term) : proc v →
                                    ( Se F (tenc t) == v ↔ ∃ n, F (enc n) (tenc t) == some v ).

Corollary Se_correct (t v : term) : lambda v → (Se F (tenc t) == v ↔ ∃ n, F (enc n) (tenc t) == some v).

End PartialFunctions.