typedec0 "nil"      false						      null\
typedec2 "cons"     (x\l\ item x oplus l)				      cons\
typedec3 "append"   (l\k\m\ ((l oplus k) o-o m))			      append\
typedec4 "split"    (x\l\k\m\ (item x oplus l) o-o (item x oplus k oplus m))  split\
typedec2 "sort"     (l\k\ (l o-o k))					      qsort\
typedec2 "gr"       (x\y\ one)						      gr\

clauses (

(qi "K" K\ append null K K) 
  &&
(qi "X" X\ qi "L" L\ qi "K" K\ qi "M" M\ append (cons X L) K (cons X M) <== append L K M) 
  && 
(qi "X" X\ split X null null null)
 &&
(qi "X" X\ qi "A" A\ qi "B" B\ qi "R" R\ qi "S" S\
    split X (cons X R) S B <== split X R S B)
 &&
(qi "X" X\ qi "A" A\ qi "B" B\ qi "R" R\ qi "S" S\
    split X (cons A R) (cons A S) B <== gr X A <== split X R S B)
 &&
(qi "X" X\ qi "A" A\ qi "B" B\ qi "R" R\ qi "S" S\
    split X (cons A R) S (cons A B) <== gr  A X <== split X R S B)
 &&
(qsort null null)
 &&
(qi "F" F\ qi "R" R\ qi "S" S\ qi "Sm" Small\ qi "Bg" Big\ qi "SS" SS\ qi "BS" BS\ 
  qsort (cons F R) S <== split F R Small Big <== qsort Small SS <== qsort Big BS <== append SS (cons F BS) S)
).