Welcome to Abella 2.0.4-dev
Abella < Specification "eval".
Reading specification "eval"

Abella < Theorem eval_det : 
forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2.


============================
 forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2

eval_det < induction on 1.

IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
============================
 forall E V1 V2, {eval E V1}@ -> {eval E V2} -> V1 = V2

eval_det < intros.

Variables: E V1 V2
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H1 : {eval E V1}@
H2 : {eval E V2}
============================
 V1 = V2

eval_det < case H1.
Subgoal 1:

Variables: V2 R
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H2 : {eval (abs R) V2}
============================
 abs R = V2

Subgoal 2 is:
 V1 = V2

eval_det < case H2.
Subgoal 1:

Variables: R
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
============================
 abs R = abs R

Subgoal 2 is:
 V1 = V2

eval_det < search.
Subgoal 2:

Variables: V1 V2 N R M
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H2 : {eval (app M N) V2}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V1}*
============================
 V1 = V2

eval_det < case H2.
Subgoal 2:

Variables: V1 V2 N R M R1
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H3 : {eval M (abs R)}*
H4 : {eval (R N) V1}*
H5 : {eval M (abs R1)}
H6 : {eval (R1 N) V2}
============================
 V1 = V2

eval_det < apply IH to H3 H5.
Subgoal 2:

Variables: V1 V2 N M R1
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H3 : {eval M (abs R1)}*
H4 : {eval (R1 N) V1}*
H5 : {eval M (abs R1)}
H6 : {eval (R1 N) V2}
============================
 V1 = V2

eval_det < apply IH to H4 H6.
Subgoal 2:

Variables: V2 N M R1
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H3 : {eval M (abs R1)}*
H4 : {eval (R1 N) V2}*
H5 : {eval M (abs R1)}
H6 : {eval (R1 N) V2}
============================
 V2 = V2

eval_det < search.
Proof completed.
Abella < Theorem step_det : 
forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3.


============================
 forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3

step_det < induction on 1.

IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
============================
 forall E1 E2 E3, {step E1 E2}@ -> {step E1 E3} -> E2 = E3

step_det < intros.

Variables: E1 E2 E3
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H1 : {step E1 E2}@
H2 : {step E1 E3}
============================
 E2 = E3

step_det < case H1.
Subgoal 1:

Variables: E3 M R
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H2 : {step (app (abs R) M) E3}
============================
 R M = E3

Subgoal 2 is:
 app M' N = E3

step_det < case H2.
Subgoal 1.1:

Variables: M R
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
============================
 R M = R M

Subgoal 1.2 is:
 R M = app M' M

Subgoal 2 is:
 app M' N = E3

step_det < search.
Subgoal 1.2:

Variables: M R M'
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step (abs R) M'}
============================
 R M = app M' M

Subgoal 2 is:
 app M' N = E3

step_det < case H3.
Subgoal 2:

