| | Some definitions of interest. |
|
| append | Def as @ bs == Case of as; nil  bs ; a.as' [a / (as' @ bs)] (recursive) |
| | | Thm*  T:Type, as,bs:T List. (as @ bs)  T List |
|
| dfsl | Def dfsl(G;L) == list_accum(s,i.dfs(G;s;i);nil;L) |
| | | Thm* For any graph
the_obj:GraphObject(the_graph), L:V List. dfsl(the_obj;L) 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 |
|
| graphobj | Def GraphObject(the_graph) == eq:Vertices(the_graph)  Vertices(the_graph)  (x,y:Vertices(the_graph).  (eq(x,y))   x = y)(eacc:( T:Type. (TVertices(the_graph)T)TVertices(the_graph)T)(T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T).  L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))(vacc:(T:Type. (TVertices(the_graph)T)TT)(T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L))Top)) |
| | | Thm* the_graph:Graph. GraphObject(the_graph) Type{i'} |
|
| traversal | Def traversal(G) == (Vertices(G)+Vertices(G)) List |
| | | Thm* For any graph
Traversal Type |
|
| gr_v | Def Vertices(t) == 1of(t) |
| | | Thm* t:Graph. Vertices(t) Type |
|
| graph | Def Graph == v:Typee:Type(evv)Top |
| | | Thm* Graph Type{i'} |
|
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | | Thm* A:Type, l:A List. ||l||  |
| | | Thm* ||nil|| |
|
| 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' |
|
| nat | Def  == {i:| 0 i } |
| | | Thm* Type |
|
| not | Def  A == A  False |
| | | Thm* A:Prop. (A) Prop |
|
| null | Def null(as) == Case of as; nil true ; a.as' false |
| | | Thm* T:Type, as:T List. null(as) |
| | | Thm* null(nil) |
