Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
%ID: $Id$
%Author: Jia Meng, NICTA
%full-typed combinator reduction for B', C'
%B' c f g x --> c (f (g x))
input_clause(a6,axiom,
[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B))]).
%C' c f g x --> c (f x) g
input_clause(a7,axiom,
[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U))]).