Nuprl - Proof: dfs-cases 2 2

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

At: dfs-cases 2 2

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
6. 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)
7. 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)
8. ((inl(i) s) (inr(i) s))
9. L:Vertices(the_graph) List, s:traversal(the_graph). s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);s;L) = (s2 @ s)

s':traversal(the_graph). ((inr(i) s) (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))) & [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)] 6 THEN ReduceSOAps -1 THEN ExRepD THEN HypSubst -1 0 THEN Thin -1 THEN InstHyp [L;[inr(i) / s]] 9 THEN ExRepD THEN HypSubst -1 0 THEN Thin -1 THEN InstConcl [[inl(i)] @ s2 @ [inr(i)]]

Generated subgoals:

1 10. L: Vertices(the_graph) List
11. y:Vertices(the_graph). i-the_graph- > y (y L)
12. s2: traversal(the_graph)
13. (inr(i) s) (inl(i) s)
([inl(i)] @ s2 @ [inr(i)]) = nil traversal(the_graph) 1 step

2 10. L: Vertices(the_graph) List
11. y:Vertices(the_graph). i-the_graph- > y (y L)
12. s2: traversal(the_graph)
13. (inr(i) s)
14. (inl(i) s)
s2@0:traversal(the_graph). ([inl(i)] @ s2 @ [inr(i)]) = ([inl(i)] @ s2@0 @ [inr(i)]) traversal(the_graph) 1 step

3 10. L: Vertices(the_graph) List
11. y:Vertices(the_graph). i-the_graph- > y (y L)
12. s2: traversal(the_graph)
[inl(i) / (s2 @ [inr(i) / s])] = (([inl(i)] @ s2 @ [inr(i)]) @ s) traversal(the_graph) 1 step

About:

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

1	10. `L:` `Vertices(the_graph) List` 11. `y:Vertices(the_graph). i-the_graph- > y (y L)` 12. `s2:` `traversal(the_graph)` 13. `(inr(i) s) (inl(i) s)` `([inl(i)] @ s2 @ [inr(i)]) = nil traversal(the_graph)`	1 step

2	10. `L:` `Vertices(the_graph) List` 11. `y:Vertices(the_graph). i-the_graph- > y (y L)` 12. `s2:` `traversal(the_graph)` 13. `(inr(i) s)` 14. `(inl(i) s)` `s2@0:traversal(the_graph). ([inl(i)] @ s2 @ [inr(i)]) = ([inl(i)] @ s2@0 @ [inr(i)]) traversal(the_graph)`	1 step

3	10. `L:` `Vertices(the_graph) List` 11. `y:Vertices(the_graph). i-the_graph- > y (y L)` 12. `s2:` `traversal(the_graph)` `[inl(i) / (s2 @ [inr(i) / s])] = (([inl(i)] @ s2 @ [inr(i)]) @ s) traversal(the_graph)`	1 step