proposition: Lemma pdfs_correct (p : {set T} * seq T) x : let (s, l) := p in uniq l /\ {subset l <= ~: s} -> let p1 := pdfs p x in let (s1, l1) := p1 in if x \notin s then p1 = p else [/\ #|s1| <= #|s| & uniq l1] /\ exists l2 : seq T, [/\ x \in l2, s1 = s :\: [set y in l2], l1 = l2 ++ l, TS[[pred x in s], l2] & forall y, y \in l2 -> x -[[pred x in s]]-> y].
proof: Proof. rewrite /pdfs. have: #|p.1| <= #|T| by apply/subset_leq_card/subsetP=> i. elim: #|T| x p => /= [x [s l]|n IH x [s l]]/=. rewrite leqn0 => /eqP/cards0_eq-> [HUl HS]. by rewrite inE. have [xIs Hl [HUl HS]/=|xNIs Hl [HUl HS]//] := boolP (x \in s). set p := (_, l); set F := rpdfs _; set L := g _. have: [/\ #|p.1| < #|s| & uniq p.2] /\ exists l2, [/\ x \notin p.1, p.1 = (s :\ x) :\: [set z in l2], p.2 = l2 ++ l, TS[[predD1 s & x], l2] & forall y, y \in l2 -> x -[[predD1 s & x]]-> y ]. split; [split => // | exists [::]; split => //=]. - by rewrite /p /= [#|s|](cardsD1 x) xIs. - by rewrite !inE eqxx. - by rewrite setD0. by exact: tsorted_nil. have: forall y, (grel g) x y -> (y \notin p.1) || (y \in L). by move => y; rewrite /= orbC => ->. have: forall y, (y \in L) -> (grel g) x y by move=> y. rewrite {}/p. elim: L (_, _) => /= [[s1 l1] /= _ yIp [[sSs1 Ul1] [l2 [xIs1 s1E l1E Rwl2 xCy]]]| y l' IH1 [s1 l1] /= Rx yIp [[sSs1 Ul1] [l2 [xIs1 s1E l1E Rwl2 xCy]]]]. split; [split=> // |exists (x :: l2); split] => // [||||||y]. - rewrite subset_leqif_cards // s1E. by apply: subset_trans (subsetDl _ _) (subD1set _ _). - rewrite Ul1 andbT l1E mem_cat negb_or. have [/= Dl2 _] := Rwl2. have /subsetP/(_ x)/implyP/= := Dl2. rewrite !inE /= eqxx implybF => ->. have /implyP := HS x. by rewrite !inE xIs implybF. - by rewrite inE eqxx. - by apply/setP => z; rewrite s1E !inE negb_or andbC andbAC. - by rewrite l1E. - apply: tsorted_cons_r => // [y yInl2|y /yIp]. rewrite connect_to_C1_id (eq_connect (_ : _ =2 (relto [predD1 s & x] (grel g)))) ?xCy //. by move=> x1 y1; rewrite /= !inE andbA. rewrite orbF s1E 3!inE negb_and => /orP[]; first by rewrite negbK. by rewrite !inE negb_and => /orP[] /negPf->. rewrite inE => /orP[/eqP->|yIl2]. by apply: connect0. apply: sub_connect_to (xCy _ yIl2); apply/subsetP => i /=. by rewrite !inE => /andP[]. have F1 : #|s1| <= n. by rewrite -ltnS (leq_trans _ Hl). have F2 : {subset l1 <= ~: s1}. move=> i; rewrite l1E s1E !inE mem_cat => /orP[->//|/HS]. by rewrite inE => /negPf->; rewrite !andbF. have := IH y (s1, l1) F1 (conj Ul1 F2). rewrite /F /=; case: rpdfs => s3 l3 /= Hv. apply: IH1 => [z zIl|z Rxz /=|]; first by apply: Rx; rewrite inE zIl orbT. case: (boolP (y \in s1)) Hv => [yIs1/= [[Ss1s3 Ul3] [l4 [yIl4 s3E l3E Rwl4 Cyz]]] |yNIs1/= [-> _]]; last first. case/orP: (yIp _ Rxz) => [->//|]. by rewrite inE => /orP[/eqP->|->]; [rewrite yNIs1|rewrite orbT]. rewrite s3E !inE !negb_and. case/orP: (yIp _ Rxz) => [->//|]; first by rewrite orbT. rewrite inE => /orP[/eqP->|->]; last by rewrite orbT. by rewrite yIl4. case: (boolP (y \in s1)) Hv => [yIs1 [[Ss1s3 Ul3] [l4 [yIl4 s3E l3E Rwl4 Cyz]]] |yNIs1 [-> ->]]; last first. by split=> //; exists l2; split. split; [split=> //= | exists (l4 ++ l2); split => //= [||||z]]. - by apply: leq_ltn_trans Ss1s3 _. - by rewrite s3E s1E !inE eqxx !andbF. - by apply/setP => i; rewrite s3E s1E !inE mem_cat negb_or -!andbA. - by rewrite l3E l1E catA. - apply: tsorted_cat => //. apply: eq_tsorted Rwl4 => i. by rewrite /= s1E !inE. rewrite mem_cat => /orP[] zIl4; last by apply: xCy. apply: connect_trans (_: y -[_]-> z); last first. apply: sub_connect_to (Cyz _ zIl4); apply/subsetP => i. by rewrite /= s1E !inE => /andP[]. apply: connect_to1 (Rx _ _); rewrite !inE ?eqxx //. by move: yIs1; rewrite s1E !inE=> /and3P[_ ->]. Qed.
imports: mathcomp(all_ssreflect) extra