mod! EQBOOL {
  op _=_ : Bool Bool -> Bool {comm}
  var B : Bool
  eq (B = B) = true .
  eq (true = false) = false .
-- Lemmas
  op eqbool-lemma1 : Bool -> Bool .
  eq eqbool-lemma1(B) = not((not B) = B) .
}

mod! PNAT {
  [Nat]
  op 0 : -> Nat 
  op s : Nat -> Nat 
  op _=_ : Nat Nat -> Bool {comm}
  vars X Y : Nat 
  eq (X = X) = true .
  eq (0 = 0) = true .
  eq (0 = s(X)) = false .
  eq (s(X) = s(Y)) = (X = Y) .
}

mod! PACKET {
  pr(PNAT)
  [Packet]
  op pac : Nat -> Packet
  op _=_ : Packet Packet -> Bool {comm}
  var P : Packet
  vars X Y : Nat
  eq (P = P) = true .
  eq (pac(X) = pac(Y)) = (X = Y) .
}

mod* EQTRIV {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
}

mod! PAIR(M :: EQTRIV,N :: EQTRIV) {
  [Pair]
  op <_,_> : Elt.M Elt.N -> Pair
  op fst : Pair -> Elt.M
  op snd : Pair -> Elt.N
  op _=_ : Pair Pair -> Bool {comm}
  var P : Pair
  vars X1 X2 : Elt.M
  vars Y1 Y2 : Elt.N
  eq fst(< X1,Y1 >) = X1 .
  eq snd(< X1,Y1 >) = Y1 .
  eq (P = P) = true .
  eq (< X1,Y1 > = < X2,Y2 >) = (X1 = X2) and (Y1 = Y2) .
}

mod! CELL(M :: EQTRIV) {
  [Cell]
  op empty : -> Cell
  op c : Elt.M -> Cell
  op get : Cell -> Elt.M
  op _=_ : Cell Cell -> Bool {comm}
  var C : Cell
  vars X Y : Elt.M
  eq get(c(X)) = X .
  eq (C = C) = true .
  eq (empty = empty) = true .
  eq (empty = c(X)) = false .
  eq (c(X) = c(Y)) = (X = Y) .
}

mod! LIST(M :: EQTRIV) {
  [List]
  op nil : -> List
  op __ : Elt.M List -> List
  op hd : List -> Elt.M
  op tl : List -> List 
  op _=_ : List List -> Bool {comm}
  vars L L1 L2 : List
  vars X Y : Elt.M
  eq hd(X L) = X .
  eq tl(X L) = L .
  eq (L = L) = true .
  eq (nil = nil) = true .
  eq (nil = X L) = false .
  eq (X L1 = Y L2) = (X = Y and L1 = L2) .
}

view EQTRIV2PACKET from EQTRIV to PACKET {
  sort Elt -> Packet,
  op _=_ -> _=_
}

mod! PACKET-LIST {
  pr(LIST(M <= EQTRIV2PACKET))
  op mk : Nat -> List 
  var X : Nat
  eq mk(0) = pac(0) nil .
  eq mk(s(X)) = pac(s(X)) mk(X) .
}

view EQTRIV2EQBOOL from EQTRIV to EQBOOL {
  sort Elt -> Bool,
  op _=_ -> _=_
}

mod! BOOL-PACKET-PAIR {
  pr(PAIR(M <= EQTRIV2EQBOOL,N <= EQTRIV2PACKET)*{sort Pair -> BPPair})
}

view EQTRIV2BOOL-PACKET-PAIR from EQTRIV to BOOL-PACKET-PAIR {
  sort Elt -> BPPair,
  op _=_ -> _=_
}

mod! BOOL-CELL {
  pr(CELL(M <= EQTRIV2EQBOOL)*{sort Cell -> BCell})
}

mod! BOOL-PACKET-PAIR-CELL {
  pr(CELL(M <= EQTRIV2BOOL-PACKET-PAIR)*{sort Cell -> PCell})
}