| | Who Cites topsort? |
|
| topsort | Def topsort(G) == mapoutl(depthfirst(G)) |
| | | Thm* For any graph
 the_obj:GraphObject(the_graph). topsort(the_obj)  V List |
|
| depthfirst | Def depthfirst(the_obj) == the_obj.vacc(( s,i. dfs(the_obj;s;i)),nil) |
| | | Thm* For any graph
the_obj:GraphObject(the_graph). depthfirst(the_obj) Traversal |
|
| mapoutl | Def mapoutl(s) == mapfilter(x.outl(x);x.isl(x);s) |
| | | Thm* A,B:Type, s:(A+B) List. mapoutl(s) A List |
|
| dfs | Def dfs(the_obj;s;i) == if member-paren(x,y.the_obj.eq(x,y);i;s) s else [inl(i) / (the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i))] fi (recursive) |
| | | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V. dfs(the_obj;s;i) Traversal |
|
| gro_vacc | Def t.vacc == 1of(2of(2of(2of(2of(t))))) |
| | | Thm* For any graph
t:GraphObject(the_graph), T:Type. t.vacc (T  VT)TT |
|
| isl | Def isl(x) == InjCase(x; y. true ; z. false) |
| | | Thm* A,B:Type, x:A+B. isl(x)  |
|
| outl | Def outl(x) == InjCase(x; y. y; z. "???") |
| | | Thm* A,B:Type, x:A+B. isl(x)   outl(x) A |
|
| mapfilter | Def mapfilter(f;P;L) == map(f;filter(P;L)) |
| | | Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List. mapfilter(f;P;L) T' List |
|
| 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 |
|
| member-paren | Def member-paren(x,y.E(x;y);i;s) == ( xs.InjCase(x; a. E(a;i), E(a;i))) |
|
| pi2 | Def 2of(t) == t.2 |
| | | Thm* A:Type, B:(AType), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
|
| 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 |
|
| map | Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] (recursive) |
| | | Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List |
| | | Thm* A,B:Type, f:(AB), l:A List . map(f;l) B List |
|
| 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)) |
|
| 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 |
|
| bor | Def p q == if p true else q fi |
| | | Thm* p,q:. (p q) |
