- axiom "ZERO" "0+?x" "?x"; (* declarations made above still in force *) (* 0 is a numeral, so predeclared *) - declarepretheorem "ZEROES"; (* declare intention of proving a theorem ZEROES *) - s "0+?x"; (* display omitted *) - ri "ZERO"; ex(); {?x} (* the expected display *) ?x - ri "ZEROES"; {ZEROES => ?x} (* we leave the intention hanging; after all, ZEROES => ?x what does ZEROES do? *) - prove "ZEROES"; ZEROES: (* the ``theorem'' *) 0 + ?x = ZEROES => ?x (* note presence of recursion *) ZERO , 0 (* axioms used *) (* now we test it *) - s "0+0+0+?x"; (* display omitted *) - ri "ZEROES"; ex(); {?x} (* the final display *) ?x (* demonstration of trace feature *) - startover(); (* this command resets both sides of the equation to the left side *) {0 + 0 + 0 + ?x} 0 + 0 + 0 + ?x - ri "ZEROES"; steps(); (* the steps command traces tactic execution *) ZEROES => 0 + 0 + 0 + ?x (* display traced steps *) ZEROES => 0 + 0 + ?x ZEROES => 0 + ?x ZEROES => ?x ?x (* note that the embedded theorem is simply dropped when it does not apply; this makes termination possible *)

This extremely simple example gives the basic idea of Watson's tactic
language; `ZEROES` as an equational theorem is certainly true
(this follows from the axiom `ZERO` and the fact that embedded
theorems have no effect on term reference); as seen here, this
``equational theorem'' has execution behavior more general than can be
achieved with any single application of a rewrite rule.