isabelle: src/HOL/Tools/atp-inputs/u_comb_inclS.dfg@2742cec21579 (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	%untyped combinator reduction (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([P, Q],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	7	or( equal(hAPP(hAPP(c_COMBK,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, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	12	or( equal(hAPP(hAPP(hAPP(c_COMBS,P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
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],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	17	or( equal(hAPP(c_COMBI,P),P))),
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([P, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	22	or( equal(hAPP(hAPP(hAPP(c_COMBB,P),Q),R),hAPP(P,hAPP(Q,R))))),
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([P, Q, R],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	27	or( equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q)))),
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	or( not(equal(c_COMBI,c_COMBK))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	32	a6 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	33
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	34	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	35	or( not(equal(c_COMBI,c_COMBS))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	36	a7 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	37
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	38	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	39	or( not(equal(c_COMBI,c_COMBB))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	40	a8 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	41
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	42	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	43	or( not(equal(c_COMBI,c_COMBC))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	44	a9 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	45
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	46	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	47	or( not(equal(c_COMBK,c_COMBS))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	48	a10 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	49
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	50	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	51	or( not(equal(c_COMBK,c_COMBB))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	52	a11 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	53
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	54	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	55	or( not(equal(c_COMBK,c_COMBC))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	56	a12 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	57
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	58	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	59	or( not(equal(c_COMBS,c_COMBB))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	60	a13 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	61
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	62	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	63	or( not(equal(c_COMBS,c_COMBC))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	64	a14 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	65
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	66	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	67	or( not(equal(c_COMBB,c_COMBC))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	68	a15 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	69
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	70	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	71	forall([X, Y],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	72	or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	73	equal(X,Y))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	74	a16 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	75
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	76	clause(
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	77	forall([X, Y],
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	78	or( not(equal(X,Y)),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	79	hBOOL(hAPP(hAPP(fequal,X),Y)))),
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	80	a17 ).
2742cec21579 Helper files in DFG format. mengj parents: diff changeset	81

author	mengj
	Thu, 25 May 2006 08:07:02 +0200
changeset 19717	2742cec21579
child 19969	c72e2110c026
permissions	-rw-r--r--