| | Who Cites adjl to adjm? |
|
| adjl_to_adjm | Def adjl_to_adjm(l) == Case(l) Case mk_adjlist(n; out ) = > mk_adjmatrix(n,  i,j. ( k out(i).k= j)) |
| | | Thm*  l:AdjList. adjl_to_adjm(l) AdjMatrix |
|
| eq_int | Def i=j == if i=j true ; false fi |
| | | Thm* i,j: . (i=j)  |
|
| l_bexists | Def (xL.P(x)) == reduce(x,b. P(x)  b;false;L) |
| | | Thm* T:Type, L:T List, P:(T  ). (xL.P(x)) |
|
| mk_adjmatrix | Def mk_adjmatrix(size, adj) == < size,adj > |
| | | Thm* size: , adj:(sizesize). mk_adjmatrix(size, adj) AdjMatrix |
|
| case_mk_adjlist | Def Case mk_adjlist(size; out ) = > body(size;out)(x,z) == x/x2,x1. body(x2;x1) |
|
| case | Def Case(value) body == body(value,value) |
|
| bor | Def p q == if p true else q fi |
| | | Thm* p,q:. (p q) |
|
| 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 |
