// Fig. 4.1
// Axiom taclets for an exponentiation function on integers

\functions {
  int exp(int, int);
}
\schemaVariables {
  \term int a, b;
}
\rules {
  expZero { \find(exp(a, 0)) \replacewith(1) };
  expSucc { \find(exp(a, b)) \sameUpdateLevel
                             \replacewith(a * exp(a, b-1));
                             \add(==> b > 0) };
}