|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %typed combinator reduction for full-types (include S) |
|
4 |
|
5 %K P Q --> P |
|
6 input_clause(a1,axiom, |
|
7 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A))]). |
|
8 |
|
9 %S P Q R --> P R (Q R) |
|
10 input_clause(a2,axiom, |
|
11 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(tc_fun(A,B),tc_fun(A,C))),typeinfo(Q,tc_fun(A,B))),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(hAPP(typeinfo(Q,tc_fun(A,B)),typeinfo(R,A)),B)),C))]). |
|
12 |
|
13 %I P --> P |
|
14 input_clause(a3,axiom, |
|
15 [++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]). |
|
16 |
|
17 %B P Q R --> P(Q R) |
|
18 input_clause(a4,axiom, |
|
19 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))),typeinfo(P,tc_fun(A,B))),tc_fun(tc_fun(C,A),tc_fun(C,B))),typeinfo(Q,tc_fun(C,A))),tc_fun(C,B)),typeinfo(R,C)),B),typeinfo(hAPP(typeinfo(P,tc_fun(A,B)),typeinfo(hAPP(typeinfo(Q,tc_fun(C,A)),typeinfo(R,C)),A)),B))]). |
|
20 |
|
21 |
|
22 %C P Q R --> P R Q |
|
23 input_clause(a5,axiom, |
|
24 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C))]). |
|
25 |
|
26 %the combinators are all different |
|
27 input_clause(a6,axiom, |
|
28 [--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))]). |
|
29 |
|
30 input_clause(a7,axiom, |
|
31 [--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))))]). |
|
32 |
|
33 |
|
34 input_clause(a8,axiom, |
|
35 [--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))]). |
|
36 |
|
37 |
|
38 input_clause(a9,axiom, |
|
39 [--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))]). |
|
40 |
|
41 |
|
42 input_clause(a10,axiom, |
|
43 [--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))))]). |
|
44 |
|
45 input_clause(a11,axiom, |
|
46 [--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]). |
|
47 |
|
48 |
|
49 input_clause(a12,axiom, |
|
50 [--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). |
|
51 |
|
52 |
|
53 input_clause(a13,axiom, |
|
54 [--equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]). |
|
55 |
|
56 |
|
57 input_clause(a14,axiom, |
|
58 [--equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). |
|
59 |
|
60 input_clause(a15,axiom, |
|
61 [--equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]). |
|
62 |
|
63 input_clause(a16,axiom, |
|
64 [--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)), |
|
65 ++equal(typeinfo(X,A),typeinfo(Y,A))]). |
|
66 |
|
67 input_clause(a17,axiom, |
|
68 [++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)), |
|
69 --equal(typeinfo(X,A),typeinfo(Y,A))]). |
|
70 |
|
71 |