proposition: Lemma supp_eval s (x : MD) : label (tagged x) |> s -> eval (interp' s) x.
proof: Proof. case: s x. elim => [|p|s IHs t IHt|s IHs|s IHs t IHt|s IHs t IHt] [|] x. - rewrite /= => inL. move: (label_lcon x). by rewrite /lcons inL. - by simpl. - done. - rewrite /= => inL. case e : (fV p^+ \in label (tagged x)); last by rewrite /MLabel /= e. move => _. move: (label_lcon x) => /andP [_ /allP /(_ _ e)]. by rewrite inL. - rewrite /=. by case/orP => [/IHs|/IHt] /=; intuition. - rewrite /=. case/andP => /IHs A /IHt B. by simpl in *; intuition. - rewrite /= -RE => HR y /MRel_R H. apply: (IHs true). rewrite -suppC1 /=. apply: suppC_sub H. by rewrite fsub1. - rewrite /=. case/MRel_D => y xy Hy. move => /(_ y xy). exact: (IHs false). - rewrite [supp]lock /= -lock. move: x. cofix supp_eval => x. rewrite /=. case/andP => [/IHt A]. case/orP => [/IHs B|B]; first exact: AR0. apply: ARs => //= y /MRel_R => H. apply: supp_eval. rewrite -suppC1. apply: suppC_sub H. by rewrite fsub1 RE. - move => L_x. apply: cAR_cEU. apply: EU_strengthen (IHs false) (IHt false) _ => {IHs IHt}. change (EU_M s t x). case: x L_x => p x Lx. rewrite [tagged _]/= in Lx. wlog ? : p x Lx / x = root (Frag p) => [W|]; subst. apply: EU_lift Lx => L' HL'. exact: W HL' _. wlog inF : / fAX (fAR s t)^- \in Fs D => [W|]. rewrite /= classic_orb in Lx. case/orP : Lx => [?|/and3P [pt ps pX]]. exact: EU0. apply: W. exact: rlabel_Fs pX. have Fgt0 : 0 < #|{: DF }|. apply/card_gt0P. by exists (SeqSub _ inF). case: p Lx => u E. move En : (dist Fgt0 u (SeqSub _ inF)) => n. elim: n u E En => [|n IHn] u E. + move/dist0 => -> {u} L. exact: EU_this. + move/distS. move/IHn => {IHn} - IHn. apply: EU_lift => L'. exact: IHn. - move => L_x. apply: AU_strengthen (IHs true) (IHt true) _ => {IHs IHt}. change (AU_M s t x). case: x L_x => p x Lx. rewrite [tagged _]/= in Lx. wlog ? : p x Lx / x = root (Frag p) => [W|]; subst. apply: AU_lift Lx => L' HL'. exact: W HL' _. wlog inF : / (fAX (fAU s t)^+ \in Fs D). move => W. rewrite /= classic_orb in Lx. case/orP : Lx => [?|/and3P [Lx ? px]]. exact: AU0. apply: W. exact: rlabel_Fs px. have Fgt0 : 0 < #|{: DF }|. apply/card_gt0P. by exists (SeqSub _ inF). case: p Lx => u. move En : (dist Fgt0 u (SeqSub _ inF)) => n. elim: n u En => [|n IHn] u. + move/dist0 => -> {u} L Lx. exact: AU_this. + move/distS. move/IHn => {IHn} - IHn L Lx. apply: AU_lift (Lx) => L' HL'. exact: IHn. - move => H /=. apply: cAU_cER. apply: ER_strengthen (IHs false) (IHt false) _ => {IHs IHt}. move: x H. cofix supp_eval => x. rewrite /= => /andP [Lt]. case/orP => Ls; first exact: ER0. case: (MRel_D Ls) => y xy Ly. apply: ERs xy _. exact: Lt. exact: supp_eval. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)