is mentioned by

Thm* G:Graph. (x,y:Vertices(G). Dec(x = y)) (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s))	[paren-df-traversal]
Thm* s:(T+T) List. paren(T;s) no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))	[paren_interval]
Thm* s:(T+T) List. paren(T;s) (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2))	[paren_order1]
Thm* s',s3:(T+T) List. paren(T;s') paren(T;s3) paren(T;s3 @ s')	[append_paren]
Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s'))	[paren_balance2]
Thm* s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s'))	[paren_balance1]
Thm* P:(((T+T) List)Prop). P(nil) (s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s))	[paren_induction]
Def dfsl-traversal(the_graph;L;s) == df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s) L-the_graph- > *i) & ((i:Vertices(the_graph). L-the_graph- > *i non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ L2) (s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j)))))	[dfsl-traversal]

Try larger context: Graphs