*** This module converts a BV structure to an equivalent 
*** structure in *normal form*, i.e. negation is pushed to 
*** the atoms and all the units are equivalently removed. 

fmod NF is
  sorts Atom Unit Structure .
  subsort Atom < Structure .
  subsort Unit < Structure .
  
  op o : -> Unit [ctor] .
  op -_ : Structure -> Structure .                *** negation
  op [_,_] : Structure Structure -> Structure .   *** par structure
  op {_,_} : Structure Structure -> Structure .   *** copar structure
  op <_;_> : Structure Structure -> Structure .   *** seq structure  

  ops a b c d e : -> Atom [ctor] .                *** positive atoms

  var R T U : Structure .

    eq - o = o .
    eq - [ R , T ] = { - R , - T } .
    eq - { R , T } = [ - R , - T ] .
    eq - < R ; T > = < - R ; - T > .
    eq - - R  = R .
    
    eq   [ R , o ] = R .
    eq   [ o , R ] = R .
    eq   { R , o } = R .
    eq   { o , R } = R .
    eq   < R ; o > = R .
    eq   < o ; R > = R .

endfm

*** Example query

*** reduce  - { [ a  , b ] , o } .