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'.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for B, C
+
+clause(
+forall([A, B, C, P, Q, R],
+or( equal(hAPP(hAPP(hAPP(c_COMBB(A,B,C),P),Q),R),hAPP(P,hAPP(Q,R))))),
+a4 ).
+
+clause(
+forall([A, B, C, P, Q, R],
+or( equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q)))),
+a5 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for B, C
+
+%B P Q R --> P(Q R)
+input_clause(a4,axiom,
+[++equal(hAPP(hAPP(hAPP(c_COMBB(A,B,C),P),Q),R),hAPP(P,hAPP(Q,R)))]).
+
+
+%C P Q R --> P R Q
+input_clause(a5,axiom,
+[++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for B', C'
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
+a6 ).
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
+a7 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for B', C'
+
+%B' c f g x -->  c (f (g x))
+input_clause(a6,axiom,
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
+
+%C' c f g x --> c (f x) g
+input_clause(a7,axiom,
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,14 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for I, K
+
+clause(
+forall([A, B, P, Q],
+or( equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P))),
+a1 ).
+
+clause(
+forall([P, T],
+or( equal(hAPP(c_COMBI(T),P),P))),
+a3 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,12 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for I, K
+
+%K P Q --> P
+input_clause(a1,axiom,
+[++equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P)]).
+
+%I P --> P
+input_clause(a3,axiom,
+[++equal(hAPP(c_COMBI(T),P),P)]).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,9 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for S
+
+clause(
+forall([A, B, C, P, Q, R],
+or( equal(hAPP(hAPP(hAPP(c_COMBS(A,B,C),P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
+a2 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,7 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for S
+
+%S P Q R --> P R (Q R)
+input_clause(a2,axiom,
+[++equal(hAPP(hAPP(hAPP(c_COMBS(A,B,C),P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R)))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for S'
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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))))),
+a8 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,7 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%const-typed combinator reduction for S'
+
+%S' c f g x --> c (f x) (g x)
+input_clause(a8,axiom,
+[++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)))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,14 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for B, C
+
+clause(
+forall([A, B, C, P, Q, R],
+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)))),
+a4 ).
+
+clause(
+forall([A, B, C, P, Q, R],
+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)))),
+a5 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,11 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for B, C
+
+%B P Q R --> P(Q R)
+input_clause(a4,axiom,
+[++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))]).
+
+%C P Q R --> P R Q
+input_clause(a5,axiom,
+[++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))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for B', C'
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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)))),
+a6 ).
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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)))),
+a7 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,12 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for B', C'
+
+%B' c f g x -->  c (f (g x))
+input_clause(a6,axiom,
+[++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))]).
+
+
+%C' c f g x --> c (f x) g
+input_clause(a7,axiom,
+[++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))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for I, K
+
+clause(
+forall([A, B, P, Q],
+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)))),
+a1 ).
+
+clause(
+forall([P, T],
+or( equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T)))),
+a3 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,11 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for I, K
+
+%K P Q --> P
+input_clause(a1,axiom,
+[++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))]).
+
+%I P --> P
+input_clause(a3,axiom,
+[++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for S
+
+clause(
+forall([A, B, C, P, Q, R],
+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)))),
+a2 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,7 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for S
+
+%S P Q R --> P R (Q R)
+input_clause(a2,axiom,
+[++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))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,9 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for S'
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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)))),
+a8 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%full-typed combinator reduction for S'
+
+
+%S' c f g x --> c (f x) (g x)
+input_clause(a8,axiom,
+[++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))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for B, C
+
+clause(
+forall([A, B, C, P, Q, R],
+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))))),
+a4 ).
+
+clause(
+forall([A, B, C, P, Q, R],
+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))))),
+a5 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,12 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for B, C
+
+%B P Q R --> P(Q R)
+input_clause(a4,axiom,
+[++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)))]).
+
+
+%C P Q R --> P R Q
+input_clause(a5,axiom,
+[++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)))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for B', C'
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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))))),
+a6 ).
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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))))),
+a7 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,11 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for B', C'
+
+%B' c f g x -->  c (f (g x))
+input_clause(a6,axiom,
+[++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)))]).
+
+%C' c f g x --> c (f x) g
+input_clause(a7,axiom,
+[++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)))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for I, K
+
+clause(
+forall([A, B, P, Q],
+or( equal(hAPP(hAPP(c_COMBK,P,tc_fun(A,tc_fun(B,A))),Q,tc_fun(B,A)),P))),
+a1 ).
+
+clause(
+forall([P, T],
+or( equal(hAPP(c_COMBI,P,tc_fun(T,T)),P))),
+a3 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,12 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for I, K
+
+%K P Q --> P
+input_clause(a1,axiom,
+[++equal(hAPP(hAPP(c_COMBK,P,tc_fun(A,tc_fun(B,A))),Q,tc_fun(B,A)),P)]).
+
+%I P --> P
+input_clause(a3,axiom,
+[++equal(hAPP(c_COMBI,P,tc_fun(T,T)),P)]).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for S
+
+clause(
+forall([A, B, C, P, Q, R],
+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))))),
+a2 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for S
+
+%S P Q R --> P R (Q R)
+input_clause(a2,axiom,
+[++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)))]).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for S'
+
+clause(
+forall([A, B, C, F, G, U, V, X],
+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))))),
+a8 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%partial-typed combinator reduction for S'
+
+%S' c f g x --> c (f x) (g x)
+input_clause(a8,axiom,
+[++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)))]).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combBC.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,14 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for B, C
+
+clause(
+forall([P, Q, R],
+or( equal(hAPP(hAPP(hAPP(c_COMBB,P),Q),R),hAPP(P,hAPP(Q,R))))),
+a4 ).
+
+clause(
+forall([P, Q, R],
+or( equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q)))),
+a5 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combBC.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,11 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for B, C
+
+%B P Q R --> P(Q R)
+input_clause(a4,axiom,
+[++equal(hAPP(hAPP(hAPP(c_COMBB,P),Q),R),hAPP(P,hAPP(Q,R)))]).
+
+%C P Q R --> P R Q
+input_clause(a5,axiom,
+[++equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,13 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for B', C'
+
+clause(
+forall([C, F, G, X],
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
+a6 ).
+
+clause(
+forall([C, F, G, X],
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
+a7 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,11 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for B', C'
+
+%B' c f g x -->  c (f (g x))
+input_clause(a6,axiom,
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
+
+%C' c f g x --> c (f x) g
+input_clause(a7,axiom,
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combIK.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,14 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for I, K
+
+clause(
+forall([P, Q],
+or( equal(hAPP(hAPP(c_COMBK,P),Q),P))),
+a1 ).
+
+clause(
+forall([P],
+or( equal(hAPP(c_COMBI,P),P))),
+a3 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combIK.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,11 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for I, K
+
+%K
+input_clause(a1,axiom,
+[++equal(hAPP(hAPP(c_COMBK,P),Q),P)]).
+
+%I
+input_clause(a3,axiom,
+[++equal(hAPP(c_COMBI,P),P)]).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combS.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,9 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for S
+
+clause(
+forall([P, Q, R],
+or( equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
+a2 ).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combS.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for S
+
+%S P Q R
+input_clause(a2,axiom,
+[++equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R)))]).
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,8 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for S'
+
+clause(
+forall([C, F, G, X],
+or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
+a8 ).

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Wed Sep 20 14:02:41 2006 +0200
@@ -0,0 +1,7 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%untyped combinator reduction for S'
+
+%S' c f g x --> c (f x) (g x)
+input_clause(a8,axiom,
+[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).