fact: Fixpoint eval (s: form) := match s with | fF => (fun _ => False) | fV x => label x | fImp s t => (fun v => eval s v -> eval t v) | fAX p s => (fun v => forall w, reach p v w -> eval s w) end with reach (p: prog) : M -> M -> Prop := match p with | pV a => trans a | pSeq p0 p1 => (fun v w => exists2 u, reach p0 v u & reach p1 u w) | pCh p0 p1 => (fun v w => reach p0 v w \/ reach p1 v w) | pStar p => star (reach p) | pTest s => fun v w => w = v /\ eval s v | pConv p => fun v w => reach p w v end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)