Who Cites adjm-rep?
adjm-rep	Def adjm-rep{\\\\v:l,i:l}() == mkgraphrep(AdjMatrix, M.adjm-graph(M), M.adjm-obj{\\\\v:l,i:l}(M))
adjm-obj	Def adjm-obj{\\\\v:l,i:l}(M) == mkgraphobj(x,y. x =M= y, ext{assert_eq_adjm}(M), f,s,x. adjm-edge-accum(M;s',x'.f(s',x');s;x), ext{adjm_DASH_edge_DASH_accum_DASH_properties}{i:l}(M), f,s. adjm-vertex-accum(M;s',x'.f(s',x');s), ext{adjm_DASH_vertex_DASH_accum_DASH_properties}{i:l}(M), )
adjm-graph	Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e >
adjmatrix	Def AdjMatrix == size:sizesize
	Thm* AdjMatrix Type
mkgraphrep	Def mkgraphrep(type, graph, obj) == < type,graph,obj >
	Thm* type:Type, graph:(typeGraph), obj:(r:typeGraphObject(graph(r))). mkgraphrep(type, graph, obj) Graph Representation
adjm-vertex-accum	Def adjm-vertex-accum(M;s',x.f(s';x);s) == primrec(M.size;s;x,s'. f(s';x))
adjm-edge-accum	Def adjm-edge-accum(M;s',x'.f(s';x');s;x) == primrec(M.size;s;y,s'. if M.adj(x,y) f(s';y) else s' fi)
eq_adjm	Def x =M= y == x=y
	Thm* M:AdjMatrix, x,y:Vertices(adjm-graph(M)). x =M= y
mkgraphobj	Def mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other) == < eq,eqw,eacc,eaccw,vacc,vaccw,other >
	Thm* For any graph eq:(VV), eqw:(x,y:V. eq(x,y) x = y), eacc:(T:Type. (TVT)TVT), eaccw:(T:Type, s:T, x:V, f:(TVT). 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. (TVT)TT), vaccw:(T:Type, s:T, f:(TVT). 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)
adjm_adj	Def t.adj == 2of(t)
	Thm* t:AdjMatrix. t.adj t.sizet.size
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
adjm_size	Def t.size == 1of(t)
	Thm* t:AdjMatrix. t.size
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
assert	Def b == if b True else False fi
	Thm* b:. b Prop
int_seg	Def {i..j} == {k:| i k < j }
	Thm* m,n:. {m..n} Type
mkgraph	Def < vertices = v, edges = e, incidence = f > == < v,e,f,o >
	Thm* v,e:Type, f:(evv), o:Top. < vertices = v, edges = e, incidence = f > Graph
nat	Def == {i:| 0i }
	Thm* Type
primrec	Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive)
	Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
lelt	Def i j < k == ij & j < k
le	Def AB == B < A
	Thm* i,j:. (ij) Prop
not	Def A == A False
	Thm* A:Prop. (A) Prop

Syntax:

adjm-rep{\\\\v:l,i:l}()

has structure:

adjm-rep{\\v:l,i:l}

About: