# HG changeset patch # User mengj # Date 1151662949 -7200 # Node ID c72e2110c026cbb907191cb9fce1efcf1fe7a53d # Parent 2180f0f443af8d0f74ac4aaadb9a1e57be762179 Removed some incorrect axioms. diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/const_comb_inclS.dfg --- a/src/HOL/Tools/atp-inputs/const_comb_inclS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/const_comb_inclS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -28,64 +28,14 @@ a5 ). clause( -forall([A, B, T], -or( not(equal(c_COMBI(T),c_COMBK(A,B))))), -a6 ). - -clause( -forall([A, B, C, T], -or( not(equal(c_COMBI(T),c_COMBS(A,B,C))))), -a7 ). - -clause( -forall([A, B, C, T], -or( not(equal(c_COMBI(T),c_COMBB(A,B,C))))), -a8 ). - -clause( -forall([A, B, C, T], -or( not(equal(c_COMBI(T),c_COMBC(A,B,C))))), -a9 ). - -clause( -forall([A, A3, B, B3, C3], -or( not(equal(c_COMBK(A,B),c_COMBS(A3,B3,C3))))), -a10 ). - -clause( -forall([A, A1, B, B1, C1], -or( not(equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))))), -a11 ). - -clause( -forall([A, A2, B, B2, C2], -or( not(equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))))), -a12 ). - -clause( -forall([A1, A3, B1, B3, C1, C3], -or( not(equal(c_COMBS(A3,B3,C3),c_COMBB(A1,B1,C1))))), -a13 ). - -clause( -forall([A2, A3, B2, B3, C2, C3], -or( not(equal(c_COMBS(A3,B3,C3),c_COMBC(A2,B2,C2))))), -a14 ). - -clause( -forall([A1, A2, B1, B2, C1, C2], -or( not(equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))))), -a15 ). - -clause( forall([A, X, Y], or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))), equal(X,Y))), -a16 ). +a6 ). clause( forall([A, X, Y], or( not(equal(X,Y)), hBOOL(hAPP(hAPP(fequal(A),X),Y)))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/const_comb_inclS.tptp --- a/src/HOL/Tools/atp-inputs/const_comb_inclS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/const_comb_inclS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -24,41 +24,10 @@ input_clause(a5,axiom, [++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(c_COMBI(T),c_COMBK(A,B))]). +[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]). input_clause(a7,axiom, -[--equal(c_COMBI(T),c_COMBS(A,B,C))]). - -input_clause(a8,axiom, -[--equal(c_COMBI(T),c_COMBB(A,B,C))]). - -input_clause(a9,axiom, -[--equal(c_COMBI(T),c_COMBC(A,B,C))]). - -input_clause(a10,axiom, -[--equal(c_COMBK(A,B),c_COMBS(A3,B3,C3))]). - -input_clause(a11,axiom, -[--equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))]). - -input_clause(a12,axiom, -[--equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))]). - -input_clause(a13,axiom, -[--equal(c_COMBS(A3,B3,C3),c_COMBB(A1,B1,C1))]). - -input_clause(a14,axiom, -[--equal(c_COMBS(A3,B3,C3),c_COMBC(A2,B2,C2))]). - -input_clause(a15,axiom, -[--equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))]). - -input_clause(a16,axiom, -[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]). - -input_clause(a17,axiom, [++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/const_comb_noS.dfg --- a/src/HOL/Tools/atp-inputs/const_comb_noS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/const_comb_noS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -23,45 +23,15 @@ a5 ). clause( -forall([A, B, T], -or( not(equal(c_COMBI(T),c_COMBK(A,B))))), -a6 ). - -clause( -forall([A, B, C, T], -or( not(equal(c_COMBI(T),c_COMBB(A,B,C))))), -a8 ). - -clause( -forall([A, B, C, T], -or( not(equal(c_COMBI(T),c_COMBC(A,B,C))))), -a9 ). - -clause( -forall([A, A1, B, B1, C1], -or( not(equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))))), -a11 ). - -clause( -forall([A, A2, B, B2, C2], -or( not(equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))))), -a12 ). - -clause( -forall([A1, A2, B1, B2, C1, C2], -or( not(equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))))), -a15 ). - -clause( forall([A, X, Y], or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))), equal(X,Y))), -a16 ). +a6 ). clause( forall([A, X, Y], or( not(equal(X,Y)), hBOOL(hAPP(hAPP(fequal(A),X),Y)))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/const_comb_noS.tptp --- a/src/HOL/Tools/atp-inputs/const_comb_noS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/const_comb_noS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -19,29 +19,10 @@ input_clause(a5,axiom, [++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(c_COMBI(T),c_COMBK(A,B))]). - -input_clause(a8,axiom, -[--equal(c_COMBI(T),c_COMBB(A,B,C))]). - -input_clause(a9,axiom, -[--equal(c_COMBI(T),c_COMBC(A,B,C))]). - -input_clause(a11,axiom, -[--equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))]). - -input_clause(a12,axiom, -[--equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))]). - -input_clause(a15,axiom, -[--equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))]). - -input_clause(a16,axiom, [--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]). -input_clause(a17,axiom, +input_clause(a7,axiom, [++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/full_comb_inclS.dfg --- a/src/HOL/Tools/atp-inputs/full_comb_inclS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/full_comb_inclS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -28,64 +28,14 @@ a5 ). clause( -forall([A, B, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))))), -a6 ). - -clause( -forall([A, B, C, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))))))), -a7 ). - -clause( -forall([A, B, C, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))))), -a8 ). - -clause( -forall([A, B, C, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))))), -a9 ). - -clause( -forall([A, A3, B, B3, C3], -or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))))))), -a10 ). - -clause( -forall([A, A1, B, B1, C1], -or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))), -a11 ). - -clause( -forall([A, A2, B, B2, C2], -or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), -a12 ). - -clause( -forall([A1, A3, B1, B3, C1, C3], -or( not(equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))), -a13 ). - -clause( -forall([A2, A3, B2, B3, C2, C3], -or( not(equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), -a14 ). - -clause( -forall([A1, A2, B1, B2, C1, C2], -or( not(equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), -a15 ). - -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)))), -a16 ). +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)))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/full_comb_inclS.tptp --- a/src/HOL/Tools/atp-inputs/full_comb_inclS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/full_comb_inclS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -23,48 +23,11 @@ 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))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))]). - -input_clause(a7,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))))]). - - -input_clause(a8,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))]). - - -input_clause(a9,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))]). - - -input_clause(a10,axiom, -[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))))]). - -input_clause(a11,axiom, -[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]). - - -input_clause(a12,axiom, -[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). - - -input_clause(a13,axiom, -[--equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]). - - -input_clause(a14,axiom, -[--equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). - -input_clause(a15,axiom, -[--equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). - -input_clause(a16,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(a17,axiom, +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 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/full_comb_noS.dfg --- a/src/HOL/Tools/atp-inputs/full_comb_noS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/full_comb_noS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -23,44 +23,14 @@ a5 ). clause( -forall([A, B, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))))), -a6 ). - -clause( -forall([A, B, C, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))))), -a8 ). - -clause( -forall([A, B, C, T], -or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))))), -a9 ). - -clause( -forall([A, A1, B, B1, C1], -or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))), -a11 ). - -clause( -forall([A, A2, B, B2, C2], -or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), -a12 ). - -clause( -forall([A1, A2, B1, B2, C1, C2], -or( not(equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))), -a15 ). - -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)))), -a16 ). +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)))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/full_comb_noS.tptp --- a/src/HOL/Tools/atp-inputs/full_comb_noS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/full_comb_noS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -19,33 +19,11 @@ 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))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))]). - -input_clause(a8,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))]). - - -input_clause(a9,axiom, -[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))]). - -input_clause(a11,axiom, -[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]). - - -input_clause(a12,axiom, -[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). - - -input_clause(a15,axiom, -[--equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). - -input_clause(a16,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(a17,axiom, +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 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/par_comb_inclS.dfg --- a/src/HOL/Tools/atp-inputs/par_comb_inclS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/par_comb_inclS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -28,54 +28,14 @@ a5 ). clause( -or( not(equal(c_COMBI,c_COMBK))), -a6 ). - -clause( -or( not(equal(c_COMBI,c_COMBS))), -a7 ). - -clause( -or( not(equal(c_COMBI,c_COMBB))), -a8 ). - -clause( -or( not(equal(c_COMBI,c_COMBC))), -a9 ). - -clause( -or( not(equal(c_COMBK,c_COMBS))), -a10 ). - -clause( -or( not(equal(c_COMBK,c_COMBB))), -a11 ). - -clause( -or( not(equal(c_COMBK,c_COMBC))), -a12 ). - -clause( -or( not(equal(c_COMBS,c_COMBB))), -a13 ). - -clause( -or( not(equal(c_COMBS,c_COMBC))), -a14 ). - -clause( -or( not(equal(c_COMBB,c_COMBC))), -a15 ). - -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))), -a16 ). +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))))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/par_comb_inclS.tptp --- a/src/HOL/Tools/atp-inputs/par_comb_inclS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/par_comb_inclS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -25,42 +25,11 @@ 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)))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(c_COMBI,c_COMBK)]). - -input_clause(a7,axiom, -[--equal(c_COMBI,c_COMBS)]). - -input_clause(a8,axiom, -[--equal(c_COMBI,c_COMBB)]). - -input_clause(a9,axiom, -[--equal(c_COMBI,c_COMBC)]). - -input_clause(a10,axiom, -[--equal(c_COMBK,c_COMBS)]). - -input_clause(a11,axiom, -[--equal(c_COMBK,c_COMBB)]). - -input_clause(a12,axiom, -[--equal(c_COMBK,c_COMBC)]). - -input_clause(a13,axiom, -[--equal(c_COMBS,c_COMBB)]). - -input_clause(a14,axiom, -[--equal(c_COMBS,c_COMBC)]). - -input_clause(a15,axiom, -[--equal(c_COMBB,c_COMBC)]). - -input_clause(a16,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(a17,axiom, +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 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/par_comb_noS.dfg --- a/src/HOL/Tools/atp-inputs/par_comb_noS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/par_comb_noS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -23,38 +23,14 @@ a5 ). clause( -or( not(equal(c_COMBI,c_COMBK))), -a6 ). - -clause( -or( not(equal(c_COMBI,c_COMBB))), -a8 ). - -clause( -or( not(equal(c_COMBI,c_COMBC))), -a9 ). - -clause( -or( not(equal(c_COMBK,c_COMBB))), -a11 ). - -clause( -or( not(equal(c_COMBK,c_COMBC))), -a12 ). - -clause( -or( not(equal(c_COMBB,c_COMBC))), -a15 ). - -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))), -a16 ). +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))))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/par_comb_noS.tptp --- a/src/HOL/Tools/atp-inputs/par_comb_noS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/par_comb_noS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -20,30 +20,11 @@ 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)))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(c_COMBI,c_COMBK)]). - -input_clause(a8,axiom, -[--equal(c_COMBI,c_COMBB)]). - -input_clause(a9,axiom, -[--equal(c_COMBI,c_COMBC)]). - -input_clause(a11,axiom, -[--equal(c_COMBK,c_COMBB)]). - -input_clause(a12,axiom, -[--equal(c_COMBK,c_COMBC)]). - -input_clause(a15,axiom, -[--equal(c_COMBB,c_COMBC)]). - -input_clause(a16,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(a17,axiom, +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 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/u_comb_inclS.dfg --- a/src/HOL/Tools/atp-inputs/u_comb_inclS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/u_comb_inclS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -28,54 +28,14 @@ a5 ). clause( -or( not(equal(c_COMBI,c_COMBK))), -a6 ). - -clause( -or( not(equal(c_COMBI,c_COMBS))), -a7 ). - -clause( -or( not(equal(c_COMBI,c_COMBB))), -a8 ). - -clause( -or( not(equal(c_COMBI,c_COMBC))), -a9 ). - -clause( -or( not(equal(c_COMBK,c_COMBS))), -a10 ). - -clause( -or( not(equal(c_COMBK,c_COMBB))), -a11 ). - -clause( -or( not(equal(c_COMBK,c_COMBC))), -a12 ). - -clause( -or( not(equal(c_COMBS,c_COMBB))), -a13 ). - -clause( -or( not(equal(c_COMBS,c_COMBC))), -a14 ). - -clause( -or( not(equal(c_COMBB,c_COMBC))), -a15 ). - -clause( forall([X, Y], or( not(hBOOL(hAPP(hAPP(fequal,X),Y))), equal(X,Y))), -a16 ). +a6 ). clause( forall([X, Y], or( not(equal(X,Y)), hBOOL(hAPP(hAPP(fequal,X),Y)))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/u_comb_inclS.tptp --- a/src/HOL/Tools/atp-inputs/u_comb_inclS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/u_comb_inclS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -20,41 +20,10 @@ input_clause(a5,axiom, [++equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(c_COMBI,c_COMBK)]). +[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]). input_clause(a7,axiom, -[--equal(c_COMBI,c_COMBS)]). - -input_clause(a8,axiom, -[--equal(c_COMBI,c_COMBB)]). - -input_clause(a9,axiom, -[--equal(c_COMBI,c_COMBC)]). - -input_clause(a10,axiom, -[--equal(c_COMBK,c_COMBS)]). - -input_clause(a11,axiom, -[--equal(c_COMBK,c_COMBB)]). - -input_clause(a12,axiom, -[--equal(c_COMBK,c_COMBC)]). - -input_clause(a13,axiom, -[--equal(c_COMBS,c_COMBB)]). - -input_clause(a14,axiom, -[--equal(c_COMBS,c_COMBC)]). - -input_clause(a15,axiom, -[--equal(c_COMBB,c_COMBC)]). - -input_clause(a16,axiom, -[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]). - -input_clause(a17,axiom, [++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/u_comb_noS.dfg --- a/src/HOL/Tools/atp-inputs/u_comb_noS.dfg Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/u_comb_noS.dfg Fri Jun 30 12:22:29 2006 +0200 @@ -23,38 +23,14 @@ a5 ). clause( -or( not(equal(c_COMBI,c_COMBK))), -a6 ). - -clause( -or( not(equal(c_COMBI,c_COMBB))), -a8 ). - -clause( -or( not(equal(c_COMBI,c_COMBC))), -a9 ). - -clause( -or( not(equal(c_COMBK,c_COMBB))), -a11 ). - -clause( -or( not(equal(c_COMBK,c_COMBC))), -a12 ). - -clause( -or( not(equal(c_COMBB,c_COMBC))), -a15 ). - -clause( forall([X, Y], or( not(hBOOL(hAPP(hAPP(fequal,X),Y))), equal(X,Y))), -a16 ). +a6 ). clause( forall([X, Y], or( not(equal(X,Y)), hBOOL(hAPP(hAPP(fequal,X),Y)))), -a17 ). +a7 ). diff -r 2180f0f443af -r c72e2110c026 src/HOL/Tools/atp-inputs/u_comb_noS.tptp --- a/src/HOL/Tools/atp-inputs/u_comb_noS.tptp Fri Jun 30 12:04:17 2006 +0200 +++ b/src/HOL/Tools/atp-inputs/u_comb_noS.tptp Fri Jun 30 12:22:29 2006 +0200 @@ -16,29 +16,10 @@ input_clause(a5,axiom, [++equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q))]). -%the combinators are all different input_clause(a6,axiom, -[--equal(c_COMBI,c_COMBK)]). - -input_clause(a8,axiom, -[--equal(c_COMBI,c_COMBB)]). - -input_clause(a9,axiom, -[--equal(c_COMBI,c_COMBC)]). - -input_clause(a11,axiom, -[--equal(c_COMBK,c_COMBB)]). - -input_clause(a12,axiom, -[--equal(c_COMBK,c_COMBC)]). - -input_clause(a15,axiom, -[--equal(c_COMBB,c_COMBC)]). - -input_clause(a16,axiom, [--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]). -input_clause(a17,axiom, +input_clause(a7,axiom, [++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).