; Section 8.1
(infer (member X (cons X L))
  from (print member base)
       (print x = X l = L))
(infer (member X (cons Y M))
  from (print entering member recursive)
       (print x = X y = Y m = M)
       (member X M)
       (print exiting member recursive)
       (print x = X m = M))

; section 8.2.3
(infer (addtoend nil X (cons X nil))
  from (print addtoend base)
       (print x = X))
(infer (addtoend (cons Y L) X (cons Y M))
  from (print entering addtoend recursive)
       (print y = Y l = L x = X m = M)
       (addtoend L X M)
       (print exiting addtoend recursive)
       (print l = L x = X m = M))
;
(infer (reverse nil nil)
  from (print reverse base))
(infer (reverse (cons X L) M)
  from (print entering reverse recursive)
       (print x = X l = L m = M)
       (reverse L N)
       (addtoend N X M)
       (print exiting reverse recursive)
       (print n = N x = X m = M))
;
(infer (append nil L L)
  from (print append base) (print l = L))
(infer (append (cons X L) M (cons X N))
  from (print entering append recursive)
       (print x = X l = L m = M n = N)
       (append L M N)
       (print exiting append recursive)
       (print x = X l = L m = M n = N))
;
(infer (mult 0 Y 0)
  from (print mult base))
(infer (mult X Y Z)
  from (print entering mult recursive)
       (print x = X y = Y z = Z v = V w = W)
       (minus X 1 V) (mult V Y W) (plus W Y Z)
       (print exiting mult recursive)
       (print x = X y = Y z = Z v = V w = W))
(infer (fac 0 1)
  from (print fact basse))
(infer (fac N R)
  from (print entering fact recursive)
       (print n = N r = R n1 = N1 r1 = R1)
       (minus N 1 N1) (fac N1 R1) (mult R1 N R)
       (print entering fact recursive)
       (print n = N r = R n1 = N1 r1 = R1))
(infer (naive-sort L M)
  from (print entering naive-sort)
       (print l = L m = M)
       (permutation L M)
       (ordered M)
       (print exiting naive-sort)
       (print l = L m = M))
(infer (<= X X))
(infer (<= X Y) from (less X Y))
;
(infer (ordered nil))
(infer (ordered (cons A nil)))
(infer (ordered (cons A (cons B L))) from (<= A B) (ordered (cons B L)))
;
(infer (permutation nil nil)
  from (print permutation base))
(infer (permutation L (cons H T))
  from (print entering permutation recursive)
       (print l = L h = H t = T)
       (append V (cons H U) L)
       (print in permutation after first append)
       (print l = L h = H t = T)
       (print v = V u = U)
       (append V U W)
       (print in permutation after second append)
       (print l = L h = H t = T)
       (print v = V u = U w = W)
       (permutation W T)
       (print exiting permutation recursive)
       (print l = L h = H t = T)
       (print v = V u = U w = W))
;
(infer (simplify (diff X X) nil)
  from (print simplify base)
       (print x = X))
(infer (simplify (diff (cons X Y) Z) (cons X W))
  from (print entering simplify recursive)
       (print x = X y = Y z = Z w = W)
       (simplify (diff Y Z) W)
       (print exiting simplify recursive)
       (print x = X y = Y z = Z w = W))
(infer (diffappend (diff L X) (diff X Y) (diff L Y))
  from (print diffappend base)
       (print l = L x = X y = Y))