in nat.maude

fmod NAT-MSET is
   protecting NAT .

   sorts NeMset Mset .
   subsort Nat < Mset .

   op empty-mset : -> Mset .
   op __ : Mset Mset -> Mset [assoc comm id: empty-mset] .

   op size : Mset -> Nat .
   op mult : Nat Mset -> Nat .
   op delete : Nat Mset -> Mset .
   op is-in : Nat Mset -> Bool .

   vars N N' : Nat .
   var S : Mset .

   eq size(empty-mset) = 0 .
   eq size(N S) = s(0) + size(S) .
   eq mult(N, empty-mset) = 0 .
   eq mult(N, N S) = s(0) + mult(N, S) .
   ceq mult(N, N' S) = mult(N, S) if N =/= N' .
   eq delete(N, empty-mset) = empty-mset .
   eq delete(N, N S) = delete(N, S) .
   ceq delete(N, N' S) = N' delete(N, S) if N =/= N' .
   eq is-in(N, S) = mult(N, S) > 0 .
endfm

red size(0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0)))) .
***(
reduce in NAT-MSET : size(0 s(0) s(s(0)) s(s(s(0))) s(0) s(
    s(s(0))) s(s(s(s(0))))) .
rewrites: 22 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(s(s(s(s(0)))))))

*** 7
)

red mult(s(s(0)), 0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0)))) .
***(
reduce in NAT-MSET : mult(s(s(0)), 0 s(0) s(s(0)) s(s(s(
    0))) s(0) s(s(s(0))) s(s(s(s(0))))) .
rewrites: 16 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(0)
)

red mult(s(0), 0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0)))) .
***(
reduce in NAT-MSET : mult(s(0), 0 s(0) s(s(0)) s(s(s(0)))
    s(0) s(s(s(0))) s(s(s(s(0))))) .
rewrites: 17 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(0))
)

red size(
      delete(s(s(0)), 
             0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0))))) .
***(
reduce in NAT-MSET : size(delete(s(s(0)), 0 s(0) s(s(0)) s(
    s(s(0))) s(0) s(s(s(0))) s(s(s(s(0)))))) .
rewrites: 33 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(s(s(s(0))))))
)

red is-in(s(s(0)), 0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0)))) .
***(
reduce in NAT-MSET : is-in(s(s(0)), 0 s(0) s(s(0)) s(s(s(
    0))) s(0) s(s(s(0))) s(s(s(s(0))))) .
rewrites: 21 in -10ms cpu (0ms real) (~ rewrites/second)
result Bool: true
)

red is-in(s(s(0)), 
      delete(s(s(0)), 
             0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0))))) .
***(
reduce in NAT-MSET : is-in(s(s(0)), delete(s(s(0)), 0 s(0)
    s(s(0)) s(s(s(0))) s(0) s(s(s(0))) s(s(s(s(0)))))) .
rewrites: 32 in -10ms cpu (0ms real) (~ rewrites/second)
result Bool: false
)