2 %Author: Jia Meng, NICTA |
2 %Author: Jia Meng, NICTA |
3 %const-typed combinator reduction for B', C' |
3 %const-typed combinator reduction for B', C' |
4 |
4 |
5 %B' c f g x --> c (f (g x)) |
5 %B' c f g x --> c (f (g x)) |
6 input_clause(a6,axiom, |
6 input_clause(a6,axiom, |
7 [++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]). |
7 [++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]). |
8 |
8 |
9 %C' c f g x --> c (f x) g |
9 %C' c f g x --> c (f x) g |
10 input_clause(a7,axiom, |
10 input_clause(a7,axiom, |
11 [++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]). |
11 [++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]). |
12 |
12 |
13 |
13 |