fact: Fixpoint reach_demo cls p : rel clause := match p with | pV a => rtrans a | pSeq p0 p1 => (fun C D => [some C' in cls, reach_demo cls p0 C C' && reach_demo cls p1 C' D]) | pCh p0 p1 => (fun C D => reach_demo cls p0 C D || reach_demo cls p1 C D) | pStar p => (fun C D => connect_in cls (reach_demo cls p) C D) | pTest s => (fun C D => (C == D) && (s^+ \in C)) end.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.PDL(PDL_def)