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 <