2 %Author: Jia Meng, NICTA |
2 %Author: Jia Meng, NICTA |
3 %untyped combinator reduction for B', C' |
3 %untyped 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,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]). |
7 [++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,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,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]). |
11 [++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]). |