Nuprl - Proof: dfs wf

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

At: dfs wf

For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. dfs(the_obj;s;i) Traversal

By: RepeatFor 2 (Analyze 0) THEN Inst Thm* dfs-measure [the_graph;the_obj] THEN ExRepDHyps THEN Assert (d:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d dfs(the_obj;s;i) {s':traversal(the_graph)| M(s')d })

Generated subgoals:

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)
d:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d dfs(the_obj;s;i) {s':traversal(the_graph)| M(s')d } 9 steps

2 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:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d dfs(the_obj;s;i) {s':traversal(the_graph)| M(s')d }
s:traversal(the_graph), i:Vertices(the_graph). dfs(the_obj;s;i) traversal(the_graph) 1 step

About:

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

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)` `d:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d dfs(the_obj;s;i) {s':traversal(the_graph)\| M(s')d }`	9 steps

2	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:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d dfs(the_obj;s;i) {s':traversal(the_graph)\| M(s')d }` `s:traversal(the_graph), i:Vertices(the_graph). dfs(the_obj;s;i) traversal(the_graph)`	1 step