typedec0 "z"     	    bottom				   z\
typedec1 "s"    	    (n\ stroke par n)			   s\
typedec0 "nil"     	    bottom				   null\
typedec2 "cons"    	    (x\l\ item x par l)			   cons\
typedec3 "append"  	    (l\k\m\ ((l par k) o-o m))		   append\
typedec2 "leq"     	    (x\y\ (x par false) -o y)		   leq\ 
typedec2 "gr"      	    (x\y\ (y par stroke par false) -o x)   gr\
typedec0 "root"          bottom				   root\
typedec3 "bt"            (x\l\r\ (item x) par l par r)		   bt\
typedec3 "insert"        (x\t\s\ ((item x) par t) o-o s)	   insert\
typedec2 "lookup"        (x\t\   ((item x) par false) -o t)	   lookup\
typedec2 "build"         (l\t\   (l o-o t))			   build\
typedec2 "tsort"         (l\t\   (l o-o t))			   tsort\
typedec2 "rsort"         (l\t\   (l o-o t))			   rsort\
typedec2 "rotate"        (t\s\   (t o-o s))			   rotate\
typedec2 "traverse"      (t\s\   (t o-o s))			   traverse\
typedec2 "rtraverse"     (t\s\   (t o-o s))			   rtraverse\

clauses (

(qi "N" N\ leq z N)
  &&
(qi "M" M\ qi "N" N\ leq (s N) (s M) <== leq N M)
  &&
(qi "M" M\ gr (s M) z)
  &&
(qi "M" M\ qi "N" N\ gr (s N) (s M) <== gr N M)
  &&
(qi "X" X\ insert X root (bt X root root))
  &&
(qi "NewL" NewL\ qi "D" D\ qi "R" R\ qi "L" L\ qi "X" X\ qi "N" N\ insert X (bt D L R) (bt D NewL R) <== leq X D <== insert X L NewL)
  &&
(qi "NewR" NewR\ qi "D" D\ qi "R" R\ qi "L" L\ qi "X" X\ qi "N" N\ insert X (bt D L R) (bt D L NewR) <== gr  X D <== insert X R NewR)
  &&
(qi "R" R\ qi "L" L\ qi "X" X\ lookup X (bt X L R))
  &&
(qi "D" D\ qi "R" R\ qi "L" L\ qi "X" X\ lookup X (bt D L R) <== leq X D <== lookup X L)
  &&
(qi "D" D\ qi "R" R\ qi "L" L\ qi "X" X\ lookup X (bt D L R) <== gr  X D <== lookup X R)
  &&
(build null root)
  &&
(qi "T1" T1\ qi "T2" T2\ qi "L" L\ qi "X" X\ build (cons X L) T1 <== build L T2 <== insert X T2 T1)
  &&
(traverse root null)
  &&
(qi "Left" Left\ qi "Right" Right\ qi "S" S\ qi "D" D\ qi "R" R\ qi "L" L\ traverse (bt D L R) S <== traverse L Left <== traverse R Right <== append Left (cons D Right) S)
  &&
(qi "S" S\ qi "L" L\ tsort L S <== build L T <== traverse T S)
  &&
(rotate root root)
  &&
(qi "T" T\ qi "N" N\ rotate (bt N root T) (bt N root T))
  &&
(qi "Res" Res\ qi "T" T\ qi "R" R\ qi "L" L\ qi "M" M\ qi "N" N\ rotate (bt N (bt M L R) T) Res <== rotate (bt M L (bt N R T)) Res)
  &&
(rtraverse root null)
  &&
(qi "S" S\ qi "R" R\ qi "N" N\ rtraverse (bt N root R) (cons N S) <== rtraverse R S)
  &&
(qi "U" U\ qi "T" T\ qi "S" S\ qi "R" R\ qi "L" L\ qi "M" M\ qi "N" N\ rtraverse (bt N (bt M L R) T) S <== rotate (bt N (bt M L R) T) U <== rtraverse U S)
  &&
(qi "T" T\ qi "S" S\ qi "L" L\ rsort L S <== build L T <== rtraverse T S)

).