At:
depthfirst-properties
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
i:Vertices(the_graph). (inr(i) 
depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))
4.
paren(Vertices(the_graph);depthfirst(the_obj))
5.
no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj))
6.
df-traversal(the_graph;depthfirst(the_obj))
7.
x: Vertices(the_graph)
8.
y: Vertices(the_graph)
Dec(x = y)
By:
Using [`the_obj',the_obj]
(BackThru
Thm* For any graph
the_obj:GraphObject(the_graph), x,y:V. Dec(x = y))
Generated subgoals:
None
About:
