fact: Definition check_inconsistent (f : NFormula) : bool := let (e, op) := f in match e with | Pc c => match op with | Equal => cneqb c cO | NonStrict => c [<] cO | Strict => c [<=] cO | NonEqual => c [=] cO end | _ => false end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl