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
U:N
V:N
I:N → B
P:N
X1:N
Y1:N
U1:N
V1:N
W1:N
J1:N → B
X2:N
Y2:N
U2:N

Rules

rec · F · (Z · 0)⇒Z
g · U⇒true
h · V · I · P⇒false
iszero · X1 · Y1⇒rec · h · (g · X1) · Y1
pred · 0⇒0
pred · (s · U1)⇒U1
g2 · V1⇒iszero · V1 · 0
h2 · W1 · J1 · X2⇒J1 · (pred · X2)
geq · Y2 · U2⇒rec · h2 · (g2 · Y2) · U2