Welcome to Abella 1.3.6-dev1
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: E, V1, 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: E, V1, V2, 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: E, 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: E, 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: E, V1, V2, N, R, 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: E, V1, V2, N, R, 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: E1, E2, 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: E1, E2, E3, 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: E1, E2, E3, 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: E1, E2, 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: E1, E2, E3, M', 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: E1, E2, E3, 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: E1, E2, E3, M', 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: E, 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: E, R1, 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: E, 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: E, 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, B, 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, R1, R2, B, 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: M, 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: E, V, 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: E, 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: E, 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: E, 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: E, 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: A, B, 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: A, B, 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: A, B, 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: A, B, 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: E, 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: E, V, 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: E, 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: E, 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: E, 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: E, 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: E, 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: E, 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: E, 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: E1, E2, 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: E1, E2, 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: E1, E2, 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: E1, E2, 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: E1, E2, 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: E1, E2, 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: E1, E2, 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: E1, E2, 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: E1, 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 (x1\app x1 x1)) T} -> false.
============================
forall T, {of (abs (x1\app x1 x1)) T} -> false
of_self_app_absurd < intros.
Variables: T
H1 : {of (abs (x1\app x1 x1)) T}
============================
false
of_self_app_absurd < case H1.
Variables: T, U, T1
H2 : {of n1 T1 |- of (app n1 n1) U}
============================
false
of_self_app_absurd < case H2.
Subgoal 1:
Variables: T, U, T1
H3 : member (of (app n1 n1) U) (of n1 T1 :: nil)
============================
false
Subgoal 2 is:
false
of_self_app_absurd < case H3.
Subgoal 1:
Variables: T, U, T1
H4 : member (of (app n1 n1) U) nil
============================
false
Subgoal 2 is:
false
of_self_app_absurd < case H4.
Subgoal 2:
Variables: T, U, T1, U1
H3 : {of n1 T1 |- of n1 (arrow (U1 n1) U)}
H4 : {of n1 T1 |- of n1 (U1 n1)}
============================
false
of_self_app_absurd < case H4.
Subgoal 2:
Variables: T, U, T1, U1
H3 : {of n1 T1 |- of n1 (arrow (U1 n1) U)}
H5 : member (of n1 (U1 n1)) (of n1 T1 :: nil)
============================
false
of_self_app_absurd < case H5.
Subgoal 2.1:
Variables: T, U, T1, U1
H3 : {of n1 T1 |- of n1 (arrow T1 U)}
============================
false
Subgoal 2.2 is:
false
of_self_app_absurd < case H3.
Subgoal 2.1:
Variables: T, U, T1, U1
H6 : member (of n1 (arrow T1 U)) (of n1 T1 :: nil)
============================
false
Subgoal 2.2 is:
false
of_self_app_absurd < case H6.
Subgoal 2.1:
Variables: T, U, T1, U1
H7 : member (of n1 (arrow T1 U)) nil
============================
false
Subgoal 2.2 is:
false
of_self_app_absurd < case H7.
Subgoal 2.2:
Variables: T, U, T1, U1
H3 : {of n1 T1 |- of n1 (arrow (U1 n1) U)}
H6 : member (of n1 (U1 n1)) nil
============================
false
of_self_app_absurd < case H6.
Proof completed.
Abella < Theorem no_eval :
forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V} -> false.
============================
forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V} ->
false
no_eval < induction on 1.
IH : forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V}* ->
false
============================
forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V}@ ->
false
no_eval < intros.
Variables: V
IH : forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V}* ->
false
H1 : {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V}@
============================
false
no_eval < case H1.
Variables: V, R
IH : forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V}* ->
false
H2 : {eval (abs (x1\app x1 x1)) (abs R)}*
H3 : {eval (R (abs (x1\app x1 x1))) V}*
============================
false
no_eval < case H2.
Variables: V, R
IH : forall V, {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) V}* ->
false
H3 : {eval (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) 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 (x1\app x1 x1)) (abs (x1\app x1 x1))).
============================
diverge (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1)))
omega_diverge < coinduction.
CH : diverge (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) +
============================
diverge (app (abs (x1\app x1 x1)) (abs (x1\app x1 x1))) #
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: M, V, 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: M, 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: M, 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: M, 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: M, V, N, R, 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 < Goodbye.
