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

At: dfs induction3 1 1 2
1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop
4. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
5. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
6. s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)
7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph). i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)
8. s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) (j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
9. M: traversal(the_graph)
10. i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)
11. i:Vertices(the_graph), s:traversal(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s)
12. d:
13. d1:. d1 < d (s:traversal(the_graph), i:Vertices(the_graph). M(s)d1 (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)))
14. s: traversal(the_graph)
15. i: Vertices(the_graph)
16. M(s)d
17. member-paren(x,y.the_obj.eq(x,y);i;s)
18. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
19. T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
20. T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
21. L:Vertices(the_graph) List. (y:Vertices(the_graph). (y L) i-the_graph- > y) (s2:traversal(the_graph). M(s2) < d member-paren(x,y.the_obj.eq(x,y);i;s2) (s':traversal(the_graph). M(s' @ s2)M(s2) & P(i,s2,s') & list_accum(s',x'.dfs(the_obj;s';x');s2;L) = (s' @ s2)))
s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & [inl(i) / (the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i))] = (s' @ s) traversal(the_graph)
By:
((InstHyp [traversal(the_graph);[inr(i) / s];i;s',j. dfs(the_obj;s';j)] -3) THEN ExRepD THEN (InstHyp [L;[inr(i) / s]] -4)) THENA (Auto THEN EasyHyp THEN (Try ((RWO Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s)) 0) THEN ObviousConcl)) THEN (AutoInst [i;s]))
THEN
ExRepD
THEN
InstConcl [[inl(i)] @ s' @ [inr(i)]]
THEN
Reduce 0
THEN
EasyHyp
THEN
Try ((RWO Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c) 0) THEN (Reduce 0) THEN Analyze)
Generated subgoals:

122. L: Vertices(the_graph) List
23. y:Vertices(the_graph). i-the_graph- > y (y L)
24. the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L)
25. s': traversal(the_graph)
26. M(s' @ [inr(i) / s])M([inr(i) / s])
27. P(i,[inr(i) / s],s')
28. list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L) = (s' @ [inr(i) / s])
M([inl(i) / ((s' @ [inr(i)]) @ s)])M(s)		1 step
 
222. L: Vertices(the_graph) List
23. y:Vertices(the_graph). i-the_graph- > y (y L)
24. the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L)
25. s': traversal(the_graph)
26. M(s' @ [inr(i) / s])M([inr(i) / s])
27. P(i,[inr(i) / s],s')
28. list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L) = (s' @ [inr(i) / s])
P(i,s,[inl(i) / (s' @ [inr(i)])])		7 steps
 
322. L: Vertices(the_graph) List
23. y:Vertices(the_graph). i-the_graph- > y (y L)
24. the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L)
25. s': traversal(the_graph)
26. M(s' @ [inr(i) / s])M([inr(i) / s])
27. P(i,[inr(i) / s],s')
28. list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L) = (s' @ [inr(i) / s])
the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = (s' @ [inr(i) / s]) (Vertices(the_graph)+Vertices(the_graph)) List		1 step
 
422. L: Vertices(the_graph) List
23. y:Vertices(the_graph). i-the_graph- > y (y L)
24. the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L)
25. s': traversal(the_graph)
26. M(s' @ [inr(i) / s])M([inr(i) / s])
27. P(i,[inr(i) / s],s')
28. list_accum(s',x'.dfs(the_obj;s';x');[inr(i) / s];L) = (s' @ [inr(i) / s])
29. s1: traversal(the_graph)
the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) (Vertices(the_graph)+Vertices(the_graph)) List		1 step

About:
listconsconsnilboolassertless_thanunioninlinrlambdaapplyfunction
universeequalmembersqequaltoppropimpliesandorallexists

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