is mentioned by

Thm* For any graph the_obj:GraphObject(the_graph), L:V List, s:Traversal, x:V. dfl-traversal(the_graph;L;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x))	[dfs-dfl-traversal]
Thm* For any graph the_obj:GraphObject(the_graph), P:((V List)TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & P(L,dfsl(the_obj;L)))	[dfsl-induction2]
Thm* For any graph the_obj:GraphObject(the_graph), P:((V List)TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. P(L,dfsl(the_obj;L)))	[dfsl-induction1]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s) (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) (k:V. (inr(k) s2) j-the_graph- > *k) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inr(i) s1) (inl(i) s1) paren(V;s2) l_disjoint(V+V;s2;s1) no_repeats(V+V;s2) (j:V. (inr(j) s2) i-the_graph- > *j) (j:V. i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction4]
Thm* 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)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)	[dfs-properties]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s)	[dfs-connect]
Thm* 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)	[dfs-cases]
Thm* 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) (j:V. i-the_graph- > j j = i (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;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))	[dfs_induction3]
Thm* For any graph the_obj:GraphObject(the_graph), l:V List, s:Traversal. s':Traversal. (i:V. (i l) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & list_accum(s',j.dfs(the_obj;s';j);s;l) = (s' @ s)	[dfs_accum_member]
Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. s':Traversal. (inl(i) s') (inl(i) s) (inr(i) s) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & dfs(the_obj;s;i) = (s' @ s)	[dfs_member]
Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s) (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inl(i) s1) (inr(i) s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & dfs(the_obj;s;i) = (s' @ s))	[dfs_induction2]
Thm* 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))	[dfs_induction]

In prior sections: list 1 mb list 1 mb list 2 graph 1 1 graph 1 2

Try larger context: Graphs