isabelle: src/HOL/Tools/atp-inputs/const_comb_noS.dfg@46832fee1215 (annotated)

19717 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	1	%ID: $Id$
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	2	%Author: Jia Meng, NICTA
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	3	%typed combinator reduction for const-types-only (no S)
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	4
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	5	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	6	forall([A, B, P, Q],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	7	or( equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	8	a1 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	9
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	10	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	11	forall([P, T],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	12	or( equal(hAPP(c_COMBI(T),P),P))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	13	a3 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	14
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	15	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	16	forall([A, B, C, P, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	17	or( equal(hAPP(hAPP(hAPP(c_COMBB(A,B,C),P),Q),R),hAPP(P,hAPP(Q,R))))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	18	a4 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	19
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	20	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	21	forall([A, B, C, P, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	22	or( equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q)))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	23	a5 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	24
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	25	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	26	forall([A, X, Y],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	27	or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	28	equal(X,Y))),
19969 c72e2110c026 Removed some incorrect axioms. mengj parents: 19717 diff changeset	29	a6 ).
19717 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	30
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	31	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	32	forall([A, X, Y],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	33	or( not(equal(X,Y)),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	34	hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
19969 c72e2110c026 Removed some incorrect axioms. mengj parents: 19717 diff changeset	35	a7 ).
19717 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	36
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	37

author	paulson
	Thu, 21 Sep 2006 17:33:11 +0200
changeset 20661	46832fee1215
parent 19969	c72e2110c026
permissions	-rw-r--r--