| cons | : | [t × f] ⟶ f |
| heightf | : | [f] ⟶ N |
| heightt | : | [t] ⟶ N |
| leaf | : | t |
| max | : | [N × N] ⟶ N |
| nil | : | f |
| node | : | [f] ⟶ t |
| s | : | [N] ⟶ N |
| z | : | N |
| X | : | t |
| Y | : | f |
| U | : | f |
| heightf(nil) | ⇒ | z |
| heightf(cons(X, Y)) | ⇒ | max(heightt(X), heightf(Y)) |
| heightt(leaf) | ⇒ | z |
| heightt(node(U)) | ⇒ | s(heightf(U)) |