PrintForm Definitions graph 1 3 Sections Graphs Doc

At: graphobj-properties
For any graph the_obj:GraphObject(the_graph). (x,y:V. the_obj.eq(x,y) x = y) & (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)) & (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L))
By:
RepeatFor 2 (Analyze 0)
THEN
RepeatFor 6 (Analyze -1)
THEN
Reduce 0
THEN
RepeatFor 2 ((Analyze 0) THEN (Try Trivial))
Generated subgoals:

None

About:
listassertapplyfunctionuniverseequalandallexists

PrintForm Definitions graph 1 3 Sections Graphs Doc