(16steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: dfs accum member 1
1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. l: Vertices(the_graph) List
4. s: traversal(the_graph)
s':traversal(the_graph). (i:Vertices(the_graph). (i nil) (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') & s = (s' @ s) traversal(the_graph)
By:
InstConcl [nil]
THEN
Reduce 0
Generated subgoals:

15. i: Vertices(the_graph)
6. (i nil)
(inl(i) nil) (inl(i) s) (inr(i) s)		1 step
 
2 l_disjoint(Vertices(the_graph)+Vertices(the_graph);nil;s)1 step
 
3 no_repeats(Vertices(the_graph)+Vertices(the_graph);nil)1 step
 
4 paren(Vertices(the_graph);nil)1 step

About:
listnilunioninlinrequal
impliesandorall
exists

(16steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc