(11steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
topsort-properties
1
1
1
3
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.
(inl(j)
s2)
inl(i) before inl(j)
depthfirst(the_obj)
By:
HypSubst -2 0
THEN
RWO
Thm*
L:T List, x,y:T. x before y
L
(
L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3)) 0
THEN
ListMemD -1
THEN
HypSubst -1 0
THEN
Reduce 0
Generated subgoal:
1
19.
s3:
(Vertices(the_graph)+Vertices(the_graph)) List
20.
s2@0:
(Vertices(the_graph)+Vertices(the_graph)) List
21.
s2 = (s3 @ [inl(j) / s2@0])
L1,L2,L3:(Vertices(the_graph)+Vertices(the_graph)) List. (s1 @ [inl(i) / (s3 @ [inl(j) / s2@0])]) = (L1 @ [inl(i) / (L2 @ [inl(j) / L3])])
1
step
About:
(11steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc