in nat-div.maude fmod NAT is protecting NAT-DIV . op min : Nat Nat -> Nat . op max : Nat Nat -> Nat . op _<_ : Nat Nat -> Bool . op odd? : Nat -> Bool . op even? : Nat -> Bool . vars M N : Nat . eq min(N, M) = if M > N then N else M fi . eq max(N, M) = if M > N then M else N fi . eq N < M = N <= M and N =/= M . eq even?(0) = true . eq even?(s(M)) = odd?(M) . eq odd?(0) = false . eq odd?(s(M)) = even?(M) . endfm red (s(s(s(s(s(0))))) * s(s(s(s(0))))) div s(s(s(0))) . ***( *** (5 * 4) div 3 = 6 red (s(s(s(s(s(0))))) * s(s(s(s(0))))) div s(s(s(0))) . reduce in NAT : (s(s(s(s(s(0))))) * s(s(s(s( 0))))) div s(s(s(0))) . rewrites: 154 in -10ms cpu (0ms real) (~ rewrites/second) result NzNat: s(s(s(s(s(s(0)))))) ) red (s(s(s(s(s(0))))) * s(s(s(s(0))))) mod s(s(s(0))) . ***( *** (5 * 4) mod 3 = 2 reduce in NAT : (s(s(s(s(s(0))))) * s(s(s(s(0))))) mod s(s( s(0))) . rewrites: 154 in -10ms cpu (0ms real) (~ rewrites/second) result NzNat: s(s(0)) ) red even?((s(s(s(s(s(0))))) * s(s(s(s(0))))) div s(s(s(0)))) . ***( *** even?((5 * 4) div 3) = even?(6) = true reduce in NAT : even?((s(s(s(s(s(0))))) * s(s(s(s(0))))) div s(s(s(0)))) . rewrites: 161 in -10ms cpu (0ms real) (~ rewrites/second) result Bool: true ) red odd?((s(s(s(s(s(0))))) * s(s(s(s(0))))) mod s(s(s(0)))) . ***( *** odd?((5 * 4) mod 3) = odd?(2) = false reduce in NAT : odd?((s(s(s(s(s(0))))) * s(s(s(s(0))))) mod s(s(s(0)))) . rewrites: 157 in -10ms cpu (0ms real) (~ rewrites/second) result Bool: false ) red max(s(s(s(s(s(0))))), s(s(s(s(0))))) < min(s(s(s(s(s(0))))), s(s(s(s(0))))) . ***( *** max(5, 4) < min(5, 4) = 5 < 4 = false reduce in NAT : max(s(s(s(s(s(0))))), s(s(s(s(0))))) < min( s(s(s(s(s(0))))), s(s(s(s(0))))) . rewrites: 28 in -10ms cpu (0ms real) (~ rewrites/second) result Bool: false )