Nuprl - Proof: dfsl-traversal-append 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) & (i:Vertices(the_graph). (inl(i) s) L1-the_graph- > *i)
7. i:Vertices(the_graph). L1 @ L2-the_graph- > *i non-trivial-loop(the_graph;i)
8. 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)))

L1@0,L2@0:Vertices(the_graph) List. (L1 @ L2) = (L1@0 @ 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: Auto THEN EqualAppendsD -1 THEN Analyze -1

Generated subgoals:

1 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)) 6 steps

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

About:

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

1	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))`	6 steps

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