# Internalized Evaluation Function

Definition Eva := R (.\ "Eva","n","u";"u" (.\"";!none)
(.\"s","t"; "n" !none
(.\"n"; "Eva" "n" "s"
(.\"s"; "Eva" "n" "t"
(.\"t"; "s"
(.\""; !none)
(.\"",""; !none)
(.\"s"; "Eva" "n" (!Subst "s" !Zero "t")))
!none)
!none))
(.\"s"; !some (!Lam "s"))).

# Correctness of the internalized evaluation function

Lemma Eva_rec_var k n : Eva (enc k) (tenc (# n)) == none.

Lemma Eva_rec_lam k s : Eva (enc k) (tenc (lam s)) == some (Lam (tenc s)).

Lemma Eva_rec_app_0 s t : Eva Zero (tenc (app s t)) == none.

Lemma Eva_rec_app_Sn s t n :
Eva (enc (S n)) (tenc (app s t)) == Eva (enc n) (tenc s) (lam ((lam (Eva #0)) (enc n) (tenc t) (lam (
#1 (lam none)
(lam (lam none))
(lam ((lam (Eva #0)) (enc n) (Subst #0 Zero #1))))) none )) none.

Definition cLam s := lam(lam(lam(#0 s))).

Lemma Eva_rec_app_Sn_1 s t n s1 t1 :
proc s1
proc t1
Eva (enc n) (tenc s) == some (cLam s1) →
Eva (enc n) (tenc t) == some (cLam t1) →
Eva (enc (S n)) (tenc (app s t)) == Eva (enc n) (Subst s1 Zero (cLam t1)).

Lemma Eva_rec_app_Sn_2 s t n : Eva (enc n) (tenc s) == noneEva (enc (S n)) (tenc (s t)) == none.

Lemma Eva_rec_app_Sn_3 s t n s1 t1 : proc s1
→ proc t1
→ Eva (enc n) (tenc s) == some (cLam t1)
→ Eva (enc n) (tenc t) == none
→ Eva (enc (S n)) (tenc (s t)) == none.

Lemma Eva_correct k s : Eva (enc k) (tenc s) == oenc (eva k s).

# Internalized Evaluation

Definition Eval := Se (.\"x"; !Eva "x").

Lemma Eval_correct s v : proc v → (Eval (tenc s) == v n, Eva (enc n) (tenc s) == some v).

Lemma seval_Eval n s t: seval n s tEval (tenc s) == (tenc t).

Lemma eval_Eval s t : eval s tEval (tenc s) == (tenc t).

Lemma equiv_lambda' s t : lambda ts == ts >* t.

Lemma Eval_eval (s t : term) : Eval (tenc s) == tenc teval s t.

Lemma eval_converges s : converges s t, eval s t.

Lemma Eval_converges s : converges s converges (Eval (tenc s)).