is mentioned by

Thm* For any graph A,B,C:V List. A-- > *C B-- > *C A @ B-- > *C	[list-list-connect-append2]
Thm* For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i	[list-connect-append]
Thm* For any graph (x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y))	[connect-iff]
Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s))	[assert-member-paren]
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]

In prior sections: core bool 1 int 2 rel 1 num thy 1 list 1 sqequal 1 prog 1 mb nat mb list 1 mb list 2 graph 1 1

Try larger context: Graphs