Welcome to Abella 2.0.4-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 <