Nuprl - Proof: paren-df-traversal

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

G:Graph. (x,y:Vertices(G). Dec(x = y)) (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s))

By: Auto THEN Unfold `depthfirst-traversal` 0 THEN AllHyps (h.(Unfold `df-traversal` h) THEN (Analyze h) THEN (InstHyp [i;s1;s2;j] h+1)) THEN Inst Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s))) [Vertices(G);s2;j] THEN Analyze -1

Generated subgoal:

1 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)
(inl(j) s2) 17 steps

About:

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