fact: Record monSpec monR := { monP : symInt -> Prop ; mon_check : forall (i : symInt), option (monP i) ; mon_ok : forall (i : symInt), monP i -> Vmonotone1 (interpret (projT2 i)) monR }.
imports: Coq(Program) CoLoR(ATrs RelUtil SN AWFMInterpretation AMannaNess ACompat ListUtil ARelation LogicUtil OptUtil IntBasedChecker Problem NaryFunction Proof)