| | Some definitions of interest. |
|
| adjl-graph | Def adjl-graph(G) == < vertices =  G.size, edges = x:G.size ||G.out(x)||, incidence =  e. < 1of(e),(G.out(1of(e)))[2of(e)] > > |
|
| adjl-vertex-accum | Def adjl-vertex-accum(A;s',x.f(s';x);s) == primrec(A.size;s;x,s'. f(s';x)) |
|
| adjl_size | Def t.size == 1of(t) |
| | | Thm*  t:AdjList. t.size  |
|
| adjlist | Def AdjList == size:size  (size List) |
| | | Thm* AdjList 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 |
