fmod ASSOC-IDEMP is
   protecting QID .
   sorts List Set .
   subsorts Qid < List Set .
   op __ : List List -> List [assoc] .           *** list concatenation
   op _,_ : Set Set -> Set [assoc comm] .   *** set union
   op {_} : List -> Set .                   *** set of a list

   var I : Qid .
   var S : Set .
   vars L P Q : List .

   eq S,S = S .
   eq {I} = I .
   eq {I L} = I,{L} .
   eq L L = L .
   ceq L P Q = L Q if {L} == {Q} and {L P} == {L} .
endfm

red 'a 'b 'c .
***(
reduce in ASSOC-IDEMP : 'a 'b 'c .
rewrites: 7 in -10ms cpu (0ms real) (~ rewrites/second)
result List: 'a 'b 'c
)

red 'a 'b 'c 'b 'a 'b 'c .
***(
reduce in ASSOC-IDEMP : 'a 'b 'c 'b 'a 'b 'c .
rewrites: 6505 in 29ms cpu (39ms real) (216840 rewrites/second)
result List: 'a 'b 'c
)

red 'a 'b 'c == 'a 'b 'c 'b 'a 'b 'c .
***(
reduce in ASSOC-IDEMP : 'a 'b 'c == 'a 'b 'c 'b 'a 'b 'c .
rewrites: 6506 in 29ms cpu (39ms real) (216873 rewrites/second)
result Bool: true
)