Alphabet

0:a
cons:[b × c] ⟶ c
d:[a × a] ⟶ c
false:c
filter:[b → c × c] ⟶ c
gtr:[a × a] ⟶ c
if:[c × c × c] ⟶ c
len:[c] ⟶ a
nil:c
s:[a] ⟶ a
sub:[a × a] ⟶ a
true:c

Variables

X:c
Y:c
U:c
V:c
W:a
P:a
X1:a
Y1:a
U1:a
V1:a
W1:a
P1:a
X2:a
Y2:a
U2:b
V2:c
I2:b → c
J2:b → c
X3:b
Y3:c

Rules

if(true, X, Y)⇒X
if(false, U, V)⇒V
sub(W, 0)⇒W
sub(s(P), s(X1))⇒sub(P, X1)
gtr(0, Y1)⇒false
gtr(s(U1), 0)⇒true
gtr(s(V1), s(W1))⇒gtr(V1, W1)
d(P1, 0)⇒true
d(s(X2), s(Y2))⇒if(gtr(X2, Y2), false, d(s(X2), sub(Y2, X2)))
len(nil)⇒0
len(cons(U2, V2))⇒s(len(V2))
filter(I2, nil)⇒nil
filter(J2, cons(X3, Y3))⇒if(J2 · X3, cons(X3, filter(J2, Y3)), filter(J2, Y3))