in nat.maude

fmod NAT-SET is
   protecting NAT .

   sorts NeSet Set .
   subsort Nat < NeSet < Set .

   op empty-set : -> Set .
   op __ : Set Set -> Set [assoc comm id: empty-set] .
   op __ : NeSet NeSet -> NeSet [assoc comm id: empty-set] .

   op is-in : Nat Set -> Bool .
   op delete : Nat Set -> Set .
   op card : Set -> Nat .
   op _-_ : Set Set -> Set .

   vars N N' : Nat .
   vars S S' : Set .

   eq N N = N .
   eq is-in(N, empty-set) = false .
   eq is-in(N, N' S) = N == N' or is-in(N,S) .
   eq delete(N, empty-set) = empty-set .
   eq delete(N, N S) = delete(N, S) .
   ceq delete(N, N' S) = N' delete(N, S) if N =/= N' .
   eq S - empty-set = S .
   eq S - (N S') = delete(N, S) - S' .
   eq card(empty-set) = 0 .
   eq card(N S) = s(0) + card(delete(N,S)) .
endfm

red card(0 s(0) s(s(0)) s(s(s(0))) s(0) s(s(s(s(0)))) s(s(s(0)))) .
***(
reduce in NAT-SET : card(0 s(0) s(s(0)) s(s(
    s(0))) s(0) s(s(s(0))) s(s(s(s(0))))) .
rewrites: 43 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(s(s(0)))))

*** 5
)

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

red card(
      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-SET : card(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: 41 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: 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-SET : 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: 33 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-SET : 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: 37 in -10ms cpu (0ms real) (~ rewrites/second)
result Bool: false
)