MAYBE
MAYBE
TRS:
 {
                  mark(0()) -> active(0()),
        mark(minus(X1, X2)) -> active(minus(X1, X2)),
                 mark(s(X)) -> active(s(mark(X))),
               mark(true()) -> active(true()),
          mark(geq(X1, X2)) -> active(geq(X1, X2)),
              mark(false()) -> active(false()),
          mark(div(X1, X2)) -> active(div(mark(X1), X2)),
       mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)),
      active(minus(0(), Y)) -> mark(0()),
  active(minus(s(X), s(Y))) -> mark(minus(X, Y)),
        active(geq(X, 0())) -> mark(true()),
     active(geq(0(), s(Y))) -> mark(false()),
    active(geq(s(X), s(Y))) -> mark(geq(X, Y)),
     active(div(0(), s(Y))) -> mark(0()),
    active(div(s(X), s(Y))) ->
  mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())),
   active(if(true(), X, Y)) -> mark(X),
  active(if(false(), X, Y)) -> mark(Y),
        minus(X1, mark(X2)) -> minus(X1, X2),
      minus(X1, active(X2)) -> minus(X1, X2),
        minus(mark(X1), X2) -> minus(X1, X2),
      minus(active(X1), X2) -> minus(X1, X2),
                 s(mark(X)) -> s(X),
               s(active(X)) -> s(X),
          geq(X1, mark(X2)) -> geq(X1, X2),
        geq(X1, active(X2)) -> geq(X1, X2),
          geq(mark(X1), X2) -> geq(X1, X2),
        geq(active(X1), X2) -> geq(X1, X2),
          div(X1, mark(X2)) -> div(X1, X2),
        div(X1, active(X2)) -> div(X1, X2),
          div(mark(X1), X2) -> div(X1, X2),
        div(active(X1), X2) -> div(X1, X2),
       if(X1, X2, mark(X3)) -> if(X1, X2, X3),
     if(X1, X2, active(X3)) -> if(X1, X2, X3),
       if(X1, mark(X2), X3) -> if(X1, X2, X3),
     if(X1, active(X2), X3) -> if(X1, X2, X3),
       if(mark(X1), X2, X3) -> if(X1, X2, X3),
     if(active(X1), X2, X3) -> if(X1, X2, X3)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                    mark(0()) -> active(0()),
          mark(minus(X1, X2)) -> active(minus(X1, X2)),
                   mark(s(X)) -> active(s(mark(X))),
                 mark(true()) -> active(true()),
            mark(geq(X1, X2)) -> active(geq(X1, X2)),
                mark(false()) -> active(false()),
            mark(div(X1, X2)) -> active(div(mark(X1), X2)),
         mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)),
        active(minus(0(), Y)) -> mark(0()),
    active(minus(s(X), s(Y))) -> mark(minus(X, Y)),
          active(geq(X, 0())) -> mark(true()),
       active(geq(0(), s(Y))) -> mark(false()),
      active(geq(s(X), s(Y))) -> mark(geq(X, Y)),
       active(div(0(), s(Y))) -> mark(0()),
      active(div(s(X), s(Y))) ->
    mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())),
     active(if(true(), X, Y)) -> mark(X),
    active(if(false(), X, Y)) -> mark(Y),
          minus(X1, mark(X2)) -> minus(X1, X2),
        minus(X1, active(X2)) -> minus(X1, X2),
          minus(mark(X1), X2) -> minus(X1, X2),
        minus(active(X1), X2) -> minus(X1, X2),
                   s(mark(X)) -> s(X),
                 s(active(X)) -> s(X),
            geq(X1, mark(X2)) -> geq(X1, X2),
          geq(X1, active(X2)) -> geq(X1, X2),
            geq(mark(X1), X2) -> geq(X1, X2),
          geq(active(X1), X2) -> geq(X1, X2),
            div(X1, mark(X2)) -> div(X1, X2),
          div(X1, active(X2)) -> div(X1, X2),
            div(mark(X1), X2) -> div(X1, X2),
          div(active(X1), X2) -> div(X1, X2),
         if(X1, X2, mark(X3)) -> if(X1, X2, X3),
       if(X1, X2, active(X3)) -> if(X1, X2, X3),
         if(X1, mark(X2), X3) -> if(X1, X2, X3),
       if(X1, active(X2), X3) -> if(X1, X2, X3),
         if(mark(X1), X2, X3) -> if(X1, X2, X3),
       if(active(X1), X2, X3) -> if(X1, X2, X3)
   }
  Fail