LF Specification

%% Untyped lambda terms

tm : type.

app : tm -> tm -> tm.
abs : (tm -> tm) -> tm.

eval : tm -> tm -> type.
eval/app : {M:tm} {N:tm} {R:tm -> tm} {V:tm} eval M (abs R) -> eval (R N) V -> eval (app M N) V.
eval/abs : {R:tm -> tm} eval (abs R) (abs R).

Reasoning

Specification "lc_diverge.elf".

CoDefine diverge : lfobj -> prop by
  diverge (app M N) :=
    (diverge M \/ exists R P, <R:tm -> tm> /\ <P:eval M (abs R)> /\ diverge (R N)).

Theorem omega_diverge :
  diverge (app (abs x\ app x x) (abs x\ app x x)).
coinduction. unfold.
  right.
  exists x\ app x x. exists eval/abs (x\ app x x). split.
    search.
    search.
    search.