Nuprl - Proof: dfs-connect 3

(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: dfs-connect 3

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. s1: traversal(the_graph)
6. s2: traversal(the_graph)
7. i1: Vertices(the_graph)
8. (inl(i1) s1)
9. (inr(i1) s1)
10. j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
11. j: Vertices(the_graph)
12. (inr(j) [inl(i1) / (s2 @ [inr(i1)])])

i1-the_graph- > *j

By: RWO Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) -1 THEN Analyze -1

Generated subgoals:

1 12. inr(j) = inl(i1) Vertices(the_graph)+Vertices(the_graph)
i1-the_graph- > *j 1 step

2 12. (inr(j) s2 @ [inr(i1)])
i1-the_graph- > *j 4 steps

About:

(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc