(fmod SATISFACTION is
  sorts State Prop NewBool .
   ops tt ff : -> NewBool [ctor] .
  op _|=_ : State Prop -> NewBool [frozen] .
endfm)