k:
. x:(k List)
{y:(k+1)| y greater-bounds x }
a:T, as:T List, i:
. 0<i 
i
||as|| (a.as)[i] = as[(i-1)]a:T, as:T List, i:. i0 (a.as)[i] = a| Theorem | Name |
| k:. x:(k List){y:(k+1)| y greater-bounds x } | [sfa_doc_find_small_greater_bound] |
| cites the following: | |
| a:T, as:T List, i:. 0<i i||as|| (a.as)[i] = as[(i-1)] | [select_cons_tl] |
| a:T, as:T List, i:. i0 (a.as)[i] = a | [select_cons_hd] |