At:
dfs accum member
2
2
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
l: Vertices(the_graph) List
4.
u: Vertices(the_graph)
5.
v: Vertices(the_graph) List
6.
s:traversal(the_graph).
s':traversal(the_graph).
(i:Vertices(the_graph). (i 
v) 
(inl(i) s') 
(inl(i) s) (inr(i) s))
& l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s)
& no_repeats(Vertices(the_graph)+Vertices(the_graph);s')
& paren(Vertices(the_graph);s')
& list_accum(s',j.dfs(the_obj;s';j);s;v) = (s' @ s)
7.
s: traversal(the_graph)
8.
s1: traversal(the_graph)
9.
(inl(u) s1) (inl(u) s) (inr(u) s)
10.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s1;s)
11.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s1)
12.
paren(Vertices(the_graph);s1)
13.
dfs(the_obj;s;u) = (s1 @ s)
14.
s': traversal(the_graph)
15.
i:Vertices(the_graph).
(i v) (inl(i) s') (inl(i) dfs(the_obj;s;u)) (inr(i) dfs(the_obj;s;u))
16.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';dfs(the_obj;s;u))
17.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s')
18.
paren(Vertices(the_graph);s')
19.
list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s;u);v) = (s' @ dfs(the_obj;s;u))
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s' @ s1;s)
By:
RWO
Thm* a,b,c:T List. l_disjoint(T;a @ b;c) 
l_disjoint(T;a;c) & l_disjoint(T;b;c)
0
THEN
SubstFor dfs(the_obj;s;u) -4
THEN
RWO
Thm* a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b)
-4
Generated subgoals:
None
About:
