| nil | : | list |
| cons | : | [nat × list] ⟶ list |
| 0 | : | nat |
| s | : | [nat] ⟶ nat |
| max | : | [nat × nat] ⟶ nat |
| min | : | [nat × nat] ⟶ nat |
| insert | : | [nat × list × nat → nat → nat × nat → nat → nat] ⟶ list |
| sort | : | [list × nat → nat → nat × nat → nat → nat] ⟶ list |
| ascending_sort | : | [list] ⟶ list |
| descending_sort | : | [list] ⟶ list |
| X | : | nat → nat → nat |
| Y | : | nat → nat → nat |
| n | : | nat |
| m | : | nat |
| l | : | list |
| max(0, n) | ⇒ | n |
| max(n, 0) | ⇒ | n |
| max(s(n), s(m)) | ⇒ | s(max(n, m)) |
| min(0, n) | ⇒ | 0 |
| min(n, 0) | ⇒ | 0 |
| min(s(n), s(m)) | ⇒ | s(min(n, m)) |
| insert(n, nil, X, Y) | ⇒ | cons(n, nil) |
| insert(n, cons(m, l), X, Y) | ⇒ | cons(X · n · m, insert(Y · n · m, l, X, Y)) |
| sort(nil, X, Y) | ⇒ | nil |
| sort(cons(n, l), X, Y) | ⇒ | insert(n, sort(l, X, Y), X, Y) |
| ascending_sort(l) | ⇒ | sort(l, λx:nat.λy:nat.min(x, y), λx:nat.λy:nat.max(x, y)) |
| descending_sort(l) | ⇒ | sort(l, λx:nat.λy:nat.max(x, y), λx:nat.λy:nat.min(x, y)) |