| | Some definitions of interest. |
|
| topsortl | Def topsortl(A;L) == mapoutl(dfsl(A;L)) |
| | | Thm* For any graph
 the_obj:GraphObject(the_graph), L:V List. topsortl(the_obj;L)  V 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 |
|
| dfsl-traversal | Def dfsl-traversal(the_graph;L;s) == df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s)   L-the_graph- > *i) & ((i:Vertices(the_graph). L-the_graph- > *i  non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ L2) ( s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1)  L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j))))) |
|
| 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'} |
|
| non-trivial-loop-free | Def non-trivial-loop-free(G) == i:Vertices(G). non-trivial-loop(G;i) |
|
| topsortedl | Def topsortedl(the_graph;L;s) == (i,j:Vertices(the_graph). j = i i-the_graph- > *j i before j s) & (i,j,k:Vertices(the_graph). k-the_graph- > *j k-the_graph- > *i (k':Vertices(the_graph). k' before k L k'-the_graph- > *i) i before j s) |
| | | Thm* For any graph
L,s:V List. topsortedl(the_graph;L;s) Prop |
|
| 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'} |
|
| l_member | Def (x l) == i: . i < ||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| no_repeats | Def no_repeats(T;l) == i,j:. i < ||l|| j < ||l|| i = j l[i] = l[j] T |
| | | Thm* T:Type, l:T List. no_repeats(T;l) Prop |
|
| paren | Def paren(T;s) == s = nil (T+T) List  (t:T, s':(T+T) List. s = ([inl(t)] @ s' @ [inr(t)]) & paren(T;s')) (s',s'':(T+T) List. ||s'|| < ||s|| & ||s''|| < ||s|| & s = (s' @ s'') & paren(T;s') & paren(T;s'')) (recursive) |
| | | Thm* T:Type, s:(T+T) List. paren(T;s) Prop |
