(* (c) Copyright Christian Doczkal, Saarland University *)
(* Distributed under the terms of the CeCILL-B license *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
From CompDecModal.libs
Require Import edone bcase fset base sltype.
From CompDecModal.CTL
Require Import CTL_def gen_def.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Hint Constructors gen : core.
(* Distributed under the terms of the CeCILL-B license *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
From CompDecModal.libs
Require Import edone bcase fset base sltype.
From CompDecModal.CTL
Require Import CTL_def gen_def.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Hint Constructors gen : core.
Decidability of Gentzen Derivability
Part 1: Syntactic Universe
Section gen_closure.
Variable F : {fset sform}.
Hypothesis sfc_F : sf_closed F.
Lemma sf_AU s t b : ((fAU s t,b) \in F) = ((fAX (fAU s t),b) \in F).
Proof. apply/idP/idP; move/sfc_F => //=. by bcase. Qed.
Lemma sf_AR s t b : ((fAR s t,b) \in F) = ((fAX (fAR s t),b) \in F).
Proof. apply/idP/idP; move/sfc_F => //=. by bcase. Qed.
Definition Cs := powerset F.
Definition Hs := powerset Cs.
Definition AUs := [fset p in positives F `x` positives F | fAU p.1 p.2^+ \in F].
Definition ARs := [fset p in negatives F `x` negatives F | fAR p.1 p.2^- \in F].
Definition As :=
aVoid |` [fset aAU (p,H) | p <- AUs, H <-Hs ]
`|` [fset aAXU (p,H) | p <- AUs, H <-Hs ]
`|` [fset aAR (p,H) | p <- ARs, H <-Hs ]
`|` [fset aAXR (p,H) | p <- ARs, H <-Hs ].
Definition U : {fset clause * annot} := Cs `x` As.
Lemma AsX p H : (aAU (p, H) \in As) = (aAXU (p, H) \in As).
Proof.
rewrite /As !inE !eqF //= !in_fimset2 ?curryE ?in_fimset2F //;
split; congruence.
Qed.
Lemma AsAU s t H : aAU (s,t,H) \in As = [&& fAU s t^+ \in F & H \in Hs].
Proof.
rewrite !inE !eqF //= in_fimset2 // ; last by split; congruence.
rewrite ![aAU _]curryE !in_fimset2F // !orbF !inE in_fsetX !posE /=.
case e: (fAU _ _^+ \in F) => //. by case/and3P:(sfc_F e) => _ -> ->.
Qed.
Lemma AsAXU s t H : aAXU (s,t,H) \in As = [&& fAX (fAU s t)^+ \in F & H \in Hs].
Proof. by rewrite -AsX -sf_AU AsAU. Qed.
Lemma AsX' p H : (aAR (p, H) \in As) = (aAXR (p, H) \in As).
Proof.
rewrite /As !inE !eqF //= !in_fimset2 ?curryE ?in_fimset2F //;
split; congruence.
Qed.
Lemma AsAR s t H : aAR (s,t,H) \in As = [&& fAR s t^- \in F & H \in Hs].
Proof.
rewrite !inE !eqF //= in_fimset2 // ; last by split; congruence.
rewrite ![aAR _]curryE !in_fimset2F // !orbF !inE in_fsetX !negE /=.
case e: (fAR _ _^- \in F) => //. by case/and3P:(sfc_F e) => _ -> ->.
Qed.
Lemma AsAXR s t H : aAXR (s,t,H) \in As = [&& fAX (fAR s t)^- \in F & H \in Hs].
Proof. by rewrite -AsX' -sf_AR AsAR. Qed.
Lemma AsV : aVoid \in As.
Proof. by rewrite !in_fsetU inE. Qed.
Lemma AU_shift s t C H : (fAU s t^+ |` C \in Cs) && (H \in Hs) = ((C,aAU (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAU powersetU powersetE fsub1 -/Cs; bcase. Qed.
Lemma AXU_shift s t C H : (fAX (fAU s t)^+ |` C \in Cs) && (H \in Hs) = ((C,aAXU (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAXU powersetU powersetE fsub1 -/Cs; bcase. Qed.
Lemma AR_shift s t C H : (fAR s t^- |` C \in Cs) && (H \in Hs) = ((C,aAR (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAR powersetU powersetE fsub1 -/Cs; bcase. Qed.
Lemma AXR_shift s t C H : (fAX (fAR s t)^- |` C \in Cs) && (H \in Hs) = ((C,aAXR (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAXR powersetU powersetE fsub1 -/Cs; bcase. Qed.
Variable F : {fset sform}.
Hypothesis sfc_F : sf_closed F.
Lemma sf_AU s t b : ((fAU s t,b) \in F) = ((fAX (fAU s t),b) \in F).
Proof. apply/idP/idP; move/sfc_F => //=. by bcase. Qed.
Lemma sf_AR s t b : ((fAR s t,b) \in F) = ((fAX (fAR s t),b) \in F).
Proof. apply/idP/idP; move/sfc_F => //=. by bcase. Qed.
Definition Cs := powerset F.
Definition Hs := powerset Cs.
Definition AUs := [fset p in positives F `x` positives F | fAU p.1 p.2^+ \in F].
Definition ARs := [fset p in negatives F `x` negatives F | fAR p.1 p.2^- \in F].
Definition As :=
aVoid |` [fset aAU (p,H) | p <- AUs, H <-Hs ]
`|` [fset aAXU (p,H) | p <- AUs, H <-Hs ]
`|` [fset aAR (p,H) | p <- ARs, H <-Hs ]
`|` [fset aAXR (p,H) | p <- ARs, H <-Hs ].
Definition U : {fset clause * annot} := Cs `x` As.
Lemma AsX p H : (aAU (p, H) \in As) = (aAXU (p, H) \in As).
Proof.
rewrite /As !inE !eqF //= !in_fimset2 ?curryE ?in_fimset2F //;
split; congruence.
Qed.
Lemma AsAU s t H : aAU (s,t,H) \in As = [&& fAU s t^+ \in F & H \in Hs].
Proof.
rewrite !inE !eqF //= in_fimset2 // ; last by split; congruence.
rewrite ![aAU _]curryE !in_fimset2F // !orbF !inE in_fsetX !posE /=.
case e: (fAU _ _^+ \in F) => //. by case/and3P:(sfc_F e) => _ -> ->.
Qed.
Lemma AsAXU s t H : aAXU (s,t,H) \in As = [&& fAX (fAU s t)^+ \in F & H \in Hs].
Proof. by rewrite -AsX -sf_AU AsAU. Qed.
Lemma AsX' p H : (aAR (p, H) \in As) = (aAXR (p, H) \in As).
Proof.
rewrite /As !inE !eqF //= !in_fimset2 ?curryE ?in_fimset2F //;
split; congruence.
Qed.
Lemma AsAR s t H : aAR (s,t,H) \in As = [&& fAR s t^- \in F & H \in Hs].
Proof.
rewrite !inE !eqF //= in_fimset2 // ; last by split; congruence.
rewrite ![aAR _]curryE !in_fimset2F // !orbF !inE in_fsetX !negE /=.
case e: (fAR _ _^- \in F) => //. by case/and3P:(sfc_F e) => _ -> ->.
Qed.
Lemma AsAXR s t H : aAXR (s,t,H) \in As = [&& fAX (fAR s t)^- \in F & H \in Hs].
Proof. by rewrite -AsX' -sf_AR AsAR. Qed.
Lemma AsV : aVoid \in As.
Proof. by rewrite !in_fsetU inE. Qed.
Lemma AU_shift s t C H : (fAU s t^+ |` C \in Cs) && (H \in Hs) = ((C,aAU (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAU powersetU powersetE fsub1 -/Cs; bcase. Qed.
Lemma AXU_shift s t C H : (fAX (fAU s t)^+ |` C \in Cs) && (H \in Hs) = ((C,aAXU (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAXU powersetU powersetE fsub1 -/Cs; bcase. Qed.
Lemma AR_shift s t C H : (fAR s t^- |` C \in Cs) && (H \in Hs) = ((C,aAR (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAR powersetU powersetE fsub1 -/Cs; bcase. Qed.
Lemma AXR_shift s t C H : (fAX (fAR s t)^- |` C \in Cs) && (H \in Hs) = ((C,aAXR (s,t,H)) \in U).
Proof. by rewrite in_fsetX AsAXR powersetU powersetE fsub1 -/Cs; bcase. Qed.
U is closed under backward application of the rules
Lemma subCs s C : s |` C \in Cs -> s \in F.
Proof. by rewrite !powersetE fsubUset fsub1; bcase. Qed.
Lemma subU t X C A :
(sf_closed' F t -> X `<=` F) -> (t |` C,A) \in U -> (X `|` C,A) \in U.
Proof.
move => H. rewrite !in_fsetX ![_ && (A \in _)]andbC. case (A \in As) => //=.
rewrite !powersetE ![_ `|` C]fsetUC !fsubUset fsub1. case (C `<=` F) => //=.
by move/sfc_F.
Qed.
Lemma genU_ipl s t C E : (fImp s t^+ |` C, E) \in U -> (s^- |` C, E) \in U.
Proof. apply: subU => /=. auto with fset. Qed.
Lemma genU_ipr s t C E : (fImp s t^+ |` C, E) \in U -> (t^+ |` C, E) \in U.
Proof. apply: subU => /=. auto with fset. Qed.
Lemma genU_in s t C E : (fImp s t^- |` C, E) \in U -> ([fset s^+ , t^- & C], E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. auto with fset. Qed.
Lemma genU_aR E : E \in As -> aR E \in As.
Proof. case: E => //=; try by rewrite AsV. case => [[u v] H]. by rewrite AsX. Qed.
Let RinU := RinU sfc_F.
Lemma genU_AXn s C E : (fAX s^- |` C , E) \in U -> (s^- |` R C, aR E) \in U.
Proof.
rewrite !in_fsetX => /andP [C1 C2]. rewrite genU_aR // andbT.
move: C1. rewrite powersetU powersetE fsub1 => /andP [/sfc_F ? /RinU ?].
rewrite powersetU powersetE fsub1. by apply/andP.
Qed.
Lemma genU_AUpl s t C E : (fAU s t^+ |` C,E) \in U -> (t^+ |` C,E) \in U.
Proof. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_AUpr s t C E : (fAU s t^+ |` C,E) \in U -> ([fset s^+, fAX (fAU s t)^+ & C],E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_AUnl s t C E : (fAU s t^- |` C, E) \in U -> ([fset s^-, t^- & C], E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_AUnr s t C E : (fAU s t^- |` C, E) \in U -> ([fset t^-, fAX (fAU s t)^- & C],E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_foc s t C : (fAU s t^+ |` C , aVoid) \in U -> (C,aAU (s, t, fset0)) \in U.
Proof. by rewrite -AU_shift in_fsetX AsV [_ \in Hs]powersetE sub0x. Qed.
Lemma genU_AUhl s t H C : (C, aAU (s, t, H)) \in U -> (t^+ |` C, aVoid) \in U.
Proof. rewrite -AU_shift => /andP [A _]. apply: (@genU_AUpl s). by rewrite in_fsetX AsV. Qed.
Lemma genU_AUhr s t H C : (C, aAU (s, t, H)) \in U -> (s^+ |` C, aAXU (s, t, C |` H)) \in U.
Proof.
rewrite !in_fsetX -AsX !AsAU powersetU -/Cs -andbA.
rewrite [_ |` _ \in Hs]powersetU powersetE fsub1 => /and3P [? HF ?].
apply/and5P ; split => //. rewrite powersetE fsub1. move: (sfc_F HF) => /=. by bcase.
Qed.
Lemma genU_jmp C E : (C,E) \in U -> (R C, aR E) \in U.
Proof. rewrite !in_fsetX /= => /andP [? ?]. rewrite RinU //. exact: genU_aR. Qed.
Lemma genU_ARpl s t C E : (fAR s t^+ |` C,E) \in U -> ([fset s^+, t^+ & C],E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_ARpr s t C E : (fAR s t^+ |` C,E) \in U -> ([fset t^+, fAX (fAR s t)^+ & C],E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_ARnl s t C E : (fAR s t^- |` C,E) \in U -> (t^- |` C,E) \in U.
Proof. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_ARnr s t C E : (fAR s t^- |` C,E) \in U -> ([fset s^-, fAX (fAR s t)^- & C],E) \in U.
Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
Lemma genU_ARhl s t H C : (C, aAR (s, t, H)) \in U -> (t^- |` C, aVoid) \in U.
Proof. rewrite -AR_shift => /andP [A _]. apply: (@genU_ARnl s). by rewrite in_fsetX AsV. Qed.
Lemma genU_ARhr s t H C : (C, aAR (s, t, H)) \in U -> (s^- |` C, aAXR (s, t, C |` H)) \in U.
Proof.
rewrite !in_fsetX -AsX' !AsAR powersetU -/Cs -andbA.
rewrite [_ |` _ \in Hs]powersetU powersetE fsub1 => /and3P [? HF ?].
apply/and5P ; split => //. rewrite powersetE fsub1. move: (sfc_F HF) => /=. by bcase.
Qed.
Lemma genU_foc' s t C : (fAR s t^- |` C, aVoid) \in U -> (C, aAR (s, t, fset0)) \in U.
Proof. by rewrite -AR_shift in_fsetX AsV [_ \in Hs]powersetE sub0x. Qed.
Lemma genU_aAXR s t H C : (C, aAXR (s, t, H)) \in U -> (R C, aAR (s, t, H)) \in U.
Proof.
rewrite !in_fsetX AsX'. case: (aAXR _ \in _) => //; rewrite ?andbF // !andbT.
exact: RinU.
Qed.
Hint Resolve genU_ipl genU_ipr genU_in genU_AXn genU_AUpl genU_AUpr genU_AUnl genU_AUnr genU_AUhl genU_AUhr genU_foc genU_jmp : core.
Definition step_plain_cases (D : {fset clause * annot}) (C : clause) s E :=
match s with
| fF^+ => true
| fV p^+ => fV p^- \in C
| (fImp t1 t2)^+ => ((t1^- |` C,E) \in D) && ((t2^+ |` C,E) \in D)
| (fImp t1 t2)^- => ([fset t1^+, t2^- & C],E) \in D
| fAX s^- => (s^- |` R C,aR E) \in D
| fAU s t^+ => ((t^+ |` C,E) \in D) && (([fset s^+, fAX (fAU s t)^+ & C],E) \in D)
| fAU s t^- => (([fset s^-, t^- & C], E) \in D) && (([fset t^-, fAX (fAU s t)^- & C],E) \in D)
| fAR s t^+ => (([fset s^+, t^+ & C], E) \in D) && (([fset t^+, fAX (fAR s t)^+ & C],E) \in D)
| fAR s t^- => ((t^- |` C,E) \in D) && (([fset s^-, fAX (fAR s t)^- & C],E) \in D)
| _ => false
end.
Definition step_plain (D : {fset clause * annot}) (A : clause * annot) :=
[some s in F, [some C in Cs, [some E in As, (A == (s |` C, E)) && step_plain_cases D C s E]]].
Definition step_annot (D : {fset clause * annot}) A :=
let: (C,E) := A in
match E with
| aAU (s, t, H) => ((t^+ |` C, aVoid) \in D) && ((s^+ |` C, aAXU (s, t, C |` H)) \in D) || (C \in H)
| aVoid => [some s in positives F, [some t in positives F, [some C' in Cs,
(C == fAU s t^+ |` C') && ((C', aAU (s, t, fset0)) \in D)]]]
|| [some s in negatives F, [some t in negatives F, [some C' in Cs,
(C == fAR s t^- |` C') && ((C', aAR (s, t, fset0)) \in D)]]]
| aAR (s, t, H) => ((t^- |` C, aVoid) \in D) && ((s^- |` C, aAXR (s, t, C |` H)) \in D) || (C \in H)
| aAXR(s ,t, H) => (R C,aAR (s,t,H)) \in D
| _ => false
end.
Definition step_jmp (D : {fset clause * annot}) (A : clause * annot) :=
let (C,E) := A in (R C, aR E) \in D.
Definition step (D : {fset clause * annot}) : {fset clause * annot} :=
[fset A in U | [|| step_plain D A, step_annot D A| step_jmp D A ]].
Lemma bounded_step : bounded U step.
Proof. move => C _. by rewrite /step subsep. Qed.
Lemma mono_step : monotone step.
Proof.
move => D D' /subP subD_D'. apply: sep_sub (subxx _) _ => A inU.
case/or3P => H; apply/or3P; [apply: Or31|apply: Or32|apply: Or33].
- apply: in_sub_has H => s inF. do 2 apply: in_sub_has => ? ?.
case (A == _) => //=.
destruct s as [[|p|s t|s|s t|s t][|]] => //=;
by [apply: subD_D'|case/andP => ? ?; apply/andP; split; exact: subD_D'].
- case: A inU H => C [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] //= _.
* case e: (C \in H); rewrite ?orbF // ?orbT.
case/andP => ? ?; apply/andP; split; exact: subD_D'.
* case e: (C \in H); rewrite ?orbF // ?orbT.
case/andP => ? ?; apply/andP; split; exact: subD_D'.
* exact: subD_D'.
* case/orP => H; [leftb|rightb]; move: H.
do 3 apply: in_sub_has => ? ?. case (C == _) => //=. exact: subD_D'.
do 3 apply: in_sub_has => ? ?. case (C == _) => //=. exact: subD_D'.
- case: A inU H => C E inU H. exact: subD_D'.
Qed.
Lemma plainP C u E :
step_plain_cases (fset.lfp U step) C u E -> (u |` C,E) \in U -> step_plain (fset.lfp U step) (u |` C,E).
Proof.
move => H. rewrite in_fsetX powersetU powersetE fsub1 -andbA -/Cs.
case/and3P => ? ? ?.
apply/hasP; exists u => //. apply/hasP; exists C => //. apply/hasP; exists E => //.
by rewrite eqxx.
Qed.
Lemma stepP (A : clause * annot) : A \in U -> reflect (gen A) (A \in fset.lfp U step).
Proof.
pose lfpE := fset.lfpE mono_step bounded_step.
move => A_in_U. apply: (iffP idP) => H.
- move: A H {A_in_U}. apply: fset.lfp_ind => /= A D IH.
change (clause * annot)%type in A. change {fset clause * annot} in D.
rewrite inE => /andP [_]. case/or3P.
+ case/hasP => s _. case/hasP => C _. case/hasP => E _. case/andP => [/eqP ->].
destruct s as [[|p|s t|s|s t|s t][|]] => //=;
try solve [ move/IH => ?; auto | case/andP => /IH P1 /IH P2; auto ].
move => H. by rewrite (fset1U H).
+ case: A => C. case => [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] //=; try case/orP.
* case/andP => /IH ? /IH; auto.
* move => inH. by rewrite (fset1U inH).
* case/andP => /IH ? /IH; auto.
* move => inH. by rewrite (fset1U inH).
* move/IH. exact: gen_aAXR.
* case/hasP => s _. case/hasP => t _. case/hasP => C' _.
case/andP => [/eqP -> /IH]. auto.
* case/hasP => s _. case/hasP => t _. case/hasP => C' _.
case/andP => [/eqP -> /IH]. auto.
+ case: A => C E /= /IH. exact: gen_jmp.
- elim: H A_in_U => {A}.
+ move => C E inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. exact: plainP inU.
+ move => p C E inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply: plainP inU => /=. by rewrite !inE.
+ move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply: plainP (inU) => /=. by rewrite IHs ?IHt //; eauto.
+ move => s t C E _ IH inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply: plainP (inU) => /=. by eauto.
+ move => s C E _ IH inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply: plainP (inU) => /=. by eauto.
+ move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply: plainP (inU) => /=. rewrite IHs ?IHt //; by eauto.
+ move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply: plainP (inU) => /=. rewrite IHs ?IHt //; by eauto.
+ move => s t C _ IH inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=.
move/genU_foc : (inU). case/fsetXP => ?.
rewrite AsAU => /andP [/sfc_F /and3P [? Hs Ht] _]. rewrite -!posE in Hs Ht. leftb.
apply/hasP; exists s => //. apply/hasP; exists t => //. apply/hasP; exists C => //.
rewrite eqxx /=. by eauto.
+ move => s t H C _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=.
rewrite IHs ?IHt //. exact: genU_AUhr. exact: genU_AUhl inU.
+ move => s t H C inU. by rewrite lfpE inE inU (_ : step_annot _ _ ) //= fset1U1.
+ move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply/plainP: (inU) => /=. rewrite IHs ?IHt //; by auto using genU_ARpl,genU_ARpr.
+ move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //.
apply/plainP: (inU) => /=. rewrite IHs ?IHt //; by eauto using genU_ARnl,genU_ARnr.
+ move => s t C _ IH inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. rightb.
move/genU_foc': (inU). case/fsetXP => ?.
rewrite AsAR => /andP [/sfc_F /and3P [? Hs Ht] _]. rewrite -!negE in Hs Ht.
apply/hasP; exists s => //. apply/hasP; exists t => //. apply/hasP; exists C => //.
rewrite eqxx IH //. exact: genU_foc'.
+ move => s t H C _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=.
rewrite IHs ?IHt //. exact: genU_ARhr. exact: genU_ARhl inU.
+ move => s t H C inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=.
by rewrite !inE.
+ move => s t H C _ IH inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=.
rewrite IH //. exact: genU_aAXR.
+ move => C E _ IH inU. rewrite lfpE inE inU (_ : step_jmp _ _) //=. auto.
Qed.
Lemma gen_decF (A : clause * annot) : A \in U -> decidable (gen A).
Proof. move => H. exact: decP (stepP H). Qed.
End gen_closure.
Lemma plain_inU {C} : (C,aVoid) \in U (sfc C).
Proof. by rewrite in_fsetX !inE //= andbT powersetE sub_sfc. Qed.
Lemma aAU_inU {C s t H} :
(C,aAU (s, t, H)) \in U (sfc (fAU s t^+ |` C `|` \bigcup_(C' in H) C')).
Proof.
rewrite -AU_shift; last exact: closed_sfc. apply/andP; split.
- apply: power_sub (sub_sfc _). by rewrite powersetE.
- rewrite powersetE. apply/subP => D inH. apply: power_sub (sub_sfc _).
rewrite powersetE. apply: fsubsetU. by rewrite -[D]/(id D) bigU1.
Qed.
Lemma aAR_inU {C s t H} :
(C,aAR (s, t, H)) \in U (sfc (fAR s t^- |` C `|` \bigcup_(C' in H) C')).
Proof.
rewrite -AR_shift; last exact: closed_sfc. apply/andP; split.
- apply: power_sub (sub_sfc _). by rewrite powersetE.
- rewrite powersetE. apply/subP => D inH. apply: power_sub (sub_sfc _).
rewrite powersetE. apply: fsubsetU. by rewrite -[D]/(id D) bigU1.
Qed.
Lemma aAXU_inU {C s t H} :
(C,aAXU (s, t, H)) \in U (sfc (fAU s t^+ |` C `|` \bigcup_(C' in H) C')).
Proof. rewrite in_fsetX -AsX -in_fsetX -/(U _). exact: aAU_inU. Qed.
Lemma aAXR_inU {C s t H} :
(C,aAXR (s, t, H)) \in U (sfc (fAR s t^- |` C `|` \bigcup_(C' in H) C')).
Proof. rewrite in_fsetX -AsX' -in_fsetX -/(U _). exact: aAR_inU. Qed.
Lemma gen_dec A : decidable (gen A).
Proof.
case: A => C [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] /=;
eauto using gen_decF, aAU_inU, aAXU_inU, aAR_inU, aAXR_inU, plain_inU, closed_sfc.
Qed.