changeset 20647 | 680b58597f65 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/atp-inputs/const_combBC.tptp Wed Sep 20 14:02:41 2006 +0200 @@ -0,0 +1,13 @@ +%ID: $Id$ +%Author: Jia Meng, NICTA +%const-typed combinator reduction for B, C + +%B P Q R --> P(Q R) +input_clause(a4,axiom, +[++equal(hAPP(hAPP(hAPP(c_COMBB(A,B,C),P),Q),R),hAPP(P,hAPP(Q,R)))]). + + +%C P Q R --> P R Q +input_clause(a5,axiom, +[++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]). +