// Fig. 4.5
// Examples of rewriting taclets
// (the taclets given here already exist as base rules in KeY)

\sorts {
  \generic G;
}
\schemaVariables {
  \formula phi;         \variables G x;
  \term[strict] G t1;   \term G t2;       \term int intTerm;
}
\rules {
  zeroRight { \find (intTerm + 0) \replacewith (intTerm) };
  removeAll { \find (\forall x; phi) \varcond (\notFreeIn(x, phi))
              \replacewith (phi) };
  applyEq   { \assumes (t1 = t2 ==>) \find(t1) \sameUpdateLevel
                                     \replacewith(t2) };
  applyEqAR { \find (t1 = t2 ==>)
              \addrules ( rewrWithEq { \find (t1) \sameUpdateLevel
                                       \replacewith (t2) } ) };
}