Welcome to Abella 2.0.5-dev.
Abella < Specification "stlc-weak-norm".
Reading specification "stlc-weak-norm".
Abella < Close tm, ty.
Abella < Define halts : tm -> prop by
halts M := exists V, {steps M V} /\ {value V}.
Abella < Define reduce : tm -> ty -> prop by
reduce M top := {of M top} /\ halts M;
reduce M (arrow A B) := {of M (arrow A B)} /\ halts M /\ (forall N, reduce N A -> reduce (app M N) B).
Warning: Definition might not be stratified
("reduce" occurs to the left of ->)
Abella < Theorem reduce_halts :
forall A M, reduce M A -> halts M.
============================
forall A M, reduce M A -> halts M
reduce_halts < intros.
Variables: A M
H1 : reduce M A
============================
halts M
reduce_halts < case H1.
Subgoal 1:
Variables: M
H2 : {of M top}
H3 : halts M
============================
halts M
Subgoal 2 is:
halts M
reduce_halts < search.
Subgoal 2:
Variables: M B A1
H2 : {of M (arrow A1 B)}
H3 : halts M
H4 : forall N, reduce N A1 -> reduce (app M N) B
============================
halts M
reduce_halts < search.
Proof completed.
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 : halts 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 : halts M
H4 : forall N, reduce N A1 -> reduce (app M N) B
============================
{of M (arrow A1 B)}
reduce_of < search.
Proof completed.
Abella < Theorem absurd_step_value :
forall V M, {step V M} -> {value V} -> false.
============================
forall V M, {step V M} -> {value V} -> false
absurd_step_value < intros.
Variables: V M
H1 : {step V M}
H2 : {value V}
============================
false
absurd_step_value < case H2.
Variables: M R A
H1 : {step (abs A R) M}
============================
false
absurd_step_value < case H1.
Proof completed.
Abella < Theorem step_det :
forall M N P, {step M N} -> {step M P} -> N = P.
============================
forall M N P, {step M N} -> {step M P} -> N = P
step_det < induction on 1.
IH : forall M N P, {step M N}* -> {step M P} -> N = P
============================
forall M N P, {step M N}@ -> {step M P} -> N = P
step_det < intros.
Variables: M N P
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H1 : {step M N}@
H2 : {step M P}
============================
N = P
step_det < case H1.
Subgoal 1:
Variables: P M' M1 N1
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H2 : {step (app M1 N1) P}
H3 : {step M1 M'}*
============================
app M' N1 = P
Subgoal 2 is:
app M1 N' = P
Subgoal 3 is:
R M1 = P
step_det < case H2.
Subgoal 1.1:
Variables: M' M1 N1 M'1
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {step M1 M'}*
H4 : {step M1 M'1}
============================
app M' N1 = app M'1 N1
Subgoal 1.2 is:
app M' N1 = app M1 N'
Subgoal 1.3 is:
app M' N1 = R N1
Subgoal 2 is:
app M1 N' = P
Subgoal 3 is:
R M1 = P
step_det < apply IH to H3 H4.
Subgoal 1.1:
Variables: M1 N1 M'1
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {step M1 M'1}*
H4 : {step M1 M'1}
============================
app M'1 N1 = app M'1 N1
Subgoal 1.2 is:
app M' N1 = app M1 N'
Subgoal 1.3 is:
app M' N1 = R N1
Subgoal 2 is:
app M1 N' = P
Subgoal 3 is:
R M1 = P
step_det < search.
Subgoal 1.2:
Variables: M' M1 N1 N'
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {step M1 M'}*
H4 : {value M1}
H5 : {step N1 N'}
============================
app M' N1 = app M1 N'
Subgoal 1.3 is:
app M' N1 = R N1
Subgoal 2 is:
app M1 N' = P
Subgoal 3 is:
R M1 = P
step_det < apply absurd_step_value to H3 H4.
Subgoal 1.3:
Variables: M' N1 R A
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {step (abs A R) M'}*
H4 : {value N1}
============================
app M' N1 = R N1
Subgoal 2 is:
app M1 N' = P
Subgoal 3 is:
R M1 = P
step_det < case H3.
Subgoal 2:
Variables: P N' N1 M1
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H2 : {step (app M1 N1) P}
H3 : {value M1}*
H4 : {step N1 N'}*
============================
app M1 N' = P
Subgoal 3 is:
R M1 = P
step_det < case H2.
Subgoal 2.1:
Variables: N' N1 M1 M'
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value M1}*
H4 : {step N1 N'}*
H5 : {step M1 M'}
============================
app M1 N' = app M' N1
Subgoal 2.2 is:
app M1 N' = app M1 N'1
Subgoal 2.3 is:
app (abs A R) N' = R N1
Subgoal 3 is:
R M1 = P
step_det < apply absurd_step_value to H5 H3.
Subgoal 2.2:
Variables: N' N1 M1 N'1
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value M1}*
H4 : {step N1 N'}*
H5 : {value M1}
H6 : {step N1 N'1}
============================
app M1 N' = app M1 N'1
Subgoal 2.3 is:
app (abs A R) N' = R N1
Subgoal 3 is:
R M1 = P
step_det < apply IH to H4 H6.
Subgoal 2.2:
Variables: N1 M1 N'1
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value M1}*
H4 : {step N1 N'1}*
H5 : {value M1}
H6 : {step N1 N'1}
============================
app M1 N'1 = app M1 N'1
Subgoal 2.3 is:
app (abs A R) N' = R N1
Subgoal 3 is:
R M1 = P
step_det < search.
Subgoal 2.3:
Variables: N' N1 R A
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value (abs A R)}*
H4 : {step N1 N'}*
H5 : {value N1}
============================
app (abs A R) N' = R N1
Subgoal 3 is:
R M1 = P
step_det < apply absurd_step_value to H4 H5.
Subgoal 3:
Variables: P M1 R A
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H2 : {step (app (abs A R) M1) P}
H3 : {value M1}*
============================
R M1 = P
step_det < case H2.
Subgoal 3.1:
Variables: M1 R A M'
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value M1}*
H4 : {step (abs A R) M'}
============================
R M1 = app M' M1
Subgoal 3.2 is:
R M1 = app (abs A R) N'
Subgoal 3.3 is:
R M1 = R M1
step_det < case H4.
Subgoal 3.2:
Variables: M1 R A N'
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value M1}*
H4 : {value (abs A R)}
H5 : {step M1 N'}
============================
R M1 = app (abs A R) N'
Subgoal 3.3 is:
R M1 = R M1
step_det < apply absurd_step_value to H5 H3.
Subgoal 3.3:
Variables: M1 R A
IH : forall M N P, {step M N}* -> {step M P} -> N = P
H3 : {value M1}*
H4 : {value M1}
============================
R M1 = R M1
step_det < search.
Proof completed.
Abella < Theorem step_follows_steps :
forall M N V, {step M N} -> {steps M V} -> {value V} -> {steps N V}.
============================
forall M N V, {step M N} -> {steps M V} -> {value V} -> {steps N V}
step_follows_steps < intros.
Variables: M N V
H1 : {step M N}
H2 : {steps M V}
H3 : {value V}
============================
{steps N V}
step_follows_steps < case H2.
Subgoal 1:
Variables: N V
H1 : {step V N}
H3 : {value V}
============================
{steps N V}
Subgoal 2 is:
{steps N V}
step_follows_steps < apply absurd_step_value to H1 H3.
Subgoal 2:
Variables: M N V P
H1 : {step M N}
H3 : {value V}
H4 : {step M P}
H5 : {steps P V}
============================
{steps N V}
step_follows_steps < apply step_det to H1 H4.
Subgoal 2:
Variables: M V P
H1 : {step M P}
H3 : {value V}
H4 : {step M P}
H5 : {steps P V}
============================
{steps P V}
step_follows_steps < search.
Proof completed.
Abella < Theorem steps_right :
forall M N R, {steps M N} -> {step N R} -> {steps M R}.
============================
forall M N R, {steps M N} -> {step N R} -> {steps M R}
steps_right < induction on 1.
IH : forall M N R, {steps M N}* -> {step N R} -> {steps M R}
============================
forall M N R, {steps M N}@ -> {step N R} -> {steps M R}
steps_right < intros.
Variables: M N R
IH : forall M N R, {steps M N}* -> {step N R} -> {steps M R}
H1 : {steps M N}@
H2 : {step N R}
============================
{steps M R}
steps_right < case H1.
Subgoal 1:
Variables: N R
IH : forall M N R, {steps M N}* -> {step N R} -> {steps M R}
H2 : {step N R}
============================
{steps N R}
Subgoal 2 is:
{steps M R}
steps_right < search.
Subgoal 2:
Variables: M N R P
IH : forall M N R, {steps M N}* -> {step N R} -> {steps M R}
H2 : {step N R}
H3 : {step M P}*
H4 : {steps P N}*
============================
{steps M R}
steps_right < apply IH to H4 H2.
Subgoal 2:
Variables: M N R P
IH : forall M N R, {steps M N}* -> {step N R} -> {steps M R}
H2 : {step N R}
H3 : {step M P}*
H4 : {steps P N}*
H5 : {steps P R}
============================
{steps M R}
steps_right < search.
Proof completed.
Abella < Theorem steps_app_value :
forall M N R, {value M} -> {steps N R} -> {steps (app M N) (app M R)}.
============================
forall M N R, {value M} -> {steps N R} -> {steps (app M N) (app M R)}
steps_app_value < induction on 2.
IH : forall M N R, {value M} -> {steps N R}* -> {steps (app M N) (app M R)}
============================
forall M N R, {value M} -> {steps N R}@ -> {steps (app M N) (app M R)}
steps_app_value < intros.
Variables: M N R
IH : forall M N R, {value M} -> {steps N R}* -> {steps (app M N) (app M R)}
H1 : {value M}
H2 : {steps N R}@
============================
{steps (app M N) (app M R)}
steps_app_value < case H2.
Subgoal 1:
Variables: M R
IH : forall M N R, {value M} -> {steps N R}* -> {steps (app M N) (app M R)}
H1 : {value M}
============================
{steps (app M R) (app M R)}
Subgoal 2 is:
{steps (app M N) (app M R)}
steps_app_value < search.
Subgoal 2:
Variables: M N R P
IH : forall M N R, {value M} -> {steps N R}* -> {steps (app M N) (app M R)}
H1 : {value M}
H3 : {step N P}*
H4 : {steps P R}*
============================
{steps (app M N) (app M R)}
steps_app_value < apply IH to H1 H4.
Subgoal 2:
Variables: M N R P
IH : forall M N R, {value M} -> {steps N R}* -> {steps (app M N) (app M R)}
H1 : {value M}
H3 : {step N P}*
H4 : {steps P R}*
H5 : {steps (app M P) (app M R)}
============================
{steps (app M N) (app M R)}
steps_app_value < search.
Proof completed.
Abella < Theorem halt_step_forward :
forall M N, halts M -> {step M N} -> halts N.
============================
forall M N, halts M -> {step M N} -> halts N
halt_step_forward < intros.
Variables: M N
H1 : halts M
H2 : {step M N}
============================
halts N
halt_step_forward < case H1.
Variables: M N V
H2 : {step M N}
H3 : {steps M V}
H4 : {value V}
============================
halts N
halt_step_forward < apply step_follows_steps to H2 H3 H4.
Variables: M N V
H2 : {step M N}
H3 : {steps M V}
H4 : {value V}
H5 : {steps N V}
============================
halts N
halt_step_forward < search.
Proof completed.
Abella < Theorem halt_step_backward :
forall M N, halts N -> {step M N} -> halts M.
============================
forall M N, halts N -> {step M N} -> halts M
halt_step_backward < intros.
Variables: M N
H1 : halts N
H2 : {step M N}
============================
halts M
halt_step_backward < case H1.
Variables: M N V
H2 : {step M N}
H3 : {steps N V}
H4 : {value V}
============================
halts M
halt_step_backward < search.
Proof completed.
Abella < Theorem of_step_forward :
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_forward < induction on 2.
IH : 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_forward < intros.
Variables: M N A
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H1 : {of M A}
H2 : {step M N}@
============================
{of N A}
of_step_forward < case H2.
Subgoal 1:
Variables: A M' M1 N1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H1 : {of (app M1 N1) A}
H3 : {step M1 M'}*
============================
{of (app M' N1) A}
Subgoal 2 is:
{of (app M1 N') A}
Subgoal 3 is:
{of (R M1) A}
of_step_forward < case H1.
Subgoal 1:
Variables: A M' M1 N1 A1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {step M1 M'}*
H4 : {of M1 (arrow A1 A)}
H5 : {of N1 A1}
============================
{of (app M' N1) A}
Subgoal 2 is:
{of (app M1 N') A}
Subgoal 3 is:
{of (R M1) A}
of_step_forward < apply IH to H4 H3.
Subgoal 1:
Variables: A M' M1 N1 A1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {step M1 M'}*
H4 : {of M1 (arrow A1 A)}
H5 : {of N1 A1}
H6 : {of M' (arrow A1 A)}
============================
{of (app M' N1) A}
Subgoal 2 is:
{of (app M1 N') A}
Subgoal 3 is:
{of (R M1) A}
of_step_forward < search.
Subgoal 2:
Variables: A N' N1 M1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H1 : {of (app M1 N1) A}
H3 : {value M1}*
H4 : {step N1 N'}*
============================
{of (app M1 N') A}
Subgoal 3 is:
{of (R M1) A}
of_step_forward < case H1.
Subgoal 2:
Variables: A N' N1 M1 A1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {value M1}*
H4 : {step N1 N'}*
H5 : {of M1 (arrow A1 A)}
H6 : {of N1 A1}
============================
{of (app M1 N') A}
Subgoal 3 is:
{of (R M1) A}
of_step_forward < apply IH to H6 H4.
Subgoal 2:
Variables: A N' N1 M1 A1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {value M1}*
H4 : {step N1 N'}*
H5 : {of M1 (arrow A1 A)}
H6 : {of N1 A1}
H7 : {of N' A1}
============================
{of (app M1 N') A}
Subgoal 3 is:
{of (R M1) A}
of_step_forward < search.
Subgoal 3:
Variables: A M1 R A1
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H1 : {of (app (abs A1 R) M1) A}
H3 : {value M1}*
============================
{of (R M1) A}
of_step_forward < case H1.
Subgoal 3:
Variables: A M1 R A1 A2
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {value M1}*
H4 : {of (abs A1 R) (arrow A2 A)}
H5 : {of M1 A2}
============================
{of (R M1) A}
of_step_forward < case H4.
Subgoal 3:
Variables: A M1 R A2
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {value M1}*
H5 : {of M1 A2}
H6 : {of n1 A2 |- of (R n1) A}
============================
{of (R M1) A}
of_step_forward < inst H6 with n1 = M1.
Subgoal 3:
Variables: A M1 R A2
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {value M1}*
H5 : {of M1 A2}
H6 : {of n1 A2 |- of (R n1) A}
H7 : {of M1 A2 |- of (R M1) A}
============================
{of (R M1) A}
of_step_forward < cut H7 with H5.
Subgoal 3:
Variables: A M1 R A2
IH : forall M N A, {of M A} -> {step M N}* -> {of N A}
H3 : {value M1}*
H5 : {of M1 A2}
H6 : {of n1 A2 |- of (R n1) A}
H7 : {of M1 A2 |- of (R M1) A}
H8 : {of (R M1) A}
============================
{of (R M1) A}
of_step_forward < search.
Proof completed.
Abella < Theorem reduce_step_forward :
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_forward < 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_forward < 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_forward < 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 : halts M
============================
reduce N top
Subgoal 2 is:
reduce N (arrow A1 B)
reduce_step_forward < apply of_step_forward 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 : halts M
H5 : {of N top}
============================
reduce N top
Subgoal 2 is:
reduce N (arrow A1 B)
reduce_step_forward < apply halt_step_forward 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 : halts M
H5 : {of N top}
H6 : halts N
============================
reduce N top
Subgoal 2 is:
reduce N (arrow A1 B)
reduce_step_forward < 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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
============================
reduce N (arrow A1 B)
reduce_step_forward < 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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
============================
{of N (arrow A1 B)}
Subgoal 2.2 is:
halts N
Subgoal 2.3 is:
forall N1, reduce N1 A1 -> reduce (app N N1) B
reduce_step_forward < apply of_step_forward 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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
H6 : {of N (arrow A1 B)}
============================
{of N (arrow A1 B)}
Subgoal 2.2 is:
halts N
Subgoal 2.3 is:
forall N1, reduce N1 A1 -> reduce (app N N1) B
reduce_step_forward < 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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
============================
halts N
Subgoal 2.3 is:
forall N1, reduce N1 A1 -> reduce (app N N1) B
reduce_step_forward < apply halt_step_forward to H4 H2.
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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
H6 : halts N
============================
halts N
Subgoal 2.3 is:
forall N1, reduce N1 A1 -> reduce (app N N1) B
reduce_step_forward < search.
Subgoal 2.3:
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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
============================
forall N1, reduce N1 A1 -> reduce (app N N1) B
reduce_step_forward < intros.
Subgoal 2.3:
Variables: M N B A1 N1
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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
H6 : reduce N1 A1
============================
reduce (app N N1) B
reduce_step_forward < apply H5 to H6.
Subgoal 2.3:
Variables: M N B A1 N1
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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
H6 : reduce N1 A1
H7 : reduce (app M N1) B *
============================
reduce (app N N1) B
reduce_step_forward < apply IH to H7 _.
Subgoal 2.3:
Variables: M N B A1 N1
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 : halts M
H5 : forall N, reduce N A1 -> reduce (app M N) B *
H6 : reduce N1 A1
H7 : reduce (app M N1) B *
H8 : reduce (app N N1) B
============================
reduce (app N N1) B
reduce_step_forward < search.
Proof completed.
Abella < Theorem reduce_steps_forward :
forall M N A, reduce M A -> {steps M N} -> reduce N A.
============================
forall M N A, reduce M A -> {steps M N} -> reduce N A
reduce_steps_forward < induction on 2.
IH : forall M N A, reduce M A -> {steps M N}* -> reduce N A
============================
forall M N A, reduce M A -> {steps M N}@ -> reduce N A
reduce_steps_forward < intros.
Variables: M N A
IH : forall M N A, reduce M A -> {steps M N}* -> reduce N A
H1 : reduce M A
H2 : {steps M N}@
============================
reduce N A
reduce_steps_forward < case H2.
Subgoal 1:
Variables: N A
IH : forall M N A, reduce M A -> {steps M N}* -> reduce N A
H1 : reduce N A
============================
reduce N A
Subgoal 2 is:
reduce N A
reduce_steps_forward < search.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce M A -> {steps M N}* -> reduce N A
H1 : reduce M A
H3 : {step M P}*
H4 : {steps P N}*
============================
reduce N A
reduce_steps_forward < apply reduce_step_forward to H1 H3.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce M A -> {steps M N}* -> reduce N A
H1 : reduce M A
H3 : {step M P}*
H4 : {steps P N}*
H5 : reduce P A
============================
reduce N A
reduce_steps_forward < apply IH to H5 H4.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce M A -> {steps M N}* -> reduce N A
H1 : reduce M A
H3 : {step M P}*
H4 : {steps P N}*
H5 : reduce P A
H6 : reduce N A
============================
reduce N A
reduce_steps_forward < search.
Proof completed.
Abella < Theorem reduce_step_backward :
forall M N A, reduce N A -> {step M N} -> {of M A} -> reduce M A.
============================
forall M N A, reduce N A -> {step M N} -> {of M A} -> reduce M A
reduce_step_backward < induction on 1.
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
============================
forall M N A, reduce N A @ -> {step M N} -> {of M A} -> reduce M A
reduce_step_backward < intros.
Variables: M N A
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H1 : reduce N A @
H2 : {step M N}
H3 : {of M A}
============================
reduce M A
reduce_step_backward < case H1.
Subgoal 1:
Variables: M N
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M top}
H4 : {of N top}
H5 : halts N
============================
reduce M top
Subgoal 2 is:
reduce M (arrow A1 B)
reduce_step_backward < apply halt_step_backward to H5 H2.
Subgoal 1:
Variables: M N
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M top}
H4 : {of N top}
H5 : halts N
H6 : halts M
============================
reduce M top
Subgoal 2 is:
reduce M (arrow A1 B)
reduce_step_backward < search.
Subgoal 2:
Variables: M N B A1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
============================
reduce M (arrow A1 B)
reduce_step_backward < unfold.
Subgoal 2.1:
Variables: M N B A1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
============================
{of M (arrow A1 B)}
Subgoal 2.2 is:
halts M
Subgoal 2.3 is:
forall N, reduce N A1 -> reduce (app M N) B
reduce_step_backward < search.
Subgoal 2.2:
Variables: M N B A1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
============================
halts M
Subgoal 2.3 is:
forall N, reduce N A1 -> reduce (app M N) B
reduce_step_backward < apply halt_step_backward to H5 H2.
Subgoal 2.2:
Variables: M N B A1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
H7 : halts M
============================
halts M
Subgoal 2.3 is:
forall N, reduce N A1 -> reduce (app M N) B
reduce_step_backward < search.
Subgoal 2.3:
Variables: M N B A1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
============================
forall N, reduce N A1 -> reduce (app M N) B
reduce_step_backward < intros.
Subgoal 2.3:
Variables: M N B A1 N1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
H7 : reduce N1 A1
============================
reduce (app M N1) B
reduce_step_backward < apply H6 to H7.
Subgoal 2.3:
Variables: M N B A1 N1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
H7 : reduce N1 A1
H8 : reduce (app N N1) B *
============================
reduce (app M N1) B
reduce_step_backward < apply reduce_of to H7.
Subgoal 2.3:
Variables: M N B A1 N1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
H7 : reduce N1 A1
H8 : reduce (app N N1) B *
H9 : {of N1 A1}
============================
reduce (app M N1) B
reduce_step_backward < apply IH to H8 _ _.
Subgoal 2.3:
Variables: M N B A1 N1
IH : forall M N A, reduce N A * -> {step M N} -> {of M A} -> reduce M A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : {of N (arrow A1 B)}
H5 : halts N
H6 : forall N1, reduce N1 A1 -> reduce (app N N1) B *
H7 : reduce N1 A1
H8 : reduce (app N N1) B *
H9 : {of N1 A1}
H10 : reduce (app M N1) B
============================
reduce (app M N1) B
reduce_step_backward < search.
Proof completed.
Abella < Theorem reduce_steps_backward :
forall M N A, reduce N A -> {steps M N} -> {of M A} -> reduce M A.
============================
forall M N A, reduce N A -> {steps M N} -> {of M A} -> reduce M A
reduce_steps_backward < induction on 2.
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
============================
forall M N A, reduce N A -> {steps M N}@ -> {of M A} -> reduce M A
reduce_steps_backward < intros.
Variables: M N A
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
H1 : reduce N A
H2 : {steps M N}@
H3 : {of M A}
============================
reduce M A
reduce_steps_backward < case H2.
Subgoal 1:
Variables: N A
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
H1 : reduce N A
H3 : {of N A}
============================
reduce N A
Subgoal 2 is:
reduce M A
reduce_steps_backward < search.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
H1 : reduce N A
H3 : {of M A}
H4 : {step M P}*
H5 : {steps P N}*
============================
reduce M A
reduce_steps_backward < apply of_step_forward to H3 H4.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
H1 : reduce N A
H3 : {of M A}
H4 : {step M P}*
H5 : {steps P N}*
H6 : {of P A}
============================
reduce M A
reduce_steps_backward < apply IH to H1 H5 H6.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
H1 : reduce N A
H3 : {of M A}
H4 : {step M P}*
H5 : {steps P N}*
H6 : {of P A}
H7 : reduce P A
============================
reduce M A
reduce_steps_backward < apply reduce_step_backward to H7 H4 H3.
Subgoal 2:
Variables: M N A P
IH : forall M N A, reduce N A -> {steps M N}* -> {of M A} -> reduce M A
H1 : reduce N A
H3 : {of M A}
H4 : {step M P}*
H5 : {steps P N}*
H6 : {of P A}
H7 : reduce P A
H8 : reduce M A
============================
reduce M A
reduce_steps_backward < search.
Proof completed.
Abella < Define ctx : olist -> prop by
ctx nil;
nabla x, ctx (of x A :: L) := ctx L.
Abella < Define closed : tm -> prop by
closed M := exists A, {of M A}.
Abella < Define name : tm -> prop by
nabla x, name x.
Abella < Theorem ctx_member :
forall L E, ctx L -> member E L -> (exists X A, E = of X A /\ name X).
============================
forall L E, ctx L -> member E L -> (exists X A, E = of X A /\ name X)
ctx_member < induction on 1.
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
============================
forall L E, ctx L @ -> member E L -> (exists X A, E = of X A /\ name X)
ctx_member < intros.
Variables: L E
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
H1 : ctx L @
H2 : member E L
============================
exists X A, E = of X A /\ name X
ctx_member < case H1.
Subgoal 1:
Variables: E
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
H2 : member E nil
============================
exists X A, E = of X A /\ name X
Subgoal 2 is:
exists X A, E n1 = of X A /\ name X
ctx_member < case H2.
Subgoal 2:
Variables: E L1 A
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
H2 : member (E n1) (of n1 A :: L1)
H3 : ctx L1 *
============================
exists X A, E n1 = of X A /\ name X
ctx_member < case H2.
Subgoal 2.1:
Variables: L1 A
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
H3 : ctx L1 *
============================
exists X A1, of n1 A = of X A1 /\ name X
Subgoal 2.2 is:
exists X A, E n1 = of X A /\ name X
ctx_member < search.
Subgoal 2.2:
Variables: E L1 A
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
H3 : ctx L1 *
H4 : member (E n1) L1
============================
exists X A, E n1 = of X A /\ name X
ctx_member < apply IH to H3 H4.
Subgoal 2.2:
Variables: L1 A X A1
IH : forall L E, ctx L * -> member E L -> (exists X A, E = of X A /\ name X)
H3 : ctx L1 *
H4 : member (of (X n1) A1) L1
H5 : name (X n1)
============================
exists X1 A, of (X n1) A1 = of X1 A /\ name X1
ctx_member < search.
Proof completed.
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, 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, 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, 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, of n2 A1 |- of (R1 n1 n2) B}*
============================
exists M, z1\abs A1 (R1 z1) = y\M
Subgoal 3 is:
exists M, R = y\M
prune_of < apply IH to _ H3.
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, of n2 A1 |- of (M n2) B}*
============================
exists M1, z1\abs A1 (z2\M z2) = y\M1
Subgoal 3 is:
exists M, R = y\M
prune_of < search.
Subgoal 3:
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 ctx_member to H1 H4.
Subgoal 3:
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 n1) A1] |- of (R n1) A}*
H4 : member (of (X n1) A1) L
H5 : name (X n1)
============================
exists M, R = y\M
prune_of < case H3.
Subgoal 3:
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
H4 : member (of (R n1) A) L
H5 : name (R n1)
============================
exists M, R = y\M
prune_of < apply member_prune to H4.
Subgoal 3:
Variables: L A F2
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
(exists M, R = y\M)
H1 : ctx L
H4 : member (of F2 A) L
H5 : name F2
============================
exists M, z1\F2 = 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 V, reduce V A /\ {value V} /\ subst L (R V) 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 V M1 L1 A
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed (M n1)
H3 : reduce V A
H4 : {value V}
H5 : subst L1 (M V) M1 *
============================
M n1 = M1
closed_subst < apply prune_closed to H1.
Subgoal 2:
Variables: V M1 L1 A M2
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M2
H3 : reduce V A
H4 : {value V}
H5 : subst L1 M2 M1 *
============================
M2 = M1
closed_subst < apply IH to H1 H5.
Subgoal 2:
Variables: V M1 L1 A
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M1
H3 : reduce V A
H4 : {value V}
H5 : subst L1 M1 M1 *
============================
M1 = M1
closed_subst < 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 : 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 : ctx L1 *
============================
reduce (N n1) A1
Subgoal 2.2 is:
reduce (N n1) A
subst_var < case H3.
Subgoal 2.1:
Variables: L1 A1 V M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 V M1
============================
reduce M1 A1
Subgoal 2.2 is:
reduce (N n1) A
subst_var < apply reduce_closed to H5.
Subgoal 2.1:
Variables: L1 A1 V M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 V M1
H8 : closed V
============================
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 : ctx L1 *
H5 : reduce M1 A1
H6 : {value M1}
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 : ctx L1 *
H5 : member (of (M n1) A) L1
============================
reduce (N n1) A
subst_var < case H3.
Subgoal 2.2:
Variables: M A L1 A1 V M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : ctx L1 *
H5 : member (of (M n1) A) L1
H6 : reduce V A1
H7 : {value V}
H8 : subst L1 (M V) M1
============================
reduce M1 A
subst_var < apply member_prune to H5.
Subgoal 2.2:
Variables: A L1 A1 V M1 F1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : ctx L1 *
H5 : member (of F1 A) L1
H6 : reduce V A1
H7 : {value V}
H8 : subst L1 F1 M1
============================
reduce M1 A
subst_var < apply IH to H4 H5 H8.
Subgoal 2.2:
Variables: A L1 A1 V M1 F1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
reduce N A
H4 : ctx L1 *
H5 : member (of F1 A) L1
H6 : reduce V A1
H7 : {value V}
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 : 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 V 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 : ctx L1 *
H4 : reduce V A
H5 : {value V}
H6 : subst L1 (app (M V) (N V)) 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 H3 H6.
Subgoal 2:
Variables: M N L1 A V 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 : ctx L1 *
H4 : reduce V A
H5 : {value V}
H6 : subst L1 (app (M V) (N V)) (app MR NR)
H7 : subst L1 (M V) MR
H8 : subst L1 (N V) 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 ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V)))).
============================
forall L M R A, ctx L -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
subst_abs < induction on 1.
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
============================
forall L M R A, ctx L @ -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
subst_abs < intros.
Variables: L M R A
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H1 : ctx L @
H2 : subst L (abs A M) R
============================
exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V)))
subst_abs < case H1.
Subgoal 1:
Variables: M R A
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H2 : subst nil (abs A M) R
============================
exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: nil) (M x) (MR V)))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < case H2.
Subgoal 1:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
============================
exists MR, abs A M = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: nil) (M x) (MR V)))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < exists M.
Subgoal 1:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
============================
abs A M = abs A M /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: nil) (M x) (M V)))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < split.
Subgoal 1.1:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
============================
abs A M = abs A M
Subgoal 1.2 is:
forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: nil) (M x) (M V))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < search.
Subgoal 1.2:
Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
============================
forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: nil) (M x) (M V))
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < intros.
Subgoal 1.2:
Variables: M A V
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : reduce V A
H4 : {value V}
============================
subst (of n1 A :: nil) (M n1) (M V)
Subgoal 2 is:
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
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 ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H2 : subst (of n1 A1 :: L1) (abs A (M n1)) (R n1)
H3 : ctx L1 *
============================
exists MR, R n1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < case H2.
Subgoal 2:
Variables: M A L1 A1 V M1
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) M1
============================
exists MR, M1 = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < apply IH to H3 H6.
Subgoal 2:
Variables: M A L1 A1 V MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
============================
exists MR1, abs A MR = abs A MR1 /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR1 V)))
subst_abs < exists MR.
Subgoal 2:
Variables: M A L1 A1 V MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
============================
abs A MR = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V)))
subst_abs < split.
Subgoal 2.1:
Variables: M A L1 A1 V MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
============================
abs A MR = abs A MR
Subgoal 2.2 is:
forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V))
subst_abs < search.
Subgoal 2.2:
Variables: M A L1 A1 V MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
============================
forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR V))
subst_abs < intros.
Subgoal 2.2:
Variables: M A L1 A1 V MR V1
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
H8 : reduce (V1 n1) A
H9 : {value (V1 n1)}
============================
subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR (V1 n1))
subst_abs < apply prune_reduce to H8.
Subgoal 2.2:
Variables: M A L1 A1 V MR M2
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
H8 : reduce M2 A
H9 : {value M2}
============================
subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)
subst_abs < apply H7 to H8 H9.
Subgoal 2.2:
Variables: M A L1 A1 V MR M2
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
H8 : reduce M2 A
H9 : {value M2}
H10 : subst (of n1 A :: L1) (M V 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 V MR M2 V2
IH : forall L M R A, ctx L * -> subst L (abs A M) R ->
(exists MR, R = abs A MR /\
(forall V, reduce V A -> {value V} ->
(nabla x, subst (of x A :: L) (M x) (MR V))))
H3 : ctx L1 *
H4 : reduce V A1
H5 : {value V}
H6 : subst L1 (abs A (M V)) (abs A MR)
H7 : forall V1, reduce V1 A -> {value V1} ->
(nabla x, subst (of x A :: L1) (M V x) (MR V1))
H8 : reduce M2 A
H9 : {value M2}
H11 : reduce V2 A
H12 : {value V2}
H13 : subst L1 (M V V2) (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 : ctx L1 *
============================
{of (N n1) A}
subst_preserves_ty < case H2.
Subgoal 2:
Variables: M A L1 A1 V 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 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 (M V) M1
============================
{of M1 A}
subst_preserves_ty < apply reduce_of to H5.
Subgoal 2:
Variables: M A L1 A1 V 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 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 (M V) M1
H8 : {of V A1}
============================
{of M1 A}
subst_preserves_ty < inst H3 with n1 = V.
Subgoal 2:
Variables: M A L1 A1 V 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 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 (M V) M1
H8 : {of V A1}
H9 : {L1, of V A1 |- of (M V) A}
============================
{of M1 A}
subst_preserves_ty < cut H9 with H8.
Subgoal 2:
Variables: M A L1 A1 V 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 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 (M V) M1
H8 : {of V A1}
H9 : {L1, of V A1 |- of (M V) A}
H10 : {L1 |- of (M V) A}
============================
{of M1 A}
subst_preserves_ty < apply IH to H4 H7 H10.
Subgoal 2:
Variables: M A L1 A1 V 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 : ctx L1 *
H5 : reduce V A1
H6 : {value V}
H7 : subst L1 (M V) M1
H8 : {of V A1}
H9 : {L1, of V A1 |- of (M V) A}
H10 : {L1 |- of (M V) A}
H11 : {of M1 A}
============================
{of M1 A}
subst_preserves_ty < search.
Proof completed.
Abella < Theorem weak_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
weak_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
weak_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
weak_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
weak_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
weak_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
weak_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
weak_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 : halts MR
H12 : forall N, reduce N A1 -> reduce (app MR N) A
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
weak_norm_ext < apply H12 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 : halts MR
H12 : forall N, reduce N A1 -> reduce (app MR N) A
H13 : reduce (app MR NR) A
============================
reduce (app MR NR) A
Subgoal 2 is:
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
weak_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, of n1 A1 |- of (R1 n1) B}*
============================
reduce R (arrow A1 B)
Subgoal 3 is:
reduce R A
weak_norm_ext < apply subst_abs to H1 H3.
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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
============================
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
weak_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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
============================
reduce (abs A1 MR) (arrow A1 B)
Subgoal 3 is:
reduce R A
weak_norm_ext < unfold.
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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
============================
{of (abs A1 MR) (arrow A1 B)}
Subgoal 2.2 is:
halts (abs A1 MR)
Subgoal 2.3 is:
forall N, reduce N A1 -> reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < search.
Subgoal 2.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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
============================
halts (abs A1 MR)
Subgoal 2.3 is:
forall N, reduce N A1 -> reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < search.
Subgoal 2.3:
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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
============================
forall N, reduce N A1 -> reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < intros.
Subgoal 2.3:
Variables: L B R1 A1 MR N
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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply reduce_halts to H7.
Subgoal 2.3:
Variables: L B R1 A1 MR N
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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H8 : halts N
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < case H8.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply reduce_steps_forward to H7 H9.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply H5 to H11 H10.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
H12 : subst (of n1 A1 :: L) (R1 n1) (MR V)
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply IH to _ H4 H12.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
H12 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H13 : reduce (MR V) B
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply steps_app_value to _ H9 with M = abs A1 MR.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
H12 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H13 : reduce (MR V) B
H14 : {steps (app (abs A1 MR) N) (app (abs A1 MR) V)}
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply steps_right to H14 _ with R = MR V.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
H12 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H13 : reduce (MR V) B
H14 : {steps (app (abs A1 MR) N) (app (abs A1 MR) V)}
H15 : {steps (app (abs A1 MR) N) (MR V)}
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply reduce_of to H7.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
H12 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H13 : reduce (MR V) B
H14 : {steps (app (abs A1 MR) N) (app (abs A1 MR) V)}
H15 : {steps (app (abs A1 MR) N) (MR V)}
H16 : {of N A1}
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < apply reduce_steps_backward to H13 H15 _.
Subgoal 2.3:
Variables: L B R1 A1 MR N 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, of n1 A1 |- of (R1 n1) B}*
H5 : forall V, reduce V A1 -> {value V} ->
(nabla x, subst (of x A1 :: L) (R1 x) (MR V))
H6 : {of (abs A1 MR) (arrow A1 B)}
H7 : reduce N A1
H9 : {steps N V}
H10 : {value V}
H11 : reduce V A1
H12 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H13 : reduce (MR V) B
H14 : {steps (app (abs A1 MR) N) (app (abs A1 MR) V)}
H15 : {steps (app (abs A1 MR) N) (MR V)}
H16 : {of N A1}
H17 : reduce (app (abs A1 MR) N) B
============================
reduce (app (abs A1 MR) N) B
Subgoal 3 is:
reduce R A
weak_norm_ext < search.
Subgoal 3:
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
weak_norm_ext < apply ctx_member to H1 H5.
Subgoal 3:
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
============================
reduce R A
weak_norm_ext < case H6.
Subgoal 3:
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)
============================
reduce (R n1) A
weak_norm_ext < case H4.
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 n1)
H2 : {L n1 |- of n1 A}@
H3 : subst (L n1) n1 (R n1)
H5 : member (of n1 A) (L n1)
============================
reduce (R n1) A
weak_norm_ext < apply subst_var to H1 H5 H3.
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 n1)
H2 : {L n1 |- of n1 A}@
H3 : subst (L n1) n1 (R n1)
H5 : member (of n1 A) (L n1)
H7 : reduce (R n1) A
============================
reduce (R n1) A
weak_norm_ext < search.
Proof completed.
Abella < Theorem weak_norm :
forall M A, {of M A} -> halts M.
============================
forall M A, {of M A} -> halts M
weak_norm < intros.
Variables: M A
H1 : {of M A}
============================
halts M
weak_norm < apply weak_norm_ext to _ H1 _.
Variables: M A
H1 : {of M A}
H2 : reduce M A
============================
halts M
weak_norm < apply reduce_halts to H2.
Variables: M A
H1 : {of M A}
H2 : reduce M A
H3 : halts M
============================
halts M
weak_norm < search.
Proof completed.
Abella <
