is mentioned by

Thm* m:AdjMatrix. adjl-graph(adjm_to_adjl(m)) adjm-graph(m)	[adjm_to_adjl_graph]
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]
Def AdjListRep == mkgraphrep(AdjList, A.adjl-graph(A), A.adjl-obj{\\\\v:l,i:l}(A))	[adjl-rep]

Try larger context: Graphs