Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
authormengj
Wed Sep 20 14:02:41 2006 +0200 (2006-09-20)
changeset 20647680b58597f65
parent 20646 02729d4d6e4a
child 20648 742c30fc3fcb
Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
src/HOL/Tools/atp-inputs/const_combBC.dfg
src/HOL/Tools/atp-inputs/const_combBC.tptp
src/HOL/Tools/atp-inputs/const_combBC_e.dfg
src/HOL/Tools/atp-inputs/const_combBC_e.tptp
src/HOL/Tools/atp-inputs/const_combIK.dfg
src/HOL/Tools/atp-inputs/const_combIK.tptp
src/HOL/Tools/atp-inputs/const_combS.dfg
src/HOL/Tools/atp-inputs/const_combS.tptp
src/HOL/Tools/atp-inputs/const_combS_e.dfg
src/HOL/Tools/atp-inputs/const_combS_e.tptp
src/HOL/Tools/atp-inputs/full_combBC.dfg
src/HOL/Tools/atp-inputs/full_combBC.tptp
src/HOL/Tools/atp-inputs/full_combBC_e.dfg
src/HOL/Tools/atp-inputs/full_combBC_e.tptp
src/HOL/Tools/atp-inputs/full_combIK.dfg
src/HOL/Tools/atp-inputs/full_combIK.tptp
src/HOL/Tools/atp-inputs/full_combS.dfg
src/HOL/Tools/atp-inputs/full_combS.tptp
src/HOL/Tools/atp-inputs/full_combS_e.dfg
src/HOL/Tools/atp-inputs/full_combS_e.tptp
src/HOL/Tools/atp-inputs/par_combBC.dfg
src/HOL/Tools/atp-inputs/par_combBC.tptp
src/HOL/Tools/atp-inputs/par_combBC_e.dfg
src/HOL/Tools/atp-inputs/par_combBC_e.tptp
src/HOL/Tools/atp-inputs/par_combIK.dfg
src/HOL/Tools/atp-inputs/par_combIK.tptp
src/HOL/Tools/atp-inputs/par_combS.dfg
src/HOL/Tools/atp-inputs/par_combS.tptp
src/HOL/Tools/atp-inputs/par_combS_e.dfg
src/HOL/Tools/atp-inputs/par_combS_e.tptp
src/HOL/Tools/atp-inputs/u_combBC.dfg
src/HOL/Tools/atp-inputs/u_combBC.tptp
src/HOL/Tools/atp-inputs/u_combBC_e.dfg
src/HOL/Tools/atp-inputs/u_combBC_e.tptp
src/HOL/Tools/atp-inputs/u_combIK.dfg
src/HOL/Tools/atp-inputs/u_combIK.tptp
src/HOL/Tools/atp-inputs/u_combS.dfg
src/HOL/Tools/atp-inputs/u_combS.tptp
src/HOL/Tools/atp-inputs/u_combS_e.dfg
src/HOL/Tools/atp-inputs/u_combS_e.tptp
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/atp-inputs/const_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
     1.3 @@ -0,0 +1,13 @@
     1.4 +%ID: $Id$
     1.5 +%Author: Jia Meng, NICTA
     1.6 +%const-typed combinator reduction for B, C
     1.7 +
     1.8 +clause(
     1.9 +forall([A, B, C, P, Q, R],
    1.10 +or( equal(hAPP(hAPP(hAPP(c_COMBB(A,B,C),P),Q),R),hAPP(P,hAPP(Q,R))))),
    1.11 +a4 ).
    1.12 +
    1.13 +clause(
    1.14 +forall([A, B, C, P, Q, R],
    1.15 +or( equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q)))),
    1.16 +a5 ).
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/atp-inputs/const_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
     2.3 @@ -0,0 +1,13 @@
     2.4 +%ID: $Id$
     2.5 +%Author: Jia Meng, NICTA
     2.6 +%const-typed combinator reduction for B, C
     2.7 +
     2.8 +%B P Q R --> P(Q R)
     2.9 +input_clause(a4,axiom,
    2.10 +[++equal(hAPP(hAPP(hAPP(c_COMBB(A,B,C),P),Q),R),hAPP(P,hAPP(Q,R)))]).
    2.11 +
    2.12 +
    2.13 +%C P Q R --> P R Q
    2.14 +input_clause(a5,axiom,
    2.15 +[++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]).
    2.16 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
     3.3 @@ -0,0 +1,13 @@
     3.4 +%ID: $Id$
     3.5 +%Author: Jia Meng, NICTA
     3.6 +%const-typed combinator reduction for B', C'
     3.7 +
     3.8 +clause(
     3.9 +forall([A, B, C, F, G, U, V, X],
    3.10 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
    3.11 +a6 ).
    3.12 +
    3.13 +clause(
    3.14 +forall([A, B, C, F, G, U, V, X],
    3.15 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
    3.16 +a7 ).
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
     4.3 @@ -0,0 +1,13 @@
     4.4 +%ID: $Id$
     4.5 +%Author: Jia Meng, NICTA
     4.6 +%const-typed combinator reduction for B', C'
     4.7 +
     4.8 +%B' c f g x -->  c (f (g x))
     4.9 +input_clause(a6,axiom,
    4.10 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
    4.11 +
    4.12 +%C' c f g x --> c (f x) g
    4.13 +input_clause(a7,axiom,
    4.14 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
    4.15 +
    4.16 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/atp-inputs/const_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
     5.3 @@ -0,0 +1,14 @@
     5.4 +%ID: $Id$
     5.5 +%Author: Jia Meng, NICTA
     5.6 +%const-typed combinator reduction for I, K
     5.7 +
     5.8 +clause(
     5.9 +forall([A, B, P, Q],
    5.10 +or( equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P))),
    5.11 +a1 ).
    5.12 +
    5.13 +clause(
    5.14 +forall([P, T],
    5.15 +or( equal(hAPP(c_COMBI(T),P),P))),
    5.16 +a3 ).
    5.17 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/atp-inputs/const_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
     6.3 @@ -0,0 +1,12 @@
     6.4 +%ID: $Id$
     6.5 +%Author: Jia Meng, NICTA
     6.6 +%const-typed combinator reduction for I, K
     6.7 +
     6.8 +%K P Q --> P
     6.9 +input_clause(a1,axiom,
    6.10 +[++equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P)]).
    6.11 +
    6.12 +%I P --> P
    6.13 +input_clause(a3,axiom,
    6.14 +[++equal(hAPP(c_COMBI(T),P),P)]).
    6.15 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/atp-inputs/const_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
     7.3 @@ -0,0 +1,9 @@
     7.4 +%ID: $Id$
     7.5 +%Author: Jia Meng, NICTA
     7.6 +%const-typed combinator reduction for S
     7.7 +
     7.8 +clause(
     7.9 +forall([A, B, C, P, Q, R],
    7.10 +or( equal(hAPP(hAPP(hAPP(c_COMBS(A,B,C),P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
    7.11 +a2 ).
    7.12 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/atp-inputs/const_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
     8.3 @@ -0,0 +1,7 @@
     8.4 +%ID: $Id$
     8.5 +%Author: Jia Meng, NICTA
     8.6 +%const-typed combinator reduction for S
     8.7 +
     8.8 +%S P Q R --> P R (Q R)
     8.9 +input_clause(a2,axiom,
    8.10 +[++equal(hAPP(hAPP(hAPP(c_COMBS(A,B,C),P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R)))]).
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
     9.3 @@ -0,0 +1,8 @@
     9.4 +%ID: $Id$
     9.5 +%Author: Jia Meng, NICTA
     9.6 +%const-typed combinator reduction for S'
     9.7 +
     9.8 +clause(
     9.9 +forall([A, B, C, F, G, U, V, X],
    9.10 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
    9.11 +a8 ).
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    10.3 @@ -0,0 +1,7 @@
    10.4 +%ID: $Id$
    10.5 +%Author: Jia Meng, NICTA
    10.6 +%const-typed combinator reduction for S'
    10.7 +
    10.8 +%S' c f g x --> c (f x) (g x)
    10.9 +input_clause(a8,axiom,
   10.10 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/atp-inputs/full_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
    11.3 @@ -0,0 +1,14 @@
    11.4 +%ID: $Id$
    11.5 +%Author: Jia Meng, NICTA
    11.6 +%full-typed combinator reduction for B, C
    11.7 +
    11.8 +clause(
    11.9 +forall([A, B, C, P, Q, R],
   11.10 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),typeinfo(P,tc_fun(A,B))),tc_fun(tc_fun(C,A),tc_fun(C,B))),typeinfo(Q,tc_fun(C,A))),tc_fun(C,B)),typeinfo(R,C)),B),typeinfo(hAPP(typeinfo(P,tc_fun(A,B)),typeinfo(hAPP(typeinfo(Q,tc_fun(C,A)),typeinfo(R,C)),A)),B)))),
   11.11 +a4 ).
   11.12 +
   11.13 +clause(
   11.14 +forall([A, B, C, P, Q, R],
   11.15 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C)))),
   11.16 +a5 ).
   11.17 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/atp-inputs/full_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
    12.3 @@ -0,0 +1,11 @@
    12.4 +%ID: $Id$
    12.5 +%Author: Jia Meng, NICTA
    12.6 +%full-typed combinator reduction for B, C
    12.7 +
    12.8 +%B P Q R --> P(Q R)
    12.9 +input_clause(a4,axiom,
   12.10 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),typeinfo(P,tc_fun(A,B))),tc_fun(tc_fun(C,A),tc_fun(C,B))),typeinfo(Q,tc_fun(C,A))),tc_fun(C,B)),typeinfo(R,C)),B),typeinfo(hAPP(typeinfo(P,tc_fun(A,B)),typeinfo(hAPP(typeinfo(Q,tc_fun(C,A)),typeinfo(R,C)),A)),B))]).
   12.11 +
   12.12 +%C P Q R --> P R Q
   12.13 +input_clause(a5,axiom,
   12.14 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C))]).
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
    13.3 @@ -0,0 +1,13 @@
    13.4 +%ID: $Id$
    13.5 +%Author: Jia Meng, NICTA
    13.6 +%full-typed combinator reduction for B', C'
    13.7 +
    13.8 +clause(
    13.9 +forall([A, B, C, F, G, U, V, X],
   13.10 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B)))),
   13.11 +a6 ).
   13.12 +
   13.13 +clause(
   13.14 +forall([A, B, C, F, G, U, V, X],
   13.15 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U)))),
   13.16 +a7 ).
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    14.3 @@ -0,0 +1,12 @@
    14.4 +%ID: $Id$
    14.5 +%Author: Jia Meng, NICTA
    14.6 +%full-typed combinator reduction for B', C'
    14.7 +
    14.8 +%B' c f g x -->  c (f (g x))
    14.9 +input_clause(a6,axiom,
   14.10 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B))]).
   14.11 +
   14.12 +
   14.13 +%C' c f g x --> c (f x) g
   14.14 +input_clause(a7,axiom,
   14.15 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U))]).
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Tools/atp-inputs/full_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
    15.3 @@ -0,0 +1,13 @@
    15.4 +%ID: $Id$
    15.5 +%Author: Jia Meng, NICTA
    15.6 +%full-typed combinator reduction for I, K
    15.7 +
    15.8 +clause(
    15.9 +forall([A, B, P, Q],
   15.10 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A)))),
   15.11 +a1 ).
   15.12 +
   15.13 +clause(
   15.14 +forall([P, T],
   15.15 +or( equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T)))),
   15.16 +a3 ).
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Tools/atp-inputs/full_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
    16.3 @@ -0,0 +1,11 @@
    16.4 +%ID: $Id$
    16.5 +%Author: Jia Meng, NICTA
    16.6 +%full-typed combinator reduction for I, K
    16.7 +
    16.8 +%K P Q --> P
    16.9 +input_clause(a1,axiom,
   16.10 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A))]).
   16.11 +
   16.12 +%I P --> P
   16.13 +input_clause(a3,axiom,
   16.14 +[++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]).
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Tools/atp-inputs/full_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
    17.3 @@ -0,0 +1,8 @@
    17.4 +%ID: $Id$
    17.5 +%Author: Jia Meng, NICTA
    17.6 +%full-typed combinator reduction for S
    17.7 +
    17.8 +clause(
    17.9 +forall([A, B, C, P, Q, R],
   17.10 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(tc_fun(A,B),tc_fun(A,C))),typeinfo(Q,tc_fun(A,B))),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(hAPP(typeinfo(Q,tc_fun(A,B)),typeinfo(R,A)),B)),C)))),
   17.11 +a2 ).
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/Tools/atp-inputs/full_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
    18.3 @@ -0,0 +1,7 @@
    18.4 +%ID: $Id$
    18.5 +%Author: Jia Meng, NICTA
    18.6 +%full-typed combinator reduction for S
    18.7 +
    18.8 +%S P Q R --> P R (Q R)
    18.9 +input_clause(a2,axiom,
   18.10 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(tc_fun(A,B),tc_fun(A,C))),typeinfo(Q,tc_fun(A,B))),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(hAPP(typeinfo(Q,tc_fun(A,B)),typeinfo(R,A)),B)),C))]).
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
    19.3 @@ -0,0 +1,9 @@
    19.4 +%ID: $Id$
    19.5 +%Author: Jia Meng, NICTA
    19.6 +%full-typed combinator reduction for S'
    19.7 +
    19.8 +clause(
    19.9 +forall([A, B, C, F, G, U, V, X],
   19.10 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U)))),
   19.11 +a8 ).
   19.12 +
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    20.3 @@ -0,0 +1,8 @@
    20.4 +%ID: $Id$
    20.5 +%Author: Jia Meng, NICTA
    20.6 +%full-typed combinator reduction for S'
    20.7 +
    20.8 +
    20.9 +%S' c f g x --> c (f x) (g x)
   20.10 +input_clause(a8,axiom,
   20.11 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U))]).
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/Tools/atp-inputs/par_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
    21.3 @@ -0,0 +1,13 @@
    21.4 +%ID: $Id$
    21.5 +%Author: Jia Meng, NICTA
    21.6 +%partial-typed combinator reduction for B, C
    21.7 +
    21.8 +clause(
    21.9 +forall([A, B, C, P, Q, R],
   21.10 +or( equal(hAPP(hAPP(hAPP(c_COMBB,P,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),Q,tc_fun(tc_fun(C,A),tc_fun(C,B))),R,tc_fun(C,B)),hAPP(P,hAPP(Q,R,tc_fun(C,A)),tc_fun(A,B))))),
   21.11 +a4 ).
   21.12 +
   21.13 +clause(
   21.14 +forall([A, B, C, P, Q, R],
   21.15 +or( equal(hAPP(hAPP(hAPP(c_COMBC,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),Q,tc_fun(B,tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),Q,tc_fun(B,C))))),
   21.16 +a5 ).
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/Tools/atp-inputs/par_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
    22.3 @@ -0,0 +1,12 @@
    22.4 +%ID: $Id$
    22.5 +%Author: Jia Meng, NICTA
    22.6 +%partial-typed combinator reduction for B, C
    22.7 +
    22.8 +%B P Q R --> P(Q R)
    22.9 +input_clause(a4,axiom,
   22.10 +[++equal(hAPP(hAPP(hAPP(c_COMBB,P,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),Q,tc_fun(tc_fun(C,A),tc_fun(C,B))),R,tc_fun(C,B)),hAPP(P,hAPP(Q,R,tc_fun(C,A)),tc_fun(A,B)))]).
   22.11 +
   22.12 +
   22.13 +%C P Q R --> P R Q
   22.14 +input_clause(a5,axiom,
   22.15 +[++equal(hAPP(hAPP(hAPP(c_COMBC,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),Q,tc_fun(B,tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),Q,tc_fun(B,C)))]).
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
    23.3 @@ -0,0 +1,13 @@
    23.4 +%ID: $Id$
    23.5 +%Author: Jia Meng, NICTA
    23.6 +%partial-typed combinator reduction for B', C'
    23.7 +
    23.8 +clause(
    23.9 +forall([A, B, C, F, G, U, V, X],
   23.10 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B))))),
   23.11 +a6 ).
   23.12 +
   23.13 +clause(
   23.14 +forall([A, B, C, F, G, U, V, X],
   23.15 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U))))),
   23.16 +a7 ).
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    24.3 @@ -0,0 +1,11 @@
    24.4 +%ID: $Id$
    24.5 +%Author: Jia Meng, NICTA
    24.6 +%partial-typed combinator reduction for B', C'
    24.7 +
    24.8 +%B' c f g x -->  c (f (g x))
    24.9 +input_clause(a6,axiom,
   24.10 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B)))]).
   24.11 +
   24.12 +%C' c f g x --> c (f x) g
   24.13 +input_clause(a7,axiom,
   24.14 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U)))]).
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/HOL/Tools/atp-inputs/par_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
    25.3 @@ -0,0 +1,13 @@
    25.4 +%ID: $Id$
    25.5 +%Author: Jia Meng, NICTA
    25.6 +%partial-typed combinator reduction for I, K
    25.7 +
    25.8 +clause(
    25.9 +forall([A, B, P, Q],
   25.10 +or( equal(hAPP(hAPP(c_COMBK,P,tc_fun(A,tc_fun(B,A))),Q,tc_fun(B,A)),P))),
   25.11 +a1 ).
   25.12 +
   25.13 +clause(
   25.14 +forall([P, T],
   25.15 +or( equal(hAPP(c_COMBI,P,tc_fun(T,T)),P))),
   25.16 +a3 ).
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/HOL/Tools/atp-inputs/par_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
    26.3 @@ -0,0 +1,12 @@
    26.4 +%ID: $Id$
    26.5 +%Author: Jia Meng, NICTA
    26.6 +%partial-typed combinator reduction for I, K
    26.7 +
    26.8 +%K P Q --> P
    26.9 +input_clause(a1,axiom,
   26.10 +[++equal(hAPP(hAPP(c_COMBK,P,tc_fun(A,tc_fun(B,A))),Q,tc_fun(B,A)),P)]).
   26.11 +
   26.12 +%I P --> P
   26.13 +input_clause(a3,axiom,
   26.14 +[++equal(hAPP(c_COMBI,P,tc_fun(T,T)),P)]).
   26.15 +
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/HOL/Tools/atp-inputs/par_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
    27.3 @@ -0,0 +1,8 @@
    27.4 +%ID: $Id$
    27.5 +%Author: Jia Meng, NICTA
    27.6 +%partial-typed combinator reduction for S
    27.7 +
    27.8 +clause(
    27.9 +forall([A, B, C, P, Q, R],
   27.10 +or( equal(hAPP(hAPP(hAPP(c_COMBS,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),Q,tc_fun(tc_fun(A,B),tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),hAPP(Q,R,tc_fun(A,B)),tc_fun(B,C))))),
   27.11 +a2 ).
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/HOL/Tools/atp-inputs/par_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
    28.3 @@ -0,0 +1,8 @@
    28.4 +%ID: $Id$
    28.5 +%Author: Jia Meng, NICTA
    28.6 +%partial-typed combinator reduction for S
    28.7 +
    28.8 +%S P Q R --> P R (Q R)
    28.9 +input_clause(a2,axiom,
   28.10 +[++equal(hAPP(hAPP(hAPP(c_COMBS,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),Q,tc_fun(tc_fun(A,B),tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),hAPP(Q,R,tc_fun(A,B)),tc_fun(B,C)))]).
   28.11 +
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
    29.3 @@ -0,0 +1,8 @@
    29.4 +%ID: $Id$
    29.5 +%Author: Jia Meng, NICTA
    29.6 +%partial-typed combinator reduction for S'
    29.7 +
    29.8 +clause(
    29.9 +forall([A, B, C, F, G, U, V, X],
   29.10 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U))))),
   29.11 +a8 ).
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    30.3 @@ -0,0 +1,8 @@
    30.4 +%ID: $Id$
    30.5 +%Author: Jia Meng, NICTA
    30.6 +%partial-typed combinator reduction for S'
    30.7 +
    30.8 +%S' c f g x --> c (f x) (g x)
    30.9 +input_clause(a8,axiom,
   30.10 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U)))]).
   30.11 +
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/HOL/Tools/atp-inputs/u_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
    31.3 @@ -0,0 +1,14 @@
    31.4 +%ID: $Id$
    31.5 +%Author: Jia Meng, NICTA
    31.6 +%untyped combinator reduction for B, C
    31.7 +
    31.8 +clause(
    31.9 +forall([P, Q, R],
   31.10 +or( equal(hAPP(hAPP(hAPP(c_COMBB,P),Q),R),hAPP(P,hAPP(Q,R))))),
   31.11 +a4 ).
   31.12 +
   31.13 +clause(
   31.14 +forall([P, Q, R],
   31.15 +or( equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q)))),
   31.16 +a5 ).
   31.17 +
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/HOL/Tools/atp-inputs/u_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
    32.3 @@ -0,0 +1,11 @@
    32.4 +%ID: $Id$
    32.5 +%Author: Jia Meng, NICTA
    32.6 +%untyped combinator reduction for B, C
    32.7 +
    32.8 +%B P Q R --> P(Q R)
    32.9 +input_clause(a4,axiom,
   32.10 +[++equal(hAPP(hAPP(hAPP(c_COMBB,P),Q),R),hAPP(P,hAPP(Q,R)))]).
   32.11 +
   32.12 +%C P Q R --> P R Q
   32.13 +input_clause(a5,axiom,
   32.14 +[++equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q))]).
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
    33.3 @@ -0,0 +1,13 @@
    33.4 +%ID: $Id$
    33.5 +%Author: Jia Meng, NICTA
    33.6 +%untyped combinator reduction for B', C'
    33.7 +
    33.8 +clause(
    33.9 +forall([C, F, G, X],
   33.10 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
   33.11 +a6 ).
   33.12 +
   33.13 +clause(
   33.14 +forall([C, F, G, X],
   33.15 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
   33.16 +a7 ).
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    34.3 @@ -0,0 +1,11 @@
    34.4 +%ID: $Id$
    34.5 +%Author: Jia Meng, NICTA
    34.6 +%untyped combinator reduction for B', C'
    34.7 +
    34.8 +%B' c f g x -->  c (f (g x))
    34.9 +input_clause(a6,axiom,
   34.10 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
   34.11 +
   34.12 +%C' c f g x --> c (f x) g
   34.13 +input_clause(a7,axiom,
   34.14 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
    35.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.2 +++ b/src/HOL/Tools/atp-inputs/u_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
    35.3 @@ -0,0 +1,14 @@
    35.4 +%ID: $Id$
    35.5 +%Author: Jia Meng, NICTA
    35.6 +%untyped combinator reduction for I, K
    35.7 +
    35.8 +clause(
    35.9 +forall([P, Q],
   35.10 +or( equal(hAPP(hAPP(c_COMBK,P),Q),P))),
   35.11 +a1 ).
   35.12 +
   35.13 +clause(
   35.14 +forall([P],
   35.15 +or( equal(hAPP(c_COMBI,P),P))),
   35.16 +a3 ).
   35.17 +
    36.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    36.2 +++ b/src/HOL/Tools/atp-inputs/u_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
    36.3 @@ -0,0 +1,11 @@
    36.4 +%ID: $Id$
    36.5 +%Author: Jia Meng, NICTA
    36.6 +%untyped combinator reduction for I, K
    36.7 +
    36.8 +%K
    36.9 +input_clause(a1,axiom,
   36.10 +[++equal(hAPP(hAPP(c_COMBK,P),Q),P)]).
   36.11 +
   36.12 +%I
   36.13 +input_clause(a3,axiom,
   36.14 +[++equal(hAPP(c_COMBI,P),P)]).
    37.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.2 +++ b/src/HOL/Tools/atp-inputs/u_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
    37.3 @@ -0,0 +1,9 @@
    37.4 +%ID: $Id$
    37.5 +%Author: Jia Meng, NICTA
    37.6 +%untyped combinator reduction for S
    37.7 +
    37.8 +clause(
    37.9 +forall([P, Q, R],
   37.10 +or( equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
   37.11 +a2 ).
   37.12 +
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/src/HOL/Tools/atp-inputs/u_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
    38.3 @@ -0,0 +1,8 @@
    38.4 +%ID: $Id$
    38.5 +%Author: Jia Meng, NICTA
    38.6 +%untyped combinator reduction for S
    38.7 +
    38.8 +%S P Q R
    38.9 +input_clause(a2,axiom,
   38.10 +[++equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R)))]).
   38.11 +
    39.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    39.2 +++ b/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
    39.3 @@ -0,0 +1,8 @@
    39.4 +%ID: $Id$
    39.5 +%Author: Jia Meng, NICTA
    39.6 +%untyped combinator reduction for S'
    39.7 +
    39.8 +clause(
    39.9 +forall([C, F, G, X],
   39.10 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
   39.11 +a8 ).
    40.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    40.2 +++ b/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
    40.3 @@ -0,0 +1,7 @@
    40.4 +%ID: $Id$
    40.5 +%Author: Jia Meng, NICTA
    40.6 +%untyped combinator reduction for S'
    40.7 +
    40.8 +%S' c f g x --> c (f x) (g x)
    40.9 +input_clause(a8,axiom,
   40.10 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).