At:
dfs member
2
1
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
s: traversal(the_graph)
4.
i: Vertices(the_graph)
5.
s1: traversal(the_graph)
6.
s2: traversal(the_graph)
7.
s3: traversal(the_graph)
8.
i1: Vertices(the_graph)
9.
j: Vertices(the_graph)
10.
i1-the_graph- > j
11.
paren(Vertices(the_graph);s2)
12.
paren(Vertices(the_graph);s3)
13.
(inr(i1) 
s2)
(inl(i1) s3) 
(inl(i1) s2) (inl(i1) s1) (inr(i1) s1)
By:
FwdThru
Thm* 
s':(T+T) List. paren(T;s') 
(i:T. (inr(i) s') (inl(i) s'))
[-1]
THEN
ObviousFrom [-1]
Generated subgoals:
None
About:
