include "common/Graphs.ma".

record property_lattice : Type[1] ≝
{ l_property  :> Type[0]
; l_bottom    : l_property
; l_equal : l_property → l_property → bool
; l_included : l_property → l_property → bool
; l_is_maximal : l_property → bool
}.

definition valuation ≝ λlatt : property_lattice.label → latt.
definition rhs ≝ λlatt : property_lattice.valuation latt → latt.
definition equations ≝ λlatt : property_lattice.label → rhs latt.

record fixpoint (latt : property_lattice) : Type[0] ≝
{ fix_lfp :1> equations latt → valuation latt
; fix_correct :
  ∀eqs : equations latt.
  let sol ≝ fix_lfp eqs in
  ∀l : label.
  l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *)
}.

axiom the_fixpoint : ∀latt.fixpoint latt.