Variables: E3 M' M N
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H2 : {step (app M N) E3}
H3 : {step M M'}*
============================
 app M' N = E3

step_det < case H2.
Subgoal 2.1:

Variables: M' N R
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step (abs R) M'}*
============================
 app M' N = R N

Subgoal 2.2 is:
 app M' N = app M'1 N

step_det < case H3.
Subgoal 2.2:

Variables: M' M N M'1
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step M M'}*
H4 : {step M M'1}
============================
 app M' N = app M'1 N

step_det < apply IH to H3 H4.
Subgoal 2.2:

Variables: M N M'1
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step M M'1}*
H4 : {step M M'1}
============================
 app M'1 N = app M'1 N

step_det < search.
Proof completed.
Abella < Theorem nstep_det : 
forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2.


============================
 forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2

nstep_det < induction on 1.

IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
============================
 forall E R1 R2, {nstep E (abs R1)}@ -> {nstep E (abs R2)} -> R1 = R2

nstep_det < intros.

Variables: E R1 R2
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H1 : {nstep E (abs R1)}@
H2 : {nstep E (abs R2)}
============================
 R1 = R2

nstep_det < case H1.
Subgoal 1:

Variables: R1 R2
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H2 : {nstep (abs R1) (abs R2)}
============================
 R1 = R2

Subgoal 2 is:
 R1 = R2

nstep_det < case H2.
Subgoal 1.1:

Variables: R2
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
============================
 R2 = R2

Subgoal 1.2 is:
 R1 = R2

Subgoal 2 is:
 R1 = R2

nstep_det < search.
Subgoal 1.2:

Variables: R1 R2 B
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step (abs R1) B}
H4 : {nstep B (abs R2)}
============================
 R1 = R2

Subgoal 2 is:
 R1 = R2

nstep_det < case H3.
Subgoal 2:

Variables: E R1 R2 B
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H2 : {nstep E (abs R2)}
H3 : {step E B}*
H4 : {nstep B (abs R1)}*
============================
 R1 = R2

nstep_det < case H2.
Subgoal 2.1:

Variables: R1 R2 B
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step (abs R2) B}*
H4 : {nstep B (abs R1)}*
============================
 R1 = R2

Subgoal 2.2 is:
 R1 = R2

nstep_det < case H3.
Subgoal 2.2:

Variables: E R1 R2 B B1
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step E B}*
H4 : {nstep B (abs R1)}*
H5 : {step E B1}
H6 : {nstep B1 (abs R2)}
============================
 R1 = R2

nstep_det < apply step_det to H3 H5.
Subgoal 2.2:

Variables: E R1 R2 B1
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step E B1}*
H4 : {nstep B1 (abs R1)}*
H5 : {step E B1}
H6 : {nstep B1 (abs R2)}
============================
 R1 = R2

nstep_det < apply IH to H4 H6.
Subgoal 2.2:

Variables: E R2 B1
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step E B1}*
H4 : {nstep B1 (abs R2)}*
H5 : {step E B1}
H6 : {nstep B1 (abs R2)}
============================
 R2 = R2

nstep_det < search.
Proof completed.
Abella < Theorem nstep_lemma : 
forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}.


============================
 forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}

nstep_lemma < induction on 1.

IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
       {nstep (app M N) V}
============================
 forall M N R V, {nstep M (abs R)}@ -> {nstep (R N) V} -> {nstep (app M N) V}

nstep_lemma < intros.

Variables: M N R V
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
       {nstep (app M N) V}
H1 : {nstep M (abs R)}@
H2 : {nstep (R N) V}
============================
 {nstep (app M N) V}

nstep_lemma < case H1.
Subgoal 1:

Variables: N R V
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
       {nstep (app M N) V}
H2 : {nstep (R N) V}
============================
 {nstep (app (abs R) N) V}

Subgoal 2 is:
 {nstep (app M N) V}

nstep_lemma < search.
Subgoal 2:

Variables: M N R V B
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
       {nstep (app M N) V}
H2 : {nstep (R N) V}
H3 : {step M B}*
H4 : {nstep B (abs R)}*
============================
 {nstep (app M N) V}

nstep_lemma < apply IH to H4 H2.
Subgoal 2:

Variables: M N R V B
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
       {nstep (app M N) V}
H2 : {nstep (R N) V}
H3 : {step M B}*
H4 : {nstep B (abs R)}*
H5 : {nstep (app B N) V}
============================
 {nstep (app M N) V}

nstep_lemma < search.
Proof completed.
Abella < Theorem eval_nstep : 
forall E V, {eval E V} -> {nstep E V}.


============================
 forall E V, {eval E V} -> {nstep E V}

eval_nstep < induction on 1.

IH : forall E V, {eval E V}* -> {nstep E V}
============================
 forall E V, {eval E V}@ -> {nstep E V}

eval_nstep < intros.

Variables: E V
IH : forall E V, {eval E V}* -> {nstep E V}
H1 : {eval E V}@
============================
 {nstep E V}

eval_nstep < case H1.
Subgoal 1:

Variables: R
IH : forall E V, {eval E V}* -> {nstep E V}
============================
 {nstep (abs R) (abs R)}

