Welcome to Abella 1.1.3-dev2
Reading clauses from stlc-strong-norm.mod
Abella < Define sn M := forall N, {step M N} -> sn N.
Abella < Define neutral M := forall A R, M = abs A R -> false.
Abella < Define reduce M top := {of M top} /\ sn M.
Abella < Define reduce M (arrow A B) := {of M (arrow A B)} /\ (forall U, reduce U A -> reduce (app M U) B).
Warning: reduce/2 might not be stratified
Abella < Theorem reduce_of :
forall A M, reduce M A -> {of M A}.
1 subgoal(s).
============================
forall A M, reduce M A -> {of M A}
reduce_of < intros.
1 subgoal(s).
Variables: A, M
H1 : reduce M A
============================
{of M A}
reduce_of < case H1.
2 subgoal(s).
Variables: A, M
H2 : {of M top}
H3 : sn M
============================
{of M top}
subgoal 2 is:
{of M (arrow A1 B)}
reduce_of < search.
1 subgoal(s).
Variables: A, M, B, A1
H2 : {of M (arrow A1 B)}
H3 : forall U, reduce U A1 -> reduce (app M U) B
============================
{of M (arrow A1 B)}
reduce_of < search.
Proof completed.
Abella < Define ctx nil.
Abella < Define nabla x, ctx (of x A :: L) := {type A} /\ ctx L.
Abella < Define nabla x, name x.
Abella < Theorem ctx_member :
forall E L, ctx L -> member E L -> (exists X A, E = of X A /\ name X /\
{type A}).
1 subgoal(s).
============================
forall E L, ctx L -> member E L -> (exists X A, E = of X A /\ name X /\
{type A})
ctx_member < induction on 1.
1 subgoal(s).
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
============================
forall E L, ctx L @ -> member E L -> (exists X A, E = of X A /\ name X /\
{type A})
ctx_member < intros.
1 subgoal(s).
Variables: E, L
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
H1 : ctx L @
H2 : member E L
============================
exists X A, E = of X A /\ name X /\ {type A}
ctx_member < case H1.
2 subgoal(s).
Variables: E, L
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
H2 : member E nil
============================
exists X A, E = of X A /\ name X /\ {type A}
subgoal 2 is:
exists X A, E n1 = of X A /\ name X /\ {type A}
ctx_member < case H2.
1 subgoal(s).
Variables: E, L, L1, A
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
H2 : member (E n1) (of n1 A :: L1)
H3 : {type A}
H4 : ctx L1 *
============================
exists X A, E n1 = of X A /\ name X /\ {type A}
ctx_member < case H2.
2 subgoal(s).
Variables: E, L, L1, A
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
H3 : {type A}
H4 : ctx L1 *
============================
exists X A1, of n1 A = of X A1 /\ name X /\ {type A1}
subgoal 2 is:
exists X A, E n1 = of X A /\ name X /\ {type A}
ctx_member < search.
1 subgoal(s).
Variables: E, L, L1, A
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
H3 : {type A}
H4 : ctx L1 *
H5 : member (E n1) L1
============================
exists X A, E n1 = of X A /\ name X /\ {type A}
ctx_member < apply IH to H4 H5.
1 subgoal(s).
Variables: E, L, L1, A, X, A1
IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\
name X /\ {type A})
H3 : {type A}
H4 : ctx L1 *
H5 : member (of (X n1) (A1 n1)) L1
H6 : name (X n1)
H7 : {type (A1 n1)}
============================
exists X1 A, of (X n1) (A1 n1) = of X1 A /\ name X1 /\ {type A}
ctx_member < search.
Proof completed.
Abella < Theorem type_ignores_ctx :
forall L A, ctx L -> {L |- type A} -> {type A}.
1 subgoal(s).
============================
forall L A, ctx L -> {L |- type A} -> {type A}
type_ignores_ctx < induction on 2.
1 subgoal(s).
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
============================
forall L A, ctx L -> {L |- type A}@ -> {type A}
type_ignores_ctx < intros.
1 subgoal(s).
Variables: L, A
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
H1 : ctx L
H2 : {L |- type A}@
============================
{type A}
type_ignores_ctx < case H2.
3 subgoal(s).
Variables: L, A
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
H1 : ctx L
H3 : member (type A) L
============================
{type A}
subgoal 2 is:
{type top}
subgoal 3 is:
{type (arrow A1 B)}
type_ignores_ctx < apply ctx_member to H1 H3.
2 subgoal(s).
Variables: L, A
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
H1 : ctx L
============================
{type top}
subgoal 2 is:
{type (arrow A1 B)}
type_ignores_ctx < search.
1 subgoal(s).
Variables: L, A, B, A1
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
H1 : ctx L
H3 : {L |- type A1}*
H4 : {L |- type B}*
============================
{type (arrow A1 B)}
type_ignores_ctx < apply IH to H1 H3.
1 subgoal(s).
Variables: L, A, B, A1
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
H1 : ctx L
H3 : {L |- type A1}*
H4 : {L |- type B}*
H5 : {type A1}
============================
{type (arrow A1 B)}
type_ignores_ctx < apply IH to H1 H4.
1 subgoal(s).
Variables: L, A, B, A1
IH : forall L A, ctx L -> {L |- type A}* -> {type A}
H1 : ctx L
H3 : {L |- type A1}*
H4 : {L |- type B}*
H5 : {type A1}
H6 : {type B}
============================
{type (arrow A1 B)}
type_ignores_ctx < search.
Proof completed.
Abella < Theorem case_of_app :
forall L M N B, ctx L -> {L |- of (app M N) B} -> (exists A,
{L |- of M (arrow A B)} /\ {L |- of N A}).
1 subgoal(s).
============================
forall L M N B, ctx L -> {L |- of (app M N) B} -> (exists A,
{L |- of M (arrow A B)} /\ {L |- of N A})
case_of_app < intros.
1 subgoal(s).
Variables: L, M, N, B
H1 : ctx L
H2 : {L |- of (app M N) B}
============================
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < case H2.
2 subgoal(s).
Variables: L, M, N, B
H1 : ctx L
H3 : member (of (app M N) B) L
============================
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
subgoal 2 is:
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < apply ctx_member to H1 H3.
2 subgoal(s).
Variables: L, M, N, B, X, A
H1 : ctx L
H3 : member (of (app M N) A) L
H4 : name (app M N)
H5 : {type A}
============================
exists A1, {L |- of M (arrow A1 A)} /\ {L |- of N A1}
subgoal 2 is:
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < case H4.
1 subgoal(s).
Variables: L, M, N, B, A
H1 : ctx L
H3 : {L |- of M (arrow A B)}
H4 : {L |- of N A}
============================
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < search.
Proof completed.
Abella < Theorem case_of_abs :
forall L M A B, ctx L -> {L |- of (abs A M) B} -> (exists C, B = arrow A C /\
{type A} /\ (nabla x, {L, of x A |- of (M x) C})).
1 subgoal(s).
============================
forall L M A B, ctx L -> {L |- of (abs A M) B} -> (exists C,
B = arrow A C /\ {type A} /\ (nabla x, {L, of x A |- of (M x) C}))
case_of_abs < intros.
1 subgoal(s).
Variables: L, M, A, B
H1 : ctx L
H2 : {L |- of (abs A M) B}
============================
exists C, B = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
case_of_abs < case H2.
2 subgoal(s).
Variables: L, M, A, B
H1 : ctx L
H3 : member (of (abs A M) B) L
============================
exists C, B = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
subgoal 2 is:
exists C, arrow A B1 = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
case_of_abs < apply ctx_member to H1 H3.
2 subgoal(s).
Variables: L, M, A, B, X, A1
H1 : ctx L
H3 : member (of (abs A M) A1) L
H4 : name (abs A M)
H5 : {type A1}
============================
exists C, A1 = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
subgoal 2 is:
exists C, arrow A B1 = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
case_of_abs < case H4.
1 subgoal(s).
Variables: L, M, A, B, B1
H1 : ctx L
H3 : {L |- type A}
H4 : {L, of n1 A |- of (M n1) B1}
============================
exists C, arrow A B1 = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
case_of_abs < apply type_ignores_ctx to H1 H3.
1 subgoal(s).
Variables: L, M, A, B, B1
H1 : ctx L
H3 : {L |- type A}
H4 : {L, of n1 A |- of (M n1) B1}
H5 : {type A}
============================
exists C, arrow A B1 = arrow A C /\ {type A} /\ (nabla x,
{L, of x A |- of (M x) C})
case_of_abs < search.
Proof completed.
Abella < Theorem of_step_ext :
forall L M N A, ctx L -> {L |- of M A} -> {step M N} -> {L |- of N A}.
1 subgoal(s).
============================
forall L M N A, ctx L -> {L |- of M A} -> {step M N} -> {L |- of N A}
of_step_ext < induction on 3.
1 subgoal(s).
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
============================
forall L M N A, ctx L -> {L |- of M A} -> {step M N}@ -> {L |- of N A}
of_step_ext < intros.
1 subgoal(s).
Variables: L, M, N, A
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of M A}
H3 : {step M N}@
============================
{L |- of N A}
of_step_ext < case H3.
4 subgoal(s).
Variables: L, M, N, A, M', N1, M1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step M1 M'}*
============================
{L |- of (app M' N1) A}
subgoal 2 is:
{L |- of (app M1 N') A}
subgoal 3 is:
{L |- of (R M1) A}
subgoal 4 is:
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_app to H1 H2.
4 subgoal(s).
Variables: L, M, N, A, M', N1, M1, A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step M1 M'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
============================
{L |- of (app M' N1) A}
subgoal 2 is:
{L |- of (app M1 N') A}
subgoal 3 is:
{L |- of (R M1) A}
subgoal 4 is:
{L |- of (abs A1 R') A}
of_step_ext < apply IH to H1 H5 H4.
4 subgoal(s).
Variables: L, M, N, A, M', N1, M1, A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step M1 M'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
H7 : {L |- of M' (arrow A1 A)}
============================
{L |- of (app M' N1) A}
subgoal 2 is:
{L |- of (app M1 N') A}
subgoal 3 is:
{L |- of (R M1) A}
subgoal 4 is:
{L |- of (abs A1 R') A}
of_step_ext < search.
3 subgoal(s).
Variables: L, M, N, A, N', N1, M1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step N1 N'}*
============================
{L |- of (app M1 N') A}
subgoal 2 is:
{L |- of (R M1) A}
subgoal 3 is:
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_app to H1 H2.
3 subgoal(s).
Variables: L, M, N, A, N', N1, M1, A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step N1 N'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
============================
{L |- of (app M1 N') A}
subgoal 2 is:
{L |- of (R M1) A}
subgoal 3 is:
{L |- of (abs A1 R') A}
of_step_ext < apply IH to H1 H6 H4.
3 subgoal(s).
Variables: L, M, N, A, N', N1, M1, A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step N1 N'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
H7 : {L |- of N' A1}
============================
{L |- of (app M1 N') A}
subgoal 2 is:
{L |- of (R M1) A}
subgoal 3 is:
{L |- of (abs A1 R') A}
of_step_ext < search.
2 subgoal(s).
Variables: L, M, N, A, M1, R, A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) A}
============================
{L |- of (R M1) A}
subgoal 2 is:
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_app to H1 H2.
2 subgoal(s).
Variables: L, M, N, A, M1, R, A1, A2
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) A}
H4 : {L |- of (abs A1 R) (arrow A2 A)}
H5 : {L |- of M1 A2}
============================
{L |- of (R M1) A}
subgoal 2 is:
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_abs to H1 H4.
2 subgoal(s).
Variables: L, M, N, A, M1, R, A1, A2, C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {type A1}
H7 : {L, of n1 A1 |- of (R n1) C}
============================
{L |- of (R M1) C}
subgoal 2 is:
{L |- of (abs A1 R') A}
of_step_ext < inst H7 with n1 = M1.
2 subgoal(s).
Variables: L, M, N, A, M1, R, A1, A2, C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {type A1}
H7 : {L, of n1 A1 |- of (R n1) C}
H8 : {L, of M1 A1 |- of (R M1) C}
============================
{L |- of (R M1) C}
subgoal 2 is:
{L |- of (abs A1 R') A}
of_step_ext < cut H8 with H5.
2 subgoal(s).
Variables: L, M, N, A, M1, R, A1, A2, C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {type A1}
H7 : {L, of n1 A1 |- of (R n1) C}
H8 : {L, of M1 A1 |- of (R M1) C}
H9 : {L |- of (R M1) C}
============================
{L |- of (R M1) C}
subgoal 2 is:
{L |- of (abs A1 R') A}
of_step_ext < search.
1 subgoal(s).
Variables: L, M, N, A, R', R, A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (abs A1 R) A}
H4 : {step (R n1) (R' n1)}*
============================
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_abs to H1 H2.
1 subgoal(s).
Variables: L, M, N, A, R', R, A1, C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (abs A1 R) (arrow A1 C)}
H4 : {step (R n1) (R' n1)}*
H5 : {type A1}
H6 : {L, of n1 A1 |- of (R n1) C}
============================
{L |- of (abs A1 R') (arrow A1 C)}
of_step_ext < apply IH to _ H6 H4.
1 subgoal(s).
Variables: L, M, N, A, R', R, A1, C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (abs A1 R) (arrow A1 C)}
H4 : {step (R n1) (R' n1)}*
H5 : {type A1}
H6 : {L, of n1 A1 |- of (R n1) C}
H7 : {L, of n1 A1 |- of (R' n1) C}
============================
{L |- of (abs A1 R') (arrow A1 C)}
of_step_ext < search.
Proof completed.
Abella < Theorem of_step :
forall M N A, {of M A} -> {step M N} -> {of N A}.
1 subgoal(s).
============================
forall M N A, {of M A} -> {step M N} -> {of N A}
of_step < intros.
1 subgoal(s).
Variables: M, N, A
H1 : {of M A}
H2 : {step M N}
============================
{of N A}
of_step < apply of_step_ext to _ H1 H2.
1 subgoal(s).
Variables: M, N, A
H1 : {of M A}
H2 : {step M N}
H3 : {of N A}
============================
{of N A}
of_step < search.
Proof completed.
Abella < Theorem sn_step :
forall M N, sn M -> {step M N} -> sn N.
1 subgoal(s).
============================
forall M N, sn M -> {step M N} -> sn N
sn_step < intros.
1 subgoal(s).
Variables: M, N
H1 : sn M
H2 : {step M N}
============================
sn N
sn_step < case H1.
1 subgoal(s).
Variables: M, N
H2 : {step M N}
H3 : forall N, {step M N} -> sn N
============================
sn N
sn_step < apply H3 to H2.
1 subgoal(s).
Variables: M, N
H2 : {step M N}
H3 : forall N, {step M N} -> sn N
H4 : sn N
============================
sn N
sn_step < search.
Proof completed.
Abella < Theorem reduce_step :
forall M N A, reduce M A -> {step M N} -> reduce N A.
1 subgoal(s).
============================
forall M N A, reduce M A -> {step M N} -> reduce N A
reduce_step < induction on 1.
1 subgoal(s).
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
============================
forall M N A, reduce M A @ -> {step M N} -> reduce N A
reduce_step < intros.
1 subgoal(s).
Variables: M, N, A
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H1 : reduce M A @
H2 : {step M N}
============================
reduce N A
reduce_step < case H1.
2 subgoal(s).
Variables: M, N, A
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M top}
H4 : sn M
============================
reduce N top
subgoal 2 is:
reduce N (arrow A1 B)
reduce_step < apply of_step to H3 H2.
2 subgoal(s).
Variables: M, N, A
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M top}
H4 : sn M
H5 : {of N top}
============================
reduce N top
subgoal 2 is:
reduce N (arrow A1 B)
reduce_step < apply sn_step to H4 H2.
2 subgoal(s).
Variables: M, N, A
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M top}
H4 : sn M
H5 : {of N top}
H6 : sn N
============================
reduce N top
subgoal 2 is:
reduce N (arrow A1 B)
reduce_step < search.
1 subgoal(s).
Variables: M, N, A, B, A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
============================
reduce N (arrow A1 B)
reduce_step < unfold.
2 subgoal(s).
Variables: M, N, A, B, A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
============================
{of N (arrow A1 B)}
subgoal 2 is:
forall U, reduce U A1 -> reduce (app N U) B
reduce_step < apply of_step to H3 H2.
2 subgoal(s).
Variables: M, N, A, B, A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : {of N (arrow A1 B)}
============================
{of N (arrow A1 B)}
subgoal 2 is:
forall U, reduce U A1 -> reduce (app N U) B
reduce_step < search.
1 subgoal(s).
Variables: M, N, A, B, A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
============================
forall U, reduce U A1 -> reduce (app N U) B
reduce_step < intros.
1 subgoal(s).
Variables: M, N, A, B, A1, U
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : reduce U A1
============================
reduce (app N U) B
reduce_step < apply H4 to H5.
1 subgoal(s).
Variables: M, N, A, B, A1, U
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : reduce U A1
H6 : reduce (app M U) B *
============================
reduce (app N U) B
reduce_step < apply IH to H6 _.
1 subgoal(s).
Variables: M, N, A, B, A1, U
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : reduce U A1
H6 : reduce (app M U) B *
H7 : reduce (app N U) B
============================
reduce (app N U) B
reduce_step < search.
Proof completed.
Abella < Theorem sn_app_c :
forall M, sn (app M c) -> sn M.
1 subgoal(s).
============================
forall M, sn (app M c) -> sn M
sn_app_c < induction on 1.
1 subgoal(s).
IH : forall M, sn (app M c) * -> sn M
============================
forall M, sn (app M c) @ -> sn M
sn_app_c < intros.
1 subgoal(s).
Variables: M
IH : forall M, sn (app M c) * -> sn M
H1 : sn (app M c) @
============================
sn M
sn_app_c < case H1.
1 subgoal(s).
Variables: M
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
============================
sn M
sn_app_c < unfold.
1 subgoal(s).
Variables: M
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
============================
forall N, {step M N} -> sn N
sn_app_c < intros.
1 subgoal(s).
Variables: M, N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
============================
sn N
sn_app_c < assert {step (app M c) (app N c)}.
1 subgoal(s).
Variables: M, N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
H4 : {step (app M c) (app N c)}
============================
sn N
sn_app_c < apply H2 to H4.
1 subgoal(s).
Variables: M, N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
H4 : {step (app M c) (app N c)}
H5 : sn (app N c) *
============================
sn N
sn_app_c < apply IH to H5.
1 subgoal(s).
Variables: M, N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
H4 : {step (app M c) (app N c)}
H5 : sn (app N c) *
H6 : sn N
============================
sn N
sn_app_c < search.
Proof completed.
Abella < Theorem cr1_cr3 :
(forall A M, {type A} -> reduce M A -> sn M) /\ (forall A M, neutral M ->
{of M A} -> {type A} -> (forall P, {step M P} -> reduce P A) -> reduce M A).
1 subgoal(s).
============================
(forall A M, {type A} -> reduce M A -> sn M) /\ (forall A M, neutral M ->
{of M A} -> {type A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A)
cr1_cr3 < induction on 1 3.
1 subgoal(s).
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
============================
(forall A M, {type A}@ -> reduce M A -> sn M) /\ (forall A M, neutral M ->
{of M A} -> {type A}@ -> (forall P, {step M P} -> reduce P A) ->
reduce M A)
cr1_cr3 < split*.
2 subgoal(s).
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
============================
forall A M, {type A}@ -> reduce M A -> sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < intros.
2 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : {type A}@
H2 : reduce M A
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < case H2.
3 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : {type top}@
H3 : {of M top}
H4 : sn M
============================
sn M
subgoal 2 is:
sn M
subgoal 3 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < search.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : {type (arrow A1 B)}@
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < case H1.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < assert neutral c.
3 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
============================
neutral c
subgoal 2 is:
sn M
subgoal 3 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < unfold.
3 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
============================
forall A R, c = abs A R -> false
subgoal 2 is:
sn M
subgoal 3 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < intros.
3 subgoal(s).
Variables: A, M, B, A1, A2, R
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : c = abs A2 R
============================
false
subgoal 2 is:
sn M
subgoal 3 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < case H7.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < assert {of c A1}.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < assert forall P, {step c P} -> reduce P A1.
3 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
============================
forall P, {step c P} -> reduce P A1
subgoal 2 is:
sn M
subgoal 3 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < intros.
3 subgoal(s).
Variables: A, M, B, A1, P
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
H9 : {step c P}
============================
reduce P A1
subgoal 2 is:
sn M
subgoal 3 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < case H9.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < apply IH1 to H7 H8 H5 H9.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : reduce c A1
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < apply H4 to H10.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : reduce c A1
H11 : reduce (app M c) B
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < apply IH to H6 H11.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : reduce c A1
H11 : reduce (app M c) B
H12 : sn (app M c)
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < apply sn_app_c to H12.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {type A1}*
H6 : {type B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : reduce c A1
H11 : reduce (app M c) B
H12 : sn (app M c)
H13 : sn M
============================
sn M
subgoal 2 is:
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < search.
1 subgoal(s).
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
============================
forall A M, neutral M -> {of M A} -> {type A}@ -> (forall P, {step M P} ->
reduce P A) -> reduce M A
cr1_cr3 < intros.
1 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M A}
H4 : {type A}@
H5 : forall P, {step M P} -> reduce P A
============================
reduce M A
cr1_cr3 < case H4 (keep).
2 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
============================
reduce M top
subgoal 2 is:
reduce M (arrow A1 B)
cr1_cr3 < unfold.
3 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
============================
{of M top}
subgoal 2 is:
sn M
subgoal 3 is:
reduce M (arrow A1 B)
cr1_cr3 < search.
2 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
============================
sn M
subgoal 2 is:
reduce M (arrow A1 B)
cr1_cr3 < unfold.
2 subgoal(s).
Variables: A, M
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
============================
forall N, {step M N} -> sn N
subgoal 2 is:
reduce M (arrow A1 B)
cr1_cr3 < intros.
2 subgoal(s).
Variables: A, M, N
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
============================
sn N
subgoal 2 is:
reduce M (arrow A1 B)
cr1_cr3 < apply H5 to H6.
2 subgoal(s).
Variables: A, M, N
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
H7 : reduce N top
============================
sn N
subgoal 2 is:
reduce M (arrow A1 B)
cr1_cr3 < apply H1 to H4 H7.
2 subgoal(s).
Variables: A, M, N
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M top}
H4 : {type top}@
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
H7 : reduce N top
H8 : sn N
============================
sn N
subgoal 2 is:
reduce M (arrow A1 B)
cr1_cr3 < search.
1 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
============================
reduce M (arrow A1 B)
cr1_cr3 < unfold.
2 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
============================
{of M (arrow A1 B)}
subgoal 2 is:
forall U, reduce U A1 -> reduce (app M U) B
cr1_cr3 < search.
1 subgoal(s).
Variables: A, M, B, A1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
============================
forall U, reduce U A1 -> reduce (app M U) B
cr1_cr3 < intros.
1 subgoal(s).
Variables: A, M, B, A1, U
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
============================
reduce (app M U) B
cr1_cr3 < apply IH to H6 H8.
1 subgoal(s).
Variables: A, M, B, A1, U
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
============================
reduce (app M U) B
cr1_cr3 < assert forall U, sn U -> reduce U A1 -> reduce (app M U) B.
2 subgoal(s).
Variables: A, M, B, A1, U
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
============================
forall U, sn U -> reduce U A1 -> reduce (app M U) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < induction on 1.
2 subgoal(s).
Variables: A, M, B, A1, U
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
============================
forall U, sn U @@ -> reduce U A1 -> reduce (app M U) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < intros.
2 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H10 : sn U1 @@
H11 : reduce U1 A1
============================
reduce (app M U1) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < case H10.
2 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
============================
reduce (app M U1) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < assert forall P, {step (app M U1) P} -> reduce P B.
3 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
============================
forall P, {step (app M U1) P} -> reduce P B
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < intros.
3 subgoal(s).
Variables: A, M, B, A1, U, U1, P
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : {step (app M U1) P}
============================
reduce P B
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < case H13.
5 subgoal(s).
Variables: A, M, B, A1, U, U1, P, M'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step M M'}
============================
reduce (app M' U1) B
subgoal 2 is:
reduce (app M N') B
subgoal 3 is:
reduce (R U1) B
subgoal 4 is:
reduce (app M U1) B
subgoal 5 is:
reduce (app M U) B
cr1_cr3 < apply H5 to H14.
5 subgoal(s).
Variables: A, M, B, A1, U, U1, P, M'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step M M'}
H15 : reduce M' (arrow A1 B)
============================
reduce (app M' U1) B
subgoal 2 is:
reduce (app M N') B
subgoal 3 is:
reduce (R U1) B
subgoal 4 is:
reduce (app M U1) B
subgoal 5 is:
reduce (app M U) B
cr1_cr3 < case H15.
5 subgoal(s).
Variables: A, M, B, A1, U, U1, P, M'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step M M'}
H16 : {of M' (arrow A1 B)}
H17 : forall U, reduce U A1 -> reduce (app M' U) B
============================
reduce (app M' U1) B
subgoal 2 is:
reduce (app M N') B
subgoal 3 is:
reduce (R U1) B
subgoal 4 is:
reduce (app M U1) B
subgoal 5 is:
reduce (app M U) B
cr1_cr3 < apply H17 to H11.
5 subgoal(s).
Variables: A, M, B, A1, U, U1, P, M'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step M M'}
H16 : {of M' (arrow A1 B)}
H17 : forall U, reduce U A1 -> reduce (app M' U) B
H18 : reduce (app M' U1) B
============================
reduce (app M' U1) B
subgoal 2 is:
reduce (app M N') B
subgoal 3 is:
reduce (R U1) B
subgoal 4 is:
reduce (app M U1) B
subgoal 5 is:
reduce (app M U) B
cr1_cr3 < search.
4 subgoal(s).
Variables: A, M, B, A1, U, U1, P, N'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step U1 N'}
============================
reduce (app M N') B
subgoal 2 is:
reduce (R U1) B
subgoal 3 is:
reduce (app M U1) B
subgoal 4 is:
reduce (app M U) B
cr1_cr3 < apply H12 to H14.
4 subgoal(s).
Variables: A, M, B, A1, U, U1, P, N'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step U1 N'}
H15 : sn N' **
============================
reduce (app M N') B
subgoal 2 is:
reduce (R U1) B
subgoal 3 is:
reduce (app M U1) B
subgoal 4 is:
reduce (app M U) B
cr1_cr3 < apply reduce_step to H11 H14.
4 subgoal(s).
Variables: A, M, B, A1, U, U1, P, N'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step U1 N'}
H15 : sn N' **
H16 : reduce N' A1
============================
reduce (app M N') B
subgoal 2 is:
reduce (R U1) B
subgoal 3 is:
reduce (app M U1) B
subgoal 4 is:
reduce (app M U) B
cr1_cr3 < apply IH2 to H15 H16.
4 subgoal(s).
Variables: A, M, B, A1, U, U1, P, N'
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : {step U1 N'}
H15 : sn N' **
H16 : reduce N' A1
H17 : reduce (app M N') B
============================
reduce (app M N') B
subgoal 2 is:
reduce (R U1) B
subgoal 3 is:
reduce (app M U1) B
subgoal 4 is:
reduce (app M U) B
cr1_cr3 < search.
3 subgoal(s).
Variables: A, M, B, A1, U, U1, P, R, A2
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral (abs A2 R)
H3 : {of (abs A2 R) (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step (abs A2 R) P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app (abs A2 R) U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
============================
reduce (R U1) B
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < case H2.
3 subgoal(s).
Variables: A, M, B, A1, U, U1, P, R, A2
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H3 : {of (abs A2 R) (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step (abs A2 R) P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app (abs A2 R) U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H14 : forall A R1, abs A2 R = abs A R1 -> false
============================
reduce (R U1) B
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < apply H14 to _.
2 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
============================
reduce (app M U1) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < assert neutral (app M U1).
3 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
============================
neutral (app M U1)
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < unfold.
3 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
============================
forall A R, app M U1 = abs A R -> false
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < intros.
3 subgoal(s).
Variables: A, M, B, A1, U, U1, A2, R
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
H14 : app M U1 = abs A2 R
============================
false
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < case H14.
2 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
H14 : neutral (app M U1)
============================
reduce (app M U1) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < assert {of (app M U1) B}.
3 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
H14 : neutral (app M U1)
============================
{of (app M U1) B}
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < apply reduce_of to H11.
3 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
H14 : neutral (app M U1)
H15 : {of U1 A1}
============================
{of (app M U1) B}
subgoal 2 is:
reduce (app M U1) B
subgoal 3 is:
reduce (app M U) B
cr1_cr3 < search.
2 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
H14 : neutral (app M U1)
H15 : {of (app M U1) B}
============================
reduce (app M U1) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < apply IH1 to H14 H15 H7 H13.
2 subgoal(s).
Variables: A, M, B, A1, U, U1
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
IH2 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H11 : reduce U1 A1
H12 : forall N, {step U1 N} -> sn N **
H13 : forall P, {step (app M U1) P} -> reduce P B
H14 : neutral (app M U1)
H15 : {of (app M U1) B}
H16 : reduce (app M U1) B
============================
reduce (app M U1) B
subgoal 2 is:
reduce (app M U) B
cr1_cr3 < search.
1 subgoal(s).
Variables: A, M, B, A1, U
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
H10 : forall U, sn U -> reduce U A1 -> reduce (app M U) B
============================
reduce (app M U) B
cr1_cr3 < apply H10 to H9 H8.
1 subgoal(s).
Variables: A, M, B, A1, U
IH : forall A M, {type A}* -> reduce M A -> sn M
IH1 : forall A M, neutral M -> {of M A} -> {type A}* -> (forall P,
{step M P} -> reduce P A) -> reduce M A
H1 : forall A M, {type A}@ -> reduce M A -> sn M
H2 : neutral M
H3 : {of M (arrow A1 B)}
H4 : {type (arrow A1 B)}@
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {type A1}*
H7 : {type B}*
H8 : reduce U A1
H9 : sn U
H10 : forall U, sn U -> reduce U A1 -> reduce (app M U) B
H11 : reduce (app M U) B
============================
reduce (app M U) B
cr1_cr3 < search.
Proof completed.
Abella < Theorem reduce_sn :
forall A M, {type A} -> reduce M A -> sn M.
1 subgoal(s).
============================
forall A M, {type A} -> reduce M A -> sn M
reduce_sn < apply cr1_cr3.
1 subgoal(s).
H1 : forall A M, {type A} -> reduce M A -> sn M
H2 : forall A M, neutral M -> {of M A} -> {type A} -> (forall P,
{step M P} -> reduce P A) -> reduce M A
============================
forall A M, {type A} -> reduce M A -> sn M
reduce_sn < search.
Proof completed.
Abella < Theorem neutral_step_reduce :
forall A M, neutral M -> {of M A} -> {type A} -> (forall P, {step M P} ->
reduce P A) -> reduce M A.
1 subgoal(s).
============================
forall A M, neutral M -> {of M A} -> {type A} -> (forall P, {step M P} ->
reduce P A) -> reduce M A
neutral_step_reduce < apply cr1_cr3.
1 subgoal(s).
H1 : forall A M, {type A} -> reduce M A -> sn M
H2 : forall A M, neutral M -> {of M A} -> {type A} -> (forall P,
{step M P} -> reduce P A) -> reduce M A
============================
forall A M, neutral M -> {of M A} -> {type A} -> (forall P, {step M P} ->
reduce P A) -> reduce M A
neutral_step_reduce < search.
Proof completed.
Abella < Theorem of_type_ext :
forall L M A, ctx L -> {L |- of M A} -> {type A}.
1 subgoal(s).
============================
forall L M A, ctx L -> {L |- of M A} -> {type A}
of_type_ext < induction on 2.
1 subgoal(s).
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
============================
forall L M A, ctx L -> {L |- of M A}@ -> {type A}
of_type_ext < intros.
1 subgoal(s).
Variables: L, M, A
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H2 : {L |- of M A}@
============================
{type A}
of_type_ext < case H2.
4 subgoal(s).
Variables: L, M, A
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : member (of M A) L
============================
{type A}
subgoal 2 is:
{type A}
subgoal 3 is:
{type (arrow A1 B)}
subgoal 4 is:
{type A}
of_type_ext < apply ctx_member to H1 H3.
4 subgoal(s).
Variables: L, M, A, X, A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : member (of X A1) L
H4 : name X
H5 : {type A1}
============================
{type A1}
subgoal 2 is:
{type A}
subgoal 3 is:
{type (arrow A1 B)}
subgoal 4 is:
{type A}
of_type_ext < search.
3 subgoal(s).
Variables: L, M, A, A1, N, M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
============================
{type A}
subgoal 2 is:
{type (arrow A1 B)}
subgoal 3 is:
{type A}
of_type_ext < apply IH to H1 H3.
3 subgoal(s).
Variables: L, M, A, A1, N, M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
H5 : {type (arrow A1 A)}
============================
{type A}
subgoal 2 is:
{type (arrow A1 B)}
subgoal 3 is:
{type A}
of_type_ext < case H5.
3 subgoal(s).
Variables: L, M, A, A1, N, M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
H6 : {type A1}
H7 : {type A}
============================
{type A}
subgoal 2 is:
{type (arrow A1 B)}
subgoal 3 is:
{type A}
of_type_ext < search.
2 subgoal(s).
Variables: L, M, A, B, R, A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- type A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
============================
{type (arrow A1 B)}
subgoal 2 is:
{type A}
of_type_ext < apply type_ignores_ctx to H1 H3.
2 subgoal(s).
Variables: L, M, A, B, R, A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- type A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
H5 : {type A1}
============================
{type (arrow A1 B)}
subgoal 2 is:
{type A}
of_type_ext < apply IH to _ H4.
2 subgoal(s).
Variables: L, M, A, B, R, A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- type A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
H5 : {type A1}
H6 : {type B}
============================
{type (arrow A1 B)}
subgoal 2 is:
{type A}
of_type_ext < search.
1 subgoal(s).
Variables: L, M, A
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- type A}*
============================
{type A}
of_type_ext < apply type_ignores_ctx to H1 H3.
1 subgoal(s).
Variables: L, M, A
IH : forall L M A, ctx L -> {L |- of M A}* -> {type A}
H1 : ctx L
H3 : {L |- type A}*
H4 : {type A}
============================
{type A}
of_type_ext < search.
Proof completed.
Abella < Theorem of_type :
forall M A, {of M A} -> {type A}.
1 subgoal(s).
============================
forall M A, {of M A} -> {type A}
of_type < intros.
1 subgoal(s).
Variables: M, A
H1 : {of M A}
============================
{type A}
of_type < apply of_type_ext to _ H1.
1 subgoal(s).
Variables: M, A
H1 : {of M A}
H2 : {type A}
============================
{type A}
of_type < search.
Proof completed.
Abella < Theorem reduce_const :
forall C, {type C} -> reduce c C.
1 subgoal(s).
============================
forall C, {type C} -> reduce c C
reduce_const < intros.
1 subgoal(s).
Variables: C
H1 : {type C}
============================
reduce c C
reduce_const < assert neutral c.
2 subgoal(s).
Variables: C
H1 : {type C}
============================
neutral c
subgoal 2 is:
reduce c C
reduce_const < unfold.
2 subgoal(s).
Variables: C
H1 : {type C}
============================
forall A R, c = abs A R -> false
subgoal 2 is:
reduce c C
reduce_const < intros.
2 subgoal(s).
Variables: C, A, R
H1 : {type C}
H2 : c = abs A R
============================
false
subgoal 2 is:
reduce c C
reduce_const < case H2.
1 subgoal(s).
Variables: C
H1 : {type C}
H2 : neutral c
============================
reduce c C
reduce_const < assert forall P, {step c P} -> reduce P C.
2 subgoal(s).
Variables: C
H1 : {type C}
H2 : neutral c
============================
forall P, {step c P} -> reduce P C
subgoal 2 is:
reduce c C
reduce_const < intros.
2 subgoal(s).
Variables: C, P
H1 : {type C}
H2 : neutral c
H3 : {step c P}
============================
reduce P C
subgoal 2 is:
reduce c C
reduce_const < case H3.
1 subgoal(s).
Variables: C
H1 : {type C}
H2 : neutral c
H3 : forall P, {step c P} -> reduce P C
============================
reduce c C
reduce_const < apply neutral_step_reduce to H2 _ H1 H3.
1 subgoal(s).
Variables: C
H1 : {type C}
H2 : neutral c
H3 : forall P, {step c P} -> reduce P C
H4 : reduce c C
============================
reduce c C
reduce_const < search.
Proof completed.
Abella < Theorem abs_step_reduce_lemma :
forall U M A B, sn U -> sn (M c) -> reduce U A -> (forall V, reduce V A ->
reduce (M V) B) -> {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B.
1 subgoal(s).
============================
forall U M A B, sn U -> sn (M c) -> reduce U A -> (forall V, reduce V A ->
reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
abs_step_reduce_lemma < induction on 1.
1 subgoal(s).
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
============================
forall U M A B, sn U @ -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
abs_step_reduce_lemma < induction on 2.
1 subgoal(s).
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
============================
forall U M A B, sn U @ -> sn (M c) @@ -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
1 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < assert forall P, {step (app (abs A M) U) P} -> reduce P B.
2 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
============================
forall P, {step (app (abs A M) U) P} -> reduce P B
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
2 subgoal(s).
Variables: U, M, A, B, P
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : {step (app (abs A M) U) P}
============================
reduce P B
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H6.
4 subgoal(s).
Variables: U, M, A, B, P, M'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step (abs A M) M'}
============================
reduce (app M' U) B
subgoal 2 is:
reduce (app (abs A M) N') B
subgoal 3 is:
reduce (M U) B
subgoal 4 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H7.
4 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
============================
reduce (app (abs A R') U) B
subgoal 2 is:
reduce (app (abs A M) N') B
subgoal 3 is:
reduce (M U) B
subgoal 4 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < inst H8 with n1 = c.
4 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
============================
reduce (app (abs A R') U) B
subgoal 2 is:
reduce (app (abs A M) N') B
subgoal 3 is:
reduce (M U) B
subgoal 4 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H2.
4 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
============================
reduce (app (abs A R') U) B
subgoal 2 is:
reduce (app (abs A M) N') B
subgoal 3 is:
reduce (M U) B
subgoal 4 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H10 to H9.
4 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
============================
reduce (app (abs A R') U) B
subgoal 2 is:
reduce (app (abs A M) N') B
subgoal 3 is:
reduce (M U) B
subgoal 4 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply IH1 to H1 H11 H3 _ _ with M = R', B = B.
6 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
============================
{of (abs A R') (arrow A B)}
subgoal 2 is:
forall V, reduce V A -> reduce (R' V) B
subgoal 3 is:
reduce (app (abs A R') U) B
subgoal 4 is:
reduce (app (abs A M) N') B
subgoal 5 is:
reduce (M U) B
subgoal 6 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply of_step to H5 _.
6 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : {of (abs A (x1\R' x1)) (arrow A B)}
============================
{of (abs A R') (arrow A B)}
subgoal 2 is:
forall V, reduce V A -> reduce (R' V) B
subgoal 3 is:
reduce (app (abs A R') U) B
subgoal 4 is:
reduce (app (abs A M) N') B
subgoal 5 is:
reduce (M U) B
subgoal 6 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
5 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
============================
forall V, reduce V A -> reduce (R' V) B
subgoal 2 is:
reduce (app (abs A R') U) B
subgoal 3 is:
reduce (app (abs A M) N') B
subgoal 4 is:
reduce (M U) B
subgoal 5 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
5 subgoal(s).
Variables: U, M, A, B, P, M', R', V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
============================
reduce (R' V) B
subgoal 2 is:
reduce (app (abs A R') U) B
subgoal 3 is:
reduce (app (abs A M) N') B
subgoal 4 is:
reduce (M U) B
subgoal 5 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H4 to H12.
5 subgoal(s).
Variables: U, M, A, B, P, M', R', V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
H13 : reduce (M V) B
============================
reduce (R' V) B
subgoal 2 is:
reduce (app (abs A R') U) B
subgoal 3 is:
reduce (app (abs A M) N') B
subgoal 4 is:
reduce (M U) B
subgoal 5 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < inst H8 with n1 = V.
5 subgoal(s).
Variables: U, M, A, B, P, M', R', V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
H13 : reduce (M V) B
H14 : {step (M V) (R' V)}
============================
reduce (R' V) B
subgoal 2 is:
reduce (app (abs A R') U) B
subgoal 3 is:
reduce (app (abs A M) N') B
subgoal 4 is:
reduce (M U) B
subgoal 5 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply reduce_step to H13 H14.
5 subgoal(s).
Variables: U, M, A, B, P, M', R', V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
H13 : reduce (M V) B
H14 : {step (M V) (R' V)}
H15 : reduce (R' V) B
============================
reduce (R' V) B
subgoal 2 is:
reduce (app (abs A R') U) B
subgoal 3 is:
reduce (app (abs A M) N') B
subgoal 4 is:
reduce (M U) B
subgoal 5 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
4 subgoal(s).
Variables: U, M, A, B, P, M', R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce (app (abs A R') U) B
============================
reduce (app (abs A R') U) B
subgoal 2 is:
reduce (app (abs A M) N') B
subgoal 3 is:
reduce (M U) B
subgoal 4 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
3 subgoal(s).
Variables: U, M, A, B, P, N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
============================
reduce (app (abs A M) N') B
subgoal 2 is:
reduce (M U) B
subgoal 3 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H1.
3 subgoal(s).
Variables: U, M, A, B, P, N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
============================
reduce (app (abs A M) N') B
subgoal 2 is:
reduce (M U) B
subgoal 3 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H8 to H7.
3 subgoal(s).
Variables: U, M, A, B, P, N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
H9 : sn N' *
============================
reduce (app (abs A M) N') B
subgoal 2 is:
reduce (M U) B
subgoal 3 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply reduce_step to H3 H7.
3 subgoal(s).
Variables: U, M, A, B, P, N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
H9 : sn N' *
H10 : reduce N' A
============================
reduce (app (abs A M) N') B
subgoal 2 is:
reduce (M U) B
subgoal 3 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply IH to H9 H2 H10 H4 H5 with M = M.
3 subgoal(s).
Variables: U, M, A, B, P, N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
H9 : sn N' *
H10 : reduce N' A
H11 : reduce (app (abs A M) N') B
============================
reduce (app (abs A M) N') B
subgoal 2 is:
reduce (M U) B
subgoal 3 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
2 subgoal(s).
Variables: U, M, A, B, P
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
============================
reduce (M U) B
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H4 to H3.
2 subgoal(s).
Variables: U, M, A, B, P
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : reduce (M U) B
============================
reduce (M U) B
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
1 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < assert neutral (app (abs A M) U).
2 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
============================
neutral (app (abs A M) U)
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < unfold.
2 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
============================
forall A1 R, app (abs A M) U = abs A1 R -> false
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
2 subgoal(s).
Variables: U, M, A, B, A1, R
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : app (abs A M) U = abs A1 R
============================
false
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H7.
1 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < assert {of (app (abs A M) U) B}.
2 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
============================
{of (app (abs A M) U) B}
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply reduce_of to H3.
2 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of U A}
============================
{of (app (abs A M) U) B}
subgoal 2 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
1 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of (app (abs A M) U) B}
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply of_type to H8.
1 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of (app (abs A M) U) B}
H9 : {type B}
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply neutral_step_reduce to H7 H8 H9 H6.
1 subgoal(s).
Variables: U, M, A, B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A -> (forall V,
reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of (app (abs A M) U) B}
H9 : {type B}
H10 : reduce (app (abs A M) U) B
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
Proof completed.
Abella < Theorem abs_step_reduce :
forall M A B, {of (abs A M) (arrow A B)} -> (forall V, reduce V A ->
reduce (M V) B) -> reduce (abs A M) (arrow A B).
1 subgoal(s).
============================
forall M A B, {of (abs A M) (arrow A B)} -> (forall V, reduce V A ->
reduce (M V) B) -> reduce (abs A M) (arrow A B)
abs_step_reduce < intros.
1 subgoal(s).
Variables: M, A, B
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
============================
reduce (abs A M) (arrow A B)
abs_step_reduce < unfold.
2 subgoal(s).
Variables: M, A, B
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
============================
{of (abs A M) (arrow A B)}
subgoal 2 is:
forall U, reduce U A -> reduce (app (abs A M) U) B
abs_step_reduce < search.
1 subgoal(s).
Variables: M, A, B
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
============================
forall U, reduce U A -> reduce (app (abs A M) U) B
abs_step_reduce < intros.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply of_type to H1.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H4 : {type (arrow A B)}
============================
reduce (app (abs A M) U) B
abs_step_reduce < case H4.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {type A}
H6 : {type B}
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply reduce_const to H5.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {type A}
H6 : {type B}
H7 : reduce c A
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply H2 to H7.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {type A}
H6 : {type B}
H7 : reduce c A
H8 : reduce (M c) B
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply reduce_sn to H5 H3.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {type A}
H6 : {type B}
H7 : reduce c A
H8 : reduce (M c) B
H9 : sn U
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply reduce_sn to H6 H8.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {type A}
H6 : {type B}
H7 : reduce c A
H8 : reduce (M c) B
H9 : sn U
H10 : sn (M c)
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply abs_step_reduce_lemma to H9 H10 H3 H2 H1 with M = M.
1 subgoal(s).
Variables: M, A, B, U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {type A}
H6 : {type B}
H7 : reduce c A
H8 : reduce (M c) B
H9 : sn U
H10 : sn (M c)
H11 : reduce (app (abs A M) U) B
============================
reduce (app (abs A M) U) B
abs_step_reduce < search.
Proof completed.
Abella < Define closed M := exists A, {of M A}.
Abella < Define nabla x, fresh x M.
Abella < Theorem member_fresh :
forall X L E, member E L -> fresh X L -> fresh X E.
1 subgoal(s).
============================
forall X L E, member E L -> fresh X L -> fresh X E
member_fresh < induction on 1.
1 subgoal(s).
IH : forall X L E, member E L * -> fresh X L -> fresh X E
============================
forall X L E, member E L @ -> fresh X L -> fresh X E
member_fresh < intros.
1 subgoal(s).
Variables: X, L, E
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H1 : member E L @
H2 : fresh X L
============================
fresh X E
member_fresh < case H1.
2 subgoal(s).
Variables: X, L, E, L1
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H2 : fresh X (E :: L1)
============================
fresh X E
subgoal 2 is:
fresh X E
member_fresh < case H2.
2 subgoal(s).
Variables: X, L, E, L1, M2, M1
IH : forall X L E, member E L * -> fresh X L -> fresh X E
============================
fresh n1 M1
subgoal 2 is:
fresh X E
member_fresh < search.
1 subgoal(s).
Variables: X, L, E, L1, B
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H2 : fresh X (B :: L1)
H3 : member E L1 *
============================
fresh X E
member_fresh < assert fresh X L1.
2 subgoal(s).
Variables: X, L, E, L1, B
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H2 : fresh X (B :: L1)
H3 : member E L1 *
============================
fresh X L1
subgoal 2 is:
fresh X E
member_fresh < case H2.
2 subgoal(s).
Variables: X, L, E, L1, B, M2, M1
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H3 : member (E n1) M2 *
============================
fresh n1 M2
subgoal 2 is:
fresh X E
member_fresh < search.
1 subgoal(s).
Variables: X, L, E, L1, B
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H2 : fresh X (B :: L1)
H3 : member E L1 *
H4 : fresh X L1
============================
fresh X E
member_fresh < apply IH to H3 H4.
1 subgoal(s).
Variables: X, L, E, L1, B
IH : forall X L E, member E L * -> fresh X L -> fresh X E
H2 : fresh X (B :: L1)
H3 : member E L1 *
H4 : fresh X L1
H5 : fresh X E
============================
fresh X E
member_fresh < search.
Proof completed.
Abella < Theorem prune_type :
forall A, nabla x, {type (A x)} -> (exists B, A = x1\B).
1 subgoal(s).
============================
forall A, nabla x, {type (A x)} -> (exists B, A = x1\B)
prune_type < induction on 1.
1 subgoal(s).
IH : forall A, nabla x, {type (A x)}* -> (exists B, A = x1\B)
============================
forall A, nabla x, {type (A x)}@ -> (exists B, A = x1\B)
prune_type < intros.
1 subgoal(s).
Variables: A
IH : forall A, nabla x, {type (A x)}* -> (exists B, A = x1\B)
H1 : {type (A n1)}@
============================
exists B, A = x1\B
prune_type < case H1.
2 subgoal(s).
Variables: A
IH : forall A, nabla x, {type (A x)}* -> (exists B, A = x1\B)
============================
exists B, x1\top = x1\B
subgoal 2 is:
exists B1, x1\arrow (A1 x1) (B x1) = x1\B1
prune_type < search.
1 subgoal(s).
Variables: A, B, A1
IH : forall A, nabla x, {type (A x)}* -> (exists B, A = x1\B)
H2 : {type (A1 n1)}*
H3 : {type (B n1)}*
============================
exists B1, x1\arrow (A1 x1) (B x1) = x1\B1
prune_type < apply IH to H2.
1 subgoal(s).
Variables: A, B, A1, B1
IH : forall A, nabla x, {type (A x)}* -> (exists B, A = x1\B)
H2 : {type B1}*
H3 : {type (B n1)}*
============================
exists B2, x1\arrow B1 (B x1) = x1\B2
prune_type < apply IH to H3.
1 subgoal(s).
Variables: A, B, A1, B1, B2
IH : forall A, nabla x, {type (A x)}* -> (exists B, A = x1\B)
H2 : {type B1}*
H3 : {type B2}*
============================
exists B3, x1\arrow B1 B2 = x1\B3
prune_type < search.
Proof completed.
Abella < Theorem prune_of :
forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)} -> (exists M, R = x1\M).
1 subgoal(s).
============================
forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)} -> (exists M,
R = x1\M)
prune_of < induction on 2.
1 subgoal(s).
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
============================
forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}@ -> (exists M,
R = x1\M)
prune_of < intros.
1 subgoal(s).
Variables: L, R, A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H2 : {L |- of (R n1) (A n1)}@
============================
exists M, R = x1\M
prune_of < case H2.
4 subgoal(s).
Variables: L, R, A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : member (of (R n1) (A n1)) L
============================
exists M, R = x1\M
subgoal 2 is:
exists M1, x1\app (M x1) (N x1) = x1\M1
subgoal 3 is:
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 4 is:
exists M, x1\c = x1\M
prune_of < apply member_fresh to H3 _.
4 subgoal(s).
Variables: L, R, A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : member (of (R n1) (A n1)) L
H4 : fresh n1 (of (R n1) (A n1))
============================
exists M, R = x1\M
subgoal 2 is:
exists M1, x1\app (M x1) (N x1) = x1\M1
subgoal 3 is:
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 4 is:
exists M, x1\c = x1\M
prune_of < case H4.
4 subgoal(s).
Variables: L, R, A, M2, M1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : member (of M1 M2) L
============================
exists M, x1\M1 = x1\M
subgoal 2 is:
exists M1, x1\app (M x1) (N x1) = x1\M1
subgoal 3 is:
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 4 is:
exists M, x1\c = x1\M
prune_of < search.
3 subgoal(s).
Variables: L, R, A, A1, N, M
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- of (M n1) (arrow (A1 n1) (A n1))}*
H4 : {L |- of (N n1) (A1 n1)}*
============================
exists M1, x1\app (M x1) (N x1) = x1\M1
subgoal 2 is:
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 3 is:
exists M, x1\c = x1\M
prune_of < apply IH to H1 H3.
3 subgoal(s).
Variables: L, R, A, A1, N, M, M1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- of M1 (arrow (A1 n1) (A n1))}*
H4 : {L |- of (N n1) (A1 n1)}*
============================
exists M2, x1\app M1 (N x1) = x1\M2
subgoal 2 is:
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 3 is:
exists M, x1\c = x1\M
prune_of < apply IH to H1 H4.
3 subgoal(s).
Variables: L, R, A, A1, N, M, M1, M2
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- of M1 (arrow (A1 n1) (A n1))}*
H4 : {L |- of M2 (A1 n1)}*
============================
exists M3, x1\app M1 M2 = x1\M3
subgoal 2 is:
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 3 is:
exists M, x1\c = x1\M
prune_of < search.
2 subgoal(s).
Variables: L, R, A, B, R1, A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- type (A1 n1)}*
H4 : {L, of n2 (A1 n1) |- of (R1 n1 n2) (B n1)}*
============================
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 2 is:
exists M, x1\c = x1\M
prune_of < apply type_ignores_ctx to H1 H3.
2 subgoal(s).
Variables: L, R, A, B, R1, A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- type (A1 n1)}*
H4 : {L, of n2 (A1 n1) |- of (R1 n1 n2) (B n1)}*
H5 : {type (A1 n1)}
============================
exists M, x1\abs (A1 x1) (R1 x1) = x1\M
subgoal 2 is:
exists M, x1\c = x1\M
prune_of < apply prune_type to H5.
2 subgoal(s).
Variables: L, R, A, B, R1, A1, B1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- type B1}*
H4 : {L, of n2 B1 |- of (R1 n1 n2) (B n1)}*
H5 : {type B1}
============================
exists M, x1\abs B1 (R1 x1) = x1\M
subgoal 2 is:
exists M, x1\c = x1\M
prune_of < apply IH to _ H4.
2 subgoal(s).
Variables: L, R, A, B, R1, A1, B1, M
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- type B1}*
H4 : {L, of n2 B1 |- of (M n2) (B n1)}*
H5 : {type B1}
============================
exists M1, x1\abs B1 (x2\M x2) = x1\M1
subgoal 2 is:
exists M, x1\c = x1\M
prune_of < search.
1 subgoal(s).
Variables: L, R, A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) (A x)}* -> (exists M,
R = x1\M)
H1 : ctx L
H3 : {L |- type (A n1)}*
============================
exists M, x1\c = x1\M
prune_of < search.
Proof completed.
Abella < Theorem prune_closed :
forall R, nabla x, closed (R x) -> (exists M, R = x1\M).
1 subgoal(s).
============================
forall R, nabla x, closed (R x) -> (exists M, R = x1\M)
prune_closed < intros.
1 subgoal(s).
Variables: R
H1 : closed (R n1)
============================
exists M, R = x1\M
prune_closed < case H1.
1 subgoal(s).
Variables: R, A
H2 : {of (R n1) (A n1)}
============================
exists M, R = x1\M
prune_closed < apply prune_of to _ H2.
1 subgoal(s).
Variables: R, A, M
H2 : {of M (A n1)}
============================
exists M1, x1\M = x1\M1
prune_closed < search.
Proof completed.
Abella < Theorem reduce_closed :
forall M A, reduce M A -> closed M.
1 subgoal(s).
============================
forall M A, reduce M A -> closed M
reduce_closed < intros.
1 subgoal(s).
Variables: M, A
H1 : reduce M A
============================
closed M
reduce_closed < apply reduce_of to H1.
1 subgoal(s).
Variables: M, A
H1 : reduce M A
H2 : {of M A}
============================
closed M
reduce_closed < search.
Proof completed.
Abella < Theorem prune_reduce :
forall R A, nabla x, reduce (R x) A -> (exists M, R = x1\M).
1 subgoal(s).
============================
forall R A, nabla x, reduce (R x) A -> (exists M, R = x1\M)
prune_reduce < intros.
1 subgoal(s).
Variables: R, A
H1 : reduce (R n1) A
============================
exists M, R = x1\M
prune_reduce < apply reduce_closed to H1.
1 subgoal(s).
Variables: R, A
H1 : reduce (R n1) A
H2 : closed (R n1)
============================
exists M, R = x1\M
prune_reduce < apply prune_closed to H2.
1 subgoal(s).
Variables: R, A, M
H1 : reduce M A
H2 : closed M
============================
exists M1, x1\M = x1\M1
prune_reduce < search.
Proof completed.
Abella < Define subst nil M M.
Abella < Define nabla x, subst (of x A :: L) (R x) M := exists U, reduce U A /\ subst L (R U) M.
Abella < Theorem closed_subst :
forall L M N, closed M -> subst L M N -> M = N.
1 subgoal(s).
============================
forall L M N, closed M -> subst L M N -> M = N
closed_subst < induction on 2.
1 subgoal(s).
IH : forall L M N, closed M -> subst L M N * -> M = N
============================
forall L M N, closed M -> subst L M N @ -> M = N
closed_subst < intros.
1 subgoal(s).
Variables: L, M, N
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M
H2 : subst L M N @
============================
M = N
closed_subst < case H2.
2 subgoal(s).
Variables: L, M, N
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed N
============================
N = N
subgoal 2 is:
M n1 = M1
closed_subst < search.
1 subgoal(s).
Variables: L, M, N, U, M1, L1, A
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed (M n1)
H3 : reduce U A
H4 : subst L1 (M U) M1 *
============================
M n1 = M1
closed_subst < apply prune_closed to H1.
1 subgoal(s).
Variables: L, M, N, U, M1, L1, A, M2
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M2
H3 : reduce U A
H4 : subst L1 M2 M1 *
============================
M2 = M1
closed_subst < apply IH to H1 H4.
1 subgoal(s).
Variables: L, M, N, U, M1, L1, A, M2
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M1
H3 : reduce U A
H4 : subst L1 M1 M1 *
============================
M1 = M1
closed_subst < search.
Proof completed.
Abella < Theorem subst_const :
forall L M, subst L c M -> M = c.
1 subgoal(s).
============================
forall L M, subst L c M -> M = c
subst_const < induction on 1.
1 subgoal(s).
IH : forall L M, subst L c M * -> M = c
============================
forall L M, subst L c M @ -> M = c
subst_const < intros.
1 subgoal(s).
Variables: L, M
IH : forall L M, subst L c M * -> M = c
H1 : subst L c M @
============================
M = c
subst_const < case H1.
2 subgoal(s).
Variables: L, M
IH : forall L M, subst L c M * -> M = c
============================
c = c
subgoal 2 is:
M1 = c
subst_const < search.
1 subgoal(s).
Variables: L, M, U, M1, L1, A
IH : forall L M, subst L c M * -> M = c
H2 : reduce U A
H3 : subst L1 c M1 *
============================
M1 = c
subst_const < apply IH to H3.
1 subgoal(s).
Variables: L, M, U, M1, L1, A
IH : forall L M, subst L c M * -> M = c
H2 : reduce U A
H3 : subst L1 c c *
============================
c = c
subst_const < search.
Proof completed.
Abella < Theorem subst_var :
forall L M N A, ctx L -> member (of M A) L -> subst L M N -> reduce N A.
1 subgoal(s).
============================
forall L M N A, ctx L -> member (of M A) L -> subst L M N -> reduce N A
subst_var < induction on 1.
1 subgoal(s).
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
============================
forall L M N A, ctx L @ -> member (of M A) L -> subst L M N -> reduce N A
subst_var < intros.
1 subgoal(s).
Variables: L, M, N, A
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H1 : ctx L @
H2 : member (of M A) L
H3 : subst L M N
============================
reduce N A
subst_var < case H1.
2 subgoal(s).
Variables: L, M, N, A
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H2 : member (of M A) nil
H3 : subst nil M N
============================
reduce N A
subgoal 2 is:
reduce (N n1) (A n1)
subst_var < case H2.
1 subgoal(s).
Variables: L, M, N, A, L1, A1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H2 : member (of (M n1) (A n1)) (of n1 A1 :: L1)
H3 : subst (of n1 A1 :: L1) (M n1) (N n1)
H4 : {type A1}
H5 : ctx L1 *
============================
reduce (N n1) (A n1)
subst_var < case H2.
2 subgoal(s).
Variables: L, M, N, A, L1, A1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H3 : subst (of n1 A1 :: L1) n1 (N n1)
H4 : {type A1}
H5 : ctx L1 *
============================
reduce (N n1) A1
subgoal 2 is:
reduce (N n1) (A n1)
subst_var < case H3.
2 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 U M1
============================
reduce M1 A1
subgoal 2 is:
reduce (N n1) (A n1)
subst_var < apply reduce_closed to H6.
2 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 U M1
H8 : closed U
============================
reduce M1 A1
subgoal 2 is:
reduce (N n1) (A n1)
subst_var < apply closed_subst to H8 H7.
2 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : reduce M1 A1
H7 : subst L1 M1 M1
H8 : closed M1
============================
reduce M1 A1
subgoal 2 is:
reduce (N n1) (A n1)
subst_var < search.
1 subgoal(s).
Variables: L, M, N, A, L1, A1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H3 : subst (of n1 A1 :: L1) (M n1) (N n1)
H4 : {type A1}
H5 : ctx L1 *
H6 : member (of (M n1) (A n1)) L1
============================
reduce (N n1) (A n1)
subst_var < case H3.
1 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : member (of (M n1) (A n1)) L1
H7 : reduce U A1
H8 : subst L1 (M U) M1
============================
reduce M1 (A n1)
subst_var < apply member_fresh to H6 _.
1 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : member (of (M n1) (A n1)) L1
H7 : reduce U A1
H8 : subst L1 (M U) M1
H9 : fresh n1 (of (M n1) (A n1))
============================
reduce M1 (A n1)
subst_var < case H9.
1 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1, M4, M3
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : member (of M3 M4) L1
H7 : reduce U A1
H8 : subst L1 M3 M1
============================
reduce M1 M4
subst_var < apply IH to H5 H6 H8.
1 subgoal(s).
Variables: L, M, N, A, L1, A1, U, M1, M4, M3
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {type A1}
H5 : ctx L1 *
H6 : member (of M3 M4) L1
H7 : reduce U A1
H8 : subst L1 M3 M1
H10 : reduce M1 M4
============================
reduce M1 M4
subst_var < search.
Proof completed.
Abella < Theorem subst_app :
forall L M N R, ctx L -> subst L (app M N) R -> (exists MR NR,
R = app MR NR /\ subst L M MR /\ subst L N NR).
1 subgoal(s).
============================
forall L M N R, ctx L -> subst L (app M N) R
