At:
mkgraphobj wf
For any graph
eq:(V
V

), eqw:(
x,y:V. eq(x,y) 
x = y), eacc:(
T:Type. (T
V
T)
T
V
T), eaccw:(
T:Type, s:T, x:V, f:(T
V
T).
L:V List. (
y:V. x-the_graph- > y 
(y
L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)), vacc:(
T:Type. (T
V
T)
T
T), vaccw:(
T:Type, s:T, f:(T
V
T).
L:V List. no_repeats(V;L) & (
y:V. (y
L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L)), other:Top. mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other)
GraphObject(the_graph)
By:
Unfolds [`graphobj`;`mkgraphobj`] 0
THEN
AllHyps (
h.IsectHD T h)
Generated subgoals:
None
About: