COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00006 ENDMK
C⊗;

	SIMPLE is a simplifier designed for use in program manipulation
and verification.  It finds a normal form for any expression over the
language consisting of individual variables, the usual boolean
connectives, the conditional function cond (denoting if-then-else), the
integers (numerals), the arithmetic functions and predicates +, - and ≤,
the LISP constants, functions and predicates nil, car, cdr, cons and atom,
the functions store and select for storing into and selecting from arrays,
and uninterpreted function symbols.  Individual variables range over the
union of the rationals, the set of arrays, the LISP s-expressions and the
booleans true and false.  The constant, function and predicate symbols
take their natural interpretations.

	The simplifier is complete; that is, it simplifies every valid
formula to true.  Thus it is also a decision procedure for the
quantifier-free theory of rationals, arrays and s-expressions under the
above functions and predicates.

	To run the simplifier, R SIMPLE.   Here are some examples of 
simplifications:

P ⊃ ¬ P;   
¬ P;

X = F(X) ⊃ F(F(F(X))) = X;
true;

cons(X,Y) = Z ⊃ car(Z) + cdr(Z) - X - Y = 0;
true;

X ≤ Y ∧ Y + D ≤ X ∧ 3 * D ≥ 2 * D ⊃ V[2 * X - Y] = V[X + D];
true;

V = store(store(V, I, V[J]), J, V[I]) ⊃ V[I] = V[J];
true

	This formula expresses the theorem that if the Ith and
Jth elements of a vector V are swapped, and if the resulting vector is
identical to the original vector, then the Ith and Jth elements were the same.

	A paper describing the simplifier is available from Derek Oppen.