Subgoal 2 is:
 {nstep (app M N) V}

eval_nstep < search.
Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
============================
 {nstep (app M N) V}

eval_nstep < apply IH to H2.
Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
H4 : {nstep M (abs R)}
============================
 {nstep (app M N) V}

eval_nstep < apply IH to H3.
Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
H4 : {nstep M (abs R)}
H5 : {nstep (R N) V}
============================
 {nstep (app M N) V}

eval_nstep < apply nstep_lemma to H4 H5.
Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
H4 : {nstep M (abs R)}
H5 : {nstep (R N) V}
H6 : {nstep (app M N) V}
============================
 {nstep (app M N) V}

eval_nstep < search.
Proof completed.
Abella < Theorem step_eval_lemma : 
forall A B C, {step A B} -> {eval B C} -> {eval A C}.


============================
 forall A B C, {step A B} -> {eval B C} -> {eval A C}

step_eval_lemma < induction on 1.

IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
============================
 forall A B C, {step A B}@ -> {eval B C} -> {eval A C}

step_eval_lemma < intros.

Variables: A B C
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H1 : {step A B}@
H2 : {eval B C}
============================
 {eval A C}

step_eval_lemma < case H1.
Subgoal 1:

Variables: C M R
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H2 : {eval (R M) C}
============================
 {eval (app (abs R) M) C}

Subgoal 2 is:
 {eval (app M N) C}

step_eval_lemma < search.
Subgoal 2:

Variables: C M' M N
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H2 : {eval (app M' N) C}
H3 : {step M M'}*
============================
 {eval (app M N) C}

step_eval_lemma < case H2.
Subgoal 2:

Variables: C M' M N R
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H3 : {step M M'}*
H4 : {eval M' (abs R)}
H5 : {eval (R N) C}
============================
 {eval (app M N) C}

step_eval_lemma < apply IH to H3 H4.
Subgoal 2:

Variables: C M' M N R
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H3 : {step M M'}*
H4 : {eval M' (abs R)}
H5 : {eval (R N) C}
H6 : {eval M (abs R)}
============================
 {eval (app M N) C}

step_eval_lemma < search.
Proof completed.
Abella < Theorem nstep_eval : 
forall E R, {nstep E (abs R)} -> {eval E (abs R)}.


============================
 forall E R, {nstep E (abs R)} -> {eval E (abs R)}

nstep_eval < induction on 1.

IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
============================
 forall E R, {nstep E (abs R)}@ -> {eval E (abs R)}

nstep_eval < intros.

Variables: E R
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H1 : {nstep E (abs R)}@
============================
 {eval E (abs R)}

nstep_eval < case H1.
Subgoal 1:

Variables: R
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
============================
 {eval (abs R) (abs R)}

Subgoal 2 is:
 {eval E (abs R)}

nstep_eval < search.
Subgoal 2:

Variables: E R B
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H2 : {step E B}*
H3 : {nstep B (abs R)}*
============================
 {eval E (abs R)}

nstep_eval < apply IH to H3.
Subgoal 2:

Variables: E R B
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H2 : {step E B}*
H3 : {nstep B (abs R)}*
H4 : {eval B (abs R)}
============================
 {eval E (abs R)}

nstep_eval < apply step_eval_lemma to H2 H4.
Subgoal 2:

Variables: E R B
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H2 : {step E B}*
H3 : {nstep B (abs R)}*
H4 : {eval B (abs R)}
H5 : {eval E (abs R)}
============================
 {eval E (abs R)}

nstep_eval < search.
Proof completed.
Abella < Theorem sr_eval : 
forall E V T, {eval E V} -> {of E T} -> {of V T}.


============================
 forall E V T, {eval E V} -> {of E T} -> {of V T}

sr_eval < induction on 1.

IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
============================
 forall E V T, {eval E V}@ -> {of E T} -> {of V T}

sr_eval < intros.

Variables: E V T
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H1 : {eval E V}@
H2 : {of E T}
============================
 {of V T}

sr_eval < case H1.
Subgoal 1:

Variables: T R
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H2 : {of (abs R) T}
============================
 {of (abs R) T}

Subgoal 2 is:
 {of V T}

sr_eval < search.
Subgoal 2:

Variables: V T N R M
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H2 : {of (app M N) T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
============================
 {of V T}

sr_eval < case H2.
Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
============================
 {of V T}

sr_eval < apply IH to H3 H5.
Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H7 : {of (abs R) (arrow U T)}
============================
 {of V T}

sr_eval < case H7.
Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
============================
 {of V T}

sr_eval <  inst H8 with n1 = N.
Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
H9 : {of N U |- of (R N) T}
============================
 {of V T}

sr_eval < cut H9 with H6.
Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
H9 : {of N U |- of (R N) T}
H10 : {of (R N) T}
============================
 {of V T}

sr_eval < apply IH to H4 H10.
Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
H9 : {of N U |- of (R N) T}
H10 : {of (R N) T}
H11 : {of V T}
============================
 {of V T}

sr_eval < search.
Proof completed.
Abella < Theorem sr_step : 
forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}.


============================
 forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}

sr_step < induction on 1.

IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
============================
 forall E1 E2 T, {step E1 E2}@ -> {of E1 T} -> {of E2 T}

sr_step < intros.

Variables: E1 E2 T
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H1 : {step E1 E2}@
H2 : {of E1 T}
============================
 {of E2 T}

sr_step < case H1.
Subgoal 1:

Variables: T M R
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of (app (abs R) M) T}
============================
 {of (R M) T}

Subgoal 2 is:
 {of (app M' N) T}

sr_step < case H2.
Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H3 : {of (abs R) (arrow U T)}
H4 : {of M U}
============================
 {of (R M) T}

Subgoal 2 is:
 {of (app M' N) T}

sr_step < case H3.
Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H4 : {of M U}
H5 : {of n1 U |- of (R n1) T}
============================
 {of (R M) T}

Subgoal 2 is:
 {of (app M' N) T}

sr_step <  inst H5 with n1 = M.
Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H4 : {of M U}
H5 : {of n1 U |- of (R n1) T}
H6 : {of M U |- of (R M) T}
============================
 {of (R M) T}

Subgoal 2 is:
 {of (app M' N) T}

sr_step < cut H6 with H4.
Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H4 : {of M U}
H5 : {of n1 U |- of (R n1) T}
H6 : {of M U |- of (R M) T}
H7 : {of (R M) T}
============================
 {of (R M) T}

Subgoal 2 is:
 {of (app M' N) T}

sr_step < search.
Subgoal 2:

Variables: T M' M N
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of (app M N) T}
H3 : {step M M'}*
============================
 {of (app M' N) T}

sr_step < case H2.
Subgoal 2:

Variables: T M' M N U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H3 : {step M M'}*
H4 : {of M (arrow U T)}
H5 : {of N U}
============================
 {of (app M' N) T}

sr_step < apply IH to H3 H4.
Subgoal 2:

Variables: T M' M N U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H3 : {step M M'}*
H4 : {of M (arrow U T)}
H5 : {of N U}
H6 : {of M' (arrow U T)}
============================
 {of (app M' N) T}

sr_step < search.
Proof completed.
Abella < Theorem sr_nstep : 
forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}.


============================
 forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}

sr_nstep < induction on 1.

IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
============================
 forall E1 E2 T, {nstep E1 E2}@ -> {of E1 T} -> {of E2 T}

sr_nstep < intros.

Variables: E1 E2 T
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H1 : {nstep E1 E2}@
H2 : {of E1 T}
============================
 {of E2 T}

sr_nstep < case H1.
Subgoal 1:

Variables: E2 T
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E2 T}
============================
 {of E2 T}

Subgoal 2 is:
 {of E2 T}

sr_nstep < search.
Subgoal 2:

Variables: E1 E2 T B
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E1 T}
H3 : {step E1 B}*
H4 : {nstep B E2}*
============================
 {of E2 T}

sr_nstep < apply sr_step to H3 H2.
Subgoal 2:

Variables: E1 E2 T B
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E1 T}
H3 : {step E1 B}*
H4 : {nstep B E2}*
H5 : {of B T}
============================
 {of E2 T}

sr_nstep < apply IH to H4 H5.
Subgoal 2:

Variables: E1 E2 T B
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E1 T}
H3 : {step E1 B}*
H4 : {nstep B E2}*
H5 : {of B T}
H6 : {of E2 T}
============================
 {of E2 T}

sr_nstep < search.
Proof completed.
Abella < Theorem type_subst : 
forall L E E' T T', nabla x, {L, of x T' |- of (E x) T} -> {L |- of E' T'} ->
  {L |- of (E E') T}.


============================
 forall L E E' T T', nabla x, {L, of x T' |- of (E x) T} ->
   {L |- of E' T'} -> {L |- of (E E') T}

type_subst < intros.

Variables: L E E' T T'
H1 : {L, of n1 T' |- of (E n1) T}
H2 : {L |- of E' T'}
============================
 {L |- of (E E') T}

type_subst <  inst H1 with n1 = E'.

Variables: L E E' T T'
H1 : {L, of n1 T' |- of (E n1) T}
H2 : {L |- of E' T'}
H3 : {L, of E' T' |- of (E E') T}
============================
 {L |- of (E E') T}

type_subst < cut H3 with H2.

Variables: L E E' T T'
H1 : {L, of n1 T' |- of (E n1) T}
H2 : {L |- of E' T'}
H3 : {L, of E' T' |- of (E E') T}
H4 : {L |- of (E E') T}
============================
 {L |- of (E E') T}

type_subst < search.
Proof completed.
Abella < Theorem of_self_app_absurd : 
forall T, {of (abs (x\app x x)) T} -> false.


============================
 forall T, {of (abs (x\app x x)) T} -> false

of_self_app_absurd < intros.

Variables: T
H1 : {of (abs (x\app x x)) T}
============================
 false

of_self_app_absurd < case H1.

Variables: U T1
H2 : {of n1 T1 |- of (app n1 n1) U}
============================
 false

of_self_app_absurd < case H2.
Subgoal 1:

Variables: U T1 U1
H3 : {of n1 T1 |- of n1 (arrow (U1 n1) U)}
H4 : {of n1 T1 |- of n1 (U1 n1)}
============================
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H3.
Subgoal 1:

Variables: U T1 U1 F
H4 : {of n1 T1 |- of n1 (U1 n1)}
H5 : {of n1 T1, [F n1] |- of n1 (arrow (U1 n1) U)}
H6 : member (F n1) (of n1 T1 :: nil)
============================
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H6.
Subgoal 1.1:

Variables: U T1 U1
H4 : {of n1 T1 |- of n1 (U1 n1)}
H5 : {of n1 T1, [of n1 T1] |- of n1 (arrow (U1 n1) U)}
============================
 false

Subgoal 1.2 is:
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H5.
Subgoal 1.1:

Variables: U T2
H4 : {of n1 (arrow T2 U) |- of n1 T2}
============================
 false

Subgoal 1.2 is:
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H4.
Subgoal 1.1:

Variables: U T2 F1
H7 : {of n1 (arrow T2 U), [F1 n1] |- of n1 T2}
H8 : member (F1 n1) (of n1 (arrow T2 U) :: nil)
============================
 false

Subgoal 1.2 is:
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H8.
Subgoal 1.1.1:

Variables: U T2
H7 : {of n1 (arrow T2 U), [of n1 (arrow T2 U)] |- of n1 T2}
============================
 false

Subgoal 1.1.2 is:
 false

Subgoal 1.2 is:
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H7.
Subgoal 1.1.2:

Variables: U T2 F1
H7 : {of n1 (arrow T2 U), [F1 n1] |- of n1 T2}
H9 : member (F1 n1) nil
============================
 false

Subgoal 1.2 is:
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H9.
Subgoal 1.2:

Variables: U T1 U1 F
H4 : {of n1 T1 |- of n1 (U1 n1)}
H5 : {of n1 T1, [F n1] |- of n1 (arrow (U1 n1) U)}
H7 : member (F n1) nil
============================
 false

Subgoal 2 is:
 false

of_self_app_absurd < case H7.
Subgoal 2:

Variables: U T1 F
H3 : {of n1 T1, [F n1] |- of (app n1 n1) U}
H4 : member (F n1) (of n1 T1 :: nil)
============================
 false

of_self_app_absurd < case H4.
Subgoal 2.1:

Variables: U T1
H3 : {of n1 T1, [of n1 T1] |- of (app n1 n1) U}
============================
 false

Subgoal 2.2 is:
 false

of_self_app_absurd < case H3.
Subgoal 2.2:

Variables: U T1 F
H3 : {of n1 T1, [F n1] |- of (app n1 n1) U}
H5 : member (F n1) nil
============================
 false

of_self_app_absurd < case H5.
Proof completed.
Abella < Theorem no_eval : 
forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V} -> false.


============================
 forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V} -> false

no_eval < induction on 1.

IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
============================
 forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}@ -> false

no_eval < intros.

Variables: V
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
H1 : {eval (app (abs (x\app x x)) (abs (x\app x x))) V}@
============================
 false

no_eval < case H1.

Variables: V R
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
H2 : {eval (abs (x\app x x)) (abs R)}*
H3 : {eval (R (abs (x\app x x))) V}*
============================
 false

no_eval < case H2.

Variables: V
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
H3 : {eval (app (abs (x\app x x)) (abs (x\app x x))) V}*
============================
 false

no_eval < apply IH to H3.
Proof completed.
Abella < CoDefine diverge : tm -> prop by 
diverge (app M N) := diverge M;
diverge (app M N) := exists R, {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 < search.
Proof completed.
Abella < Theorem eval_diverge_absurd : 
forall M V, {eval M V} -> diverge M -> false.


============================
 forall M V, {eval M V} -> diverge M -> false

eval_diverge_absurd < induction on 1.

IH : forall M V, {eval M V}* -> diverge M -> false
============================
 forall M V, {eval M V}@ -> diverge M -> false

eval_diverge_absurd < intros.

Variables: M V
IH : forall M V, {eval M V}* -> diverge M -> false
H1 : {eval M V}@
H2 : diverge M
============================
 false

eval_diverge_absurd < case H1.
Subgoal 1:

Variables: R
IH : forall M V, {eval M V}* -> diverge M -> false
H2 : diverge (abs R)
============================
 false

Subgoal 2 is:
 false

eval_diverge_absurd < case H2.
Subgoal 2:

Variables: V N R M1
IH : forall M V, {eval M V}* -> diverge M -> false
H2 : diverge (app M1 N)
H3 : {eval M1 (abs R)}*
H4 : {eval (R N) V}*
============================
 false

eval_diverge_absurd < case H2.
Subgoal 2.1:

Variables: V N R M1
IH : forall M V, {eval M V}* -> diverge M -> false
H3 : {eval M1 (abs R)}*
H4 : {eval (R N) V}*
H5 : diverge M1
============================
 false

Subgoal 2.2 is:
 false

eval_diverge_absurd < apply IH to H3 H5.
Subgoal 2.2:

Variables: V N R M1 R1
IH : forall M V, {eval M V}* -> diverge M -> false
H3 : {eval M1 (abs R)}*
H4 : {eval (R N) V}*
H5 : {eval M1 (abs R1)}
H6 : diverge (R1 N)
============================
 false

eval_diverge_absurd < apply eval_det to H3 H5.
Subgoal 2.2:

Variables: V N M1 R1
IH : forall M V, {eval M V}* -> diverge M -> false
H3 : {eval M1 (abs R1)}*
H4 : {eval (R1 N) V}*
H5 : {eval M1 (abs R1)}
H6 : diverge (R1 N)
============================
 false

eval_diverge_absurd < apply IH to H4 H6.
Proof completed.
Abella <