# HG changeset patch
# User mengj
# Date 1159697277 -7200
# Node ID 3728dba101f19c961e4f6bda5878f93859b59384
# Parent  35574b9b59aa3b7bbc308cca8c09b631793bf23d
Removed the helper files (combinator rewrite rules, function extensionality and fequal rules).

diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combBC.dfg
--- a/src/HOL/Tools/atp-inputs/const_combBC.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combBC.tptp
--- a/src/HOL/Tools/atp-inputs/const_combBC.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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))]).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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))]).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combIK.dfg
--- a/src/HOL/Tools/atp-inputs/const_combIK.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combIK.tptp
--- a/src/HOL/Tools/atp-inputs/const_combIK.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-%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)]).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combS.dfg
--- a/src/HOL/Tools/atp-inputs/const_combS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combS.tptp
--- a/src/HOL/Tools/atp-inputs/const_combS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-%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)))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-%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)))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_comb_inclS.dfg
--- a/src/HOL/Tools/atp-inputs/const_comb_inclS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for const-types-only (include S)
-
-clause(
-forall([A, B, P, Q],
-or( equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P))),
-a1 ).
-
-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 ).
-
-clause(
-forall([P, T],
-or( equal(hAPP(c_COMBI(T),P),P))),
-a3 ).
-
-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 ).
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
-    equal(X,Y))),
-a6 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_comb_inclS.tptp
--- a/src/HOL/Tools/atp-inputs/const_comb_inclS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for const-types-only (include S)
-
-%K P Q --> P
-input_clause(a1,axiom,
-[++equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P)]).
-
-%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)))]).
-
-
-%I P --> P
-input_clause(a3,axiom,
-[++equal(hAPP(c_COMBI(T),P),P)]).
-
-%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))]).
-
-input_clause(a6,axiom,
-[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
-
-input_clause(a7,axiom,
-[++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).
-
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_comb_noS.dfg
--- a/src/HOL/Tools/atp-inputs/const_comb_noS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for const-types-only (no S)
-
-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 ).
-
-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 ).
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
-    equal(X,Y))),
-a6 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
-a7 ).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_comb_noS.tptp
--- a/src/HOL/Tools/atp-inputs/const_comb_noS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for const-types-only (no S)
-
-%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)]).
-
-%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))]).
-
-input_clause(a6,axiom,
-[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
-
-input_clause(a7,axiom,
-[++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).
-
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/const_helper1.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality for const-types-only
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
-    equal(X,Y))),
-a9 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
-a10 ).
-
-clause(
-forall([A, B, F, G],
-or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G)))),
-    equal(F,G))),
-a11 ).
\ No newline at end of file
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/const_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/const_helper1.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality for const-types-only
-
-input_clause(a9,axiom,
-[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
-
-input_clause(a10,axiom,
-[++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).
-
-input_clause(a11,axiom,
-[--equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G))),
-++equal(F,G)]).
-
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combBC.dfg
--- a/src/HOL/Tools/atp-inputs/full_combBC.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combBC.tptp
--- a/src/HOL/Tools/atp-inputs/full_combBC.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combIK.dfg
--- a/src/HOL/Tools/atp-inputs/full_combIK.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combIK.tptp
--- a/src/HOL/Tools/atp-inputs/full_combIK.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combS.dfg
--- a/src/HOL/Tools/atp-inputs/full_combS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combS.tptp
--- a/src/HOL/Tools/atp-inputs/full_combS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_comb_inclS.dfg
--- a/src/HOL/Tools/atp-inputs/full_comb_inclS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for full-types (include S)
-
-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([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 ).
-
-clause(
-forall([P, T],
-or( equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T)))),
-a3 ).
-
-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 ).
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))),
-    equal(typeinfo(X,A),typeinfo(Y,A)))),
-a6 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
-    hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_comb_inclS.tptp
--- a/src/HOL/Tools/atp-inputs/full_comb_inclS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for full-types (include S)
-
-%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))]).
-
-%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))]).
-
-%I P --> P
-input_clause(a3,axiom,
-[++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]).
-
-%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))]).
-
-input_clause(a6,axiom,
-[--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
-++equal(typeinfo(X,A),typeinfo(Y,A))]).
-
-input_clause(a7,axiom,
-[++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
---equal(typeinfo(X,A),typeinfo(Y,A))]).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_comb_noS.dfg
--- a/src/HOL/Tools/atp-inputs/full_comb_noS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for full-types (no S)
-
-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 ).
-
-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 ).
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))),
-    equal(typeinfo(X,A),typeinfo(Y,A)))),
-a6 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
-    hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_comb_noS.tptp
--- a/src/HOL/Tools/atp-inputs/full_comb_noS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for full-types (no S)
-
-%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))]).
-
-%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))]).
-
-input_clause(a6,axiom,
-[--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
-++equal(typeinfo(X,A),typeinfo(Y,A))]).
-
-input_clause(a7,axiom,
-[++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
---equal(typeinfo(X,A),typeinfo(Y,A))]).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/full_helper1.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality for full-types
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))),
-    equal(typeinfo(X,A),typeinfo(Y,A)))),
-a9 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
-    hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))),
-a10 ).
-
-clause(
-forall([A, B, F, G],
-or( not(equal(typeinfo(hAPP(typeinfo(F,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B),typeinfo(hAPP(typeinfo(G,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B))),
-    equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B))))),
-a11 ).
\ No newline at end of file
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/full_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/full_helper1.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality for full-types
-
-input_clause(a9,axiom,
-[--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
-++equal(typeinfo(X,A),typeinfo(Y,A))]).
-
-input_clause(a10,axiom,
-[++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
---equal(typeinfo(X,A),typeinfo(Y,A))]).
-
-input_clause(a11,axiom,
-[--equal(typeinfo(hAPP(typeinfo(F,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B),typeinfo(hAPP(typeinfo(G,tc_fun(A,B)),typeinfo(hAPP(typeinfo(hAPP(typeinfo(hEXTENT,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),typeinfo(F,tc_fun(A,B))),tc_fun(tc_fun(A,B),A)),typeinfo(G,tc_fun(A,B))),A)),B)),
-++equal(typeinfo(F,tc_fun(A,B)),typeinfo(G,tc_fun(A,B)))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combBC.dfg
--- a/src/HOL/Tools/atp-inputs/par_combBC.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combBC.tptp
--- a/src/HOL/Tools/atp-inputs/par_combBC.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-%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)))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%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)))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combIK.dfg
--- a/src/HOL/Tools/atp-inputs/par_combIK.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combIK.tptp
--- a/src/HOL/Tools/atp-inputs/par_combIK.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-%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)]).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combS.dfg
--- a/src/HOL/Tools/atp-inputs/par_combS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combS.tptp
--- a/src/HOL/Tools/atp-inputs/par_combS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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)))]).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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)))]).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_comb_inclS.dfg
--- a/src/HOL/Tools/atp-inputs/par_comb_inclS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for partial-types (include S)
-
-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([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 ).
-
-clause(
-forall([P, T],
-or( equal(hAPP(c_COMBI,P,tc_fun(T,T)),P))),
-a3 ).
-
-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 ).
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))),
-    equal(X,Y))),
-a6 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_comb_inclS.tptp
--- a/src/HOL/Tools/atp-inputs/par_comb_inclS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for partial-types (include S)
-
-%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)]).
-
-
-%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)))]).
-
-%I P --> P
-input_clause(a3,axiom,
-[++equal(hAPP(c_COMBI,P,tc_fun(T,T)),P)]).
-
-
-%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)))]).
-
-input_clause(a6,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
-++equal(X,Y)]).
-
-input_clause(a7,axiom,
-[++hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
---equal(X,Y)]).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_comb_noS.dfg
--- a/src/HOL/Tools/atp-inputs/par_comb_noS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for partial-types (no S)
-
-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 ).
-
-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 ).
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))),
-    equal(X,Y))),
-a6 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_comb_noS.tptp
--- a/src/HOL/Tools/atp-inputs/par_comb_noS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%typed combinator reduction for partial-types (no S)
-
-%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)]).
-
-
-%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)))]).
-
-input_clause(a6,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
-++equal(X,Y)]).
-
-input_clause(a7,axiom,
-[++hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
---equal(X,Y)]).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/par_helper1.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality for partial types
-
-clause(
-forall([A, X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))),
-    equal(X,Y))),
-a9 ).
-
-clause(
-forall([A, X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))),
-a10 ).
-
-clause(
-forall([A, B, F, G],
-or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)))),
-    equal(F,G))),
-a11 ).
\ No newline at end of file
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/par_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/par_helper1.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality for partial types
-
-input_clause(a9,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
-++equal(X,Y)]).
-
-input_clause(a10,axiom,
-[++hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
---equal(X,Y)]).
-
-input_clause(a11,axiom,
-[--equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B))),
-++equal(F,G)]).
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combBC.dfg
--- a/src/HOL/Tools/atp-inputs/u_combBC.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combBC.tptp
--- a/src/HOL/Tools/atp-inputs/u_combBC.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combBC_e.dfg
--- a/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combBC_e.tptp
--- a/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%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))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combIK.dfg
--- a/src/HOL/Tools/atp-inputs/u_combIK.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combIK.tptp
--- a/src/HOL/Tools/atp-inputs/u_combIK.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%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)]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combS.dfg
--- a/src/HOL/Tools/atp-inputs/u_combS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%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 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combS.tptp
--- a/src/HOL/Tools/atp-inputs/u_combS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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)))]).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combS_e.dfg
--- a/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%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 ).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_combS_e.tptp
--- a/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-%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)))]).
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_comb_inclS.dfg
--- a/src/HOL/Tools/atp-inputs/u_comb_inclS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%untyped combinator reduction (include S)
-
-clause(
-forall([P, Q],
-or( equal(hAPP(hAPP(c_COMBK,P),Q),P))),
-a1 ).
-
-clause(
-forall([P, Q, R],
-or( equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
-a2 ).
-
-clause(
-forall([P],
-or( equal(hAPP(c_COMBI,P),P))),
-a3 ).
-
-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 ).
-
-clause(
-forall([X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
-    equal(X,Y))),
-a6 ).
-
-clause(
-forall([X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal,X),Y)))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_comb_inclS.tptp
--- a/src/HOL/Tools/atp-inputs/u_comb_inclS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%untyped combinator reduction (include S)
-
-input_clause(a1,axiom,
-[++equal(hAPP(hAPP(c_COMBK,P),Q),P)]).
-
-%S P Q R
-input_clause(a2,axiom,
-[++equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R)))]).
-
-input_clause(a3,axiom,
-[++equal(hAPP(c_COMBI,P),P)]).
-
-%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))]).
-
-input_clause(a6,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
-
-input_clause(a7,axiom,
-[++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
-
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_comb_noS.dfg
--- a/src/HOL/Tools/atp-inputs/u_comb_noS.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%untyped combinator reduction (no S)
-
-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 ).
-
-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 ).
-
-clause(
-forall([X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
-    equal(X,Y))),
-a6 ).
-
-clause(
-forall([X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal,X),Y)))),
-a7 ).
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_comb_noS.tptp
--- a/src/HOL/Tools/atp-inputs/u_comb_noS.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%untyped combinator reduction (no S)
-
-input_clause(a1,axiom,
-[++equal(hAPP(hAPP(c_COMBK,P),Q),P)]).
-
-input_clause(a3,axiom,
-[++equal(hAPP(c_COMBI,P),P)]).
-
-%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))]).
-
-input_clause(a6,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
-
-input_clause(a7,axiom,
-[++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
-
-
-
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_helper1.dfg
--- a/src/HOL/Tools/atp-inputs/u_helper1.dfg	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality, untyped
-
-clause(
-forall([X, Y],
-or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
-    equal(X,Y))),
-a9 ).
-
-clause(
-forall([X, Y],
-or( not(equal(X,Y)),
-    hBOOL(hAPP(hAPP(fequal,X),Y)))),
-a10 ).
-
-clause(
-forall([F, G],
-or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G)))),
-    equal(F,G))),
-a11 ).
\ No newline at end of file
diff -r 35574b9b59aa -r 3728dba101f1 src/HOL/Tools/atp-inputs/u_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/u_helper1.tptp	Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%functional equality and extensionality, untyped
-
-input_clause(a9,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
-
-input_clause(a10,axiom,
-[++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
-
-input_clause(a11,axiom,
-[--equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G))),
-++equal(F,G)]).
-