Nuprl - Proof: topsort-properties 1 1 1

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

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

inl(i) before inl(j) depthfirst(the_obj)

By: InstHyp [i] -6 THEN ListMemD -1 THEN AllHyps (h.((Unfold `depthfirst-traversal` h) THEN (InstHyp [i;s1;s2;j] h)) THENA (Reduce 0))

Generated subgoals:

1 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) 1 step

2 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
j = i 1 step

3 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) 2 steps

About:

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

1	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)`	1 step

2	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` `j = i`	1 step

3	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)`	2 steps