0 | : | N |
even | : | N → N → B |
false | : | B |
g | : | N → B |
h | : | N → (N → B) → N → B |
not | : | B → B |
rec | : | (N → (N → B) → N → B) → B → N → B |
s | : | N → N |
true | : | B |
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 |
rec · F · (Z · 0) | ⇒ | Z |
rec · G · (H · (s · W)) | ⇒ | G · W · (rec · G · (H · W)) |
g · P | ⇒ | true |
h · X1 · Z1 · U1 | ⇒ | not · (Z1 · U1) |
not · true | ⇒ | false |
not · false | ⇒ | true |
even · V1 · W1 | ⇒ | rec · h · (g · V1) · W1 |