t:AdjList. t.out 
t.size
(t.size List)t:AdjList. t.size 
size(size List) Type
} == {k:
| i 
k < j }m,n:. {m..n} Type| Some definitions of interest. | |
| adjl_out | Def t.out == 2of(t) |
| Thm* t:AdjList. t.out t.size(t.size List) | |
| adjl_size | Def t.size == 1of(t) |
| Thm* t:AdjList. t.size | |
| adjlist | Def AdjList == size:size(size List) |
| Thm* AdjList Type | |
| int_seg | Def {i..j} == {k:| i k < j } |
| Thm* m,n:. {m..n} Type |
About:
 |  |  |  |  |
 |  |  |  |  |