append : list A -> list A -> list A -> type.
append1 : append nil L L.
append2 : append (cons H L1) L (cons H R) <- append L1 L R.

min : (A -> A -> type) -> list A -> A -> A -> type.

mina : min P nil X X.
minb : min P (cons H T) M R <- P H M <- min P T H R.
minc : min P (cons H T) M R <- P M H <- min P T M R.

minim : (A -> A -> type) -> list A -> A -> type.
minim1 : minim P (cons H T) Min <- min P T H Min.

sterg : A -> list A -> list A -> type.

sterga : sterg X nil nil.
stergb : sterg X (cons X L) L .
stergc : sterg X (cons Y L) (cons Y R) <- sterg X L R.

sort_sel : (A -> A -> type) -> list A -> list A -> type.

sort_sela : sort_sel P nil nil.
sort_selb : sort_sel P L (cons M R) <- minim P L M <- sterg M L R1 <- sort_sel P R1 R.

insert : (A -> A -> type) -> A -> list A -> list A -> type.
inserta : insert P X nil (cons X nil).
insertb : insert P X (cons H T) (cons H R) <- P H X <- insert P X T R.
insertc : insert P X (cons H T) (cons X (cons H T)) <- P X H.

sort_ins : (A -> A -> type) -> list A -> list A -> type.

sort_ins1 : sort_ins P nil nil.
sort_ins2 : sort_ins P (cons X L) R <- sort_ins P L R1 <- insert P X R1 R.

partitionare : (A -> A -> type) -> list A -> A -> list A -> list A -> type.
partitionare1 : partitionare P nil X nil nil.
partitionare2 : partitionare P (cons H T) X L1 (cons H L2) <- P X H <- partitionare P T X L1 L2.
partitionare3 : partitionare P (cons H T) X (cons H L1) L2 <- P H X <- partitionare P T X L1 L2.

quicksort : (A -> A -> type ) -> list A -> list A -> type.
quicksort1 : quicksort P (cons H L) R <- partitionare P L H Lst Ldr <- quicksort P Lst R1 <- quicksort P Ldr R2 <- append R1 (cons H R2) R.
quicksort2 : quicksort P nil nil.

interclasare : (A -> A -> type) -> list A -> list A -> list A -> type.

interclas1 : interclasare P nil L L.
interclas2 : interclasare P L nil L.
interclas3 : interclasare P (cons H1 L1) (cons H2 L2) (cons H1 R) <- P H1 H2 <- interclasare P L1 (cons H2 L2 ) R.
interclas4 : interclasare P (cons H1 L1) (cons H2 L2) (cons H2 R) <- P H2 H1 <- interclasare P (cons H1 L1) L2 R.