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

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

By: Analyze -1 THEN Analyze -2 THEN Analyze -2 THEN ObviousContradiction [-3]

Generated subgoals:

None

About:

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