Nuprl - Proof: depthfirst member

PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

For any graph the_obj:GraphObject(the_graph), i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))

By: UnivCD THEN Inst Thm* For any graph the_obj:GraphObject(the_graph). L:V List. no_repeats(V;L) & (y:V. (y L)) & depthfirst(the_obj) = dfsl(the_obj;L) [the_graph;the_obj] THEN ExRepD THEN HypSubst -1 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 Unfold `l_all` -1 THEN InstHyp [i] -1 THEN EasyHyp

Generated subgoals:

None

About:

PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc