Nuprl - Proof: dfs-cases

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

For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. ((inr(i) s) (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & dfs(the_obj;s;i) = (s' @ s)

By: Auto THEN Inst Thm* graphobj-properties [the_graph;the_obj] THEN Analyze -1 THEN Analyze -1 THEN RecUnfold `dfs` 0 THEN SplitOnConclITE THEN 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)) -1

Generated subgoals:

1 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)
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))) & s = (s' @ s) traversal(the_graph) 1 step

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))
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) 9 steps

About:

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

1	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)` `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))) & s = (s' @ s) traversal(the_graph)`	1 step

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))` `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)`	9 steps