proposition: Lemma tarjan_recP : tarjan_rec N setT e0 = (#|V|, set0, Env gsccs #|V| [ffun x => #|V|]).
proof: Proof. case: tarjan_rec_terminates; first by rewrite seen0 setC0 cardsT. - constructor; rewrite /= ?serialE ?seen0 ?cards0 ?sub0set// => x; rewrite !ffunE//. + by rewrite ltnNge leqW//. + by rewrite gtn_eqF// /cover big_set0 inE. + by move=> y; rewrite !ffunE//= andbC ltnNge leqW// ?max_card. + by move=> y; rewrite !inE !ffunE/= ltnNge leqW// max_card. move=> _ _ _ e -> e_wf _ [-> -> _]; rewrite stack0 setD0. have [stacke _|[x xe]] := set_0Vmem (stack e); last first. by move=> /(_ _ xe)[?]; rewrite inE. rewrite seen0 set0U setC0 nextsT => seene. have numE x : num e x = #|V|. apply/eqP; have /setP/(_ x) := seene. by rewrite seenE// stacke set0U !inE -num_sccs. have serialE : serial e = #|V| by rewrite serialE// seene cardsT. have sccse : esccs e = gsccs. apply/eqP; rewrite eqEsubset sub_gsccs//=; apply/subsetP => _/imsetP[/=x _->]. have: x \in cover (esccs e) by rewrite -num_sccs ?numE//. move=> /bigcupP [C Csccs /(def_scc (subsetP (sub_gsccs e_wf) _ Csccs))] eqC. rewrite -eqC (_ : [set _ in _ | _] = gscc_of x)// in Csccs *. by apply/setP => y; rewrite !inE mem_scc /=. rewrite big1; last by move=> x _; apply: val_inj; rewrite /= inordK// ?numE. congr (_, _, _) => //. case: e {stacke seene e_wf} => /= sccs sn num in numE serialE sccse *. by congr (Env _ _) => //; apply/ffunP=> x; rewrite ffunE. Qed.
imports: mathcomp(all_ssreflect) bigmin extra