Alphabet

0:d
cons:[d × c] ⟶ c
false:a
height:d → d
if:[a × d] ⟶ d
le:[d × d] ⟶ a
map:[d → d × c] ⟶ c
maxlist:[d × c] ⟶ d
nil:c
node:[b × c] ⟶ d
s:[d] ⟶ d
true:a

Variables

F:d → d
Z:d → d
U:d
V:c
W:d
P:d
X1:d
Y1:d
U1:d
V1:d
W1:c
P1:d
X2:b
Y2:c

Rules

map(F, nil)⇒nil
map(Z, cons(U, V))⇒cons(Z · U, map(Z, V))
le(0, W)⇒true
le(s(P), 0)⇒false
le(s(X1), s(Y1))⇒le(X1, Y1)
maxlist(U1, cons(V1, W1))⇒if(le(U1, V1), maxlist(V1, W1))
maxlist(P1, nil)⇒P1
height · node(X2, Y2)⇒s(maxlist(0, map(height, Y2)))