| | Who Cites depthfirst? |
|
| 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 |
|
| 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 |
|
| 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 |
|
| 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)) |
|
| 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 |
