PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: depthfirst paren
For any graph the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj))
By:
RepeatFor 2 (Analyze 0)
THEN
Inst Thm* depthfirst_induction2 [the_graph;the_obj;s. True]
Generated subgoals:

None

About:
nilunionfunctionpropimpliesandtrueall

PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc