Who Cites allgrep?
allgrep	Def For any graph representationP(the_graph;the_obj) == R:Graph Representation, r:R.type. P(R.graph(r);R.obj(r))
	Thm* P:(g:GraphGraphObject(g)Prop{i}). allgrep{i:l}(the_graph,the_obj.P(the_graph,the_obj)) Prop{i'}
grr_obj	Def t.obj == 2of(2of(t))
	Thm* t:Graph Representation. t.obj r:t.typeGraphObject(t.graph(r))
grr_graph	Def t.graph == 1of(2of(t))
	Thm* t:Graph Representation. t.graph t.typeGraph
grr_type	Def t.type == 1of(t)
	Thm* t:Graph Representation. t.type Type
graphrep	Def Graph Representation == type:Typegraph:typeGraphr:typeGraphObject(graph(r))
	Thm* Graph Representation Type{i'}
graphobj	Def GraphObject(the_graph) == eq:Vertices(the_graph)Vertices(the_graph)(x,y:Vertices(the_graph). (eq(x,y)) x = y)(eacc:(T:Type. (TVertices(the_graph)T)TVertices(the_graph)T)(T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))(vacc:(T:Type. (TVertices(the_graph)T)TT)(T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L))Top))
	Thm* the_graph:Graph. GraphObject(the_graph) Type{i'}
edge	Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,y >
	Thm* For any graph x,y:V. x-the_graph- > y Prop
gr_f	Def Incidence(t) == 1of(2of(2of(t)))
	Thm* t:Graph. Incidence(t) Edges(t)Vertices(t)Vertices(t)
gr_e	Def Edges(t) == 1of(2of(t))
	Thm* t:Graph. Edges(t) Type
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
gr_v	Def Vertices(t) == 1of(t)
	Thm* t:Graph. Vertices(t) Type
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
graph	Def Graph == v:Typee:Type(evv)Top
	Thm* Graph Type{i'}
top	Def Top == Void given Void
	Thm* Top Type
list_accum	Def list_accum(x,a.f(x;a);y;l) == Case of l; nil y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive)
	Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T'
l_member	Def (x l) == i:. i < ||l|| & x = l[i] T
	Thm* T:Type, x:T, l:T List. (x l) Prop
no_repeats	Def no_repeats(T;l) == i,j:. i < ||l|| j < ||l|| i = j l[i] = l[j] T
	Thm* T:Type, l:T List. no_repeats(T;l) Prop
iff	Def P Q == (P Q) & (P Q)
	Thm* A,B:Prop. (A B) Prop
assert	Def b == if b True else False fi
	Thm* b:. b Prop
select	Def l[i] == hd(nth_tl(i;l))
	Thm* A:Type, l:A List, n:. 0n n < ||l|| l[n] A
length	Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
nat	Def == {i:| 0i }
	Thm* Type
le	Def AB == B < A
	Thm* i,j:. (ij) Prop
not	Def A == A False
	Thm* A:Prop. (A) Prop
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop
nth_tl	Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi (recursive)
	Thm* A:Type, as:A List, i:. nth_tl(i;as) A List
hd	Def hd(l) == Case of l; nil "?" ; h.t h
	Thm* A:Type, l:A List. ||l||1 hd(l) A
	Thm* A:Type, l:A List. hd(l) A
tl	Def tl(l) == Case of l; nil nil ; h.t t
	Thm* A:Type, l:A List. tl(l) A List
le_int	Def ij == j < i
	Thm* i,j:. (ij)
lt_int	Def i < j == if i < j true ; false fi
	Thm* i,j:. (i < j)
bnot	Def b == if b false else true fi
	Thm* b:. b

Syntax:

For any graph representation P(the_graph;the_obj)

has structure:

allgrep{i:l}(the_graph,the_obj.P(the_graph;the_obj))

About: