At:
dfs-properties
3
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
s: traversal(the_graph)
4.
i: Vertices(the_graph)
5.
s2: traversal(the_graph)
6.
(inl(i) 
s2) 
(inl(i) s) (inr(i) s)
7.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)
8.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
9.
paren(Vertices(the_graph);s2)
10.
dfs(the_obj;s;i) = (s2 @ s)
11.
s1: traversal(the_graph)
12.
j:Vertices(the_graph). (inr(j) s1) 
i-the_graph- > *j
13.
dfs(the_obj;s;i) = (s1 @ s)
14.
s': traversal(the_graph)
15.
(inr(i) s) (inl(i) s) s' = nil
16.
(inr(i) s) & (inl(i) s)
(
s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))
17.
dfs(the_obj;s;i) = (s' @ s)
18.
j: Vertices(the_graph)
19.
(inr(j) s2)
i-the_graph- > *j
By:
BackThruSomeHyp
Generated subgoal:
| 1 | (inr(j) s1) | 4 steps |
About:
