At:
dfs-dfl-traversal
3
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
L: Vertices(the_graph) List
4.
s: traversal(the_graph)
5.
x: Vertices(the_graph)
6.
dfl-traversal(the_graph;L;s)
7.
j:Vertices(the_graph). (inr(j) 
s) 
(inl(j) s) j-the_graph- > *x
8.
s': traversal(the_graph)
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.
j:Vertices(the_graph). (inr(j) s') x-the_graph- > *j
13.
dfs(the_obj;s;x) = (s' @ s)
14.
x-the_graph- > *x
15.
dfl-traversal(the_graph;L @ [x];s) dfl-traversal(the_graph;L @ [x];s' @ s)
dfl-traversal(the_graph;L @ [x];s)
By:
Using [`L2',L]
(BackThru
Thm* For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s))
THEN
BackThru
Thm* For any graph
A,B,C:V List. A-- > *C 
B-- > *C A @ B-- > *C
THEN
OrLeft
THEN
BackThru
Thm* For any graph
A,B:V List. B 
A A-- > *B
THEN
ObviousConcl
Generated subgoals:
None
About:
