| | Some definitions of interest. |
|
| adjm-graph | Def adjm-graph(A) == < vertices =  A.size, edges = {p:(A.size A.size)|  (A.adj(1of(p),2of(p))) }, incidence =  e.e > |
|
| adjm-vertex-accum | Def adjm-vertex-accum(M;s',x.f(s';x);s) == primrec(M.size;s;x,s'. f(s';x)) |
|
| adjm_size | Def t.size == 1of(t) |
| | | Thm*  t:AdjMatrix. t.size  |
|
| adjmatrix | Def AdjMatrix == size:size  size |
| | | Thm* AdjMatrix Type |
|
| gr_v | Def Vertices(t) == 1of(t) |
| | | Thm* t:Graph. Vertices(t) Type |
|
| int_seg | Def {i..j } == {k: | i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| l_member | Def (x l) ==  i:. i < ||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) 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' |
|
| 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 |
|
| primrec | Def primrec(n;b;c) == if n= 0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| | | Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T |
|
| upto | Def upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi (recursive) |
| | | Thm* i,j:. upto(i;j) {i..j} List |
