%sig Order = {
  %include FOL %open i o forall ded == and =>.
  leq : i -> i -> o.  %infix none 4 leq.
  refl : ded forall [x] (x leq x).
  antisym : ded forall [x] (forall [y] (x leq y and y leq x => x == y)).
  trans : ded forall [x] (forall [y] (forall [z] (x leq y and y leq z => x leq z))).
}.

%view Opposite : Order -> Order = {
  leq := [x][y] (y leq x).
  refl := refl.
  antisym := FOL..forallI [x] FOL..forallI [y] FOL..impI [z] (FOL..impE (FOL..forallE y (FOL..forallE x antisym)) (FOL..andI (FOL..andEr z) (FOL..andEl z))).
  trans := FOL..forallI [x] FOL..forallI [y] FOL..forallI [z] FOL..impI [u] (FOL..impE (FOL..forallE x (FOL..forallE y (FOL..forallE z trans))) (FOL..andI (FOL..andEr u) (FOL..andEl u))).
}.

%sig Semilattice = {
  %include FOL %open ded forall == <=>.
  %struct sgc : SemigroupCommut.
  %struct midem : MagmaIdempotent = {%struct mag := sgc.sg.mag.} %open *.
  %struct ord : Order %open leq.
  ax : ded forall [x] (forall [y] (x * y == x <=> x leq y)).
}.

%sig SemilatticeBounded = {
  %include FOL.
  %struct sl : Semilattice.
  %struct mon : Monoid = {%struct sg := sl.sgc.sg.}.
}.

%sig Lattice = {
  %include FOL.
  %struct meet : Semilattice = {}.
  %struct join : Semilattice = {%struct ord := Opposite meet.ord.}.
  /\ = [x][y] x meet.midem.mag.* y.
  \/ = [x][y] x join.midem.mag.* y.
}.

%sig LatticeBounded = {
  %include FOL.
  %struct lat : Lattice = {}.
  %struct meetBdd : SemilatticeBounded = {%struct sl := lat.meet.}. 
  %struct joinBdd : SemilatticeBounded = {%struct sl := lat.join.}. 
  bot = meetBdd.mon.rid.e.
  top = joinBdd.mon.rid.e.
}.