(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:

119. 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:
listconsconsnilunioninlinr
universeequalimpliesandallexists

(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc