Nuprl - Proof: dfs induction

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

For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s1,s2:Traversal, i:V. P(i,s1,s2) l_disjoint(V+V;s2;s1) & no_repeats(V+V;s2)) (s:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))

By: Auto 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 (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)))

Generated subgoals:

1 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop
4. s: traversal(the_graph)
5. i: Vertices(the_graph)
6. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
7. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
8. s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)
9. 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)
10. s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
11. M: traversal(the_graph)
12. i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)
13. 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 (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)) 20 steps

2 1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop
4. s: traversal(the_graph)
5. i: Vertices(the_graph)
6. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
7. s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
8. s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)
9. 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)
10. s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
11. M: traversal(the_graph)
12. i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)
13. 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)
14. d:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))
s':traversal(the_graph). P(i,s,s') & dfs(the_obj;s;i) = (s' @ s) 1 step

About:

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

1	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `P:` `Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop` 4. `s:` `traversal(the_graph)` 5. `i:` `Vertices(the_graph)` 6. `s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)` 7. `s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)` 8. `s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)` 9. `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)` 10. `s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])` 11. `M:` `traversal(the_graph)` 12. `i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)` 13. `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 (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))`	20 steps

2	1. `the_graph:` `Graph` 2. `the_obj:` `GraphObject(the_graph)` 3. `P:` `Vertices(the_graph)traversal(the_graph)traversal(the_graph)Prop` 4. `s:` `traversal(the_graph)` 5. `i:` `Vertices(the_graph)` 6. `s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)` 7. `s1,s2:traversal(the_graph), i:Vertices(the_graph). P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)` 8. `s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)` 9. `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)` 10. `s1,s2:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])` 11. `M:` `traversal(the_graph)` 12. `i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)` 13. `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)` 14. `d:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d (s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s))` `s':traversal(the_graph). P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)`	1 step