| 0 | : | nat |
| add | : | [nat × nat] ⟶ nat |
| rec | : | [nat → nat → nat × nat × nat] ⟶ nat |
| s | : | [nat] ⟶ nat |
| succ | : | nat → nat → nat |
| xap | : | [nat → nat → nat × nat] ⟶ nat → nat |
| yap | : | [nat → nat × nat] ⟶ nat |
| F | : | nat → nat → nat |
| Y | : | nat |
| G | : | nat → nat → nat |
| V | : | nat |
| W | : | nat |
| P | : | nat |
| X1 | : | nat |
| Y1 | : | nat |
| U1 | : | nat |
| V1 | : | nat |
| W1 | : | nat |
| P1 | : | nat |
| F2 | : | nat → nat → nat |
| Y2 | : | nat |
| G2 | : | nat → nat |
| V2 | : | nat |
| rec(λ%X:nat.λ%Y:nat.yap(xap(F, %X), %Y), Y, 0) | ⇒ | Y |
| rec(λ%Z:nat.λ%U:nat.yap(xap(G, %Z), %U), V, s(W)) | ⇒ | yap(xap(G, W), rec(λ%V:nat.λ%W:nat.yap(xap(G, %V), %W), V, W)) |
| succ · P · X1 | ⇒ | s(X1) |
| add(Y1, U1) | ⇒ | rec(λ%F:nat.λ%G:nat.yap(xap(succ, %F), %G), Y1, U1) |
| add(V1, 0) | ⇒ | V1 |
| add(W1, s(P1)) | ⇒ | s(add(W1, P1)) |
| xap(F2, Y2) | ⇒ | F2 · Y2 |
| yap(G2, V2) | ⇒ | G2 · V2 |