0 :: b
cons :: b → b → b
del :: b → b → b
eq :: b → b → a
false :: a
filter :: (b → a) → b → b
filter2 :: a → (b → a) → b → b → b
if :: a → b → b → b
le :: b → b → a
map :: (b → b) → b → b
min :: b → b → b
minsort :: b → b
nil :: b
s :: b → b
true :: a
le(0, X) → true
le(s(Y), 0) → false
le(s(U), s(V)) → le(U, V)
eq(0, 0) → true
eq(0, s(W)) → false
eq(s(P), 0) → false
eq(s(X1), s(Y1)) → eq(X1, Y1)
if(true, U1, V1) → U1
if(false, W1, P1) → P1
minsort(nil) → nil
minsort(cons(X2, Y2)) → cons(min(X2, Y2), minsort(del(min(X2, Y2), cons(X2, Y2))))
min(U2, nil) → U2
min(V2, cons(W2, P2)) → if(le(V2, W2), min(V2, P2), min(W2, P2))
del(X3, nil) → nil
del(Y3, cons(U3, V3)) → if(eq(Y3, U3), V3, cons(U3, del(Y3, V3)))
map(I3, nil) → nil
map(J3, cons(X4, Y4)) → cons(J3(X4), map(J3, Y4))
filter(G4, nil) → nil
filter(H4, cons(W4, P4)) → filter2(H4(W4), H4, W4, P4)
filter2(true, F5, Y5, U5) → cons(Y5, filter(F5, U5))
filter2(false, H5, W5, P5) → filter(H5, P5)