# Definition of evaluation

Definition eval s t := s >* t lambda t.

Notation "s '⇓' t" := (eval s t) (at level 51).

# Step indexed evaluation

Inductive seval : nattermtermProp :=
| sevalR n s : seval n (lam s) (lam s)
| sevalS n s t u v w :
seval n s (lam u) → seval n t (lam v) → seval n (subst u 0 (lam v)) wseval (S n) (s t) w.

Notation "s '⇓' n t" := (seval n s t) (at level 51).

Lemma seval_eval n s t : seval n s teval s t.

# Equivalence between step index evaluation and evaluation

Lemma seval_S n s t : seval n s tseval (S n) s t.

Lemma eval_step s s' t n : s >> s'seval n s' tseval (S n) s t.

Lemma eval_seval s t : eval s t n, seval n s t.

# Evaluation as a function

Fixpoint eva (n : nat) (u : term) :=
match u with
| var nNone
| lam sSome (lam s)
| app s tmatch n with
| 0 ⇒ None
| S nmatch eva n s, eva n t with
| Some (lam s), Some teva n (subst s 0 t)
| _ , _None
end
end
end.

# Equivalence between the evaluation function and step indexed evaluation

Lemma eva_lam n s t : eva n s = Some t u, t = lam u.

Lemma eva_seval n s t : eva n s = Some tseval n s t.

Lemma seval_eva n s t : seval n s teva n s = Some t.

Lemma equiv_eva s s' : s == lam s' n, eva n s = Some (lam s').

Lemma eva_equiv s s' n : eva n s = Some s's == s'.

Lemma eva_n_Sn n s t : eva n s = Some teva (S n) s = Some t.

Lemma eva_Sn_n n s : eva (S n) s = Noneeva n s = None.

Lemma eproc_equiv s t: eval s (lam t) s == (lam t).

# If an application converges, both sides converge

Lemma app_converges (s t : term) : (converges (s t)) → converges s converges t.