The paper introduces a method for combining decision procedures for multiple theories into a single decision procedure, which is then used to implement a simplifier. This simplifier finds a normal form for expressions involving various functions and predicates, including Boolean connectives, equality, arithmetic operations, Lisp functions, and uninterpreted function symbols. If an expression is a theorem, it is simplified to the constant true; otherwise, it is simplified to false. The simplifier is currently used in the Stanford Pascal Verifier, an interactive system for reasoning about Pascal programs. The paper discusses the importance of program manipulation systems in making programming more automatic and error-prone, but notes that they have not progressed beyond the experimental stage due to the slow and unreliable nature of mechanical theorem provers. The authors provide examples of theorems that arise in program manipulation, such as proving the commutativity of loop executions and verifying the range of a function. The simplifier combines decision procedures for four quantifier-free theories: real numbers under addition and multiplication, arrays under store and select, list structure with car, cdr, cons, and atom, and equality with uninterpreted function symbols. The method is based on equality propagation, where the satisfiability procedures detect and propagate equalities between variables. The paper also describes the correctness of the equality propagation procedure and provides a detailed algorithm for combining theories. The simplifier uses a variant of the cond normal form to simplify Boolean expressions and symbolically evaluates conditional expressions. The algorithms for the theories are incremental and resettable, allowing for efficient handling of conjunctions and case splits. The paper concludes with an example of how the simplifier handles a complex formula involving array operations.The paper introduces a method for combining decision procedures for multiple theories into a single decision procedure, which is then used to implement a simplifier. This simplifier finds a normal form for expressions involving various functions and predicates, including Boolean connectives, equality, arithmetic operations, Lisp functions, and uninterpreted function symbols. If an expression is a theorem, it is simplified to the constant true; otherwise, it is simplified to false. The simplifier is currently used in the Stanford Pascal Verifier, an interactive system for reasoning about Pascal programs. The paper discusses the importance of program manipulation systems in making programming more automatic and error-prone, but notes that they have not progressed beyond the experimental stage due to the slow and unreliable nature of mechanical theorem provers. The authors provide examples of theorems that arise in program manipulation, such as proving the commutativity of loop executions and verifying the range of a function. The simplifier combines decision procedures for four quantifier-free theories: real numbers under addition and multiplication, arrays under store and select, list structure with car, cdr, cons, and atom, and equality with uninterpreted function symbols. The method is based on equality propagation, where the satisfiability procedures detect and propagate equalities between variables. The paper also describes the correctness of the equality propagation procedure and provides a detailed algorithm for combining theories. The simplifier uses a variant of the cond normal form to simplify Boolean expressions and symbolically evaluates conditional expressions. The algorithms for the theories are incremental and resettable, allowing for efficient handling of conjunctions and case splits. The paper concludes with an example of how the simplifier handles a complex formula involving array operations.