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

At: dfsl-properties 3
1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. L: Vertices(the_graph) List
4. L:Vertices(the_graph) List. paren(Vertices(the_graph);dfsl(the_obj;L)) & no_repeats(Vertices(the_graph)+Vertices(the_graph);dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L))
paren(Vertices(the_graph);dfsl(the_obj;L)) & no_repeats(Vertices(the_graph)+Vertices(the_graph);dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:Vertices(the_graph). (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))
By:
Fold `l_all` 0
THEN
Inst Thm* For any graph the_obj:GraphObject(the_graph), L:V List. (iL.(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))) [the_graph;the_obj;L]
THEN
InstHyp [L] -2
Generated subgoals:

None

About:
listunioninlinrimpliesandall

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