n:
, x,y:n. x before y 
upto(n) 
x<ym:, n:m. upto(m)[n] = nn:. ||upto(n)|| ~ n| Rank | Theorem | Name |
| 3 | n:, x,y:n. x before y upto(n) x<y | [before-upto] |
| cites the following: | ||
| 2 | m:, n:m. upto(m)[n] = n | [select_upto] |
| 1 | n:. ||upto(n)|| ~ n | [length_upto] |