proposition: Lemma adm_P2_aux C D p u : [p]u \in F -> C \in S -> D \in S -> ~~ reach_demo S p C D -> prv ([af C] ---> [p]~~:[af D]).
proof: Proof. Proof with adm_P2_aux_tac using coref_S sfc_F sub_S. elim: p u C D => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp|s] u C D Hu CinS DinS /=. - rewrite -has_predC. case/hasP. case => s [|]; last by rewrite (negbTE (Rpos _ _ _)). rewrite RE /= => inC ninD. have inD : s^- \in D. { apply: maxS0 DinS ninD _. move: CinS => /(subP sub_S). rewrite inE powersetE. case/and3P => /subP sub _ _. apply: (@flip_drop_sign _ (s^+)). apply: flipcl_refl. move/sub : inC. by move/flip_drop_sign/sfc_F. } rewrite <- (axDN ([pV a](~~: [af D]))). rewrite -> (dmAX (pV a) (~~: [af D])). rewrite -> rEXn; last exact: axDN. rewrite -> (bigAE _ inC). rewrite -> (rEXn (pV a) (t:= ~~: s)). + rule axC. do 2 Intro. rule axB; last by do 2 Rev; exact: axDBD. rewrite -> rEXn; first exact: axnEXF. rewrite -> (axDNE (~~: s ---> ~~: s)). exact: axI. + rewrite -> bigAE; last exact: inD. exact: axI. - rewrite negb_or. case/andP => H0 H1. rewrite <- axDup. rewrite -> (IH0 u) at 1 => //... rewrite -> (IH1 u C D) => //... exact: axCh. - rewrite -all_predC. move/allP => H. rewrite <- axCon. rewrite <- (axDN ([p0][p1](~~: [af D]))). rewrite -> (dmAX p0 ([p1](~~: [af D]))). rewrite -> (rEXn p0 (t:= (\or_(E <- S) [af E]) :/\: EX p1 [af D])); last by apply: (rMP _ or_S); exact: axAI. rewrite -> rEXn; last by rewrite -> bigODr; exact: axI. rewrite -> bigEOOE. rule axC. apply: bigOE => E inS. move: (H E inS) => /=. rewrite negb_and. case/orP => [H0|H1]. + rewrite -> (IH0 [p1]u C E) => //... do 2 Intro. rule axB; last by do 2 Rev; exact: axDBD. rewrite -> rEXn; first exact: axnEXF. do 2 rule axAcase. rule axC. drop. exact: axContra. + rule axC. drop. rewrite -> rEXn; first exact: axnEXF. rule axDup. rewrite -> axAEl at 2. rewrite -> axAEr. rewrite -> (IH1 u E D) => //... - move => H. set I := [fset E in S | reach_demo S (p^*) C E]. set v := \or_(E <- I)[af E]. suff X : prv (v ---> [p]v). { Cut v; first by apply: bigOI;rewrite !inE CinS /= connect_in0. rewrite -> (rStar_ind' X). apply: rNorm. apply: bigOE => E inI. apply: neq_contra => //; first by apply/(subP subsep); exact: inI. apply: contraTN inI => /eqP->. by rewrite inE DinS /= (negbTE H). } rewrite /v. rewrite <- (axDN ([p](\or_(E<-I) [af E]))), -> (dmAX p (\or_(E<-I) [af E])). apply: bigOE => E EinI. rewrite -> rEXn; last by apply: neg_or; exact: subsep. rewrite -> bigEOOE. rule axC. apply: bigOE => G GninI. rewrite -> (IHp [p^*]u E G) => //... * apply: (subP subsep). exact: EinI. * apply: (subP (fsubDl _ _)). exact: GninI. * apply/negP => ERG. move: GninI. rewrite inE. case/andP => GinS. apply/negP. apply/negPn. rewrite inE GinS /=. apply: connect_in_trans. move: EinI. case/sepP => _ CE. exact: CE. apply: connect_in1 => //. apply: (subP subsep). exact: EinI. - rewrite <- axTestI. case: (boolP (C == D)) => /= [/eqP-> A|]. + suff X : s^- \in D. { rewrite -> (bigAE _ X) => /=. do 3 Intro. by Apply. } move/sfc_F : Hu => /andP [B _]. exact: (maxS0 DinS A). + move => A _. do 3 Intro. by ApplyH (neq_contra CinS DinS A). Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)