hmonk
COMEFROM
rm arith.adv
/bin/umodem arith.adv STOP
Compute x => E x Z;
Mult Z x => Z;
E (Add x y) q => E x (E y q);
E Z q => q;
E (S x) q => S (E x q);
E (Mult (S x) y) q => E (Mult x y) (E y q);
{ E (Mult Z x) q => q; }
E (Mult (Add x y) z) q => E (Mult x z) (E (Mult y z) q);
E (Mult (Mult x y) z) q => E (Mult x (Mult y z)) q;
.
STOP
./advise arith arith.adv