MAYBE
MAYBE
TRS:
 {
          ifPlus(true(), x, y) -> p(y),
         ifPlus(false(), x, y) -> plus(p(x), y),
                   isZero(0()) -> true(),
                isZero(s(0())) -> false(),
               isZero(s(s(x))) -> isZero(s(x)),
                        inc(x) -> s(x),
                      inc(0()) -> s(0()),
                     inc(s(x)) -> s(inc(x)),
                    plus(x, y) -> ifPlus(isZero(x), x, inc(y)),
                        p(0()) -> 0(),
                       p(s(x)) -> x,
                    p(s(s(x))) -> s(p(s(x))),
         timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z),
                   times(x, y) -> timesIter(0(), x, y, 0()),
   ifTimes(true(), i, x, y, z) -> z,
  ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)),
                    ge(x, 0()) -> true(),
                 ge(0(), s(y)) -> false(),
                ge(s(x), s(y)) -> ge(x, y),
                   f1(x, y, z) -> f2(x, y, z),
                   f1(x, y, z) -> c(),
                   f0(x, y, z) -> d(),
                 f0(0(), y, x) -> f1(x, y, x),
                 f2(x, 1(), z) -> f0(x, z, z)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
            ifPlus(true(), x, y) -> p(y),
           ifPlus(false(), x, y) -> plus(p(x), y),
                     isZero(0()) -> true(),
                  isZero(s(0())) -> false(),
                 isZero(s(s(x))) -> isZero(s(x)),
                          inc(x) -> s(x),
                        inc(0()) -> s(0()),
                       inc(s(x)) -> s(inc(x)),
                      plus(x, y) -> ifPlus(isZero(x), x, inc(y)),
                          p(0()) -> 0(),
                         p(s(x)) -> x,
                      p(s(s(x))) -> s(p(s(x))),
           timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z),
                     times(x, y) -> timesIter(0(), x, y, 0()),
     ifTimes(true(), i, x, y, z) -> z,
    ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)),
                      ge(x, 0()) -> true(),
                   ge(0(), s(y)) -> false(),
                  ge(s(x), s(y)) -> ge(x, y),
                     f1(x, y, z) -> f2(x, y, z),
                     f1(x, y, z) -> c(),
                     f0(x, y, z) -> d(),
                   f0(0(), y, x) -> f1(x, y, x),
                   f2(x, 1(), z) -> f0(x, z, z)
   }
  Fail