fmod NATUTIL is

protecting NAT .

sort NatList .
op sNatList : Nat -> NatList .
op eNatList : -> NatList .
op __ : NatList NatList -> NatList [assoc id: eNatList] .

var nat nat' : Nat .
var natlist natlist' : NatList .

op contains : NatList Nat -> Bool .
eq contains(eNatList, nat') = false .
eq contains((sNatList(nat) natlist), nat') = 
     (nat' == nat) or contains(natlist, nat') .

op add : NatList Nat -> NatList .
eq add(natlist,nat) = (natlist sNatList(nat)) .

op  add' : NatList Nat -> NatList .
ceq add'(natlist,nat) = natlist 
    if contains(natlist, nat) .
ceq add'(natlist,nat) = (natlist sNatList(nat)) 
    if not(contains(natlist, nat)) .

op  rm : NatList Nat -> NatList .
eq  rm(eNatList,nat) = eNatList .
ceq rm((sNatList(nat) natlist),nat') = rm(natlist,nat')
    if (nat' == nat) .
ceq rm((sNatList(nat) natlist),nat') = (sNatList(nat) rm(natlist,nat'))
    if (nat' =/= nat) .

op subset : NatList NatList -> Bool .
eq subset(eNatList,natlist') = true .
eq subset((sNatList(nat) natlist), natlist') = 
    contains(natlist',nat) and subset(natlist,natlist') .

------------------------

sort NatSet .
op sNatSet : Nat -> NatSet .
op eNatSet : -> NatSet .
op __ : NatSet NatSet -> NatSet [assoc comm id: eNatSet] .

eq sNatSet(nat) sNatSet(nat) = sNatSet(nat) .

var natset natset' : NatSet .

op contains : NatSet Nat -> Bool .
eq contains(eNatSet, nat') = false .
eq contains((sNatSet(nat) natset), nat') = 
     (nat' == nat) or contains(natset, nat') .

op  inter : NatSet NatSet -> NatSet .
eq  inter(eNatSet,natset') = eNatSet .
ceq inter(sNatSet(nat) natset, natset') = 
    sNatSet(nat) inter(natset,natset')
    if contains(natset',nat) .
ceq inter(sNatSet(nat) natset, natset') = 
    inter(natset,natset')
    if not(contains(natset',nat)) .

op contains-all-lt : NatSet Nat -> Bool .
eq contains-all-lt(eNatSet,0) = true .
eq contains-all-lt(eNatSet,(s nat)) = false .
eq contains-all-lt((natset sNatSet(nat)),(s nat)) = contains-all-lt(natset,nat) .

op add : NatSet Nat -> NatSet .
eq add(natset,nat) = (natset sNatSet(nat)) .

op  add' : NatSet Nat -> NatSet .
ceq add'(natset,nat) = natset 
    if contains(natset, nat) .
ceq add'(natset,nat) = (natset sNatSet(nat)) 
    if not(contains(natset, nat)) .

op  rm : NatSet Nat -> NatSet .
eq  rm(eNatSet,nat) = eNatSet .
ceq rm((sNatSet(nat) natset),nat') = rm(natset,nat')
    if (nat' == nat) .
ceq rm((sNatSet(nat) natset),nat') = (sNatSet(nat) rm(natset,nat'))
    if (nat' =/= nat) .

op subset : NatSet NatSet -> Bool .
eq subset(eNatSet,natset') = true .
eq subset((sNatSet(nat) natset), natset') = 
    contains(natset',nat) and subset(natset,natset') .

endfm