proposition: Theorem tarjan_rec_terminates n (roots : {set V}) e : n >= #|whites e| * #|V|.+1 + #|roots| -> dfs'_correct (tarjan_rec n) roots e.
proof: Proof. move=> n_ge; wlog ->: e n roots {n_ge} / roots = set0 => [noroot|]; last first. have := @dfs'_is_correct (dfs1 (tarjan_rec 0)) (tarjan_rec 0) set0 e. rewrite /tarjan_rec /dfs'_correct /dfs' /=. case: n=> [|n /=]; case: pickP => [x|_/=]; rewrite ?inE //; by apply => ?; rewrite inE. have [V0|VN0] := posnP #|V|. have := max_card (mem roots). by rewrite V0 leqn0 cards_eq0 => /eqP /noroot; apply. elim: n => [|n IHn] in roots e n_ge *. move: n_ge; rewrite leqn0 addn_eq0 cards_eq0. by move=> /andP [_ /eqP/noroot]; apply. move=> pre; rewrite /dfs'_correct /=. apply: dfs'_is_correct => //= x x_root. move=> x_white; apply: dfs1_is_correct => //; apply: IHn. rewrite whites_add_stack cardsDS ?sub1set // cards1 subn1. rewrite -ltnS (leq_trans _ n_ge) //. rewrite (@ltn_div2r #|V|.+1) ?divnMDl ?divn_small ?addn0 ?ltnS ?max_card //=. by rewrite prednK //; apply/card_gt0P; exists x. move=> e1 whites_e1; apply: IHn; rewrite -ltnS (leq_trans _ n_ge) //. have /subset_leq_card := whites_e1. rewrite leq_eqVlt => /predU1P [->|lt_wh]; last first. by rewrite (@ltn_div2r #|V|.+1) ?divnMDl ?divn_small ?addn0 ?ltnS ?max_card. by rewrite ltn_add2l [X in _ < X](cardsD1 x) x_root. Qed.
imports: mathcomp(all_ssreflect) extra