th OBJECT is
  sort Action .
  op skip : -> Action .

  sort State .
  op _--[_]->_ : State Action State -> Bool .

  var S : State .
  eq  S --[skip]-> S  =  true .
  *** this just says _--[skip]->_ is reflexive,
  *** but eq S --[skip]-> S' = (S == S') doesn't work in Eqlog
endth

obj PNAT is
  sort Nat .
  op 0 : -> Nat .
  op s : Nat -> Nat .
endo

obj NATLIST is pr PNAT .
  sort NatList .
  op [_] : Nat -> NatList .
  op _++_ : NatList NatList -> NatList [assoc] .
  op empty : -> NatList .
  var L : NatList .
  eq  L ++ empty  =  L .
endo

obj AOBJ is
  pr PNAT .

  sort Action .
  op askip : -> Action .   *** idle transition
  op inc   : -> Action .   *** increment 1st register
  op write : -> Action .   *** put value in 1st register to 2nd

  sort State .
  op A[_,_] : Nat Nat -> State .
  
  op _--A[_]->_ : State Action State -> Bool .

  vars M N : Nat .
  eq  A[M,N]  --A[askip]->  A[M,N]     =  true .
  eq  A[M,N]  --A[ inc ]->  A[s(M),N]  =  true .
  eq  A[M,N]  --A[write]->  A[M,M]     =  true .
endo


obj BOBJ is
  pr PNAT .

  sort Action .
  op bskip : -> Action .   *** idle transition
  op copy  : -> Action .   *** put value in 1st register into 2nd
  op get   : -> Action .   *** get new value into 1st register

  sort State .
  op B[_,_] : Nat Nat -> State .
  
  op _--B[_]->_ : State Action State -> Bool .

  vars M M' N : Nat .
  eq  B[M,N]  --B[bskip]->  B[M,N]   =  true .
  eq  B[M,N]  --B[copy ]->  B[M,M]   =  true .
  eq  B[M,N]  --B[ get ]->  B[M',N]  =  true .
endo

obj IN-PORT is
  pr PNAT .
  sort Action .
  op skip : -> Action .
  op be : Nat -> Action .
  sort State .
  op In[_] : Nat -> State .
  op _--I[_]->_ : State Action State -> Bool .
  vars M N : Nat .
  eq  In[M] --I[ skip]-> In[M]  =  true .
  eq  In[M] --I[be(N)]-> In[N]  =  true .
endo

obj OUT-PORT is
  pr PNAT .
  sort Action .
  op oskip : -> Action .
  op be : Nat -> Action .
  sort State .
  op Out[_] : Nat -> State .
  op _--O[_]->_ : State Action State -> Bool .
  vars M N : Nat .
  eq  Out[M] --O[oskip]-> Out[M]  =  true .
  eq  Out[M] --O[be(N)]-> Out[N]  =  true .
endo

obj CHANNEL is
  pr NATLIST .
  sort Action .
  op get : Nat -> Action .
  op send : Nat -> Action .
  op get_&send_ : Nat Nat -> Action .
  sort State .
  op ([_:_:_]) : Nat NatList Nat -> State .
  op _--C[_]->_ : State Action State -> Bool .
  var C : State .
  var L : NatList .
  vars M N P Q : Nat .

  eq  [M : L : N] --C[get(P)]->
      [P : [P] ++ L : N]  =  true .

  eq  [M : empty : N] --C[send(P)]-> C  =  false .

  eq  [M : L ++ [P] : N] --C[send(P)]->
      [M : L : P]  =  true .

  eq  [M : L ++ [P] : N] --C[get Q &send P]->
      [Q : [Q] ++ L : P]  =  true .

  eq  [M : empty : N] --C[get Q &send(Q)]->
      [Q : empty : Q]  =  true .
endo