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\ typedec4 "split" (x\l\k\m\ l o-o (k par m)) split\ typedec2 "sort" (l\k\ (l o-o k)) qsort\ typedec2 "leq" (x\y\ one) leq\ typedec2 "gr" (x\y\ one) gr\ typedec2 "perm" (l\k\ (l o-o k)) perm\ typedec2 "reverse" (l\k\ (l o-o k)) reverse\ typedec3 "rev" (l\k\m\ ((l par m) o-o k)) rev\ typedec2 "nreverse" (l\k\ (l o-o k)) nreverse\ typedec2 "memb" (x\l\ ((item x par false) -o l)) memb\ typedec3 "memb_and_rest" (x\l\k\ ((item x par false) -o l) && (k par false) -o l) memb_and_rest\ 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 A R) (cons A S) B <== leq A X <== 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) && (perm null null) && (qi "L" L\ qi "H" H\ qi "T" T\ qi "V" V\ qi "U" U\ qi "W" W\ perm L (cons H T) <== append V (cons H U) L <== append V U W <== perm W T) && (qi "L" L\ qi "K" K\ reverse L K <== rev L K null) && (qi "L" L\ rev null L L <== top) && (qi "L" L\ qi "K" K\ qi "M" M\ qi "X" X\ rev (cons X L) K M <== rev L K (cons X M)) && (nreverse null null) && (qi "X" X\ qi "L" L\ qi "K" K\ qi "M" M\ nreverse (cons X L) K <== nreverse L M <== append M (cons X null) K) && (qi "X" X\ qi "L" L\ memb X (cons X L) <== top) && (qi "X" X\ qi "L" L\ qi "Y" Y\ memb X (cons Y L) <== memb X L) && (qi "A" A\ qi "Rest" Rest\ memb_and_rest A (cons A Rest) Rest <== top) && (qi "A" A\ qi "B" B\ qi "Tail" Tail\ qi "Rest" Rest\ memb_and_rest A (cons B Tail) (cons B Rest) <== memb_and_rest A Tail Rest) ).