Welcome to Abella 2.0.5-dev.
Abella < Specification "stlc-strong-norm".
Reading specification "stlc-strong-norm".
Abella < Close tm, ty.
Abella < Define sn : tm -> prop by
sn M := forall N, {step M N} -> sn N.
Abella < Define neutral : tm -> prop by
neutral M := forall A R, M = abs A R -> false.
Abella < Define reduce : tm -> ty -> prop by
reduce M top := {of M top} /\ sn M;
reduce M (arrow A B) := {of M (arrow A B)} /\ (forall U, reduce U A -> reduce (app M U) B).
Warning: Definition might not be stratified
("reduce" occurs to the left of ->)
Abella < Theorem reduce_of :
forall A M, reduce M A -> {of M A}.
============================
forall A M, reduce M A -> {of M A}
reduce_of < intros.
Variables: A M
H1 : reduce M A
============================
{of M A}
reduce_of < case H1.
Subgoal 1:
Variables: M
H2 : {of M top}
H3 : sn M
============================
{of M top}
Subgoal 2 is:
{of M (arrow A1 B)}
reduce_of < search.
Subgoal 2:
Variables: 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 : olist -> prop by
ctx nil;
nabla x, ctx (of x A :: L) := {ty A} /\ ctx L.
Abella < Define name : tm -> prop by
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 /\ {ty A}).
============================
forall E L, ctx L -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
ctx_member < induction on 1.
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
============================
forall E L, ctx L @ -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
ctx_member < intros.
Variables: E L
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
H1 : ctx L @
H2 : member E L
============================
exists X A, E = of X A /\ name X /\ {ty A}
ctx_member < case H1.
Subgoal 1:
Variables: E
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
H2 : member E nil
============================
exists X A, E = of X A /\ name X /\ {ty A}
Subgoal 2 is:
exists X A, E n1 = of X A /\ name X /\ {ty A}
ctx_member < case H2.
Subgoal 2:
Variables: E L1 A
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
H2 : member (E n1) (of n1 A :: L1)
H3 : {ty A}
H4 : ctx L1 *
============================
exists X A, E n1 = of X A /\ name X /\ {ty A}
ctx_member < case H2.
Subgoal 2.1:
Variables: L1 A
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
H3 : {ty A}
H4 : ctx L1 *
============================
exists X A1, of n1 A = of X A1 /\ name X /\ {ty A1}
Subgoal 2.2 is:
exists X A, E n1 = of X A /\ name X /\ {ty A}
ctx_member < search.
Subgoal 2.2:
Variables: E L1 A
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
H3 : {ty A}
H4 : ctx L1 *
H5 : member (E n1) L1
============================
exists X A, E n1 = of X A /\ name X /\ {ty A}
ctx_member < apply IH to H4 H5.
Subgoal 2.2:
Variables: L1 A X A1
IH : forall E L, ctx L * -> member E L ->
(exists X A, E = of X A /\ name X /\ {ty A})
H3 : {ty A}
H4 : ctx L1 *
H5 : member (of (X n1) A1) L1
H6 : name (X n1)
H7 : {ty A1}
============================
exists X1 A, of (X n1) A1 = of X1 A /\ name X1 /\ {ty A}
ctx_member < search.
Proof completed.
Abella < Theorem ty_ignores_ctx :
forall L A, ctx L -> {L |- ty A} -> {ty A}.
============================
forall L A, ctx L -> {L |- ty A} -> {ty A}
ty_ignores_ctx < induction on 2.
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
============================
forall L A, ctx L -> {L |- ty A}@ -> {ty A}
ty_ignores_ctx < intros.
Variables: L A
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H2 : {L |- ty A}@
============================
{ty A}
ty_ignores_ctx < case H2.
Subgoal 1:
Variables: L
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
============================
{ty top}
Subgoal 2 is:
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
ty_ignores_ctx < search.
Subgoal 2:
Variables: L B A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L |- ty B}*
============================
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
ty_ignores_ctx < apply IH to H1 H3.
Subgoal 2:
Variables: L B A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L |- ty B}*
H5 : {ty A1}
============================
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
ty_ignores_ctx < apply IH to H1 H4.
Subgoal 2:
Variables: L B A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L |- ty B}*
H5 : {ty A1}
H6 : {ty B}
============================
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
ty_ignores_ctx < search.
Subgoal 3:
Variables: L A F
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L, [F] |- ty A}*
H4 : member F L
============================
{ty A}
ty_ignores_ctx < apply ctx_member to H1 H4.
Subgoal 3:
Variables: L A X A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L, [of X A1] |- ty A}*
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
{ty A}
ty_ignores_ctx < case H3.
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}).
============================
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.
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.
Subgoal 1:
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}
Subgoal 2 is:
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < search.
Subgoal 2:
Variables: L M N B F
H1 : ctx L
H3 : {L, [F] |- of (app M N) B}
H4 : member F L
============================
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < apply ctx_member to H1 H4.
Subgoal 2:
Variables: L M N B X A
H1 : ctx L
H3 : {L, [of X A] |- of (app M N) B}
H4 : member (of X A) L
H5 : name X
H6 : {ty A}
============================
exists A, {L |- of M (arrow A B)} /\ {L |- of N A}
case_of_app < case H5.
Subgoal 2:
Variables: L M N B A
H1 : ctx (L n1)
H3 : {L n1, [of n1 A] |- of (app (M n1) (N n1)) B}
H4 : member (of n1 A) (L n1)
H6 : {ty A}
============================
exists A, {L n1 |- of (M n1) (arrow A B)} /\ {L n1 |- of (N n1) A}
case_of_app < case H3.
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 /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})).
============================
forall L M A B, ctx L -> {L |- of (abs A M) B} ->
(exists C, B = arrow A C /\ {ty A} /\
(nabla x, {L, of x A |- of (M x) C}))
case_of_abs < intros.
Variables: L M A B
H1 : ctx L
H2 : {L |- of (abs A M) B}
============================
exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})
case_of_abs < case H2.
Subgoal 1:
Variables: L M A B1
H1 : ctx L
H3 : {L |- ty A}
H4 : {L, of n1 A |- of (M n1) B1}
============================
exists C, arrow A B1 = arrow A C /\ {ty A} /\
(nabla x, {L, of x A |- of (M x) C})
Subgoal 2 is:
exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})
case_of_abs < apply ty_ignores_ctx to H1 H3.
Subgoal 1:
Variables: L M A B1
H1 : ctx L
H3 : {L |- ty A}
H4 : {L, of n1 A |- of (M n1) B1}
H5 : {ty A}
============================
exists C, arrow A B1 = arrow A C /\ {ty A} /\
(nabla x, {L, of x A |- of (M x) C})
Subgoal 2 is:
exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})
case_of_abs < search.
Subgoal 2:
Variables: L M A B F
H1 : ctx L
H3 : {L, [F] |- of (abs A M) B}
H4 : member F L
============================
exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})
case_of_abs < apply ctx_member to H1 H4.
Subgoal 2:
Variables: L M A B X A1
H1 : ctx L
H3 : {L, [of X A1] |- of (abs A M) B}
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})
case_of_abs < case H5.
Subgoal 2:
Variables: L M A B A1
H1 : ctx (L n1)
H3 : {L n1, [of n1 A1] |- of (abs A (M n1)) B}
H4 : member (of n1 A1) (L n1)
H6 : {ty A1}
============================
exists C, B = arrow A C /\ {ty A} /\
(nabla x, {L n1, of x A |- of (M n1 x) C})
case_of_abs < case H3.
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}.
============================
forall L M N A, ctx L -> {L |- of M A} -> {step M N} -> {L |- of N A}
of_step_ext < induction on 3.
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.
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.
Subgoal 1:
Variables: L A M' M1 N1
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.
Subgoal 1:
Variables: L A M' M1 N1 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.
Subgoal 1:
Variables: L A M' M1 N1 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.
Subgoal 2:
Variables: L 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 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.
Subgoal 2:
Variables: L 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 3 is:
{L |- of (R M1) A}
Subgoal 4 is:
{L |- of (abs A1 R') A}
of_step_ext < apply IH to H1 H6 H4.
Subgoal 2:
Variables: L 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 3 is:
{L |- of (R M1) A}
Subgoal 4 is:
{L |- of (abs A1 R') A}
of_step_ext < search.
Subgoal 3:
Variables: L 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 4 is:
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_app to H1 H2.
Subgoal 3:
Variables: L 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 4 is:
{L |- of (abs A1 R') A}
of_step_ext < apply case_of_abs to H1 H4.
Subgoal 3:
Variables: L M1 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 (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {ty A1}
H7 : {L, of n1 A1 |- of (R n1) C}
============================
{L |- of (R M1) C}
Subgoal 4 is:
{L |- of (abs A1 R') A}
of_step_ext < inst H7 with n1 = M1.
Subgoal 3:
Variables: L M1 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 (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {ty 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 4 is:
{L |- of (abs A1 R') A}
of_step_ext < cut H8 with H5.
Subgoal 3:
Variables: L M1 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 (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {ty 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 4 is:
{L |- of (abs A1 R') A}
of_step_ext < search.
Subgoal 4:
Variables: L 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.
Subgoal 4:
Variables: L 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 : {ty 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.
Subgoal 4:
Variables: L 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 : {ty 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}.
============================
forall M N A, {of M A} -> {step M N} -> {of N A}
of_step < intros.
Variables: M N A
H1 : {of M A}
H2 : {step M N}
============================
{of N A}
of_step < apply of_step_ext to _ H1 H2.
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.
============================
forall M N, sn M -> {step M N} -> sn N
sn_step < intros.
Variables: M N
H1 : sn M
H2 : {step M N}
============================
sn N
sn_step < case H1.
Variables: M N
H2 : {step M N}
H3 : forall N, {step M N} -> sn N
============================
sn N
sn_step < apply H3 to H2.
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.
============================
forall M N A, reduce M A -> {step M N} -> reduce N A
reduce_step < induction on 1.
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.
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.
Subgoal 1:
Variables: M N
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.
Subgoal 1:
Variables: M N
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.
Subgoal 1:
Variables: M N
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.
Subgoal 2:
Variables: M N 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.
Subgoal 2.1:
Variables: M N 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.2 is:
forall U, reduce U A1 -> reduce (app N U) B
reduce_step < apply of_step to H3 H2.
Subgoal 2.1:
Variables: M N 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.2 is:
forall U, reduce U A1 -> reduce (app N U) B
reduce_step < search.
Subgoal 2.2:
Variables: M N 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.
Subgoal 2.2:
Variables: M N 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.
Subgoal 2.2:
Variables: M N 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 _.
Subgoal 2.2:
Variables: M N 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.
============================
forall M, sn (app M c) -> sn M
sn_app_c < induction on 1.
IH : forall M, sn (app M c) * -> sn M
============================
forall M, sn (app M c) @ -> sn M
sn_app_c < intros.
Variables: M
IH : forall M, sn (app M c) * -> sn M
H1 : sn (app M c) @
============================
sn M
sn_app_c < case H1.
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.
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.
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)}.
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.
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.
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, {ty A} -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A).
============================
forall A, {ty A} -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
cr1_cr3 < induction on 1.
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
============================
forall A, {ty A}@ -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
cr1_cr3 < intros.
Variables: A
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
============================
(forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
cr1_cr3 < split*.
Subgoal 1:
Variables: A
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
============================
forall M, reduce M A -> sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < intros.
Subgoal 1:
Variables: A M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
H2 : reduce M A
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < case H2.
Subgoal 1.1:
Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty top}@
H3 : {of M top}
H4 : sn M
============================
sn M
Subgoal 1.2 is:
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < search.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty (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 M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < case H1.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < assert 0 neutral c.
Subgoal 1.2.1:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
============================
neutral c
Subgoal 1.2 is:
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < unfold.
Subgoal 1.2.1:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
============================
forall A R, c = abs A R -> false
Subgoal 1.2 is:
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < intros.
Subgoal 1.2.1:
Variables: M B A1 A2 R
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : c = abs A2 R
============================
false
Subgoal 1.2 is:
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < case H7.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < assert {of c A1}.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < assert 0 forall P, {step c P} -> reduce P A1.
Subgoal 1.2.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
============================
forall P, {step c P} -> reduce P A1
Subgoal 1.2 is:
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < intros.
Subgoal 1.2.2:
Variables: M B A1 P
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : {step c P}
============================
reduce P A1
Subgoal 1.2 is:
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < case H9.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < apply IH to H5.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < apply H11 to H7 H8 H9.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < apply H4 to H12.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < apply IH to H6.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
H14 : forall M, reduce M B -> sn M
H15 : forall M, neutral M -> {of M B} ->
(forall P, {step M P} -> reduce P B) -> reduce M B
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < apply H14 to H13.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
H14 : forall M, reduce M B -> sn M
H15 : forall M, neutral M -> {of M B} ->
(forall P, {step M P} -> reduce P B) -> reduce M B
H16 : sn (app M c)
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < apply sn_app_c to H16.
Subgoal 1.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M 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 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
H14 : forall M, reduce M B -> sn M
H15 : forall M, neutral M -> {of M B} ->
(forall P, {step M P} -> reduce P B) -> reduce M B
H16 : sn (app M c)
H17 : sn M
============================
sn M
Subgoal 2 is:
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < search.
Subgoal 2:
Variables: A
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
H2 : forall M, reduce M A -> sn M
============================
forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
reduce M A
cr1_cr3 < intros.
Subgoal 2:
Variables: A M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
H2 : forall M, reduce M A -> sn M
H3 : neutral M
H4 : {of M A}
H5 : forall P, {step M P} -> reduce P A
============================
reduce M A
cr1_cr3 < case H1.
Subgoal 2.1:
Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
reduce M top
Subgoal 2.2 is:
reduce M (arrow A1 B)
cr1_cr3 < unfold.
Subgoal 2.1.1:
Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
{of M top}
Subgoal 2.1.2 is:
sn M
Subgoal 2.2 is:
reduce M (arrow A1 B)
cr1_cr3 < search.
Subgoal 2.1.2:
Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
sn M
Subgoal 2.2 is:
reduce M (arrow A1 B)
cr1_cr3 < unfold.
Subgoal 2.1.2:
Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
forall N, {step M N} -> sn N
Subgoal 2.2 is:
reduce M (arrow A1 B)
cr1_cr3 < intros.
Subgoal 2.1.2:
Variables: M N
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
============================
sn N
Subgoal 2.2 is:
reduce M (arrow A1 B)
cr1_cr3 < apply H5 to H6.
Subgoal 2.1.2:
Variables: M N
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
H7 : reduce N top
============================
sn N
Subgoal 2.2 is:
reduce M (arrow A1 B)
cr1_cr3 < apply H2 to H7.
Subgoal 2.1.2:
Variables: M N
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M 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.2 is:
reduce M (arrow A1 B)
cr1_cr3 < search.
Subgoal 2.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
============================
reduce M (arrow A1 B)
cr1_cr3 < unfold.
Subgoal 2.2.1:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
============================
{of M (arrow A1 B)}
Subgoal 2.2.2 is:
forall U, reduce U A1 -> reduce (app M U) B
cr1_cr3 < search.
Subgoal 2.2.2:
Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
============================
forall U, reduce U A1 -> reduce (app M U) B
cr1_cr3 < intros.
Subgoal 2.2.2:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
============================
reduce (app M U) B
cr1_cr3 < apply IH to H6.
Subgoal 2.2.2:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
============================
reduce (app M U) B
cr1_cr3 < apply H9 to H8.
Subgoal 2.2.2:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
============================
reduce (app M U) B
cr1_cr3 < assert forall U, sn U -> reduce U A1 -> reduce (app M U) B.
Subgoal 2.2.2.1:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
============================
forall U, sn U -> reduce U A1 -> reduce (app M U) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < induction on 1.
Subgoal 2.2.2.1:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : 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.2.2 is:
reduce (app M U) B
cr1_cr3 < intros.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H12 : sn U1 @@
H13 : reduce U1 A1
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < case H12.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < assert forall P, {step (app M U1) P} -> reduce P B.
Subgoal 2.2.2.1.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
============================
forall P, {step (app M U1) P} -> reduce P B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < intros.
Subgoal 2.2.2.1.1:
Variables: M B A1 U U1 P
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : {step (app M U1) P}
============================
reduce P B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < case H15.
Subgoal 2.2.2.1.1.1:
Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
============================
reduce (app M' U1) B
Subgoal 2.2.2.1.1.2 is:
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply H5 to H16.
Subgoal 2.2.2.1.1.1:
Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
H17 : reduce M' (arrow A1 B)
============================
reduce (app M' U1) B
Subgoal 2.2.2.1.1.2 is:
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < case H17.
Subgoal 2.2.2.1.1.1:
Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
H18 : {of M' (arrow A1 B)}
H19 : forall U, reduce U A1 -> reduce (app M' U) B
============================
reduce (app M' U1) B
Subgoal 2.2.2.1.1.2 is:
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply H19 to H13.
Subgoal 2.2.2.1.1.1:
Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
H18 : {of M' (arrow A1 B)}
H19 : forall U, reduce U A1 -> reduce (app M' U) B
H20 : reduce (app M' U1) B
============================
reduce (app M' U1) B
Subgoal 2.2.2.1.1.2 is:
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < search.
Subgoal 2.2.2.1.1.2:
Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
============================
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply H14 to H16.
Subgoal 2.2.2.1.1.2:
Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
H17 : sn N' **
============================
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply reduce_step to H13 H16.
Subgoal 2.2.2.1.1.2:
Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
H17 : sn N' **
H18 : reduce N' A1
============================
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply IH1 to H17 H18.
Subgoal 2.2.2.1.1.2:
Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
H17 : sn N' **
H18 : reduce N' A1
H19 : reduce (app M N') B
============================
reduce (app M N') B
Subgoal 2.2.2.1.1.3 is:
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < search.
Subgoal 2.2.2.1.1.3:
Variables: B A1 U U1 R A2
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral (abs A2 R)
H4 : {of (abs A2 R) (arrow A1 B)}
H5 : forall P, {step (abs A2 R) P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app (abs A2 R) U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
============================
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < case H3.
Subgoal 2.2.2.1.1.3:
Variables: B A1 U U1 R A2
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H4 : {of (abs A2 R) (arrow A1 B)}
H5 : forall P, {step (abs A2 R) P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app (abs A2 R) U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : forall A R1, abs A2 R = abs A R1 -> false
============================
reduce (R U1) B
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply H16 to _.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < assert 0 neutral (app M U1).
Subgoal 2.2.2.1.2:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
============================
neutral (app M U1)
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < unfold.
Subgoal 2.2.2.1.2:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
============================
forall A R, app M U1 = abs A R -> false
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < intros.
Subgoal 2.2.2.1.2:
Variables: M B A1 U U1 A2 R
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : app M U1 = abs A2 R
============================
false
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < case H16.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < assert {of (app M U1) B}.
Subgoal 2.2.2.1.3:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
============================
{of (app M U1) B}
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply reduce_of to H13.
Subgoal 2.2.2.1.3:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of U1 A1}
============================
{of (app M U1) B}
Subgoal 2.2.2.1 is:
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < search.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of (app M U1) B}
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply IH to H7.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of (app M U1) B}
H18 : forall M, reduce M B -> sn M
H19 : forall M, neutral M -> {of M B} ->
(forall P, {step M P} -> reduce P B) -> reduce M B
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < apply H19 to H16 H17 H15.
Subgoal 2.2.2.1:
Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of (app M U1) B}
H18 : forall M, reduce M B -> sn M
H19 : forall M, neutral M -> {of M B} ->
(forall P, {step M P} -> reduce P B) -> reduce M B
H20 : reduce (app M U1) B
============================
reduce (app M U1) B
Subgoal 2.2.2 is:
reduce (app M U) B
cr1_cr3 < search.
Subgoal 2.2.2:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
H12 : forall U, sn U -> reduce U A1 -> reduce (app M U) B
============================
reduce (app M U) B
cr1_cr3 < apply H12 to H11 H8.
Subgoal 2.2.2:
Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
(forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
(forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
H12 : forall U, sn U -> reduce U A1 -> reduce (app M U) B
H13 : reduce (app M U) B
============================
reduce (app M U) B
cr1_cr3 < search.
Proof completed.
Abella < Theorem reduce_sn :
forall A M, {ty A} -> reduce M A -> sn M.
============================
forall A M, {ty A} -> reduce M A -> sn M
reduce_sn < intros.
Variables: A M
H1 : {ty A}
H2 : reduce M A
============================
sn M
reduce_sn < apply cr1_cr3 to H1.
Variables: A M
H1 : {ty A}
H2 : reduce M A
H3 : forall M, reduce M A -> sn M
H4 : forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A
============================
sn M
reduce_sn < apply H3 to H2.
Variables: A M
H1 : {ty A}
H2 : reduce M A
H3 : forall M, reduce M A -> sn M
H4 : forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A
H5 : sn M
============================
sn M
reduce_sn < search.
Proof completed.
Abella < Theorem neutral_step_reduce :
forall A M, neutral M -> {of M A} -> {ty A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A.
============================
forall A M, neutral M -> {of M A} -> {ty A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A
neutral_step_reduce < intros.
Variables: A M
H1 : neutral M
H2 : {of M A}
H3 : {ty A}
H4 : forall P, {step M P} -> reduce P A
============================
reduce M A
neutral_step_reduce < apply cr1_cr3 to H3.
Variables: A M
H1 : neutral M
H2 : {of M A}
H3 : {ty A}
H4 : forall P, {step M P} -> reduce P A
H5 : forall M, reduce M A -> sn M
H6 : forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A
============================
reduce M A
neutral_step_reduce < apply H6 to H1 H2 H4.
Variables: A M
H1 : neutral M
H2 : {of M A}
H3 : {ty A}
H4 : forall P, {step M P} -> reduce P A
H5 : forall M, reduce M A -> sn M
H6 : forall M, neutral M -> {of M A} ->
(forall P, {step M P} -> reduce P A) -> reduce M A
H7 : reduce M A
============================
reduce M A
neutral_step_reduce < search.
Proof completed.
Abella < Theorem of_ty_ext :
forall L M A, ctx L -> {L |- of M A} -> {ty A}.
============================
forall L M A, ctx L -> {L |- of M A} -> {ty A}
of_ty_ext < induction on 2.
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
============================
forall L M A, ctx L -> {L |- of M A}@ -> {ty A}
of_ty_ext < intros.
Variables: L M A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H2 : {L |- of M A}@
============================
{ty A}
of_ty_ext < case H2.
Subgoal 1:
Variables: L A A1 N M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
============================
{ty A}
Subgoal 2 is:
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < apply IH to H1 H3.
Subgoal 1:
Variables: L A A1 N M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
H5 : {ty (arrow A1 A)}
============================
{ty A}
Subgoal 2 is:
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < case H5.
Subgoal 1:
Variables: L A A1 N M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
H6 : {ty A1}
H7 : {ty A}
============================
{ty A}
Subgoal 2 is:
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < search.
Subgoal 2:
Variables: L B R A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
============================
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < apply ty_ignores_ctx to H1 H3.
Subgoal 2:
Variables: L B R A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
H5 : {ty A1}
============================
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < apply IH to _ H4.
Subgoal 2:
Variables: L B R A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
H5 : {ty A1}
H6 : {ty B}
============================
{ty (arrow A1 B)}
Subgoal 3 is:
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < search.
Subgoal 3:
Variables: L A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A}*
============================
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < apply ty_ignores_ctx to H1 H3.
Subgoal 3:
Variables: L A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A}*
H4 : {ty A}
============================
{ty A}
Subgoal 4 is:
{ty A}
of_ty_ext < search.
Subgoal 4:
Variables: L M A F
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L, [F] |- of M A}*
H4 : member F L
============================
{ty A}
of_ty_ext < apply ctx_member to H1 H4.
Subgoal 4:
Variables: L M A X A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L, [of X A1] |- of M A}*
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
{ty A}
of_ty_ext < case H5.
Subgoal 4:
Variables: L M A A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx (L n1)
H3 : {L n1, [of n1 A1] |- of (M n1) A}*
H4 : member (of n1 A1) (L n1)
H6 : {ty A1}
============================
{ty A}
of_ty_ext < case H3.
Subgoal 4:
Variables: L A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx (L n1)
H4 : member (of n1 A) (L n1)
H6 : {ty A}
============================
{ty A}
of_ty_ext < search.
Proof completed.
Abella < Theorem of_ty :
forall M A, {of M A} -> {ty A}.
============================
forall M A, {of M A} -> {ty A}
of_ty < intros.
Variables: M A
H1 : {of M A}
============================
{ty A}
of_ty < apply of_ty_ext to _ H1.
Variables: M A
H1 : {of M A}
H2 : {ty A}
============================
{ty A}
of_ty < search.
Proof completed.
Abella < Theorem reduce_const :
forall C, {ty C} -> reduce c C.
============================
forall C, {ty C} -> reduce c C
reduce_const < intros.
Variables: C
H1 : {ty C}
============================
reduce c C
reduce_const < assert 0 neutral c.
Subgoal 1:
Variables: C
H1 : {ty C}
============================
neutral c
Subgoal is:
reduce c C
reduce_const < unfold.
Subgoal 1:
Variables: C
H1 : {ty C}
============================
forall A R, c = abs A R -> false
Subgoal is:
reduce c C
reduce_const < intros.
Subgoal 1:
Variables: C A R
H1 : {ty C}
H2 : c = abs A R
============================
false
Subgoal is:
reduce c C
reduce_const < case H2.
Variables: C
H1 : {ty C}
H2 : neutral c
============================
reduce c C
reduce_const < assert forall P, {step c P} -> reduce P C.
Subgoal 2:
Variables: C
H1 : {ty C}
H2 : neutral c
============================
forall P, {step c P} -> reduce P C
Subgoal is:
reduce c C
reduce_const < intros.
Subgoal 2:
Variables: C P
H1 : {ty C}
H2 : neutral c
H3 : {step c P}
============================
reduce P C
Subgoal is:
reduce c C
reduce_const < case H3.
Variables: C
H1 : {ty 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.
Variables: C
H1 : {ty 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.
============================
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.
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.
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.
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.
Subgoal 1:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
Subgoal 1:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H6.
Subgoal 1.1:
Variables: U M A B 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 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H7.
Subgoal 1.1:
Variables: U M A B 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 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < inst H8 with n1 = c.
Subgoal 1.1:
Variables: U M A B 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 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H2.
Subgoal 1.1:
Variables: U M A B 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 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H10 to H9.
Subgoal 1.1:
Variables: U M A B 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 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply IH1 to H1 H11 H3 _ _ with M = R', B = B.
Subgoal 1.1.1:
Variables: U M A B 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 1.1.2 is:
forall V, reduce V A -> reduce (R' V) B
Subgoal 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply of_step to H5 _.
Subgoal 1.1.1:
Variables: U M A B 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 (z1\R' z1)) (arrow A B)}
============================
{of (abs A R') (arrow A B)}
Subgoal 1.1.2 is:
forall V, reduce V A -> reduce (R' V) B
Subgoal 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
Subgoal 1.1.2:
Variables: U M A B 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 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
Subgoal 1.1.2:
Variables: U M A B 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 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H4 to H12.
Subgoal 1.1.2:
Variables: U M A B 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 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < inst H8 with n1 = V.
Subgoal 1.1.2:
Variables: U M A B 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 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply reduce_step to H13 H14.
Subgoal 1.1.2:
Variables: U M A B 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 1.1 is:
reduce (app (abs A R') U) B
Subgoal 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
Subgoal 1.1:
Variables: U M A B 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 1.2 is:
reduce (app (abs A M) N') B
Subgoal 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
Subgoal 1.2:
Variables: U M A B 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 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H1.
Subgoal 1.2:
Variables: U M A B 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 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H8 to H7.
Subgoal 1.2:
Variables: U M A B 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 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply reduce_step to H3 H7.
Subgoal 1.2:
Variables: U M A B 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 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply IH to H9 H2 H10 H4 H5 with M = M.
Subgoal 1.2:
Variables: U M A B 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 1.3 is:
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
Subgoal 1.3:
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 (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply H4 to H3.
Subgoal 1.3:
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)}
H7 : reduce (M U) B
============================
reduce (M U) B
Subgoal is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
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 0 neutral (app (abs A M) U).
Subgoal 2:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < unfold.
Subgoal 2:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < intros.
Subgoal 2:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < case H7.
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}.
Subgoal 3:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply reduce_of to H3.
Subgoal 3:
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 is:
reduce (app (abs A M) U) B
abs_step_reduce_lemma < search.
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_ty to H8.
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 : {ty B}
============================
reduce (app (abs A M) U) B
abs_step_reduce_lemma < apply neutral_step_reduce to H7 H8 H9 H6.
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 : {ty 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).
============================
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.
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.
Subgoal 1:
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.
Subgoal 2:
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.
Subgoal 2:
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_ty to H1.
Subgoal 2:
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 : {ty (arrow A B)}
============================
reduce (app (abs A M) U) B
abs_step_reduce < case H4.
Subgoal 2:
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 : {ty A}
H6 : {ty B}
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply reduce_const to H5.
Subgoal 2:
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 : {ty A}
H6 : {ty B}
H7 : reduce c A
============================
reduce (app (abs A M) U) B
abs_step_reduce < apply H2 to H7.
Subgoal 2:
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 : {ty A}
H6 : {ty 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.
Subgoal 2:
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 : {ty A}
H6 : {ty 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.
Subgoal 2:
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 : {ty A}
H6 : {ty 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.
Subgoal 2:
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 : {ty A}
H6 : {ty 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 : tm -> prop by
closed M := exists A, {of M A}.
Abella < Theorem member_prune :
forall L E, nabla x, member (E x) L -> (exists F, E = y\F).
============================
forall L E, nabla x, member (E x) L -> (exists F, E = y\F)
member_prune < induction on 1.
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
forall L E, nabla x, member (E x) L @ -> (exists F, E = y\F)
member_prune < intros.
Variables: L E
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
exists F, E = y\F
member_prune < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
exists F, z1\L2 = y\F
Subgoal 2 is:
exists F, E = y\F
member_prune < search.
Subgoal 2:
Variables: E L3 L2
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
exists F, E = y\F
member_prune < apply IH to H2.
Subgoal 2:
Variables: L3 L2 F
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
exists F1, z1\F = y\F1
member_prune < search.
Proof completed.
Abella < Theorem prune_of :
forall L R A, nabla x, ctx L -> {L |- of (R x) A} -> (exists M, R = y\M).
============================
forall L R A, nabla x, ctx L -> {L |- of (R x) A} -> (exists M, R = y\M)
prune_of < induction on 2.
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
============================
forall L R A, nabla x, ctx L -> {L |- of (R x) A}@ -> (exists M, R = y\M)
prune_of < intros.
Variables: L R A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H2 : {L |- of (R n1) A}@
============================
exists M, R = y\M
prune_of < case H2.
Subgoal 1:
Variables: L A A1 N M
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- of (M n1) (arrow A1 A)}*
H4 : {L |- of (N n1) A1}*
============================
exists M1, z1\app (M z1) (N z1) = y\M1
Subgoal 2 is:
exists M, z1\abs A1 (R1 z1) = y\M
Subgoal 3 is:
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < apply IH to H1 H3.
Subgoal 1:
Variables: L A A1 N M1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of (N n1) A1}*
============================
exists M2, z1\app M1 (N z1) = y\M2
Subgoal 2 is:
exists M, z1\abs A1 (R1 z1) = y\M
Subgoal 3 is:
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < apply IH to H1 H4.
Subgoal 1:
Variables: L A A1 M1 M2
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of M2 A1}*
============================
exists M3, z1\app M1 M2 = y\M3
Subgoal 2 is:
exists M, z1\abs A1 (R1 z1) = y\M
Subgoal 3 is:
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < search.
Subgoal 2:
Variables: L B R1 A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n2 A1 |- of (R1 n1 n2) B}*
============================
exists M, z1\abs A1 (R1 z1) = y\M
Subgoal 3 is:
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < apply ty_ignores_ctx to H1 H3.
Subgoal 2:
Variables: L B R1 A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n2 A1 |- of (R1 n1 n2) B}*
H5 : {ty A1}
============================
exists M, z1\abs A1 (R1 z1) = y\M
Subgoal 3 is:
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < apply IH to _ H4.
Subgoal 2:
Variables: L B A1 M
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n2 A1 |- of (M n2) B}*
H5 : {ty A1}
============================
exists M1, z1\abs A1 (z2\M z2) = y\M1
Subgoal 3 is:
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < search.
Subgoal 3:
Variables: L A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A}*
============================
exists M, z1\c = y\M
Subgoal 4 is:
exists M, R = y\M
prune_of < search.
Subgoal 4:
Variables: L R A F
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L, [F n1] |- of (R n1) A}*
H4 : member (F n1) L
============================
exists M, R = y\M
prune_of < apply member_prune to H4.
Subgoal 4:
Variables: L R A F1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L, [F1] |- of (R n1) A}*
H4 : member F1 L
============================
exists M, R = y\M
prune_of < apply ctx_member to H1 H4.
Subgoal 4:
Variables: L R A X A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H3 : {L, [of X A1] |- of (R n1) A}*
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
exists M, R = y\M
prune_of < case H5.
Subgoal 4:
Variables: L R A A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx (L n2)
H3 : {L n2, [of n2 A1] |- of (R n2 n1) A}*
H4 : member (of n2 A1) (L n2)
H6 : {ty A1}
============================
exists M, R n2 = y\M
prune_of < case H3.
Subgoal 4:
Variables: L A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx (L n2)
H4 : member (of n2 A) (L n2)
H6 : {ty A}
============================
exists M, z2\n2 = y\M
prune_of < search.
Proof completed.
Abella < Theorem prune_closed :
forall R, nabla x, closed (R x) -> (exists M, R = y\M).
============================
forall R, nabla x, closed (R x) -> (exists M, R = y\M)
prune_closed < intros.
Variables: R
H1 : closed (R n1)
============================
exists M, R = y\M
prune_closed < case H1.
Variables: R A
H2 : {of (R n1) A}
============================
exists M, R = y\M
prune_closed < apply prune_of to _ H2.
Variables: A M
H2 : {of M A}
============================
exists M1, z1\M = y\M1
prune_closed < search.
Proof completed.
Abella < Theorem reduce_closed :
forall M A, reduce M A -> closed M.
============================
forall M A, reduce M A -> closed M
reduce_closed < intros.
Variables: M A
H1 : reduce M A
============================
closed M
reduce_closed < apply reduce_of to H1.
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 = y\M).
============================
forall R A, nabla x, reduce (R x) A -> (exists M, R = y\M)
prune_reduce < intros.
Variables: R A
H1 : reduce (R n1) A
============================
exists M, R = y\M
prune_reduce < apply reduce_closed to H1.
Variables: R A
H1 : reduce (R n1) A
H2 : closed (R n1)
============================
exists M, R = y\M
prune_reduce < apply prune_closed to H2.
Variables: A M
H1 : reduce M A
H2 : closed M
============================
exists M1, z1\M = y\M1
prune_reduce < search.
Proof completed.
Abella < Define subst : olist -> tm -> tm -> prop by
subst nil M M;
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.
============================
forall L M N, closed M -> subst L M N -> M = N
closed_subst < induction on 2.
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.
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.
Subgoal 1:
Variables: 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.
Subgoal 2:
Variables: M 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.
Subgoal 2:
Variables: 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.
Subgoal 2:
Variables: U M1 L1 A
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.
============================
forall L M, subst L c M -> M = c
subst_const < induction on 1.
IH : forall L M, subst L c M * -> M = c
============================
forall L M, subst L c M @ -> M = c
subst_const < intros.
Variables: L M
IH : forall L M, subst L c M * -> M = c
H1 : subst L c M @
============================
M = c
subst_const < case H1.
Subgoal 1:
IH : forall L M, subst L c M * -> M = c
============================
c = c
Subgoal 2 is:
M1 = c
subst_const < search.
Subgoal 2:
Variables: 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.
Subgoal 2:
Variables: U 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.
============================
forall L M N A, ctx L -> member (of M A) L -> subst L M N -> reduce N A
subst_var < induction on 1.
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.
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.
Subgoal 1:
Variables: 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
subst_var < case H2.
Subgoal 2:
Variables: 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) (of n1 A1 :: L1)
H3 : subst (of n1 A1 :: L1) (M n1) (N n1)
H4 : {ty A1}
H5 : ctx L1 *
============================
reduce (N n1) A
subst_var < case H2.
Subgoal 2.1:
Variables: N 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 : {ty A1}
H5 : ctx L1 *
============================
reduce (N n1) A1
Subgoal 2.2 is:
reduce (N n1) A
subst_var < case H3.
Subgoal 2.1:
Variables: 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 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 U M1
============================
reduce M1 A1
Subgoal 2.2 is:
reduce (N n1) A
subst_var < apply reduce_closed to H6.
Subgoal 2.1:
Variables: 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 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 U M1
H8 : closed U
============================
reduce M1 A1
Subgoal 2.2 is:
reduce (N n1) A
subst_var < apply closed_subst to H8 H7.
Subgoal 2.1:
Variables: L1 A1 M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce M1 A1
H7 : subst L1 M1 M1
H8 : closed M1
============================
reduce M1 A1
Subgoal 2.2 is:
reduce (N n1) A
subst_var < search.
Subgoal 2.2:
Variables: 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 : {ty A1}
H5 : ctx L1 *
H6 : member (of (M n1) A) L1
============================
reduce (N n1) A
subst_var < case H3.
Subgoal 2.2:
Variables: M 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 : {ty A1}
H5 : ctx L1 *
H6 : member (of (M n1) A) L1
H7 : reduce U A1
H8 : subst L1 (M U) M1
============================
reduce M1 A
subst_var < apply member_prune to H6.
Subgoal 2.2:
Variables: A L1 A1 U M1 F1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : member (of F1 A) L1
H7 : reduce U A1
H8 : subst L1 F1 M1
============================
reduce M1 A
subst_var < apply IH to H5 H6 H8.
Subgoal 2.2:
Variables: A L1 A1 U M1 F1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : member (of F1 A) L1
H7 : reduce U A1
H8 : subst L1 F1 M1
H9 : reduce M1 A
============================
reduce M1 A
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).
============================
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)
subst_app < induction on 1.
IH : 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)
============================
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)
subst_app < intros.
Variables: L M N R
IH : 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)
H1 : ctx L @
H2 : subst L (app M N) R
============================
exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR
subst_app < case H1.
Subgoal 1:
Variables: M N R
IH : 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)
H2 : subst nil (app M N) R
============================
exists MR NR, R = app MR NR /\ subst nil M MR /\ subst nil N NR
Subgoal 2 is:
exists MR NR, R n1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
subst (of n1 A :: L1) (N n1) NR
subst_app < case H2.
Subgoal 1:
Variables: M N
IH : 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)
============================
exists MR NR, app M N = app MR NR /\ subst nil M MR /\ subst nil N NR
Subgoal 2 is:
exists MR NR, R n1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
subst (of n1 A :: L1) (N n1) NR
subst_app < search.
Subgoal 2:
Variables: M N R L1 A
IH : 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)
H2 : subst (of n1 A :: L1) (app (M n1) (N n1)) (R n1)
H3 : {ty A}
H4 : ctx L1 *
============================
exists MR NR, R n1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
subst (of n1 A :: L1) (N n1) NR
subst_app < case H2.
Subgoal 2:
Variables: M N L1 A U M1
IH : 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)
H3 : {ty A}
H4 : ctx L1 *
H5 : reduce U A
H6 : subst L1 (app (M U) (N U)) M1
============================
exists MR NR, M1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
subst (of n1 A :: L1) (N n1) NR
subst_app < apply IH to H4 H6.
Subgoal 2:
Variables: M N L1 A U MR NR
IH : 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)
H3 : {ty A}
H4 : ctx L1 *
H5 : reduce U A
H6 : subst L1 (app (M U) (N U)) (app MR NR)
H7 : subst L1 (M U) MR
H8 : subst L1 (N U) NR
============================
exists MR1 NR1, app MR NR = app MR1 NR1 /\
subst (of n1 A :: L1) (M n1) MR1 /\ subst (of n1 A :: L1) (N n1) NR1
subst_app < search.
Proof completed.
Abella < Theorem subst_abs :
forall L M R A, ctx L -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U)))).
============================
forall L M R A, ctx L -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U))))
subst_abs < induction on 1.
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
============================
forall L M R A, ctx L @ -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U))))
subst_abs < intros.
Variables: L M R A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H1 : ctx L @
H2 : subst L (abs A M) R
H3 : {ty A}
============================
exists MR, R = abs A MR /\
(forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U)))
subst_abs < case H1.
Subgoal 1:
Variables: M R A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H2 : subst nil (abs A M) R
H3 : {ty A}
============================
exists MR, R = abs A MR /\
(forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (MR U)))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < case H2.
Subgoal 1:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
exists MR, abs A M = abs A MR /\
(forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (MR U)))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < exists M.
Subgoal 1:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
abs A M = abs A M /\
(forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (M U)))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < split.
Subgoal 1.1:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
abs A M = abs A M
Subgoal 1.2 is:
forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (M U))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < search.
Subgoal 1.2:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (M U))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < intros.
Subgoal 1.2:
Variables: M A U
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : reduce U A
============================
subst (of n1 A :: nil) (M n1) (M U)
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < search.
Subgoal 2:
Variables: M R A L1 A1
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H2 : subst (of n1 A1 :: L1) (abs A (M n1)) (R n1)
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
============================
exists MR, R n1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < case H2.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) M1
============================
exists MR, M1 = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < apply IH to H5 H7 H3.
Subgoal 2:
Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
exists MR1, abs A MR = abs A MR1 /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR1 U)))
subst_abs < exists MR.
Subgoal 2:
Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
abs A MR = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))
subst_abs < split.
Subgoal 2.1:
Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
abs A MR = abs A MR
Subgoal 2.2 is:
forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U))
subst_abs < search.
Subgoal 2.2:
Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
forall U, reduce U A ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U))
subst_abs < intros.
Subgoal 2.2:
Variables: M A L1 A1 U MR U1
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce (U1 n1) A
============================
subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR (U1 n1))
subst_abs < apply prune_reduce to H9.
Subgoal 2.2:
Variables: M A L1 A1 U MR M2
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce M2 A
============================
subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)
subst_abs < apply H8 to H9.
Subgoal 2.2:
Variables: M A L1 A1 U MR M2
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce M2 A
H10 : subst (of n1 A :: L1) (M U n1) (MR M2)
============================
subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)
subst_abs < case H10.
Subgoal 2.2:
Variables: M A L1 A1 U MR M2 U2
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
(exists MR, R = abs A MR /\
(forall U, reduce U A ->
(nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
(nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce M2 A
H11 : reduce U2 A
H12 : subst L1 (M U U2) (MR M2)
============================
subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)
subst_abs < search.
Proof completed.
Abella < Theorem subst_preserves_ty :
forall L M N A, ctx L -> subst L M N -> {L |- of M A} -> {of N A}.
============================
forall L M N A, ctx L -> subst L M N -> {L |- of M A} -> {of N A}
subst_preserves_ty < induction on 1.
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
============================
forall L M N A, ctx L @ -> subst L M N -> {L |- of M A} -> {of N A}
subst_preserves_ty < intros.
Variables: L M N A
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H1 : ctx L @
H2 : subst L M N
H3 : {L |- of M A}
============================
{of N A}
subst_preserves_ty < case H1.
Subgoal 1:
Variables: M N A
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H2 : subst nil M N
H3 : {of M A}
============================
{of N A}
Subgoal 2 is:
{of (N n1) A}
subst_preserves_ty < case H2.
Subgoal 1:
Variables: N A
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {of N A}
============================
{of N A}
Subgoal 2 is:
{of (N n1) A}
subst_preserves_ty < search.
Subgoal 2:
Variables: M N A L1 A1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H2 : subst (of n1 A1 :: L1) (M n1) (N n1)
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
============================
{of (N n1) A}
subst_preserves_ty < case H2.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
============================
{of M1 A}
subst_preserves_ty < apply reduce_of to H6.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
============================
{of M1 A}
subst_preserves_ty < inst H3 with n1 = U.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
============================
{of M1 A}
subst_preserves_ty < cut H9 with H8.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
H10 : {L1 |- of (M U) A}
============================
{of M1 A}
subst_preserves_ty < apply of_ty_ext to _ H3.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
H10 : {L1 |- of (M U) A}
H11 : {ty A}
============================
{of M1 A}
subst_preserves_ty < apply IH to H5 H7 H10.
Subgoal 2:
Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
H10 : {L1 |- of (M U) A}
H11 : {ty A}
H12 : {of M1 A}
============================
{of M1 A}
subst_preserves_ty < search.
Proof completed.
Abella < Theorem strong_norm_ext :
forall L M R A, ctx L -> {L |- of M A} -> subst L M R -> reduce R A.
============================
forall L M R A, ctx L -> {L |- of M A} -> subst L M R -> reduce R A
strong_norm_ext < induction on 2.
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
============================
forall L M R A, ctx L -> {L |- of M A}@ -> subst L M R -> reduce R A
strong_norm_ext < intros.
Variables: L M R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of M A}@
H3 : subst L M R
============================
reduce R A
strong_norm_ext < case H2 (keep).
Subgoal 1:
Variables: L R A A1 N M1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) R
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
============================
reduce R A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply subst_app to H1 H3.
Subgoal 1:
Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply IH to H1 H4 H6.
Subgoal 1:
Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H8 : reduce MR (arrow A1 A)
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply IH to H1 H5 H7.
Subgoal 1:
Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H8 : reduce MR (arrow A1 A)
H9 : reduce NR A1
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < case H8.
Subgoal 1:
Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H9 : reduce NR A1
H10 : {of MR (arrow A1 A)}
H11 : forall U, reduce U A1 -> reduce (app MR U) A
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply H11 to H9.
Subgoal 1:
Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H9 : reduce NR A1
H10 : {of MR (arrow A1 A)}
H11 : forall U, reduce U A1 -> reduce (app MR U) A
H12 : reduce (app MR NR) A
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < search.
Subgoal 2:
Variables: L R B R1 A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) R
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
============================
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply ty_ignores_ctx to H1 H4.
Subgoal 2:
Variables: L R B R1 A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) R
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
============================
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply subst_abs to H1 H3 H6.
Subgoal 2:
Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
============================
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply subst_preserves_ty to H1 H3 H2.
Subgoal 2:
Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
============================
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply abs_step_reduce to H8 _.
Subgoal 2.1:
Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
============================
forall V, reduce V A1 -> reduce (MR V) B
Subgoal 2 is:
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < intros.
Subgoal 2.1:
Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
============================
reduce (MR V) B
Subgoal 2 is:
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply ty_ignores_ctx to H1 H4.
Subgoal 2.1:
Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
H10 : {ty A1}
============================
reduce (MR V) B
Subgoal 2 is:
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply H7 to H9.
Subgoal 2.1:
Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
H10 : {ty A1}
H11 : subst (of n1 A1 :: L) (R1 n1) (MR V)
============================
reduce (MR V) B
Subgoal 2 is:
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply IH to _ H5 H11.
Subgoal 2.1:
Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
H10 : {ty A1}
H11 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H12 : reduce (MR V) B
============================
reduce (MR V) B
Subgoal 2 is:
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < search.
Subgoal 2:
Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce (abs A1 MR) (arrow A1 B)
============================
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < search.
Subgoal 3:
Variables: L R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c R
H4 : {L |- ty A}*
============================
reduce R A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply subst_const to H3.
Subgoal 3:
Variables: L A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c c
H4 : {L |- ty A}*
============================
reduce c A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply ty_ignores_ctx to H1 H4.
Subgoal 3:
Variables: L A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c c
H4 : {L |- ty A}*
H5 : {ty A}
============================
reduce c A
Subgoal 4 is:
reduce R A
strong_norm_ext < apply reduce_const to H5.
Subgoal 3:
Variables: L A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c c
H4 : {L |- ty A}*
H5 : {ty A}
H6 : reduce c A
============================
reduce c A
Subgoal 4 is:
reduce R A
strong_norm_ext < search.
Subgoal 4:
Variables: L M R A F
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of M A}@
H3 : subst L M R
H4 : {L, [F] |- of M A}*
H5 : member F L
============================
reduce R A
strong_norm_ext < apply ctx_member to H1 H5.
Subgoal 4:
Variables: L M R A X A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of M A}@
H3 : subst L M R
H4 : {L, [of X A1] |- of M A}*
H5 : member (of X A1) L
H6 : name X
H7 : {ty A1}
============================
reduce R A
strong_norm_ext < case H6.
Subgoal 4:
Variables: L M R A A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx (L n1)
H2 : {L n1 |- of (M n1) A}@
H3 : subst (L n1) (M n1) (R n1)
H4 : {L n1, [of n1 A1] |- of (M n1) A}*
H5 : member (of n1 A1) (L n1)
H7 : {ty A1}
============================
reduce (R n1) A
strong_norm_ext < case H4.
Subgoal 4:
Variables: L R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx (L n1)
H2 : {L n1 |- of n1 A}@
H3 : subst (L n1) n1 (R n1)
H5 : member (of n1 A) (L n1)
H7 : {ty A}
============================
reduce (R n1) A
strong_norm_ext < apply subst_var to H1 H5 H3.
Subgoal 4:
Variables: L R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx (L n1)
H2 : {L n1 |- of n1 A}@
H3 : subst (L n1) n1 (R n1)
H5 : member (of n1 A) (L n1)
H7 : {ty A}
H8 : reduce (R n1) A
============================
reduce (R n1) A
strong_norm_ext < search.
Proof completed.
Abella < Theorem strong_norm :
forall M A, {of M A} -> sn M.
============================
forall M A, {of M A} -> sn M
strong_norm < intros.
Variables: M A
H1 : {of M A}
============================
sn M
strong_norm < apply strong_norm_ext to _ H1 _.
Variables: M A
H1 : {of M A}
H2 : reduce M A
============================
sn M
strong_norm < apply of_ty to H1.
Variables: M A
H1 : {of M A}
H2 : reduce M A
H3 : {ty A}
============================
sn M
strong_norm < apply reduce_sn to _ H2.
Variables: M A
H1 : {of M A}
H2 : reduce M A
H3 : {ty A}
H4 : sn M
============================
sn M
strong_norm < search.
Proof completed.
Abella <