; Arithmetics on numerals

; Transform the natural number n to the "term numeral"
; (succ ... (zero))
(define (make-numeral n)
  (assert (not (negative? n)))
  (if (zero? n) '(zero)
      (list 'succ (make-numeral (- n 1)))))

; Transform the term numeral back to the natural number.
; The inverse of the make-numeral above
(define (eval-numeral num)
  (cond
   ((equal? num '(zero)) 0)
   ((and (pair? num) (eq? 'succ (car num))) (+ 1 (eval-numeral (cadr num))))
   (else (error 'eval-numeral "wrong numeral " num))))


(define rule-arith
  '(
    ( (M mul (zero) $x) => (zero) )
    ( (M mul $x (zero)) => (zero) )
    ( (M mul (succ $x) $y) => (M add $y (M mult $x $y)) )

    ( (M add (zero) $x) => $x )
    ( (M add $x (zero)) => $x )
    ( (M add (succ $x) $y) => (succ (M add $x $y)))

    ( (M add (zero) $x) => $x )
    ( (M add $x (zero)) => $x )
    ( (M add (succ $x) $y) => (succ (M add $x $y)))

    ( (M min (zero) _) => (zero) )
    ( (M min _ (zero) ) => (zero) )
    ( (M min (succ $x) (succ $y)) => (succ (M min $x $y)))

    ( (M max (zero) $x) => $x )
    ( (M max $x (zero) ) => $x )
    ( (M max (succ $x) (succ $y)) => (succ (M max $x $y)))
    ))