is mentioned by

Thm* l:AdjList. adjl_to_adjm(l) AdjMatrix	[adjl_to_adjm_wf]
Thm* m:AdjMatrix. adjl-graph(adjm_to_adjl(m)) adjm-graph(m)	[adjm_to_adjl_graph]
Thm* m:AdjMatrix. adjm_to_adjl(m) AdjList	[adjm_to_adjl_wf]
Thm* M:AdjMatrix, T:Type, s:T, x:Vertices(adjm-graph(M)), f:(TVertices(adjm-graph(M))T). L:Vertices(adjm-graph(M)) List. (y:Vertices(adjm-graph(M)). x-adjm-graph(M)- > y (y L)) & adjm-edge-accum(M;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L)	[adjm-edge-accum-properties]
Thm* M:AdjMatrix, T:Type, s:T, x:Vertices(adjm-graph(M)), f:(TVertices(adjm-graph(M))T). adjm-edge-accum(M;s',x'.f(s',x');s;x) T	[adjm-edge-accum_wf]
Thm* M:AdjMatrix, T:Type, s:T, f:(TVertices(adjm-graph(M))T). L:Vertices(adjm-graph(M)) List. no_repeats(Vertices(adjm-graph(M));L) & (y:Vertices(adjm-graph(M)). (y L)) & adjm-vertex-accum(M;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)	[adjm-vertex-accum-properties]
Thm* M:AdjMatrix, T:Type, s:T, f:(TVertices(adjm-graph(M))T). adjm-vertex-accum(M;s',x'.f(s',x');s) T	[adjm-vertex-accum_wf]
Thm* M:AdjMatrix, x,y:Vertices(adjm-graph(M)). x =M= y x = y	[assert_eq_adjm]
Thm* t:AdjMatrix. t.adj t.sizet.size	[adjm_adj_wf]
Thm* t:AdjMatrix. t.size	[adjm_size_wf]
Def adjm-rep{\\\\v:l,i:l}() == mkgraphrep(AdjMatrix, M.adjm-graph(M), M.adjm-obj{\\\\v:l,i:l}(M))	[adjm-rep]

Try larger context: Graphs