Who Cites adjl-obj?
adjl-obj	Def adjl-obj{\\\\v:l,i:l}(A) == mkgraphobj(x,y. x =A= y, ext{assert_eq_adjl}(A), f,s,x. adjl-edge-accum(A;s',x'.f(s',x');s;x), ext{adjl_DASH_edge_DASH_accum_DASH_properties}{i:l}(A), f,s. adjl-vertex-accum(A;s',x'.f(s',x');s), ext{adjl_DASH_vertex_DASH_accum_DASH_properties}{i:l}(A), )
adjl-vertex-accum	Def adjl-vertex-accum(A;s',x.f(s';x);s) == primrec(A.size;s;x,s'. f(s';x))
adjl-edge-accum	Def adjl-edge-accum(A;s',x'.f(s';x');s;x) == list_accum(s',x'.f(s';x');s;A.out(x))
eq_adjl	Def x =A= y == x=y
	Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= 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)
adjl_size	Def t.size == 1of(t)
	Thm* t:AdjList. t.size
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
adjl_out	Def t.out == 2of(t)
	Thm* t:AdjList. t.out t.size(t.size List)
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'
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))

Syntax:

adjl-obj{\\\\v:l,i:l}(A)

has structure:

adjl-obj{\\v:l,i:l}(A)

About: