fmod M1 is
  sorts A B C D .
  subsorts A < B C < D .
  op a : -> A .
  op f : B -> B .
  op f : C -> C .
endfm

red in M1 : f(a) .

fmod M2 is
  sorts Zero 3*Nat Nat .
  subsorts Zero < 3*Nat < Nat .
  op zero : -> Zero .
  op s_ : Nat -> Nat .
  mb s s s N:3*Nat : 3*Nat .
endfm

red in M2 : zero .
red in M2 : s zero .
red in M2 : s s zero .
red in M2 : s s s zero .
red in M2 : s s s s zero .
red in M2 : s s s s s zero .
red in M2 : s s s s s s zero .

fmod M3 is
  pr NAT .
  sort MSet .
  subsort Nat < MSet .
  op empty : -> MSet .
  op _ _ : MSet MSet -> MSet [assoc comm id: empty] .
  op _\in_ : Nat MSet -> Bool .
  vars N M : Nat .
  var S : MSet .
  eq N \in (N S) = true .
  eq N \in empty = false .
  ceq N \in (M S) = N \in S if N =/= M .
endfm

red in M3 : 0 \in (1 2 0 2 1) .
red in M3 : 3 \in (1 2 0 2 1) .

fmod M4 is
  pr NAT .
  sort MSet .
  subsort Nat < MSet .
  op empty : -> MSet .
  op _ _ : MSet MSet -> MSet [assoc comm id: empty] .
  op _\in_ : Nat MSet -> Bool .
  var N : Nat .
  var S : MSet .
  eq N \in (N S) = true .
  eq N \in S = false [owise] .
endfm

red in M4 : 0 \in (1 2 0 2 1) .
red in M4 : 3 \in (1 2 0 2 1) .

fmod M5 is
  pr NAT .
  sort MSet .
  subsort Nat < MSet .
  op empty : -> MSet .
  op _ _ : MSet MSet -> MSet [assoc comm id: empty] .
  op enabled-\in : Nat MSet ~> Bool .
  op _\in_ : Nat MSet -> Bool .
  var N : Nat .
  var S : MSet .
  eq enabled-\in(N,N S) = true .
  eq N \in (N S) = true .
  ceq N \in S = false if enabled-\in(N,S) =/= true .
endfm

red in M5 : 0 \in (1 2 0 2 1) .
red in M5 : 3 \in (1 2 0 2 1) .

fmod M6 is
  pr NAT .
  sort MSet .
  subsort Nat < MSet .
  op empty : -> MSet .
  op _ _ : MSet MSet -> MSet [assoc comm id: empty] .
  op _\in_ : Nat MSet -> Bool .
  vars N M : Nat .
  var S : MSet .
  eq N \in (N S) = true .
  eq N \in (M S) = false [owise] .
endfm

red in M6 : 0 \in (1 2 0 2 1) .
red in M6 : 3 \in (1 2 0 2 1) .
red in M6 : 3 \in empty .