(19steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: dfsl-traversal-append 1 1
1. the_graph: Graph
2. L1: Vertices(the_graph) List
3. L2: Vertices(the_graph) List
4. s: traversal(the_graph)
5. L1-the_graph- > *L2
6. df-traversal(the_graph;s)
7. i:Vertices(the_graph). (inl(i) s) L1-the_graph- > *i
8. i:Vertices(the_graph). L1 @ L2-the_graph- > *i non-trivial-loop(the_graph;i)
9. L1@0,L2:Vertices(the_graph) List. L1 = (L1@0 @ L2) (s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1@0-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1@0-the_graph- > *j)))
10. L1@0: Vertices(the_graph) List
11. L2@0: Vertices(the_graph) List
12. (L1 @ L2) = (L1@0 @ L2@0)
13. e: Vertices(the_graph) List
14. L1 = (L1@0 @ e)
15. L2@0 = (e @ L2)
s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1@0-the_graph- > *j) & ((inl(j) s2) L2@0-the_graph- > *j & L1@0-the_graph- > *j))
By:
HypSubst -1 0
THEN
RWO Thm* For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i 0
THEN
InstHyp [L1@0;e] 9
THEN
RepeatFor 7 (ParallelOp -1)
Generated subgoals:

116. s1: traversal(the_graph)
17. s2: traversal(the_graph)
18. j:Vertices(the_graph). ((inl(j) s1) L1@0-the_graph- > *j) & ((inl(j) s2) e-the_graph- > *j & L1@0-the_graph- > *j)
19. j: Vertices(the_graph)
20. (inl(j) s2)
21. e-the_graph- > *j
22. L1@0-the_graph- > *j
e-the_graph- > *j L2-the_graph- > *j		1 step
 
216. s1: traversal(the_graph)
17. s2: traversal(the_graph)
18. j:Vertices(the_graph). ((inl(j) s1) L1@0-the_graph- > *j) & ((inl(j) s2) e-the_graph- > *j & L1@0-the_graph- > *j)
19. j: Vertices(the_graph)
20. e-the_graph- > *j L2-the_graph- > *j
21. L1@0-the_graph- > *j
e-the_graph- > *j		4 steps

About:
listunioninlequalimpliesandorallexists

(19steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc