Shared Terms and Cached Rewriting
                   Stephan Schulz

We describe the implementation of first-order terms, the central data
structure of most modern automated theorem provers, as perfectly
shared immutable term DAGs in E. We demonstrate typical gains possible
with this structure (reducing the number of term nodes typically by
orders of magnitude) and discuss some of the side benefits of such a
representation. One of these benefits is the ability to easily
implement cached rewriting, improving the performance of
rewriting-based simplification. We discuss lessons learned and some
potential future work.