Nuprl - Proof: paren-df-traversal 1 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. s1,s2@0:(Vertices(G)+Vertices(G)) List. s2 = (s1 @ [inr(i) / s2@0])

(inl(j) s2)

By: ExRepD THEN Assert ((inr(j) s3) (inr(j) s2@0))

Generated subgoals:

1 18. s3: (Vertices(G)+Vertices(G)) List
19. s2@0: (Vertices(G)+Vertices(G)) List
20. s2 = (s3 @ [inr(i) / s2@0])
(inr(j) s3) (inr(j) s2@0) 2 steps

2 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)
(inl(j) s2) 12 steps

About:

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

1	18. `s3:` `(Vertices(G)+Vertices(G)) List` 19. `s2@0:` `(Vertices(G)+Vertices(G)) List` 20. `s2 = (s3 @ [inr(i) / s2@0])` `(inr(j) s3) (inr(j) s2@0)`	2 steps

2	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)` `(inl(j) s2)`	12 steps