Nuprl - Proof: dfsl-induction1 1 1

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

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: (Vertices(the_graph) List)traversal(the_graph)Prop
4. P(nil,nil)
5. L:Vertices(the_graph) List, s:traversal(the_graph), i:Vertices(the_graph). P(L,s) P(L @ [i],dfs(the_obj;s;i))
6. n:
7. L: Vertices(the_graph) List
8. L1:Vertices(the_graph) List. ||L1|| < ||L|| P(L1,list_accum(s,i.dfs(the_obj;s;i);nil;L1))
9. L = nil
10. x: Vertices(the_graph)
11. L': Vertices(the_graph) List
12. L = (L' @ [x])
13. P(L',list_accum(s,i.dfs(the_obj;s;i);nil;L'))

P(L' @ [x],list_accum(s,i.dfs(the_obj;s;i);nil;L' @ [x]))

By: RWO Thm* l1,l2:Top List, f,y:Top. list_accum(x,a.f(x,a);y;l1 @ l2) ~ list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;l1);l2) 0 THEN Reduce 0 THEN BackThruSomeHyp

Generated subgoals:

None

About:

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