|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %typed combinator reduction for partial-types (include S) |
|
4 |
|
5 clause( |
|
6 forall([A, B, P, Q], |
|
7 or( equal(hAPP(hAPP(c_COMBK,P,tc_fun(A,tc_fun(B,A))),Q,tc_fun(B,A)),P))), |
|
8 a1 ). |
|
9 |
|
10 clause( |
|
11 forall([A, B, C, P, Q, R], |
|
12 or( 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))))), |
|
13 a2 ). |
|
14 |
|
15 clause( |
|
16 forall([P, T], |
|
17 or( equal(hAPP(c_COMBI,P,tc_fun(T,T)),P))), |
|
18 a3 ). |
|
19 |
|
20 clause( |
|
21 forall([A, B, C, P, Q, R], |
|
22 or( equal(hAPP(hAPP(hAPP(c_COMBB,P,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),Q,tc_fun(tc_fun(C,A),tc_fun(C,B))),R,tc_fun(C,B)),hAPP(P,hAPP(Q,R,tc_fun(C,A)),tc_fun(A,B))))), |
|
23 a4 ). |
|
24 |
|
25 clause( |
|
26 forall([A, B, C, P, Q, R], |
|
27 or( equal(hAPP(hAPP(hAPP(c_COMBC,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),Q,tc_fun(B,tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),Q,tc_fun(B,C))))), |
|
28 a5 ). |
|
29 |
|
30 clause( |
|
31 or( not(equal(c_COMBI,c_COMBK))), |
|
32 a6 ). |
|
33 |
|
34 clause( |
|
35 or( not(equal(c_COMBI,c_COMBS))), |
|
36 a7 ). |
|
37 |
|
38 clause( |
|
39 or( not(equal(c_COMBI,c_COMBB))), |
|
40 a8 ). |
|
41 |
|
42 clause( |
|
43 or( not(equal(c_COMBI,c_COMBC))), |
|
44 a9 ). |
|
45 |
|
46 clause( |
|
47 or( not(equal(c_COMBK,c_COMBS))), |
|
48 a10 ). |
|
49 |
|
50 clause( |
|
51 or( not(equal(c_COMBK,c_COMBB))), |
|
52 a11 ). |
|
53 |
|
54 clause( |
|
55 or( not(equal(c_COMBK,c_COMBC))), |
|
56 a12 ). |
|
57 |
|
58 clause( |
|
59 or( not(equal(c_COMBS,c_COMBB))), |
|
60 a13 ). |
|
61 |
|
62 clause( |
|
63 or( not(equal(c_COMBS,c_COMBC))), |
|
64 a14 ). |
|
65 |
|
66 clause( |
|
67 or( not(equal(c_COMBB,c_COMBC))), |
|
68 a15 ). |
|
69 |
|
70 clause( |
|
71 forall([A, X, Y], |
|
72 or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))), |
|
73 equal(X,Y))), |
|
74 a16 ). |
|
75 |
|
76 clause( |
|
77 forall([A, X, Y], |
|
78 or( not(equal(X,Y)), |
|
79 hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))), |
|
80 a17 ). |
|
81 |