fact: 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.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)