Nuprl - Proof: paren-df-traversal 1 2 2

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

1. G: Graph
2. x,y:Vertices(G). Dec(x = y)
3. s: traversal(G)
4. paren(Vertices(G);s)
5. no_repeats(Vertices(G)+Vertices(G);s)
6. i:Vertices(G), s1,s2:traversal(G). s = (s1 @ [inr(i)] @ s2) traversal(G) (j:Vertices(G). (inr(j) s2) (inl(j) s2) j-G- > *i)
7. i:Vertices(G), s1,s2:traversal(G). (j:Vertices(G). i-G- > *j non-trivial-loop(G;j)) s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2))
8. i: Vertices(G)
9. s1: traversal(G)
10. s2: traversal(G)
11. j:Vertices(G). i-G- > *j non-trivial-loop(G;j)
12. s = (s1 @ [inl(i)] @ s2) traversal(G)
13. j: Vertices(G)
14. j = i
15. i-G- > *j
16. (inr(j) s2)
17. (inl(j) s2)
18. s3: (Vertices(G)+Vertices(G)) List
19. s2@0: (Vertices(G)+Vertices(G)) List
20. s2 = (s3 @ [inr(i) / s2@0])
21. (inr(j) s3) (inr(j) s2@0)