typedec0 "z"	      bottom						         z\
typedec1 "s"	      (n\ stroke par n)						 s\
typedec3 "plus"      (n\m\p\ ((n par false) -o p) && ((m par false) -o p))	 plus\
typedec3 "pluss"     (n\m\p\ ((n par false) -o p) && ((m par stroke par false) -o p))    pluss\
typedec3 "minus"     (n\m\p\ (p par false) -o n)                                minus\
%typedec3 "divide"    (n\m\p\ (p par false) -o n)                                divide\
typedec3 "max"       (n\m\p\ ((n par false) -o p) && ((m par false) -o p))      max\   %  Also, add  (n o-o p) oplus (m o-o p)
typedec3 "min"       (n\m\p\ ((p par false) -o n) && ((p par false) -o m))      min\   %  Also, add  (n o-o p) oplus (m o-o p)

clauses (

(qi "N" N\ plus z N N)
 &&
(qi "N" N\ qi "M" M\ qi "P" P\ plus (s N) M (s P) <== plus N M P)
 &&
(qi "N" N\ pluss (s z) N (s N))
 &&
(qi "N" N\ qi "M" M\ qi "P" P\ pluss (s N) M (s P) <== pluss N M P)
 &&
(qi "N" N\ minus z N z)
 &&
(qi "N" N\ qi "M" M\ qi "P" P\ minus (s N) (s M) P <== minus N M P)
 &&
%(qi "Y" Y\ divide z Y z)
% &&
%(qi "X" X\ qi "Y" Y\ qi "D" D\ qi "M" M\ divide (s X) Y (s D) <== minus (s X) Y M <== divide M Y D)
% &&
(qi "N" N\ max z N N)
 &&
(qi "N" N\ max (s N) z (s N))
 &&
(qi "N" N\ qi "M" M\ qi "P" P\ max (s N) (s M) (s P) <== max N M P)
 &&
(qi "N" N\ min z N z)
 &&
(qi "N" N\ min (s N) z z)
 &&
(qi "N" N\ qi "M" M\ qi "P" P\ min (s N) (s M) (s P) <== min N M P)

).