Nuprl - Proof: dfsl-traversal-append 1 1 2 1 1

(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 = (L1@0 @ e)
15. L2@0 = (e @ L2)
16. 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. L2-the_graph- > *j
21. L1@0-the_graph- > *j

L1-the_graph- > *j

By: RWO "list-list-connect-singleton < " 0 THEN RWO "list-list-connect-singleton < " -2 THEN Using [`B',L2] (BackThru Thm* For any graph A,B,C:V List. A-- > *B B-- > *C A-- > *C)

Generated subgoals:

None

About:

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