Nuprl - graph_1_3 Citations of bool

Def

== Unit+Unit

is mentioned by

Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y [eq_adjl_wf]

Thm* t:AdjMatrix. t.adj t.sizet.size [adjm_adj_wf]

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 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.eq VV [gro_eq_wf]

Def AdjMatrix == size:sizesize [adjmatrix]

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: bool 1 sqequal 1 list 1 rel 1 mb basic mb nat mb list 1 mb list 2 graph 1 1 graph 1 2 prog 1

Try larger context: Graphs

graph 1 3 Sections Graphs Doc

`Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y`	[eq_adjl_wf]
`Thm* t:AdjMatrix. t.adj t.sizet.size`	[adjm_adj_wf]
`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 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.eq VV`	[gro_eq_wf]
`Def AdjMatrix == size:sizesize`	[adjmatrix]
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]