LF Specification

[View lc_diverge.elf]
%% 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).


[View lc_diverge.thm]

Click on a command or tactic to see a detailed view of its use.

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)).