proposition: Theorem rec_terminates k (roots : {set V}) e : k >= #|~: visited e| * infty.+1 + #|roots| -> dfs_correct (rec k) roots e.
proof: Proof. move=> k_ge; elim: k => [|k IHk/=] in roots e k_ge *. move: k_ge; rewrite leqn0 addn_eq0 cards_eq0 => /andP[_ /eqP-> e_wf _]/=. constructor=> //=; rewrite /outenv ?nexts0 ?setDv ?big_set0// ?setU0. by split=> // ?; rewrite inE. apply: dfsP=> x x_roots; last first. move=> e1 subee1; apply: IHk; rewrite -ltnS (leq_trans _ k_ge)//. rewrite (cardsD1 x roots) x_roots add1n -addSnnS ltn_add2r ltnS. by rewrite leq_mul2r //= subset_leq_card// setCS sub_visited. move=> e_wf xNvisited; apply: dfs1P => //; apply: IHk. rewrite visited_visit setCU setIC -setDE -ltnS (leq_trans _ k_ge)//. rewrite (cardsD1 x (~: _)) inE xNvisited add1n mulSnr -addnA ltn_add2l. by rewrite ltn_addr// ltnS max_card. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors