isabelle: src/HOL/Tools/atp-inputs/full_comb_inclS.dfg@c72e2110c026 (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 full-types (include 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(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)))),
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([A, B, C, P, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	12	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)))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	13	a2 ).
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([P, T],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	17	or( equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T)))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	18	a3 ).
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(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)))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	23	a4 ).
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, B, C, P, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	27	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)))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	28	a5 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	29
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	30	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	31	forall([A, X, Y],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	32	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))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	33	equal(typeinfo(X,A),typeinfo(Y,A)))),
19969 c72e2110c026 Removed some incorrect axioms. mengj parents: 19717 diff changeset	34	a6 ).
19717 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	35
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	36	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	37	forall([A, X, Y],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	38	or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	39	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)))),
19969 c72e2110c026 Removed some incorrect axioms. mengj parents: 19717 diff changeset	40	a7 ).
19717 2742cec21579 Helper files in DFG format. mengj parents: diff changeset	41

author	mengj
	Fri, 30 Jun 2006 12:22:29 +0200
changeset 19969	c72e2110c026
parent 19717	2742cec21579
permissions	-rw-r--r--