At:
depthfirst-df-traversal
4
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
s: traversal(the_graph)
4.
i: Vertices(the_graph)
5.
df-traversal(the_graph;s)
6.
paren(Vertices(the_graph);s)
7.
s': traversal(the_graph)
8.
(inl(i) 
s') 
(inl(i) s) (inr(i) s)
9.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s)
10.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s')
11.
paren(Vertices(the_graph);s')
12.
dfs(the_obj;s;i) = (s' @ s)
paren(Vertices(the_graph);s' @ s)
By:
BackThru
Thm* 
s',s3:(T+T) List. paren(T;s') 
paren(T;s3) paren(T;s3 @ s')
Generated subgoals:
None
About:
