// Sect. 4.4.2
// Two versions of an axiom for the exponentiation function
// on integers

\optionsDecl { expSideConditions : {splitting, ifThenElse}; }

\schemaVariables {
  \term int a, b, c;
}

\rules {
  expSplit (expSideConditions:splitting) {
        \find(exp(a, b)) \sameUpdateLevel
        \replacewith(exp(a, b-c) * exp(a, c));
        \add(==> c >= 0); \add(==> b >= c) };
  expSplit (expSideConditions:ifThenElse) {
        \find(exp(a, b)) \sameUpdateLevel
        \replacewith( \if (c >= 0 & b >= c)
                      \then (exp(a, b-c) * exp(a, c))
                      \else (exp(a, b)) ) };
}