| 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 |