Nuprl - Proof: paren-df-traversal 1 1

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

(inr(i) s2)

By: FwdThru Thm* s:(T+T) List. paren(T;s) (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)) [4;12]

Generated subgoals:

None

About:

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