proposition: Theorem tarjan_rec_terminates n (roots : {set V}) e : n >= #|~: seen e| * #|V|.+1 + #|roots| -> dfs_correct (tarjan_rec n) roots e.
proof: Proof. move=> n_ge; elim: n => [|n IHn/=] in roots e n_ge *. move: n_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: IHn; rewrite -ltnS (leq_trans _ n_ge)//. rewrite (cardsD1 x roots) x_roots add1n -addSnnS ltn_add2r ltnS. by rewrite leq_mul2r //= subset_leq_card// setCS sub_seen. move=> e_wf xNseen; apply: dfs1P => //; apply: IHn. rewrite seen_visit// setCU setIC -setDE -ltnS (leq_trans _ n_ge)//. rewrite (cardsD1 x (~: _)) inE xNseen add1n mulSnr -addnA ltn_add2l. by rewrite ltn_addr// ltnS max_card. Qed.
imports: mathcomp(all_ssreflect) bigmin extra