Welcome to Abella 2.0.2-lf

Abella < Specification "lc_diverge.elf".
Reading specification "lc_diverge.elf"
sig lc_diverge.
  type tm lftype.
  type app lfobj -> lfobj -> lfobj.
  type abs (lfobj -> lfobj) -> lfobj.
  type eval lfobj -> lfobj -> lftype.
  type eval/app lfobj -> lfobj -> (lfobj -> lfobj) -> lfobj -> lfobj -> lfobj -> lfobj.
  type eval/abs (lfobj -> lfobj) -> lfobj.
end.
module lc_diverge.
  (* tm:type *)
  lfisty tm.
  (* app:tm -> tm -> tm *)
  pi lf_1\lfhas lf_1 tm => pi lf_2\lfhas lf_2 tm => lfhas (app lf_1 lf_2) tm.
  (* abs:(tm -> tm) -> tm *)
  pi lf_1\(pi lf_2\lfhas lf_2 tm => lfhas (lf_1 lf_2) tm) =>
    lfhas (abs lf_1) tm.
  (* eval:tm -> tm -> type *)
  pi lf_1\lfhas lf_1 tm => pi lf_2\lfhas lf_2 tm => lfisty (eval lf_1 lf_2).
  (* eval/app:{M:tm} {N:tm} {R:tm -> tm} {V:tm} eval M (abs R) ->
       eval (R N) V -> eval (app M N) V *)
  pi M\lfhas M tm =>
    pi N\lfhas N tm =>
      pi R\(pi lf_1\lfhas lf_1 tm => lfhas (R lf_1) tm) =>
        pi V\lfhas V tm =>
          pi lf_1\lfhas lf_1 (eval M (abs R)) =>
            pi lf_2\lfhas lf_2 (eval (R N) V) =>
              lfhas (eval/app M N R V lf_1 lf_2) (eval (app M N) V).
  (* eval/abs:{R:tm -> tm} eval (abs R) (abs R) *)
  pi R\(pi lf_1\lfhas lf_1 tm => lfhas (R lf_1) tm) =>
    lfhas (eval/abs R) (eval (abs R) (abs R)).
end.

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

Abella < Theorem omega_diverge : 
diverge (app (abs (x\app x x)) (abs (x\app x x))).

============================
 diverge (app (abs (x\app x x)) (abs (x\app x x)))

omega_diverge < coinduction.

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 diverge (app (abs (x\app x x)) (abs (x\app x x))) #

omega_diverge < unfold.

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 diverge (abs (x\app x x)) + \/
   (exists R P, <n1:tm |- R n1:tm> /\ <P:eval (abs ([x] app x x)) (abs R)> /\
      diverge (R (abs (x\app x x))) +)

omega_diverge < right.

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 exists R P, <n1:tm |- R n1:tm> /\ <P:eval (abs ([x] app x x)) (abs R)> /\
   diverge (R (abs (x\app x x))) +

omega_diverge < exists x\app x x.

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 exists P, <n1:tm |- app n1 n1:tm> /\
   <P:eval (abs ([x] app x x)) (abs ([x] app x x))> /\
   diverge (app (abs (x\app x x)) (abs (x\app x x))) +

omega_diverge < exists eval/abs (x\app x x).

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 <n1:tm |- app n1 n1:tm> /\
   <eval/abs ([x] app x x):eval (abs ([x] app x x)) (abs ([x] app x x))> /\
   diverge (app (abs (x\app x x)) (abs (x\app x x))) +

omega_diverge < split.

Subgoal 1:

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 <n1:tm |- app n1 n1:tm>

Subgoal 2 is:
 <eval/abs ([x] app x x):eval (abs ([x] app x x)) (abs ([x] app x x))>

Subgoal 3 is:
 diverge (app (abs (x\app x x)) (abs (x\app x x))) +

omega_diverge < search.

Subgoal 2:

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 <eval/abs ([x] app x x):eval (abs ([x] app x x)) (abs ([x] app x x))>

Subgoal 3 is:
 diverge (app (abs (x\app x x)) (abs (x\app x x))) +

omega_diverge < search.

Subgoal 3:

CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
 diverge (app (abs (x\app x x)) (abs (x\app x x))) +

omega_diverge < search.
Proof completed.

Abella < Goodbye.