1: \begin{abstract}

2: This work is motivated by a challenging problem of computer-aided derivation of

3: multiscale models of arrays of micro- and nanosystems. In this domain a model is

4: a partial differential equation. Multiscale methods approximate it by another

5: partial differential equation. The challenge is to formalize these approximating

6: methods within a computer algebra system, e.g. Maple$^{\mathsf{\tiny TM}}$. Since

7: most of the transformation steps correspond to equational reasoning

8: (i.e. symbolic transformations based on equalities) we address the question of

9: extending Maple with rewriting and strategies. Our contribution consists in

10: transferring most of the term rewriting concepts and techniques to the symbolic

11: computation community. We provide a Maple package for rule-based programming and

12: its combination with standard Maple code. We illustrate its practical

13: interest by applying the package functions to provide a

14: formal proof of a convergence property of a two-scale operator.

15: \end{abstract}

16: