Nuprl - Proof: dfs wf 1 1 2 1

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

At: dfs wf 1 1 2 1

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. M: traversal(the_graph)
4. i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)
5. 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)
6. d:
7. d1:. d1 < d (s:traversal(the_graph), i:Vertices(the_graph). M(s)d1 dfs(the_obj;s;i) {s':traversal(the_graph)| M(s')d1 })
8. s: traversal(the_graph)
9. i: Vertices(the_graph)
10. M(s)d
11. member-paren(x,y.the_obj.eq(x,y);i;s)
12. M([inr(i) / s]) < M(s)
13. 0 < d
14. the_obj.eacc ({s':traversal(the_graph)| M(s')d-1 }Vertices(the_graph) {s':traversal(the_graph)| M(s')d-1 }) {s':traversal(the_graph)| M(s')d-1 }Vertices(the_graph) {s':traversal(the_graph)| M(s')d-1 }

[inl(i) / (the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i))] {s':traversal(the_graph)| M(s')d }

By: GenConclAtAddr [2;2]

Generated subgoals:

1 the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) {s':traversal(the_graph)| M(s')d-1 } 3 steps

2 15. z: {s':traversal(the_graph)| M(s')d-1 }
16. the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = z
[inl(i) / z] {s':traversal(the_graph)| M(s')d } 1 step

About:

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

1	`the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) {s':traversal(the_graph)\| M(s')d-1 }`	3 steps

2	15. `z:` `{s':traversal(the_graph)\| M(s')d-1 }` 16. `the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i) = z` `[inl(i) / z] {s':traversal(the_graph)\| M(s')d }`	1 step