At:
dfs-df-traversal
1
2
1
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.
j:Vertices(the_graph). (inr(j) 
s) 
(inl(j) s) j-the_graph- > *i
7.
s1: traversal(the_graph)
8.
s2: traversal(the_graph)
9.
s3: traversal(the_graph)
10.
i1: Vertices(the_graph)
11.
j: Vertices(the_graph)
12.
i1-the_graph- > j
13.
paren(Vertices(the_graph);s2)
14.
k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k
15.
paren(Vertices(the_graph);s3)
16.
df-traversal(the_graph;s2 @ s1)
(j:Vertices(the_graph). (inr(j) s2 @ s1) (inl(j) s2 @ s1) j-the_graph- > *i1)
df-traversal(the_graph;s3 @ s2 @ s1)
17.
df-traversal(the_graph;s1)
18.
j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i1
19.
df-traversal(the_graph;s2 @ s1)
20.
j1: Vertices(the_graph)
21.
(inr(j1) s2)
22.
(inl(j1) s2 @ s1)
j1-the_graph- > *i1
By:
Analyze -1
THEN
RWO
Thm* x:T, l1,l2:T List. (x l1 @ l2) 
(x l1) 
(x l2)
0
THEN
OrLeft
Generated subgoal:
| 1 | (inl(j1) s2) | 1 step |
About:
