(view MachineInt from TRIV to MACHINE-INT is
  sort Elt to MachineInt .
endv)

(view Qid from TRIV to QID is
  sort Elt to Qid .
endv)

(view Term from TRIV to META-LEVEL is
  sort Elt to Term .
endv)

(view Configuration from TRIV to CONFIGURATION is
  sort Elt to Configuration .
endv)


(fmod PAIR[X :: TRIV, Y :: TRIV] is
  protecting BOOL .

  sort Pair[X, Y] .
  op pair : Elt.X Elt.Y -> Pair[X, Y] .

  op fst : Pair[X, Y] -> Elt.X .
  op snd : Pair[X, Y] -> Elt.Y .

  var A : Elt.X .
  var B : Elt.Y .

  eq fst(pair(A, B)) = A .
  eq snd(pair(A, B)) = B .
endfm)


(fmod SET[X :: TRIV] is
  protecting BOOL .
  protecting MACHINE-INT .

  sort Set[X] .
  op empty : -> Set[X] [ctor] .
  op set : Elt.X Set[X] -> Set[X] [ctor] .

  op singletonSet : Elt.X -> Set[X] . 
  op choose : Set[X] -> Elt.X .
  op in : Elt.X Set[X] -> Bool .
  op union : Set[X] Set[X] -> Set[X] .
  op diff : Set[X] Set[X] -> Set[X] .
  op card : Set[X] -> MachineInt .

  vars E E' : Elt.X .
  vars S S' : Set[X] .

  eq singletonSet(E) = set(E, empty) .

  eq choose(set(E, S)) = E .

  eq in(E, empty) = false .
  eq in(E, set(E', S')) = if (E == E') then true else in(E, S') fi .

  eq union(empty, S') = S' .
  eq union(set(E, S), S') = if in(E, S')
                            then union(S, S')
                            else set(E, union(S, S')) fi .

  eq diff(empty, S') = empty .
  eq diff(set(E, S), S') = if in(E, S')
                           then diff(S, S')
                           else set(E, diff(S, S')) fi .

  eq card(empty) = 0 .
  eq card(set(E, S)) = if in(E, S)
                       then card(S)
                       else 1 + card(S) fi .
endfm)

(fmod LIST[X :: TRIV] is
  protecting MACHINE-INT .

  sort List[X] .
  op nil : -> List[X] [ctor] .
  op list : Elt.X List[X] -> List[X] [ctor] .

  op hd : List[X] -> Elt.X .
  op tl : List[X] -> List[X] .

  op cons : Elt.X List[X] -> List[X] .
  op append : List[X] List[X] -> List[X] .
  op member : Elt.X List[X] -> Bool .
  op length : List[X] -> MachineInt .
  op nth : MachineInt List[X] -> Elt.X .
  op removenth : MachineInt List[X] -> List[X] .

  vars E E' : Elt.X .
  vars L L' : List[X] .
  var N : MachineInt .

  eq hd(list(E, L)) = E .

  eq tl(list(E, L)) = L .

  eq member(E, nil) = false .
  eq member(E, list(E', L')) = (E == E') or member(E, L') .

  eq cons(E, L) = list(E, L) .

  eq append(nil, L') = L' .
  eq append(list(E, L), L') = cons(E, append(L, L')) .

  eq length(nil) = 0 .
  eq length(list(E, L)) = 1 + length(L) .

  eq nth(0, L) = hd(L) .
  ceq nth(N, L) = nth(N - 1, tl(L))
        if N > 0 .

  eq removenth(0, L) = tl(L) .
  ceq removenth(N, L) = cons(hd(L), removenth(N - 1, tl(L)))
        if N > 0 .
endfm)

(fmod MULTISET[X :: TRIV] is
  protecting BOOL .
  protecting MACHINE-INT .
  protecting LIST[X] .

  sort MultiSet[X] .
  op empty : -> MultiSet[X] [ctor] .
  op multiset : Elt.X MultiSet[X] -> MultiSet[X] [ctor] .

  op singletonMultiSet : Elt.X -> MultiSet[X] .
  op choose : MultiSet[X] -> Elt.X .
  op in : Elt.X MultiSet[X] -> Bool .
  op union : MultiSet[X] MultiSet[X] -> MultiSet[X] .
  op diff : MultiSet[X] MultiSet[X] -> MultiSet[X] .
  op elim : Elt.X MultiSet[X] -> MultiSet[X] .
  op card : MultiSet[X] -> MachineInt .
  op makeList : MultiSet[X] -> List[X] .

  vars E E' : Elt.X .
  vars M M' : MultiSet[X] .

  eq singletonMultiSet(E) = multiset(E, empty) .

  eq choose(multiset(E, M)) = E .

  eq in(E, empty) = false .
  eq in(E, multiset(E', M')) = if (E == E') then true else in(E, M') fi .

  eq union(empty, M') = M' .
  eq union(multiset(E, M), M') = multiset(E, union(M, M')) .

  eq diff(empty, M') = empty .
  eq diff(multiset(E, M), M') = if in(E, M')
                                  then diff(M, elim(E, M'))
                                  else multiset(E, diff(M, M')) fi .

  eq elim(E, empty) = empty .
  eq elim(E, multiset(E', M')) = if (E == E') then M' else multiset(E', elim(E, M')) fi .

  eq card(empty) = 0 .
  eq card(multiset(E, M)) = 1 + card(M) .

  eq makeList(empty) = nil .
  eq makeList(multiset(E, M)) = cons(E, makeList(M)) .
endfm)

(view List`[MachineInt`] from TRIV to LIST[MachineInt] is
  sort Elt to List[MachineInt] .
endv)

(view List`[Qid`] from TRIV to LIST[Qid] is
  sort Elt to List[Qid] .
endv)

eof


(fmod TEST is
  protecting LIST[MachineInt] .
  protecting LIST[List`[MachineInt`]] .
  protecting MULTISET[MachineInt] .
  protecting SET[MachineInt] .
endfm)

(select SET[MachineInt] .)
(red diff(set(1, set(2, set(2, empty))), set(2, empty)) .)

(select MULTISET[MachineInt] .)
(red diffMS(multiset(1, multiset(2, multiset(2, empty))), multiset(2, empty)) .)

quit