At:
topsort-properties
1
1
1
1
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.
i:Vertices(the_graph), s1,s2:traversal(the_graph).
(j:Vertices(the_graph). i-the_graph- > *j 
non-trivial-loop(the_graph;j))
depthfirst(the_obj) = (s1 @ [inl(i)] @ s2)
(j:Vertices(the_graph). j = i i-the_graph- > *j (inl(j) 
s2))
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.
(inr(i) depthfirst(the_obj))
14.
(inl(i) depthfirst(the_obj))
15.
s1: (Vertices(the_graph)+Vertices(the_graph)) List
16.
s2: (Vertices(the_graph)+Vertices(the_graph)) List
17.
depthfirst(the_obj) = (s1 @ [inl(i) / s2]) (Vertices(the_graph)+Vertices(the_graph)) List
18.
j1: Vertices(the_graph)
19.
i-the_graph- > *j1
non-trivial-loop(the_graph;j1)
By:
AllHyps (
h.(Unfold `non-trivial-loop-free` h) THEN (BackThru h))
Generated subgoals:
None
About:
