(synonyms valid (expr --> ok-expr))

(datatype expr

   _____________________________
  (number? X) : verified >> X : number;

  P : verified, Q : verified >> R;
  _________________________________   
  (and P Q) : verified >> R;

  X : number;
  _________
  X : expr;

  if (not (element? X [- * / +]))
  X : symbol;
  ____________
  X : expr;

  if (element? Op [+ - / *])
  __________________________
  Op : op;

  Op : op;
  _________________________________________
  (fn Op) : (number --> number --> number);

  Op : op;
  X : expr; Y : expr;
  ===================
  [X Op Y] : expr;)
  
 (datatype valid

  ___________________
  (fn arith) : valid;

   X : ok-expr;
   ____________
   X : expr;)
   
(define arith
    {expr --> expr}
    [X Op Y] -> ((fn Op) X Y)        where (and (number? X) (number? Y))
    X -> X)   

(define thrash
  {expr --> valid --> ok-expr}
   X F -> (let Y (F X)
               (if (== X Y) Y (thrash Y F))))
                              
(define walk
   {valid --> expr --> ok-expr}
   F [X Op Y] -> (F [(walk F X) Op (walk F Y)])
   F X -> (F X))
   
(define simplify
  {valid --> expr --> ok-expr}
  F E -> (thrash E (walk F)))