| | Who Cites adjm to adjl? |
|
| adjm_to_adjl | Def adjm_to_adjl(m) == Case(m) Case mk_adjmatrix(n,f) = > mk_adjlist(n,  i.filter(j.f(i,j);upto(0;n))) |
| | | Thm*  m:AdjMatrix. adjm_to_adjl(m)  AdjList |
|
| 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 |
|
| filter | Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l) |
| | | Thm* T:Type, P:(T   ), l:T List. filter(P;l) T List |
|
| mk_adjlist | Def mk_adjlist(size, out) == < size,out > |
| | | Thm* size:, out:(size(size List)). mk_adjlist(size, out) AdjList |
|
| case_mk_adjmatrix | Def Case mk_adjmatrix(size,adj) = > body(size;adj)(x,z) == x/x2,x1. body(x2;x1) |
|
| case | Def Case(value) body == body(value,value) |
|
| lt_int | Def i < j == if i < j true ; false fi |
| | | Thm* i,j: . (i < j) |
|
| reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
| | | Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |
