Alphabet

0:a
asort:[b] ⟶ b
cons:[a × b] ⟶ b
dsort:[b] ⟶ b
insert:[a → a → a × a → a → a × b × a] ⟶ b
max:a → a → a
min:a → a → a
nil:b
s:[a] ⟶ a
sort:[a → a → a × a → a → a × b] ⟶ b

Variables

F:a → a → a
Z:a → a → a
G:a → a → a
H:a → a → a
W:a
P:b
F1:a → a → a
Z1:a → a → a
U1:a
H1:a → a → a
I1:a → a → a
P1:a
X2:a
Y2:b
U2:a
V2:a
W2:a
P2:a
X3:a
Y3:a
U3:a
V3:a
W3:b
P3:b

Rules

sort(F, Z, nil)⇒nil
sort(G, H, cons(W, P))⇒insert(G, H, sort(G, H, P), W)
insert(F1, Z1, nil, U1)⇒cons(U1, nil)
insert(H1, I1, cons(P1, Y2), X2)⇒cons(H1 · P1 · X2, insert(H1, I1, Y2, I1 · P1 · X2))
max · 0 · U2⇒U2
max · V2 · 0⇒V2
max · s(W2) · s(P2)⇒max · W2 · P2
min · 0 · X3⇒0
min · Y3 · 0⇒0
min · s(U3) · s(V3)⇒min · U3 · V3
asort(W3)⇒sort(min, max, W3)
dsort(P3)⇒sort(max, min, P3)