| | Some definitions of interest. |
|
| graphobj | 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)) |
| | | Thm* the_graph:Graph. GraphObject(the_graph) Type{i'} |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| l_member | Def (x l) == i: . i < ||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| no_repeats | Def no_repeats(T;l) == i,j:. i < ||l||  j < ||l||  i = j l[i] = l[j] T |
| | | Thm* T:Type, l:T List. no_repeats(T;l) Prop |
|
| bnot | Def  b == if b false else true fi |
| | | Thm* b:. b |
|
| edge | Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,y > |
| | | Thm* For any graph
x,y:V. x-the_graph- > y Prop |
|
| traversal | Def traversal(G) == (Vertices(G)+Vertices(G)) List |
| | | Thm* For any graph
Traversal Type |
|
| gr_v | Def Vertices(t) == 1of(t) |
| | | Thm* t:Graph. Vertices(t) Type |
|
| graph | Def Graph == v:Typee:Type(evv)Top |
| | | Thm* Graph Type{i'} |
|
| gro_eacc | Def t.eacc == 1of(2of(2of(t))) |
| | | Thm* For any graph
t:GraphObject(the_graph), T:Type. t.eacc (TVT)TVT |
|
| gro_eq | Def t.eq == 1of(t) |
| | | Thm* For any graph
t:GraphObject(the_graph). t.eq VV |
|
| vertex-count | Def vertex-count(the_obj;x.P(x)) == ||vertex-subset(the_obj;x.P(x))|| |
|
| gro_vacc | Def t.vacc == 1of(2of(2of(2of(2of(t))))) |
| | | Thm* For any graph
t:GraphObject(the_graph), T:Type. t.vacc (TVT)TT |
|
| iff | Def P Q == (P Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| nat | Def == {i: | 0 i } |
| | | Thm* Type |
|
| le | Def AB == B < A |
| | | Thm* i,j:. (ij) Prop |
|
| list_accum | Def list_accum(x,a.f(x;a);y;l) == Case of l; nil y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive) |
| | | Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T' |
|
| member-paren | Def member-paren(x,y.E(x;y);i;s) == (xs.InjCase(x; a. E(a;i), E(a;i))) |
|
| member-right-paren | Def member-right-paren(x,y.E(x;y);i;s) == (xs.InjCase(x; a. false, E(a;i))) |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
