At:
topsort-properties
1
1
2
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
paren(Vertices(the_graph);depthfirst(the_obj))
4.
no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj))
5.
df-traversal(the_graph;depthfirst(the_obj))
6.
depthfirst-traversal(the_graph;depthfirst(the_obj))
7.
i:Vertices(the_graph). (inr(i) 
depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))
8.
non-trivial-loop-free(the_graph)
9.
i: Vertices(the_graph)
10.
j: Vertices(the_graph)
11.
i-the_graph- > *j
12.
i = j
13.
inl(i) before inl(j) depthfirst(the_obj)
i before j topsort(the_obj)
By:
((Unfold `topsort` 0) THEN (Unfold `mapoutl` 0)
THEN
(Inst
Thm* P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y L 
f(x) before f(y) mapfilter(f;P;L)
[Vertices(the_graph)+Vertices(the_graph);
x.isl(x);Vertices(the_graph);x.outl(x);depthfirst(the_obj);inl(i);inl(j)]))
THENA
(Auto THEN (All Reduce) THEN (Try ((Analyze -1) THEN Unhide THEN (Complete Auto))) THEN (Try (Analyze THEN (Reduce 0))))
THEN
Reduce -1
THEN
NthHyp -1
Generated subgoals:
None
About:
