((Inst Thm* dfs-properties [the_graph;the_obj;s;i]) THEN ExRepD THEN (Inst Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. df-traversal(the_graph;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;dfs(the_obj;s;i)) [the_graph;the_obj;s;i])) THENA (Auto THEN (Analyze 9) THEN (Try (Complete Auto)) THEN (Analyze -1) THEN (BackThru Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s'))))
THEN
HypSubst -2 -1
THEN
HypSubst -2 0

1

10. s': traversal(the_graph) 11. (inr(i) s) (inl(i) s) s' = nil 12. (inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph)) 13. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) 14. no_repeats(Vertices(the_graph)+Vertices(the_graph);s') 15. paren(Vertices(the_graph);s') 16. j:Vertices(the_graph). (inr(j) s') i-the_graph- > *j 17. dfs(the_obj;s;i) = (s' @ s) 18. df-traversal(the_graph;s' @ s) dfsl-traversal(the_graph;L1 @ [i];s' @ s)

154 steps

About: