| id | : | N → N |
| plus1 | : | ((N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| plus2 | : | ((((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N) → ((((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N) → (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| succ1 | : | ((N → N) → N → N) → (N → N) → N → N |
| succ2 | : | ((((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N) → (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| two1 | : | (N → N) → N → N |
| two2 | : | (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| zero1 | : | (N → N) → N → N |
| zero2 | : | (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| X | : | N |
| Z | : | N → N |
| U | : | N |
| H | : | N → N |
| W | : | N |
| J | : | (N → N) → N → N |
| F1 | : | N → N |
| Y1 | : | N |
| G1 | : | (N → N) → N → N |
| H1 | : | (N → N) → N → N |
| I1 | : | N → N |
| P1 | : | N |
| F2 | : | ((N → N) → N → N) → (N → N) → N → N |
| Z2 | : | (N → N) → N → N |
| G2 | : | N → N |
| V2 | : | N |
| I2 | : | ((N → N) → N → N) → (N → N) → N → N |
| J2 | : | (N → N) → N → N |
| F3 | : | N → N |
| Y3 | : | N |
| G3 | : | (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| H3 | : | ((N → N) → N → N) → (N → N) → N → N |
| I3 | : | (N → N) → N → N |
| J3 | : | N → N |
| X4 | : | N |
| Z4 | : | (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| G4 | : | (((N → N) → N → N) → (N → N) → N → N) → ((N → N) → N → N) → (N → N) → N → N |
| H4 | : | ((N → N) → N → N) → (N → N) → N → N |
| I4 | : | (N → N) → N → N |
| J4 | : | N → N |
| X5 | : | N |
| id · X | ⇒ | X |
| zero1 · (λ%X:N.Z · %X) · U | ⇒ | U |
| two1 · (λ%Y:N.H · %Y) · W | ⇒ | H · (H · W) |
| succ1 · (λ%U:N -> N.J · %U) · (λ%Z:N.F1 · %Z) · Y1 | ⇒ | F1 · (J · F1 · Y1) |
| plus1 · (λ%F:N -> N.G1 · %F) · (λ%W:N -> N.H1 · %W) · (λ%V:N.I1 · %V) · P1 | ⇒ | G1 · I1 · (H1 · I1 · P1) |
| zero2 · (λ%I:(N -> N) -> N -> N.F2 · %I) · (λ%H:N -> N.Z2 · %H) · (λ%G:N.G2 · %G) · V2 | ⇒ | Z2 · G2 · V2 |
| two2 · (λ%Q:(N -> N) -> N -> N.I2 · %Q) · (λ%P:N -> N.J2 · %P) · (λ%J:N.F3 · %J) · Y3 | ⇒ | I2 · (I2 · J2) · F3 · Y3 |
| succ2 · (λ%Xb:((N -> N) -> N -> N) -> (N -> N) -> N -> N.G3 · %Xb) · (λ%T:(N -> N) -> N -> N.H3 · %T) · (λ%S:N -> N.I3 · %S) · (λ%R:N.J3 · %R) · X4 | ⇒ | H3 · (G3 · H3 · I3) · J3 · X4 |
| plus2 · (λ%Wb:((N -> N) -> N -> N) -> (N -> N) -> N -> N.Z4 · %Wb) · (λ%Vb:((N -> N) -> N -> N) -> (N -> N) -> N -> N.G4 · %Vb) · (λ%Ub:(N -> N) -> N -> N.H4 · %Ub) · (λ%Zb:N -> N.I4 · %Zb) · (λ%Yb:N.J4 · %Yb) · X5 | ⇒ | Z4 · H4 · (G4 · H4 · I4) · J4 · X5 |