changeset 20647 | 680b58597f65 |
child 20660 | 8606ddd42554 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/atp-inputs/u_combBC_e.dfg Wed Sep 20 14:02:41 2006 +0200 @@ -0,0 +1,13 @@ +%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 ).