| changeset 20647 | 680b58597f65 |
| 20646:02729d4d6e4a | 20647:680b58597f65 |
|---|---|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %partial-typed combinator reduction for S |
|
4 |
|
5 %S P Q R --> P R (Q R) |
|
6 input_clause(a2,axiom, |
|
7 [++equal(hAPP(hAPP(hAPP(c_COMBS,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),Q,tc_fun(tc_fun(A,B),tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),hAPP(Q,R,tc_fun(A,B)),tc_fun(B,C)))]). |
|
8 |