is mentioned by

Thm* l:AdjList. adjl_to_adjm(l) AdjMatrix	[adjl_to_adjm_wf]
Thm* m:AdjMatrix. adjm_to_adjl(m) AdjList	[adjm_to_adjl_wf]
Thm* A:AdjList, T:Type, s:T, f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. no_repeats(Vertices(adjl-graph(A));L) & (y:Vertices(adjl-graph(A)). (y L)) & adjl-vertex-accum(A;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)	[adjl-vertex-accum-properties]
Thm* A:AdjList, T:Type, s:T, f:(TVertices(adjl-graph(A))T). adjl-vertex-accum(A;s',x'.f(s',x');s) T	[adjl-vertex-accum_wf]
Thm* A:AdjList, T:Type, s:T, x:Vertices(adjl-graph(A)), f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. (y:Vertices(adjl-graph(A)). x-adjl-graph(A)- > y (y L)) & adjl-edge-accum(A;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L)	[adjl-edge-accum-properties]
Thm* A:AdjList, T:Type, s:T, x:Vertices(adjl-graph(A)), f:(TVertices(adjl-graph(A))T). adjl-edge-accum(A;s',x'.f(s',x');s;x) T	[adjl-edge-accum_wf]
Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y x = y	[assert_eq_adjl]
Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y	[eq_adjl_wf]
Thm* A:AdjList. adjl-graph(A) Graph	[adjl-graph_wf]
Thm* t:AdjList. t.out t.size(t.size List)	[adjl_out_wf]
Thm* t:AdjList. t.size	[adjl_size_wf]
Def AdjListRep == mkgraphrep(AdjList, A.adjl-graph(A), A.adjl-obj{\\\\v:l,i:l}(A))	[adjl-rep]

Try larger context: Graphs