mod TEST-REW1 is
protecting NAT .
sort Counter .
ops rule1 rule2 rule3 : Nat -> Counter [ctor] .
op f : Counter Counter Counter -> Counter [ctor] .
vars N M K : Nat .
rl [rule1] : f(rule1(N), rule2(M), rule3(K))
=> f(rule1(s N), rule2(M), rule3(K)) .
rl [rule2] : f(rule1(N), rule2(M), rule3(K))
=> f(rule1(N), rule2(s M), rule3(K)) .
rl [rule3] : f(rule1(N), rule2(M), rule3(K))
=> f(rule1(N), rule2(M), rule3(s K)) .
endm
rew [100] f(rule1(0), rule2(0), rule3(0)) .
frew [100] f(rule1(0), rule2(0), rule3(0)) .
mod TEST-REW2 is
protecting NAT .
sort Counter .
ops rule1 rule2 rule3 : Nat -> Counter [ctor] .
op f : Counter Counter Counter -> Counter [ctor] .
var N : Nat .
rl [rule1] : rule1(N) => rule1(s N) .
rl [rule2] : rule2(N) => rule2(s N) .
rl [rule3] : rule3(N) => rule3(s N) .
endm
rew [100] f(rule1(0), rule2(0), rule3(0)) .
rew [100] f(rule3(0), rule2(0), rule1(0)) .
frew [100] f(rule1(0), rule2(0), rule3(0)) .
frew [100] f(rule3(0), rule2(0), rule1(0)) .
frew [100] f(rule1(0), rule1(0), rule1(0)) .