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* 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]
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]
Thm* For any graph the_obj:GraphObject(the_graph), L:V List. (i:V. (i L)) (non-trivial-loop-free(the_graph) topsortedl(the_graph;L;topsortl(the_obj;L))) & (i:V. (i topsortl(the_obj;L))) & no_repeats(V;topsortl(the_obj;L))	[topsortl-properties]
Thm* For any graph the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:V. (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))	[dfsl-properties]
Thm* For any graph the_obj:GraphObject(the_graph), L:V List, s:Traversal, x:V. dfl-traversal(the_graph;L;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x))	[dfs-dfl-traversal]
Thm* For any graph the_obj:GraphObject(the_graph). L:V List. (non-trivial-loop-free(the_graph) topsorted(the_graph;L)) & (i:V. (i L)) & no_repeats(V;L)	[topsort-exists]
Thm* For any graph the_obj:GraphObject(the_graph). (non-trivial-loop-free(the_graph) topsorted(the_graph;topsort(the_obj))) & (i:V. (i topsort(the_obj))) & no_repeats(V;topsort(the_obj))	[topsort-properties]
Thm* For any graph the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & df-traversal(the_graph;depthfirst(the_obj)) & depthfirst-traversal(the_graph;depthfirst(the_obj)) & (i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)))	[depthfirst-properties]
Thm* For any graph the_obj:GraphObject(the_graph). df-traversal(the_graph;depthfirst(the_obj))	[depthfirst-df-traversal]
Thm* For any graph the_obj:GraphObject(the_graph), i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))	[depthfirst_member]
Thm* For any graph the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj))	[depthfirst_paren]
Thm* For any graph the_obj:GraphObject(the_graph), P:(TraversalProp). P(nil) (s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(s) P(dfs(the_obj;s;i))) paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & P(depthfirst(the_obj))	[depthfirst_induction2]
Thm* For any graph the_obj:GraphObject(the_graph), P:(TraversalProp). P(nil) (s:Traversal, i:V. P(s) P(dfs(the_obj;s;i))) P(depthfirst(the_obj))	[depthfirst_induction]
Thm* For any graph the_obj:GraphObject(the_graph). L:V List. no_repeats(V;L) & (y:V. (y L)) & depthfirst(the_obj) = dfsl(the_obj;L)	[depthfirst-dfsl]
Thm* For any graph the_obj:GraphObject(the_graph), L:V List. (iL.(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))	[dfsl_member]
Thm* For any graph the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L))	[dfsl_paren]
Thm* For any graph the_obj:GraphObject(the_graph), P:((V List)TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & P(L,dfsl(the_obj;L)))	[dfsl-induction2]
Thm* For any graph the_obj:GraphObject(the_graph), P:((V List)TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. P(L,dfsl(the_obj;L)))	[dfsl-induction1]
Thm* For any graph the_obj:GraphObject(the_graph). depthfirst(the_obj) Traversal	[depthfirst_wf]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. df-traversal(the_graph;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;dfs(the_obj;s;i))	[dfs-df-traversal]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s) (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) (k:V. (inr(k) s2) j-the_graph- > *k) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inr(i) s1) (inl(i) s1) paren(V;s2) l_disjoint(V+V;s2;s1) no_repeats(V+V;s2) (j:V. (inr(j) s2) i-the_graph- > *j) (j:V. i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction4]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. ((inr(i) s) (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)	[dfs-properties]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)	[dfs-connect]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. ((inr(i) s) (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & dfs(the_obj;s;i) = (s' @ s)	[dfs-cases]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s1,s2:Traversal, i:V. P(i,s1,s2) l_disjoint(V+V;s2;s1) & no_repeats(V+V;s2)) (s:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s1) (j:V. i-the_graph- > j j = i (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction3]
Thm* For any graph the_obj:GraphObject(the_graph), l:V List, s:Traversal. s':Traversal. (i:V. (i l) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & list_accum(s',j.dfs(the_obj;s';j);s;l) = (s' @ s)	[dfs_accum_member]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. (inl(i) s') (inl(i) s) (inr(i) s) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & dfs(the_obj;s;i) = (s' @ s)	[dfs_member]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s) (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inl(i) s1) (inr(i) s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction2]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s1,s2:Traversal, i:V. P(i,s1,s2) l_disjoint(V+V;s2;s1) & no_repeats(V+V;s2)) (s:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. dfs(the_obj;s;i) Traversal	[dfs_wf]
Thm* For any graph the_obj:GraphObject(the_graph). M:(Traversal). (i:V, s:Traversal. M([inl(i) / s])M(s)) & (i:V, s:Traversal. member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s))	[dfs-measure]
Thm* For any graph the_obj:GraphObject(the_graph), x,y:V. Dec(x = y)	[decidable__equal_gr_v]
Thm* For any graph the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) (x:V. P(x) & Q(x)) vertex-count(the_obj;x.P(x)) < vertex-count(the_obj;x.Q(x))	[vertex-count-less]
Thm* For any graph the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) vertex-count(the_obj;x.P(x))vertex-count(the_obj;x.Q(x))	[vertex-count-le]
Thm* For any graph the_obj:GraphObject(the_graph), P:(V). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x vertex-subset(the_obj;x.P(x))) P(x))	[vertex-subset-properties]
Thm* For any graph the_obj:GraphObject(the_graph), P:(V). vertex-subset(the_obj;x.P(x)) V List	[vertex-subset_wf]
Thm* For any graph the_obj:GraphObject(the_graph). (x,y:V. the_obj.eq(x,y) x = y) & (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)) & (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L))	[graphobj-properties]
Thm* t:Graph Representation. t.obj r:t.typeGraphObject(t.graph(r))	[grr_obj_wf]
Thm* t:Graph Representation. t.graph t.typeGraph	[grr_graph_wf]
Thm* t:Graph Representation. t.type Type	[grr_type_wf]
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)	[mkgraphobj_wf]
Thm* For any graph t:GraphObject(the_graph). t.other Top	[gro_other_wf]
Thm* For any graph t:GraphObject(the_graph). t.vaccw (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & t.vacc(f,s) = list_accum(s',x'.f(s',x');s;L))	[gro_vaccw_wf]
Thm* For any graph t:GraphObject(the_graph), T:Type. t.vacc (TVT)TT	[gro_vacc_wf]
Thm* For any graph t:GraphObject(the_graph). t.eaccw (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & t.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))	[gro_eaccw_wf]
Thm* For any graph t:GraphObject(the_graph), T:Type. t.eacc (TVT)TVT	[gro_eacc_wf]
Thm* For any graph t:GraphObject(the_graph). t.eqw (x,y:V. t.eq(x,y) x = y)	[gro_eqw_wf]
Thm* For any graph t:GraphObject(the_graph). t.eq VV	[gro_eq_wf]
Thm* the_graph:Graph. GraphObject(the_graph) Type{i'}	[graphobj_wf]
Def For any graph representationP(the_graph;the_obj) == R:Graph Representation, r:R.type. P(R.graph(r);R.obj(r))	[allgrep]
Def GraphObject(the_graph) == eq:Vertices(the_graph)Vertices(the_graph)(x,y:Vertices(the_graph). (eq(x,y)) x = y)(eacc:(T:Type. (TVertices(the_graph)T)TVertices(the_graph)T)(T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))(vacc:(T:Type. (TVertices(the_graph)T)TT)(T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L))Top))	[graphobj]

In prior sections: core well fnd int 1 bool 1 sqequal 1 prog 1 fun 1 int 2 list 1 union rel 1 mb basic mb nat mb list 1 num thy 1 mb list 2 graph 1 1 graph 1 2

Try larger context: Graphs