Alphabet

0:N
false:B
g:N → B
g2:N → B
geq:N → N → B
h:N → (N → B) → N → B
h2:N → (N → B) → N → B
iszero:N → N → B
pred:N → N
rec:(N → (N → B) → N → B) → B → N → B
s:N → N
true:B

Variables

F:N → (N → B) → N → B
Z:N → B
G:N → (N → B) → N → B
H:N → B
W:N
P:N
X1:N
Z1:N → B
U1:N
V1:N
W1:N
P1:N
X2:N
Y2:N
G2:N → B
V2:N
W2:N
P2:N

Rules

rec · F · (Z · 0)⇒Z
rec · G · (H · (s · W))⇒G · W · (rec · G · (H · W))
g · P⇒true
h · X1 · Z1 · U1⇒false
iszero · V1 · W1⇒rec · h · (g · V1) · W1
pred · 0⇒0
pred · (s · P1)⇒P1
g2 · X2⇒iszero · X2 · 0
h2 · Y2 · G2 · V2⇒G2 · (pred · V2)
geq · W2 · P2⇒rec · h2 · (g2 · W2) · P2