PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: dfsl paren
For any graph the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L))
By:
UnivCD
THEN
Inst Thm* dfsl-induction2 [the_graph;the_obj;L,s. True;L]
Generated subgoals:

None

About:
listconsnilunionfunctionpropimpliesandtrueall

PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc