WhoCites
Definitions
graph
1
3
Sections
Graphs
Doc
Who Cites gro
eaccw?
gro_eaccw
Def t.eaccw == 1of(2of(2of(2of(t))))
Thm*
For any graph
t:GraphObject(the_graph). t.eaccw
(
T:Type, s:T, x:V, f:(T
V
T).
L:V List. (
y:V. x-the_graph- > y
(y
L)) & t.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 2of(p)
B(1of(p))
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
Syntax:
t.eaccw
has structure:
gro_eaccw(t)
About:
WhoCites
Definitions
graph
1
3
Sections
Graphs
Doc