is mentioned by

Thm* n,k:, c:(nk). p:(k( List)). sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n & c((p(j))[x]) = j)	[finite-partition]
Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y	[connect]
Def paren(T;s) == s = nil (T+T) List (t:T, s':(T+T) List. s = ([inl(t)] @ s' @ [inr(t)]) & paren(T;s')) (s',s'':(T+T) List. ||s'|| < ||s|| & ||s''|| < ||s|| & s = (s' @ s'') & paren(T;s') & paren(T;s'')) (recursive)	[paren]
Def r- > L^k == n:. rn (G:({s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||). c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))	[arrows]

In prior sections: mb basic mb list 1 mb list 2 graph 1 1

Try larger context: Graphs