// Fig. 4.2
// A lemma for the exponentiation function on integers

\schemaVariables {
  \term int a, b, c;
}
\rules {
  expSplit { \find(exp(a, b)) \sameUpdateLevel
                              \replacewith(exp(a, b-c) * exp(a, c));
                              \add(==> c >= 0);
                              \add(==> b >= c) };
}