Nuprl - Proof: dfsl-traversal-append 1 2

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

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@0 = (L1 @ e)
15. L2 = (e @ L2@0)

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 -2 0) THEN (RWO Thm* For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i 0) THEN (InstHyp [L1;nil] 9)) THENA (Auto THEN (RWO Thm* l:T List. (l @ nil) ~ l 0)) THEN RepeatFor 7 (ParallelOp -1)

Generated subgoals:

1 16. s1: traversal(the_graph)
17. s2: traversal(the_graph)
18. j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) nil-the_graph- > *j & L1-the_graph- > *j)
19. j: Vertices(the_graph)
20. (inl(j) s1)
21. L1-the_graph- > *j
L1-the_graph- > *j e-the_graph- > *j 1 step

2 16. s1: traversal(the_graph)
17. s2: traversal(the_graph)
18. j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) nil-the_graph- > *j & L1-the_graph- > *j)
19. j: Vertices(the_graph)
20. L1-the_graph- > *j e-the_graph- > *j
L1-the_graph- > *j 4 steps

3 16. s1: traversal(the_graph)
17. s2: traversal(the_graph)
18. j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) nil-the_graph- > *j & L1-the_graph- > *j)
19. j: Vertices(the_graph)
20. (inl(j) s2)
21. nil-the_graph- > *j & L1-the_graph- > *j
L2@0-the_graph- > *j & (L1-the_graph- > *j e-the_graph- > *j) 1 step

4 16. s1: traversal(the_graph)
17. s2: traversal(the_graph)
18. j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) nil-the_graph- > *j & L1-the_graph- > *j)
19. j: Vertices(the_graph)
20. L2@0-the_graph- > *j & (L1-the_graph- > *j e-the_graph- > *j)
nil-the_graph- > *j & L1-the_graph- > *j 4 steps

About:

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

1	16. `s1:` `traversal(the_graph)` 17. `s2:` `traversal(the_graph)` 18. `j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > j) & ((inl(j) s2) nil-the_graph- > j & L1-the_graph- > j)` 19. `j:` `Vertices(the_graph)` 20. `(inl(j) s1)` 21. `L1-the_graph- > j` `L1-the_graph- > j e-the_graph- > j`	1 step

2	16. `s1:` `traversal(the_graph)` 17. `s2:` `traversal(the_graph)` 18. `j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > j) & ((inl(j) s2) nil-the_graph- > j & L1-the_graph- > j)` 19. `j:` `Vertices(the_graph)` 20. `L1-the_graph- > j e-the_graph- > j` `L1-the_graph- > j`	4 steps

3	16. `s1:` `traversal(the_graph)` 17. `s2:` `traversal(the_graph)` 18. `j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > j) & ((inl(j) s2) nil-the_graph- > j & L1-the_graph- > j)` 19. `j:` `Vertices(the_graph)` 20. `(inl(j) s2)` 21. `nil-the_graph- > j & L1-the_graph- > j` `L2@0-the_graph- > j & (L1-the_graph- > j e-the_graph- > j)`	1 step

4	16. `s1:` `traversal(the_graph)` 17. `s2:` `traversal(the_graph)` 18. `j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > j) & ((inl(j) s2) nil-the_graph- > j & L1-the_graph- > j)` 19. `j:` `Vertices(the_graph)` 20. `L2@0-the_graph- > j & (L1-the_graph- > j e-the_graph- > j)` `nil-the_graph- > j & L1-the_graph- > j`	4 steps