Abella: Subject reduction for PCF

Welcome to Abella 1.1.3-dev2 Reading clauses from pcf.mod

Abella < Theorem subject_reduction : 
forall P V T, {eval P V} -> {of P T} -> {of V T}.

1 subgoal(s).

  
  ============================
   forall P V T, {eval P V} -> {of P T} -> {of V T}

subject_reduction < induction on 1.

1 subgoal(s).

  
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  ============================
   forall P V T, {eval P V}@ -> {of P T} -> {of V T}

subject_reduction < intros.

1 subgoal(s).

  Variables: P, V, T
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H1 : {eval P V}@
  H2 : {of P T}
  ============================
   {of V T}

subject_reduction < case H1.

13 subgoal(s).

  Variables: P, V, T
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of zero T}
  ============================
   {of zero T}

subgoal 2 is:
 {of tt T}

subgoal 3 is:
 {of ff T}

subgoal 4 is:
 {of (succ V1) T}

subgoal 5 is:
 {of zero T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of tt T}

subgoal 8 is:
 {of ff T}

subgoal 9 is:
 {of V T}

subgoal 10 is:
 {of V T}

subgoal 11 is:
 {of (abs T1 R) T}

subgoal 12 is:
 {of V T}

subgoal 13 is:
 {of V T}

subject_reduction < search.

12 subgoal(s).

  Variables: P, V, T
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of tt T}
  ============================
   {of tt T}

subgoal 2 is:
 {of ff T}

subgoal 3 is:
 {of (succ V1) T}

subgoal 4 is:
 {of zero T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of tt T}

subgoal 7 is:
 {of ff T}

subgoal 8 is:
 {of V T}

subgoal 9 is:
 {of V T}

subgoal 10 is:
 {of (abs T1 R) T}

subgoal 11 is:
 {of V T}

subgoal 12 is:
 {of V T}

subject_reduction < search.

11 subgoal(s).

  Variables: P, V, T
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of ff T}
  ============================
   {of ff T}

subgoal 2 is:
 {of (succ V1) T}

subgoal 3 is:
 {of zero T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of tt T}

subgoal 6 is:
 {of ff T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of V T}

subgoal 9 is:
 {of (abs T1 R) T}

subgoal 10 is:
 {of V T}

subgoal 11 is:
 {of V T}

subject_reduction < search.

10 subgoal(s).

  Variables: P, V, T, V1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (succ M) T}
  H3 : {eval M V1}*
  ============================
   {of (succ V1) T}

subgoal 2 is:
 {of zero T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of tt T}

subgoal 5 is:
 {of ff T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of (abs T1 R) T}

subgoal 9 is:
 {of V T}

subgoal 10 is:
 {of V T}

subject_reduction < case H2.

10 subgoal(s).

  Variables: P, V, T, V1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M V1}*
  H4 : {of M num}
  ============================
   {of (succ V1) num}

subgoal 2 is:
 {of zero T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of tt T}

subgoal 5 is:
 {of ff T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of (abs T1 R) T}

subgoal 9 is:
 {of V T}

subgoal 10 is:
 {of V T}

subject_reduction < apply IH to H3 H4.

10 subgoal(s).

  Variables: P, V, T, V1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M V1}*
  H4 : {of M num}
  H5 : {of V1 num}
  ============================
   {of (succ V1) num}

subgoal 2 is:
 {of zero T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of tt T}

subgoal 5 is:
 {of ff T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of (abs T1 R) T}

subgoal 9 is:
 {of V T}

subgoal 10 is:
 {of V T}

subject_reduction < search.

9 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (pred M) T}
  H3 : {eval M zero}*
  ============================
   {of zero T}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of tt T}

subgoal 4 is:
 {of ff T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of (abs T1 R) T}

subgoal 8 is:
 {of V T}

subgoal 9 is:
 {of V T}

subject_reduction < case H2.

9 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M zero}*
  H4 : {of M num}
  ============================
   {of zero num}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of tt T}

subgoal 4 is:
 {of ff T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of (abs T1 R) T}

subgoal 8 is:
 {of V T}

subgoal 9 is:
 {of V T}

subject_reduction < search.

8 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (pred M) T}
  H3 : {eval M (succ V)}*
  ============================
   {of V T}

subgoal 2 is:
 {of tt T}

subgoal 3 is:
 {of ff T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of (abs T1 R) T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of V T}

subject_reduction < case H2.

8 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (succ V)}*
  H4 : {of M num}
  ============================
   {of V num}

subgoal 2 is:
 {of tt T}

subgoal 3 is:
 {of ff T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of (abs T1 R) T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of V T}

subject_reduction < apply IH to H3 H4.

8 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (succ V)}*
  H4 : {of M num}
  H5 : {of (succ V) num}
  ============================
   {of V num}

subgoal 2 is:
 {of tt T}

subgoal 3 is:
 {of ff T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of (abs T1 R) T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of V T}

subject_reduction < case H5.

8 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (succ V)}*
  H4 : {of M num}
  H6 : {of V num}
  ============================
   {of V num}

subgoal 2 is:
 {of tt T}

subgoal 3 is:
 {of ff T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of (abs T1 R) T}

subgoal 7 is:
 {of V T}

subgoal 8 is:
 {of V T}

subject_reduction < search.

7 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (is_zero M) T}
  H3 : {eval M zero}*
  ============================
   {of tt T}

subgoal 2 is:
 {of ff T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of (abs T1 R) T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of V T}

subject_reduction < case H2.

7 subgoal(s).

  Variables: P, V, T, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M zero}*
  H4 : {of M num}
  ============================
   {of tt bool}

subgoal 2 is:
 {of ff T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of (abs T1 R) T}

subgoal 6 is:
 {of V T}

subgoal 7 is:
 {of V T}

subject_reduction < search.

6 subgoal(s).

  Variables: P, V, T, V1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (is_zero M) T}
  H3 : {eval M (succ V1)}*
  ============================
   {of ff T}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of (abs T1 R) T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of V T}

subject_reduction < case H2.

6 subgoal(s).

  Variables: P, V, T, V1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (succ V1)}*
  H4 : {of M num}
  ============================
   {of ff bool}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of (abs T1 R) T}

subgoal 5 is:
 {of V T}

subgoal 6 is:
 {of V T}

subject_reduction < search.

5 subgoal(s).

  Variables: P, V, T, N2, N1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (if M N1 N2) T}
  H3 : {eval M tt}*
  H4 : {eval N1 V}*
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of (abs T1 R) T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subject_reduction < case H2.

5 subgoal(s).

  Variables: P, V, T, N2, N1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M tt}*
  H4 : {eval N1 V}*
  H5 : {of M bool}
  H6 : {of N1 T}
  H7 : {of N2 T}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of (abs T1 R) T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subject_reduction < apply IH to H4 H6.

5 subgoal(s).

  Variables: P, V, T, N2, N1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M tt}*
  H4 : {eval N1 V}*
  H5 : {of M bool}
  H6 : {of N1 T}
  H7 : {of N2 T}
  H8 : {of V T}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of (abs T1 R) T}

subgoal 4 is:
 {of V T}

subgoal 5 is:
 {of V T}

subject_reduction < search.

4 subgoal(s).

  Variables: P, V, T, N2, N1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (if M N1 N2) T}
  H3 : {eval M ff}*
  H4 : {eval N2 V}*
  ============================
   {of V T}

subgoal 2 is:
 {of (abs T1 R) T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of V T}

subject_reduction < case H2.

4 subgoal(s).

  Variables: P, V, T, N2, N1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M ff}*
  H4 : {eval N2 V}*
  H5 : {of M bool}
  H6 : {of N1 T}
  H7 : {of N2 T}
  ============================
   {of V T}

subgoal 2 is:
 {of (abs T1 R) T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of V T}

subject_reduction < apply IH to H4 H7.

4 subgoal(s).

  Variables: P, V, T, N2, N1, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M ff}*
  H4 : {eval N2 V}*
  H5 : {of M bool}
  H6 : {of N1 T}
  H7 : {of N2 T}
  H8 : {of V T}
  ============================
   {of V T}

subgoal 2 is:
 {of (abs T1 R) T}

subgoal 3 is:
 {of V T}

subgoal 4 is:
 {of V T}

subject_reduction < search.

3 subgoal(s).

  Variables: P, V, T, R, T1
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (abs T1 R) T}
  ============================
   {of (abs T1 R) T}

subgoal 2 is:
 {of V T}

subgoal 3 is:
 {of V T}

subject_reduction < search.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (app M N) T}
  H3 : {eval M (abs T1 R)}*
  H4 : {eval (R N) V}*
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < case H2.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M, U
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (abs T1 R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arr U T)}
  H6 : {of N U}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < apply IH to H3 H5.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M, U
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (abs T1 R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arr U T)}
  H6 : {of N U}
  H7 : {of (abs T1 R) (arr U T)}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < case H7.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M, U
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (abs U R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arr U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < inst H8 with n1 = N.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M, U
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (abs U R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arr U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  H9 : {of N U |- of (R N) T}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < cut H9 with H6.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M, U
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (abs U R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arr U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  H9 : {of N U |- of (R N) T}
  H10 : {of (R N) T}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < apply IH to H4 H10.

2 subgoal(s).

  Variables: P, V, T, R, T1, N, M, U
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H3 : {eval M (abs U R)}*
  H4 : {eval (R N) V}*
  H5 : {of M (arr U T)}
  H6 : {of N U}
  H8 : {of n1 U |- of (R n1) T}
  H9 : {of N U |- of (R N) T}
  H10 : {of (R N) T}
  H11 : {of V T}
  ============================
   {of V T}

subgoal 2 is:
 {of V T}

subject_reduction < search.

1 subgoal(s).

  Variables: P, V, T, R, T1
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (rec T1 R) T}
  H3 : {eval (R (rec T1 R)) V}*
  ============================
   {of V T}

subject_reduction < case H2 (keep).

1 subgoal(s).

  Variables: P, V, T, R, T1
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (rec T R) T}
  H3 : {eval (R (rec T R)) V}*
  H4 : {of n1 T |- of (R n1) T}
  ============================
   {of V T}

subject_reduction < inst H4 with n1 = rec T R.

1 subgoal(s).

  Variables: P, V, T, R, T1
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (rec T R) T}
  H3 : {eval (R (rec T R)) V}*
  H4 : {of n1 T |- of (R n1) T}
  H5 : {of (rec T R) T |- of (R (rec T R)) T}
  ============================
   {of V T}

subject_reduction < cut H5 with H2.

1 subgoal(s).

  Variables: P, V, T, R, T1
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (rec T R) T}
  H3 : {eval (R (rec T R)) V}*
  H4 : {of n1 T |- of (R n1) T}
  H5 : {of (rec T R) T |- of (R (rec T R)) T}
  H6 : {of (R (rec T R)) T}
  ============================
   {of V T}

subject_reduction < apply IH to H3 H6.

1 subgoal(s).

  Variables: P, V, T, R, T1
  IH : forall P V T, {eval P V}* -> {of P T} -> {of V T}
  H2 : {of (rec T R) T}
  H3 : {eval (R (rec T R)) V}*
  H4 : {of n1 T |- of (R n1) T}
  H5 : {of (rec T R) T |- of (R (rec T R)) T}
  H6 : {of (R (rec T R)) T}
  H7 : {of V T}
  ============================
   {of V T}

subject_reduction < search.
Proof completed.

Abella < Goodbye.