x1,x2:T, L1,L2:T List.
Thm* [x1 / L1]
[x2 / L2] 
x1 = x2 & L1 L2 
[x1 / L1] L2k:
, f:(k
), x:k. increasing(f;k) 
f(0)+x
f(x)a:T, as:T List, i:. i0 [a / as][i] = aa:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)]| Theorem | Name |
| x1,x2:T, L1,L2:T List.
Thm* [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 | [cons_sublist_cons] |
| cites the following: | |
| k:, f:(k), x:k. increasing(f;k) f(0)+xf(x) | [increasing_lower_bound] |
| a:T, as:T List, i:. i0 [a / as][i] = a | [select_cons_hd] |
| a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |