|
1 %ID: $Id$ |
|
2 %Author: Jia Meng, NICTA |
|
3 %typed combinator reduction for full-types (no 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 %I P --> P |
|
10 input_clause(a3,axiom, |
|
11 [++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]). |
|
12 |
|
13 %B P Q R --> P(Q R) |
|
14 input_clause(a4,axiom, |
|
15 [++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))]). |
|
16 |
|
17 |
|
18 %C P Q R --> P R Q |
|
19 input_clause(a5,axiom, |
|
20 [++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))]). |
|
21 |
|
22 %the combinators are all different |
|
23 input_clause(a6,axiom, |
|
24 [--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))]). |
|
25 |
|
26 input_clause(a8,axiom, |
|
27 [--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)))))]). |
|
28 |
|
29 |
|
30 input_clause(a9,axiom, |
|
31 [--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)))))]). |
|
32 |
|
33 input_clause(a11,axiom, |
|
34 [--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)))))]). |
|
35 |
|
36 |
|
37 input_clause(a12,axiom, |
|
38 [--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)))))]). |
|
39 |
|
40 |
|
41 input_clause(a15,axiom, |
|
42 [--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)))))]). |
|
43 |
|
44 input_clause(a16,axiom, |
|
45 [--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)), |
|
46 ++equal(typeinfo(X,A),typeinfo(Y,A))]). |
|
47 |
|
48 input_clause(a17,axiom, |
|
49 [++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)), |
|
50 --equal(typeinfo(X,A),typeinfo(Y,A))]). |
|
51 |
|
52 |