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

At: dfs-connect 3 2
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) s2 @ [inr(i1)])
i1-the_graph- > *j
By:
RWO Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) -1
THEN
RWO Thm* a,x:T. (x [a]) x = a -1
THEN
Analyze -1
THEN
EasyHyp
Generated subgoal:

112. inr(j) = inr(i1) Vertices(the_graph)+Vertices(the_graph)
i1-the_graph- > *j		3 steps

About:
listconsnilunioninlinruniverseequalimpliesorall

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