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