MAYBE
TRS:
 {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
               zero(mark(X)) -> mark(zero(X)),
                 zero(ok(X)) -> ok(zero(X)),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(X)),
          prod(X1, mark(X2)) -> mark(prod(X1, X2)),
          prod(mark(X1), X2) -> mark(prod(X1, X2)),
        prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
               fact(mark(X)) -> mark(fact(X)),
                 fact(ok(X)) -> ok(fact(X)),
                  p(mark(X)) -> mark(p(X)),
                    p(ok(X)) -> ok(p(X)),
      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
    active(if(true(), X, Y)) -> mark(X),
   active(if(false(), X, Y)) -> mark(Y),
             active(zero(X)) -> zero(active(X)),
          active(zero(s(X))) -> mark(false()),
           active(zero(0())) -> mark(true()),
                active(s(X)) -> s(active(X)),
        active(prod(X1, X2)) -> prod(X1, active(X2)),
        active(prod(X1, X2)) -> prod(active(X1), X2),
       active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
        active(prod(0(), X)) -> mark(0()),
             active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
             active(fact(X)) -> fact(active(X)),
                active(p(X)) -> p(active(X)),
             active(p(s(X))) -> mark(X),
         active(add(X1, X2)) -> add(X1, active(X2)),
         active(add(X1, X2)) -> add(active(X1), X2),
        active(add(s(X), Y)) -> mark(s(add(X, Y))),
         active(add(0(), X)) -> mark(X),
           add(X1, mark(X2)) -> mark(add(X1, X2)),
           add(mark(X1), X2) -> mark(add(X1, X2)),
         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
             proper(zero(X)) -> zero(proper(X)),
                proper(s(X)) -> s(proper(X)),
                 proper(0()) -> ok(0()),
        proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
             proper(fact(X)) -> fact(proper(X)),
                proper(p(X)) -> p(proper(X)),
         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
              proper(true()) -> ok(true()),
             proper(false()) -> ok(false()),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {      if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
    if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3),
                 zero#(mark(X)) -> zero#(X),
                   zero#(ok(X)) -> zero#(X),
                    s#(mark(X)) -> s#(X),
                      s#(ok(X)) -> s#(X),
            prod#(X1, mark(X2)) -> prod#(X1, X2),
            prod#(mark(X1), X2) -> prod#(X1, X2),
          prod#(ok(X1), ok(X2)) -> prod#(X1, X2),
                 fact#(mark(X)) -> fact#(X),
                   fact#(ok(X)) -> fact#(X),
                    p#(mark(X)) -> p#(X),
                      p#(ok(X)) -> p#(X),
        active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3),
        active#(if(X1, X2, X3)) -> active#(X1),
               active#(zero(X)) -> zero#(active(X)),
               active#(zero(X)) -> active#(X),
                  active#(s(X)) -> s#(active(X)),
                  active#(s(X)) -> active#(X),
          active#(prod(X1, X2)) -> prod#(X1, active(X2)),
          active#(prod(X1, X2)) -> prod#(active(X1), X2),
          active#(prod(X1, X2)) -> active#(X1),
          active#(prod(X1, X2)) -> active#(X2),
         active#(prod(s(X), Y)) -> prod#(X, Y),
         active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)),
               active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))),
               active#(fact(X)) -> zero#(X),
               active#(fact(X)) -> s#(0()),
               active#(fact(X)) -> prod#(X, fact(p(X))),
               active#(fact(X)) -> fact#(p(X)),
               active#(fact(X)) -> fact#(active(X)),
               active#(fact(X)) -> p#(X),
               active#(fact(X)) -> active#(X),
                  active#(p(X)) -> p#(active(X)),
                  active#(p(X)) -> active#(X),
           active#(add(X1, X2)) -> active#(X1),
           active#(add(X1, X2)) -> active#(X2),
           active#(add(X1, X2)) -> add#(X1, active(X2)),
           active#(add(X1, X2)) -> add#(active(X1), X2),
          active#(add(s(X), Y)) -> s#(add(X, Y)),
          active#(add(s(X), Y)) -> add#(X, Y),
             add#(X1, mark(X2)) -> add#(X1, X2),
             add#(mark(X1), X2) -> add#(X1, X2),
           add#(ok(X1), ok(X2)) -> add#(X1, X2),
        proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)),
        proper#(if(X1, X2, X3)) -> proper#(X1),
        proper#(if(X1, X2, X3)) -> proper#(X2),
        proper#(if(X1, X2, X3)) -> proper#(X3),
               proper#(zero(X)) -> zero#(proper(X)),
               proper#(zero(X)) -> proper#(X),
                  proper#(s(X)) -> s#(proper(X)),
                  proper#(s(X)) -> proper#(X),
          proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)),
          proper#(prod(X1, X2)) -> proper#(X1),
          proper#(prod(X1, X2)) -> proper#(X2),
               proper#(fact(X)) -> fact#(proper(X)),
               proper#(fact(X)) -> proper#(X),
                  proper#(p(X)) -> p#(proper(X)),
                  proper#(p(X)) -> proper#(X),
           proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)),
           proper#(add(X1, X2)) -> proper#(X1),
           proper#(add(X1, X2)) -> proper#(X2),
                  top#(mark(X)) -> proper#(X),
                  top#(mark(X)) -> top#(proper(X)),
                    top#(ok(X)) -> active#(X),
                    top#(ok(X)) -> top#(active(X))}
  Weak:
  {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                zero(mark(X)) -> mark(zero(X)),
                  zero(ok(X)) -> ok(zero(X)),
                   s(mark(X)) -> mark(s(X)),
                     s(ok(X)) -> ok(s(X)),
           prod(X1, mark(X2)) -> mark(prod(X1, X2)),
           prod(mark(X1), X2) -> mark(prod(X1, X2)),
         prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                fact(mark(X)) -> mark(fact(X)),
                  fact(ok(X)) -> ok(fact(X)),
                   p(mark(X)) -> mark(p(X)),
                     p(ok(X)) -> ok(p(X)),
       active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
     active(if(true(), X, Y)) -> mark(X),
    active(if(false(), X, Y)) -> mark(Y),
              active(zero(X)) -> zero(active(X)),
           active(zero(s(X))) -> mark(false()),
            active(zero(0())) -> mark(true()),
                 active(s(X)) -> s(active(X)),
         active(prod(X1, X2)) -> prod(X1, active(X2)),
         active(prod(X1, X2)) -> prod(active(X1), X2),
        active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
         active(prod(0(), X)) -> mark(0()),
              active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
              active(fact(X)) -> fact(active(X)),
                 active(p(X)) -> p(active(X)),
              active(p(s(X))) -> mark(X),
          active(add(X1, X2)) -> add(X1, active(X2)),
          active(add(X1, X2)) -> add(active(X1), X2),
         active(add(s(X), Y)) -> mark(s(add(X, Y))),
          active(add(0(), X)) -> mark(X),
            add(X1, mark(X2)) -> mark(add(X1, X2)),
            add(mark(X1), X2) -> mark(add(X1, X2)),
          add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
              proper(zero(X)) -> zero(proper(X)),
                 proper(s(X)) -> s(proper(X)),
                  proper(0()) -> ok(0()),
         proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
              proper(fact(X)) -> fact(proper(X)),
                 proper(p(X)) -> p(proper(X)),
          proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
               proper(true()) -> ok(true()),
              proper(false()) -> ok(false()),
                 top(mark(X)) -> top(proper(X)),
                   top(ok(X)) -> top(active(X))}
  EDG:
   {
    (zero#(ok(X)) -> zero#(X), zero#(ok(X)) -> zero#(X))
    (zero#(ok(X)) -> zero#(X), zero#(mark(X)) -> zero#(X))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (fact#(ok(X)) -> fact#(X), fact#(ok(X)) -> fact#(X))
    (fact#(ok(X)) -> fact#(X), fact#(mark(X)) -> fact#(X))
    (p#(ok(X)) -> p#(X), p#(ok(X)) -> p#(X))
    (p#(ok(X)) -> p#(X), p#(mark(X)) -> p#(X))
    (active#(s(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(s(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(p(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(p(X)) -> p#(active(X)))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> p#(X))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> fact#(active(X)))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> fact#(p(X)))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> s#(0()))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> zero#(X))
    (active#(s(X)) -> active#(X), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(s(X)) -> active#(X), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(s(X)) -> active#(X), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(s(X)) -> active#(X), active#(zero(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(zero(X)) -> zero#(active(X)))
    (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(fact(X)) -> p#(X), p#(ok(X)) -> p#(X))
    (active#(fact(X)) -> p#(X), p#(mark(X)) -> p#(X))
    (active#(p(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(p(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X))
    (active#(p(X)) -> active#(X), active#(p(X)) -> p#(active(X)))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> active#(X))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> p#(X))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> fact#(active(X)))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> fact#(p(X)))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> s#(0()))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> zero#(X))
    (active#(p(X)) -> active#(X), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(p(X)) -> active#(X), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(p(X)) -> active#(X), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
    (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
    (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(p(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(p(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(p(X)) -> active#(X), active#(zero(X)) -> active#(X))
    (active#(p(X)) -> active#(X), active#(zero(X)) -> zero#(active(X)))
    (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
    (proper#(p(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X)))
    (proper#(p(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
    (proper#(p(X)) -> proper#(X), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(p(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(p(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
    (proper#(p(X)) -> proper#(X), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (top#(ok(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (top#(ok(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(p(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(p(X)) -> p#(active(X)))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> p#(X))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> fact#(active(X)))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> fact#(p(X)))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> prod#(X, fact(p(X))))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> s#(0()))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> zero#(X))
    (top#(ok(X)) -> active#(X), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (top#(ok(X)) -> active#(X), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (top#(ok(X)) -> active#(X), active#(prod(s(X), Y)) -> prod#(X, Y))
    (top#(ok(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (top#(ok(X)) -> active#(X), active#(zero(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(zero(X)) -> zero#(active(X)))
    (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(add(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(add(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(p(X)) -> p#(active(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> p#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> fact#(active(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> fact#(p(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> s#(0()))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> zero#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(add(X1, X2)) -> active#(X2), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(add(X1, X2)) -> active#(X2), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(add(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(zero(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(zero(X)) -> zero#(active(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(p(X)) -> p#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> active#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> p#(active(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> p#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> fact#(active(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> fact#(p(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> s#(0()))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> zero#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(zero(X)) -> active#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(zero(X)) -> zero#(active(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(add(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(add(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(p(X)) -> p#(active(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> p#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> fact#(active(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> fact#(p(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> s#(0()))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> zero#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(add(X1, X2)) -> active#(X1), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(add(X1, X2)) -> active#(X1), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(zero(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(zero(X)) -> zero#(active(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(p(X)) -> p#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(prod(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (prod#(X1, mark(X2)) -> prod#(X1, X2), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (prod#(X1, mark(X2)) -> prod#(X1, X2), prod#(mark(X1), X2) -> prod#(X1, X2))
    (prod#(X1, mark(X2)) -> prod#(X1, X2), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (prod#(ok(X1), ok(X2)) -> prod#(X1, X2), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (prod#(ok(X1), ok(X2)) -> prod#(X1, X2), prod#(mark(X1), X2) -> prod#(X1, X2))
    (prod#(ok(X1), ok(X2)) -> prod#(X1, X2), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (add#(X1, mark(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(p(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(p(X)) -> p#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(fact(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> s#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(zero(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(X1, mark(X2)) -> add#(X1, X2))
    (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(mark(X1), X2) -> add#(X1, X2))
    (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(prod(s(X), Y)) -> prod#(X, Y), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (active#(prod(s(X), Y)) -> prod#(X, Y), prod#(mark(X1), X2) -> prod#(X1, X2))
    (active#(prod(s(X), Y)) -> prod#(X, Y), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (active#(zero(X)) -> zero#(active(X)), zero#(ok(X)) -> zero#(X))
    (active#(zero(X)) -> zero#(active(X)), zero#(mark(X)) -> zero#(X))
    (active#(fact(X)) -> fact#(p(X)), fact#(ok(X)) -> fact#(X))
    (active#(fact(X)) -> fact#(p(X)), fact#(mark(X)) -> fact#(X))
    (active#(p(X)) -> p#(active(X)), p#(ok(X)) -> p#(X))
    (active#(p(X)) -> p#(active(X)), p#(mark(X)) -> p#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X))
    (proper#(p(X)) -> p#(proper(X)), p#(ok(X)) -> p#(X))
    (proper#(p(X)) -> p#(proper(X)), p#(mark(X)) -> p#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(fact(X)) -> fact#(proper(X)), fact#(mark(X)) -> fact#(X))
    (proper#(fact(X)) -> fact#(proper(X)), fact#(ok(X)) -> fact#(X))
    (proper#(zero(X)) -> zero#(proper(X)), zero#(mark(X)) -> zero#(X))
    (proper#(zero(X)) -> zero#(proper(X)), zero#(ok(X)) -> zero#(X))
    (active#(fact(X)) -> fact#(active(X)), fact#(mark(X)) -> fact#(X))
    (active#(fact(X)) -> fact#(active(X)), fact#(ok(X)) -> fact#(X))
    (active#(s(X)) -> s#(active(X)), s#(mark(X)) -> s#(X))
    (active#(s(X)) -> s#(active(X)), s#(ok(X)) -> s#(X))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(mark(X)) -> s#(X))
    (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(ok(X)) -> s#(X))
    (proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)), prod#(mark(X1), X2) -> prod#(X1, X2))
    (proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (active#(prod(X1, X2)) -> prod#(X1, active(X2)), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (active#(prod(X1, X2)) -> prod#(X1, active(X2)), prod#(mark(X1), X2) -> prod#(X1, X2))
    (active#(prod(X1, X2)) -> prod#(X1, active(X2)), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (active#(fact(X)) -> prod#(X, fact(p(X))), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (active#(fact(X)) -> prod#(X, fact(p(X))), prod#(mark(X1), X2) -> prod#(X1, X2))
    (active#(fact(X)) -> prod#(X, fact(p(X))), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (prod#(mark(X1), X2) -> prod#(X1, X2), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (prod#(mark(X1), X2) -> prod#(X1, X2), prod#(mark(X1), X2) -> prod#(X1, X2))
    (prod#(mark(X1), X2) -> prod#(X1, X2), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(p(X)) -> p#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> p#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(prod(X1, X2)) -> active#(X1), active#(zero(X)) -> zero#(active(X)))
    (active#(prod(X1, X2)) -> active#(X1), active#(zero(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
    (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
    (active#(prod(X1, X2)) -> active#(X1), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(prod(X1, X2)) -> active#(X1), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> zero#(X))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> s#(0()))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> fact#(p(X)))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> fact#(active(X)))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> p#(X))
    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X1), active#(p(X)) -> p#(active(X)))
    (active#(prod(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(prod(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(prod(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(prod(X1, X2)) -> prod#(active(X1), X2), prod#(X1, mark(X2)) -> prod#(X1, X2))
    (active#(prod(X1, X2)) -> prod#(active(X1), X2), prod#(mark(X1), X2) -> prod#(X1, X2))
    (active#(prod(X1, X2)) -> prod#(active(X1), X2), prod#(ok(X1), ok(X2)) -> prod#(X1, X2))
    (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(p(X)) -> p#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> p#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (active#(prod(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(prod(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(prod(X1, X2)) -> active#(X2), active#(zero(X)) -> zero#(active(X)))
    (active#(prod(X1, X2)) -> active#(X2), active#(zero(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(prod(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
    (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
    (active#(prod(X1, X2)) -> active#(X2), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(prod(X1, X2)) -> active#(X2), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> zero#(X))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> s#(0()))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> fact#(p(X)))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> fact#(active(X)))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> p#(X))
    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X2), active#(p(X)) -> p#(active(X)))
    (active#(prod(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X))
    (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
    (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
    (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(prod(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(prod(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (top#(mark(X)) -> proper#(X), proper#(zero(X)) -> zero#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(fact(X)) -> fact#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(fact(X)) -> proper#(X), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(fact(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
    (proper#(fact(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(fact(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(fact(X)) -> proper#(X), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(fact(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
    (proper#(fact(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X)))
    (proper#(fact(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
    (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> zero#(proper(X)))
    (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
    (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> prod#(proper(X1), proper(X2)))
    (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
    (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
    (proper#(zero(X)) -> proper#(X), proper#(fact(X)) -> fact#(proper(X)))
    (proper#(zero(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
    (proper#(zero(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X)))
    (proper#(zero(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
    (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(fact(X)) -> active#(X), active#(zero(X)) -> zero#(active(X)))
    (active#(fact(X)) -> active#(X), active#(zero(X)) -> active#(X))
    (active#(fact(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
    (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
    (active#(fact(X)) -> active#(X), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(fact(X)) -> active#(X), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> zero#(X))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> s#(0()))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> fact#(p(X)))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> fact#(active(X)))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> p#(X))
    (active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
    (active#(fact(X)) -> active#(X), active#(p(X)) -> p#(active(X)))
    (active#(fact(X)) -> active#(X), active#(p(X)) -> active#(X))
    (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(fact(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(fact(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(fact(X)) -> zero#(X), zero#(mark(X)) -> zero#(X))
    (active#(fact(X)) -> zero#(X), zero#(ok(X)) -> zero#(X))
    (active#(zero(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(zero(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(zero(X)) -> active#(X), active#(zero(X)) -> zero#(active(X)))
    (active#(zero(X)) -> active#(X), active#(zero(X)) -> active#(X))
    (active#(zero(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(zero(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(zero(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(X1, active(X2)))
    (active#(zero(X)) -> active#(X), active#(prod(X1, X2)) -> prod#(active(X1), X2))
    (active#(zero(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
    (active#(zero(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
    (active#(zero(X)) -> active#(X), active#(prod(s(X), Y)) -> prod#(X, Y))
    (active#(zero(X)) -> active#(X), active#(prod(s(X), Y)) -> add#(Y, prod(X, Y)))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> zero#(X))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> s#(0()))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> prod#(X, fact(p(X))))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> fact#(p(X)))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> fact#(active(X)))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> p#(X))
    (active#(zero(X)) -> active#(X), active#(fact(X)) -> active#(X))
    (active#(zero(X)) -> active#(X), active#(p(X)) -> p#(active(X)))
    (active#(zero(X)) -> active#(X), active#(p(X)) -> active#(X))
    (active#(zero(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (active#(zero(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (active#(zero(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(zero(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(zero(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(zero(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (p#(mark(X)) -> p#(X), p#(mark(X)) -> p#(X))
    (p#(mark(X)) -> p#(X), p#(ok(X)) -> p#(X))
    (fact#(mark(X)) -> fact#(X), fact#(mark(X)) -> fact#(X))
    (fact#(mark(X)) -> fact#(X), fact#(ok(X)) -> fact#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (zero#(mark(X)) -> zero#(X), zero#(mark(X)) -> zero#(X))
    (zero#(mark(X)) -> zero#(X), zero#(ok(X)) -> zero#(X))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(if(X1, X2, X3)) -> proper#(X1),
      proper#(if(X1, X2, X3)) -> proper#(X2),
      proper#(if(X1, X2, X3)) -> proper#(X3),
             proper#(zero(X)) -> proper#(X),
                proper#(s(X)) -> proper#(X),
        proper#(prod(X1, X2)) -> proper#(X1),
        proper#(prod(X1, X2)) -> proper#(X2),
             proper#(fact(X)) -> proper#(X),
                proper#(p(X)) -> proper#(X),
         proper#(add(X1, X2)) -> proper#(X1),
         proper#(add(X1, X2)) -> proper#(X2)}
    Scc:
     {  add#(X1, mark(X2)) -> add#(X1, X2),
        add#(mark(X1), X2) -> add#(X1, X2),
      add#(ok(X1), ok(X2)) -> add#(X1, X2)}
    Scc:
     {active#(if(X1, X2, X3)) -> active#(X1),
             active#(zero(X)) -> active#(X),
                active#(s(X)) -> active#(X),
        active#(prod(X1, X2)) -> active#(X1),
        active#(prod(X1, X2)) -> active#(X2),
             active#(fact(X)) -> active#(X),
                active#(p(X)) -> active#(X),
         active#(add(X1, X2)) -> active#(X1),
         active#(add(X1, X2)) -> active#(X2)}
    Scc:
     {p#(mark(X)) -> p#(X),
        p#(ok(X)) -> p#(X)}
    Scc:
     {fact#(mark(X)) -> fact#(X),
        fact#(ok(X)) -> fact#(X)}
    Scc:
     {  prod#(X1, mark(X2)) -> prod#(X1, X2),
        prod#(mark(X1), X2) -> prod#(X1, X2),
      prod#(ok(X1), ok(X2)) -> prod#(X1, X2)}
    Scc:
     {s#(mark(X)) -> s#(X),
        s#(ok(X)) -> s#(X)}
    Scc:
     {zero#(mark(X)) -> zero#(X),
        zero#(ok(X)) -> zero#(X)}
    Scc:
     {      if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
      if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      {proper#(if(X1, X2, X3)) -> proper#(X1),
       proper#(if(X1, X2, X3)) -> proper#(X2),
       proper#(if(X1, X2, X3)) -> proper#(X3),
              proper#(zero(X)) -> proper#(X),
                 proper#(s(X)) -> proper#(X),
         proper#(prod(X1, X2)) -> proper#(X1),
         proper#(prod(X1, X2)) -> proper#(X2),
              proper#(fact(X)) -> proper#(X),
                 proper#(p(X)) -> proper#(X),
          proper#(add(X1, X2)) -> proper#(X1),
          proper#(add(X1, X2)) -> proper#(X2)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(if(X1, X2, X3)) -> proper#(X1),
        proper#(if(X1, X2, X3)) -> proper#(X2),
               proper#(zero(X)) -> proper#(X),
                  proper#(s(X)) -> proper#(X),
          proper#(prod(X1, X2)) -> proper#(X1),
          proper#(prod(X1, X2)) -> proper#(X2),
               proper#(fact(X)) -> proper#(X),
                  proper#(p(X)) -> proper#(X),
           proper#(add(X1, X2)) -> proper#(X1),
           proper#(add(X1, X2)) -> proper#(X2)}
      EDG:
       {(proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
        (proper#(p(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
        (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(p(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
        (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(prod(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(fact(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
        (proper#(fact(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(fact(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
        (proper#(fact(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
        (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
        (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X1))
        (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
        (proper#(zero(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
        (proper#(zero(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
        (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
        (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))}
       SCCS:
        Scc:
         {proper#(if(X1, X2, X3)) -> proper#(X1),
          proper#(if(X1, X2, X3)) -> proper#(X2),
                 proper#(zero(X)) -> proper#(X),
                    proper#(s(X)) -> proper#(X),
            proper#(prod(X1, X2)) -> proper#(X1),
            proper#(prod(X1, X2)) -> proper#(X2),
                 proper#(fact(X)) -> proper#(X),
                    proper#(p(X)) -> proper#(X),
             proper#(add(X1, X2)) -> proper#(X1),
             proper#(add(X1, X2)) -> proper#(X2)}
        SCC:
         Strict:
          {proper#(if(X1, X2, X3)) -> proper#(X1),
           proper#(if(X1, X2, X3)) -> proper#(X2),
                  proper#(zero(X)) -> proper#(X),
                     proper#(s(X)) -> proper#(X),
             proper#(prod(X1, X2)) -> proper#(X1),
             proper#(prod(X1, X2)) -> proper#(X2),
                  proper#(fact(X)) -> proper#(X),
                     proper#(p(X)) -> proper#(X),
              proper#(add(X1, X2)) -> proper#(X1),
              proper#(add(X1, X2)) -> proper#(X2)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {proper#(if(X1, X2, X3)) -> proper#(X1),
            proper#(if(X1, X2, X3)) -> proper#(X2),
                   proper#(zero(X)) -> proper#(X),
                      proper#(s(X)) -> proper#(X),
              proper#(prod(X1, X2)) -> proper#(X2),
                   proper#(fact(X)) -> proper#(X),
                      proper#(p(X)) -> proper#(X),
               proper#(add(X1, X2)) -> proper#(X1),
               proper#(add(X1, X2)) -> proper#(X2)}
          EDG:
           {(proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(zero(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
            (proper#(zero(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
            (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
            (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(fact(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
            (proper#(fact(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
            (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(fact(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(fact(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
            (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(p(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
            (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(p(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
            (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
            (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))}
           SCCS:
            Scc:
             {proper#(if(X1, X2, X3)) -> proper#(X1),
              proper#(if(X1, X2, X3)) -> proper#(X2),
                     proper#(zero(X)) -> proper#(X),
                        proper#(s(X)) -> proper#(X),
                proper#(prod(X1, X2)) -> proper#(X2),
                     proper#(fact(X)) -> proper#(X),
                        proper#(p(X)) -> proper#(X),
                 proper#(add(X1, X2)) -> proper#(X1),
                 proper#(add(X1, X2)) -> proper#(X2)}
            SCC:
             Strict:
              {proper#(if(X1, X2, X3)) -> proper#(X1),
               proper#(if(X1, X2, X3)) -> proper#(X2),
                      proper#(zero(X)) -> proper#(X),
                         proper#(s(X)) -> proper#(X),
                 proper#(prod(X1, X2)) -> proper#(X2),
                      proper#(fact(X)) -> proper#(X),
                         proper#(p(X)) -> proper#(X),
                  proper#(add(X1, X2)) -> proper#(X1),
                  proper#(add(X1, X2)) -> proper#(X2)}
             Weak:
             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                           zero(mark(X)) -> mark(zero(X)),
                             zero(ok(X)) -> ok(zero(X)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                           fact(mark(X)) -> mark(fact(X)),
                             fact(ok(X)) -> ok(fact(X)),
                              p(mark(X)) -> mark(p(X)),
                                p(ok(X)) -> ok(p(X)),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                         active(zero(X)) -> zero(active(X)),
                      active(zero(s(X))) -> mark(false()),
                       active(zero(0())) -> mark(true()),
                            active(s(X)) -> s(active(X)),
                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                    active(prod(X1, X2)) -> prod(active(X1), X2),
                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                    active(prod(0(), X)) -> mark(0()),
                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                         active(fact(X)) -> fact(active(X)),
                            active(p(X)) -> p(active(X)),
                         active(p(s(X))) -> mark(X),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(zero(X)) -> zero(proper(X)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                         proper(fact(X)) -> fact(proper(X)),
                            proper(p(X)) -> p(proper(X)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {proper#(if(X1, X2, X3)) -> proper#(X1),
                proper#(if(X1, X2, X3)) -> proper#(X2),
                       proper#(zero(X)) -> proper#(X),
                          proper#(s(X)) -> proper#(X),
                  proper#(prod(X1, X2)) -> proper#(X2),
                       proper#(fact(X)) -> proper#(X),
                          proper#(p(X)) -> proper#(X),
                   proper#(add(X1, X2)) -> proper#(X2)}
              EDG:
               {(proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(zero(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
                (proper#(zero(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(fact(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
                (proper#(fact(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(fact(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(fact(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(p(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(p(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(p(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
                (proper#(p(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))}
               SCCS:
                Scc:
                 {proper#(if(X1, X2, X3)) -> proper#(X1),
                  proper#(if(X1, X2, X3)) -> proper#(X2),
                         proper#(zero(X)) -> proper#(X),
                            proper#(s(X)) -> proper#(X),
                    proper#(prod(X1, X2)) -> proper#(X2),
                         proper#(fact(X)) -> proper#(X),
                            proper#(p(X)) -> proper#(X),
                     proper#(add(X1, X2)) -> proper#(X2)}
                SCC:
                 Strict:
                  {proper#(if(X1, X2, X3)) -> proper#(X1),
                   proper#(if(X1, X2, X3)) -> proper#(X2),
                          proper#(zero(X)) -> proper#(X),
                             proper#(s(X)) -> proper#(X),
                     proper#(prod(X1, X2)) -> proper#(X2),
                          proper#(fact(X)) -> proper#(X),
                             proper#(p(X)) -> proper#(X),
                      proper#(add(X1, X2)) -> proper#(X2)}
                 Weak:
                 {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                               zero(mark(X)) -> mark(zero(X)),
                                 zero(ok(X)) -> ok(zero(X)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                          prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                          prod(mark(X1), X2) -> mark(prod(X1, X2)),
                        prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                               fact(mark(X)) -> mark(fact(X)),
                                 fact(ok(X)) -> ok(fact(X)),
                                  p(mark(X)) -> mark(p(X)),
                                    p(ok(X)) -> ok(p(X)),
                      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                    active(if(true(), X, Y)) -> mark(X),
                   active(if(false(), X, Y)) -> mark(Y),
                             active(zero(X)) -> zero(active(X)),
                          active(zero(s(X))) -> mark(false()),
                           active(zero(0())) -> mark(true()),
                                active(s(X)) -> s(active(X)),
                        active(prod(X1, X2)) -> prod(X1, active(X2)),
                        active(prod(X1, X2)) -> prod(active(X1), X2),
                       active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                        active(prod(0(), X)) -> mark(0()),
                             active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                             active(fact(X)) -> fact(active(X)),
                                active(p(X)) -> p(active(X)),
                             active(p(s(X))) -> mark(X),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                             proper(zero(X)) -> zero(proper(X)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                        proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                             proper(fact(X)) -> fact(proper(X)),
                                proper(p(X)) -> p(proper(X)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(true()) -> ok(true()),
                             proper(false()) -> ok(false()),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {proper#(if(X1, X2, X3)) -> proper#(X1),
                    proper#(if(X1, X2, X3)) -> proper#(X2),
                           proper#(zero(X)) -> proper#(X),
                              proper#(s(X)) -> proper#(X),
                      proper#(prod(X1, X2)) -> proper#(X2),
                           proper#(fact(X)) -> proper#(X),
                       proper#(add(X1, X2)) -> proper#(X2)}
                  EDG:
                   {(proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(prod(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
                    (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                    (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(fact(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(s(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(fact(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(fact(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                    (proper#(fact(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(fact(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(fact(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                    (proper#(fact(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                    (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(zero(X)) -> proper#(X), proper#(fact(X)) -> proper#(X))
                    (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(fact(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))}
                   SCCS:
                    Scc:
                     {proper#(if(X1, X2, X3)) -> proper#(X1),
                      proper#(if(X1, X2, X3)) -> proper#(X2),
                             proper#(zero(X)) -> proper#(X),
                                proper#(s(X)) -> proper#(X),
                        proper#(prod(X1, X2)) -> proper#(X2),
                             proper#(fact(X)) -> proper#(X),
                         proper#(add(X1, X2)) -> proper#(X2)}
                    SCC:
                     Strict:
                      {proper#(if(X1, X2, X3)) -> proper#(X1),
                       proper#(if(X1, X2, X3)) -> proper#(X2),
                              proper#(zero(X)) -> proper#(X),
                                 proper#(s(X)) -> proper#(X),
                         proper#(prod(X1, X2)) -> proper#(X2),
                              proper#(fact(X)) -> proper#(X),
                          proper#(add(X1, X2)) -> proper#(X2)}
                     Weak:
                     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                   zero(mark(X)) -> mark(zero(X)),
                                     zero(ok(X)) -> ok(zero(X)),
                                      s(mark(X)) -> mark(s(X)),
                                        s(ok(X)) -> ok(s(X)),
                              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                              prod(mark(X1), X2) -> mark(prod(X1, X2)),
                            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                   fact(mark(X)) -> mark(fact(X)),
                                     fact(ok(X)) -> ok(fact(X)),
                                      p(mark(X)) -> mark(p(X)),
                                        p(ok(X)) -> ok(p(X)),
                          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                        active(if(true(), X, Y)) -> mark(X),
                       active(if(false(), X, Y)) -> mark(Y),
                                 active(zero(X)) -> zero(active(X)),
                              active(zero(s(X))) -> mark(false()),
                               active(zero(0())) -> mark(true()),
                                    active(s(X)) -> s(active(X)),
                            active(prod(X1, X2)) -> prod(X1, active(X2)),
                            active(prod(X1, X2)) -> prod(active(X1), X2),
                           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                            active(prod(0(), X)) -> mark(0()),
                                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                 active(fact(X)) -> fact(active(X)),
                                    active(p(X)) -> p(active(X)),
                                 active(p(s(X))) -> mark(X),
                             active(add(X1, X2)) -> add(X1, active(X2)),
                             active(add(X1, X2)) -> add(active(X1), X2),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                               add(mark(X1), X2) -> mark(add(X1, X2)),
                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                 proper(zero(X)) -> zero(proper(X)),
                                    proper(s(X)) -> s(proper(X)),
                                     proper(0()) -> ok(0()),
                            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                 proper(fact(X)) -> fact(proper(X)),
                                    proper(p(X)) -> p(proper(X)),
                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                  proper(true()) -> ok(true()),
                                 proper(false()) -> ok(false()),
                                    top(mark(X)) -> top(proper(X)),
                                      top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(proper#) = 0
                      Strict:
                       {proper#(if(X1, X2, X3)) -> proper#(X1),
                        proper#(if(X1, X2, X3)) -> proper#(X2),
                               proper#(zero(X)) -> proper#(X),
                                  proper#(s(X)) -> proper#(X),
                          proper#(prod(X1, X2)) -> proper#(X2),
                           proper#(add(X1, X2)) -> proper#(X2)}
                      EDG:
                       {(proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(zero(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                        (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                        (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(prod(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(prod(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                        (proper#(prod(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(prod(X1, X2)) -> proper#(X2), proper#(prod(X1, X2)) -> proper#(X2))
                        (proper#(prod(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(prod(X1, X2)) -> proper#(X2))
                        (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(prod(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
                       SCCS:
                        Scc:
                         {proper#(if(X1, X2, X3)) -> proper#(X1),
                          proper#(if(X1, X2, X3)) -> proper#(X2),
                                 proper#(zero(X)) -> proper#(X),
                                    proper#(s(X)) -> proper#(X),
                            proper#(prod(X1, X2)) -> proper#(X2),
                             proper#(add(X1, X2)) -> proper#(X2)}
                        SCC:
                         Strict:
                          {proper#(if(X1, X2, X3)) -> proper#(X1),
                           proper#(if(X1, X2, X3)) -> proper#(X2),
                                  proper#(zero(X)) -> proper#(X),
                                     proper#(s(X)) -> proper#(X),
                             proper#(prod(X1, X2)) -> proper#(X2),
                              proper#(add(X1, X2)) -> proper#(X2)}
                         Weak:
                         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                       zero(mark(X)) -> mark(zero(X)),
                                         zero(ok(X)) -> ok(zero(X)),
                                          s(mark(X)) -> mark(s(X)),
                                            s(ok(X)) -> ok(s(X)),
                                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                       fact(mark(X)) -> mark(fact(X)),
                                         fact(ok(X)) -> ok(fact(X)),
                                          p(mark(X)) -> mark(p(X)),
                                            p(ok(X)) -> ok(p(X)),
                              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                            active(if(true(), X, Y)) -> mark(X),
                           active(if(false(), X, Y)) -> mark(Y),
                                     active(zero(X)) -> zero(active(X)),
                                  active(zero(s(X))) -> mark(false()),
                                   active(zero(0())) -> mark(true()),
                                        active(s(X)) -> s(active(X)),
                                active(prod(X1, X2)) -> prod(X1, active(X2)),
                                active(prod(X1, X2)) -> prod(active(X1), X2),
                               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                active(prod(0(), X)) -> mark(0()),
                                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                     active(fact(X)) -> fact(active(X)),
                                        active(p(X)) -> p(active(X)),
                                     active(p(s(X))) -> mark(X),
                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                 active(add(X1, X2)) -> add(active(X1), X2),
                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                 active(add(0(), X)) -> mark(X),
                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                     proper(zero(X)) -> zero(proper(X)),
                                        proper(s(X)) -> s(proper(X)),
                                         proper(0()) -> ok(0()),
                                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                     proper(fact(X)) -> fact(proper(X)),
                                        proper(p(X)) -> p(proper(X)),
                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                      proper(true()) -> ok(true()),
                                     proper(false()) -> ok(false()),
                                        top(mark(X)) -> top(proper(X)),
                                          top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(proper#) = 0
                          Strict:
                           {proper#(if(X1, X2, X3)) -> proper#(X1),
                            proper#(if(X1, X2, X3)) -> proper#(X2),
                                   proper#(zero(X)) -> proper#(X),
                                      proper#(s(X)) -> proper#(X),
                               proper#(add(X1, X2)) -> proper#(X2)}
                          EDG:
                           {(proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                            (proper#(s(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                            (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                            (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                            (proper#(zero(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                            (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))}
                           SCCS:
                            Scc:
                             {proper#(if(X1, X2, X3)) -> proper#(X1),
                              proper#(if(X1, X2, X3)) -> proper#(X2),
                                     proper#(zero(X)) -> proper#(X),
                                        proper#(s(X)) -> proper#(X),
                                 proper#(add(X1, X2)) -> proper#(X2)}
                            SCC:
                             Strict:
                              {proper#(if(X1, X2, X3)) -> proper#(X1),
                               proper#(if(X1, X2, X3)) -> proper#(X2),
                                      proper#(zero(X)) -> proper#(X),
                                         proper#(s(X)) -> proper#(X),
                                  proper#(add(X1, X2)) -> proper#(X2)}
                             Weak:
                             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                           zero(mark(X)) -> mark(zero(X)),
                                             zero(ok(X)) -> ok(zero(X)),
                                              s(mark(X)) -> mark(s(X)),
                                                s(ok(X)) -> ok(s(X)),
                                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                           fact(mark(X)) -> mark(fact(X)),
                                             fact(ok(X)) -> ok(fact(X)),
                                              p(mark(X)) -> mark(p(X)),
                                                p(ok(X)) -> ok(p(X)),
                                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                active(if(true(), X, Y)) -> mark(X),
                               active(if(false(), X, Y)) -> mark(Y),
                                         active(zero(X)) -> zero(active(X)),
                                      active(zero(s(X))) -> mark(false()),
                                       active(zero(0())) -> mark(true()),
                                            active(s(X)) -> s(active(X)),
                                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                                    active(prod(X1, X2)) -> prod(active(X1), X2),
                                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                    active(prod(0(), X)) -> mark(0()),
                                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                         active(fact(X)) -> fact(active(X)),
                                            active(p(X)) -> p(active(X)),
                                         active(p(s(X))) -> mark(X),
                                     active(add(X1, X2)) -> add(X1, active(X2)),
                                     active(add(X1, X2)) -> add(active(X1), X2),
                                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                     active(add(0(), X)) -> mark(X),
                                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                                       add(mark(X1), X2) -> mark(add(X1, X2)),
                                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                         proper(zero(X)) -> zero(proper(X)),
                                            proper(s(X)) -> s(proper(X)),
                                             proper(0()) -> ok(0()),
                                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                         proper(fact(X)) -> fact(proper(X)),
                                            proper(p(X)) -> p(proper(X)),
                                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                          proper(true()) -> ok(true()),
                                         proper(false()) -> ok(false()),
                                            top(mark(X)) -> top(proper(X)),
                                              top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(proper#) = 0
                              Strict:
                               {proper#(if(X1, X2, X3)) -> proper#(X1),
                                proper#(if(X1, X2, X3)) -> proper#(X2),
                                       proper#(zero(X)) -> proper#(X),
                                   proper#(add(X1, X2)) -> proper#(X2)}
                              EDG:
                               {(proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(zero(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(zero(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                                (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                                (proper#(zero(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                                (proper#(zero(X)) -> proper#(X), proper#(zero(X)) -> proper#(X))
                                (proper#(zero(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))}
                               SCCS:
                                Scc:
                                 {proper#(if(X1, X2, X3)) -> proper#(X1),
                                  proper#(if(X1, X2, X3)) -> proper#(X2),
                                         proper#(zero(X)) -> proper#(X),
                                     proper#(add(X1, X2)) -> proper#(X2)}
                                SCC:
                                 Strict:
                                  {proper#(if(X1, X2, X3)) -> proper#(X1),
                                   proper#(if(X1, X2, X3)) -> proper#(X2),
                                          proper#(zero(X)) -> proper#(X),
                                      proper#(add(X1, X2)) -> proper#(X2)}
                                 Weak:
                                 {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                               zero(mark(X)) -> mark(zero(X)),
                                                 zero(ok(X)) -> ok(zero(X)),
                                                  s(mark(X)) -> mark(s(X)),
                                                    s(ok(X)) -> ok(s(X)),
                                          prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                          prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                        prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                               fact(mark(X)) -> mark(fact(X)),
                                                 fact(ok(X)) -> ok(fact(X)),
                                                  p(mark(X)) -> mark(p(X)),
                                                    p(ok(X)) -> ok(p(X)),
                                      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                    active(if(true(), X, Y)) -> mark(X),
                                   active(if(false(), X, Y)) -> mark(Y),
                                             active(zero(X)) -> zero(active(X)),
                                          active(zero(s(X))) -> mark(false()),
                                           active(zero(0())) -> mark(true()),
                                                active(s(X)) -> s(active(X)),
                                        active(prod(X1, X2)) -> prod(X1, active(X2)),
                                        active(prod(X1, X2)) -> prod(active(X1), X2),
                                       active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                        active(prod(0(), X)) -> mark(0()),
                                             active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                             active(fact(X)) -> fact(active(X)),
                                                active(p(X)) -> p(active(X)),
                                             active(p(s(X))) -> mark(X),
                                         active(add(X1, X2)) -> add(X1, active(X2)),
                                         active(add(X1, X2)) -> add(active(X1), X2),
                                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                         active(add(0(), X)) -> mark(X),
                                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                                           add(mark(X1), X2) -> mark(add(X1, X2)),
                                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                             proper(zero(X)) -> zero(proper(X)),
                                                proper(s(X)) -> s(proper(X)),
                                                 proper(0()) -> ok(0()),
                                        proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                             proper(fact(X)) -> fact(proper(X)),
                                                proper(p(X)) -> p(proper(X)),
                                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                              proper(true()) -> ok(true()),
                                             proper(false()) -> ok(false()),
                                                top(mark(X)) -> top(proper(X)),
                                                  top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(proper#) = 0
                                  Strict:
                                   {proper#(if(X1, X2, X3)) -> proper#(X1),
                                    proper#(if(X1, X2, X3)) -> proper#(X2),
                                       proper#(add(X1, X2)) -> proper#(X2)}
                                  EDG:
                                   {(proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                                    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                                    (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))}
                                   SCCS:
                                    Scc:
                                     {proper#(if(X1, X2, X3)) -> proper#(X1),
                                      proper#(if(X1, X2, X3)) -> proper#(X2),
                                         proper#(add(X1, X2)) -> proper#(X2)}
                                    SCC:
                                     Strict:
                                      {proper#(if(X1, X2, X3)) -> proper#(X1),
                                       proper#(if(X1, X2, X3)) -> proper#(X2),
                                          proper#(add(X1, X2)) -> proper#(X2)}
                                     Weak:
                                     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                   zero(mark(X)) -> mark(zero(X)),
                                                     zero(ok(X)) -> ok(zero(X)),
                                                      s(mark(X)) -> mark(s(X)),
                                                        s(ok(X)) -> ok(s(X)),
                                              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                              prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                                   fact(mark(X)) -> mark(fact(X)),
                                                     fact(ok(X)) -> ok(fact(X)),
                                                      p(mark(X)) -> mark(p(X)),
                                                        p(ok(X)) -> ok(p(X)),
                                          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                        active(if(true(), X, Y)) -> mark(X),
                                       active(if(false(), X, Y)) -> mark(Y),
                                                 active(zero(X)) -> zero(active(X)),
                                              active(zero(s(X))) -> mark(false()),
                                               active(zero(0())) -> mark(true()),
                                                    active(s(X)) -> s(active(X)),
                                            active(prod(X1, X2)) -> prod(X1, active(X2)),
                                            active(prod(X1, X2)) -> prod(active(X1), X2),
                                           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                            active(prod(0(), X)) -> mark(0()),
                                                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                                 active(fact(X)) -> fact(active(X)),
                                                    active(p(X)) -> p(active(X)),
                                                 active(p(s(X))) -> mark(X),
                                             active(add(X1, X2)) -> add(X1, active(X2)),
                                             active(add(X1, X2)) -> add(active(X1), X2),
                                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                             active(add(0(), X)) -> mark(X),
                                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                                               add(mark(X1), X2) -> mark(add(X1, X2)),
                                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                 proper(zero(X)) -> zero(proper(X)),
                                                    proper(s(X)) -> s(proper(X)),
                                                     proper(0()) -> ok(0()),
                                            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                                 proper(fact(X)) -> fact(proper(X)),
                                                    proper(p(X)) -> p(proper(X)),
                                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                  proper(true()) -> ok(true()),
                                                 proper(false()) -> ok(false()),
                                                    top(mark(X)) -> top(proper(X)),
                                                      top(ok(X)) -> top(active(X))}
                                     SPSC:
                                      Simple Projection:
                                       pi(proper#) = 0
                                      Strict:
                                       {proper#(if(X1, X2, X3)) -> proper#(X1),
                                        proper#(if(X1, X2, X3)) -> proper#(X2)}
                                      EDG:
                                       {(proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))}
                                       SCCS:
                                        Scc:
                                         {proper#(if(X1, X2, X3)) -> proper#(X1),
                                          proper#(if(X1, X2, X3)) -> proper#(X2)}
                                        SCC:
                                         Strict:
                                          {proper#(if(X1, X2, X3)) -> proper#(X1),
                                           proper#(if(X1, X2, X3)) -> proper#(X2)}
                                         Weak:
                                         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                       zero(mark(X)) -> mark(zero(X)),
                                                         zero(ok(X)) -> ok(zero(X)),
                                                          s(mark(X)) -> mark(s(X)),
                                                            s(ok(X)) -> ok(s(X)),
                                                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                                       fact(mark(X)) -> mark(fact(X)),
                                                         fact(ok(X)) -> ok(fact(X)),
                                                          p(mark(X)) -> mark(p(X)),
                                                            p(ok(X)) -> ok(p(X)),
                                              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                            active(if(true(), X, Y)) -> mark(X),
                                           active(if(false(), X, Y)) -> mark(Y),
                                                     active(zero(X)) -> zero(active(X)),
                                                  active(zero(s(X))) -> mark(false()),
                                                   active(zero(0())) -> mark(true()),
                                                        active(s(X)) -> s(active(X)),
                                                active(prod(X1, X2)) -> prod(X1, active(X2)),
                                                active(prod(X1, X2)) -> prod(active(X1), X2),
                                               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                                active(prod(0(), X)) -> mark(0()),
                                                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                                     active(fact(X)) -> fact(active(X)),
                                                        active(p(X)) -> p(active(X)),
                                                     active(p(s(X))) -> mark(X),
                                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                                 active(add(X1, X2)) -> add(active(X1), X2),
                                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                 active(add(0(), X)) -> mark(X),
                                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                     proper(zero(X)) -> zero(proper(X)),
                                                        proper(s(X)) -> s(proper(X)),
                                                         proper(0()) -> ok(0()),
                                                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                                     proper(fact(X)) -> fact(proper(X)),
                                                        proper(p(X)) -> p(proper(X)),
                                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                      proper(true()) -> ok(true()),
                                                     proper(false()) -> ok(false()),
                                                        top(mark(X)) -> top(proper(X)),
                                                          top(ok(X)) -> top(active(X))}
                                         SPSC:
                                          Simple Projection:
                                           pi(proper#) = 0
                                          Strict:
                                           {proper#(if(X1, X2, X3)) -> proper#(X2)}
                                          EDG:
                                           {(proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))}
                                           SCCS:
                                            Scc:
                                             {proper#(if(X1, X2, X3)) -> proper#(X2)}
                                            SCC:
                                             Strict:
                                              {proper#(if(X1, X2, X3)) -> proper#(X2)}
                                             Weak:
                                             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                           zero(mark(X)) -> mark(zero(X)),
                                                             zero(ok(X)) -> ok(zero(X)),
                                                              s(mark(X)) -> mark(s(X)),
                                                                s(ok(X)) -> ok(s(X)),
                                                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                                           fact(mark(X)) -> mark(fact(X)),
                                                             fact(ok(X)) -> ok(fact(X)),
                                                              p(mark(X)) -> mark(p(X)),
                                                                p(ok(X)) -> ok(p(X)),
                                                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                                active(if(true(), X, Y)) -> mark(X),
                                               active(if(false(), X, Y)) -> mark(Y),
                                                         active(zero(X)) -> zero(active(X)),
                                                      active(zero(s(X))) -> mark(false()),
                                                       active(zero(0())) -> mark(true()),
                                                            active(s(X)) -> s(active(X)),
                                                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                                                    active(prod(X1, X2)) -> prod(active(X1), X2),
                                                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                                    active(prod(0(), X)) -> mark(0()),
                                                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                                         active(fact(X)) -> fact(active(X)),
                                                            active(p(X)) -> p(active(X)),
                                                         active(p(s(X))) -> mark(X),
                                                     active(add(X1, X2)) -> add(X1, active(X2)),
                                                     active(add(X1, X2)) -> add(active(X1), X2),
                                                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                     active(add(0(), X)) -> mark(X),
                                                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                                                       add(mark(X1), X2) -> mark(add(X1, X2)),
                                                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                         proper(zero(X)) -> zero(proper(X)),
                                                            proper(s(X)) -> s(proper(X)),
                                                             proper(0()) -> ok(0()),
                                                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                                         proper(fact(X)) -> fact(proper(X)),
                                                            proper(p(X)) -> p(proper(X)),
                                                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                          proper(true()) -> ok(true()),
                                                         proper(false()) -> ok(false()),
                                                            top(mark(X)) -> top(proper(X)),
                                                              top(ok(X)) -> top(active(X))}
                                             SPSC:
                                              Simple Projection:
                                               pi(proper#) = 0
                                              Strict:
                                               {}
                                              Qed
    SCC:
     Strict:
      {  add#(X1, mark(X2)) -> add#(X1, X2),
         add#(mark(X1), X2) -> add#(X1, X2),
       add#(ok(X1), ok(X2)) -> add#(X1, X2)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {add#(X1, mark(X2)) -> add#(X1, X2),
        add#(mark(X1), X2) -> add#(X1, X2)}
      EDG:
       {(add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
        (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
        (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
        (add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))}
       SCCS:
        Scc:
         {add#(X1, mark(X2)) -> add#(X1, X2),
          add#(mark(X1), X2) -> add#(X1, X2)}
        SCC:
         Strict:
          {add#(X1, mark(X2)) -> add#(X1, X2),
           add#(mark(X1), X2) -> add#(X1, X2)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(add#) = 0
          Strict:
           {add#(X1, mark(X2)) -> add#(X1, X2)}
          EDG:
           {(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))}
           SCCS:
            Scc:
             {add#(X1, mark(X2)) -> add#(X1, X2)}
            SCC:
             Strict:
              {add#(X1, mark(X2)) -> add#(X1, X2)}
             Weak:
             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                           zero(mark(X)) -> mark(zero(X)),
                             zero(ok(X)) -> ok(zero(X)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                           fact(mark(X)) -> mark(fact(X)),
                             fact(ok(X)) -> ok(fact(X)),
                              p(mark(X)) -> mark(p(X)),
                                p(ok(X)) -> ok(p(X)),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                         active(zero(X)) -> zero(active(X)),
                      active(zero(s(X))) -> mark(false()),
                       active(zero(0())) -> mark(true()),
                            active(s(X)) -> s(active(X)),
                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                    active(prod(X1, X2)) -> prod(active(X1), X2),
                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                    active(prod(0(), X)) -> mark(0()),
                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                         active(fact(X)) -> fact(active(X)),
                            active(p(X)) -> p(active(X)),
                         active(p(s(X))) -> mark(X),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(zero(X)) -> zero(proper(X)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                         proper(fact(X)) -> fact(proper(X)),
                            proper(p(X)) -> p(proper(X)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(add#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {active#(if(X1, X2, X3)) -> active#(X1),
              active#(zero(X)) -> active#(X),
                 active#(s(X)) -> active#(X),
         active#(prod(X1, X2)) -> active#(X1),
         active#(prod(X1, X2)) -> active#(X2),
              active#(fact(X)) -> active#(X),
                 active#(p(X)) -> active#(X),
          active#(add(X1, X2)) -> active#(X1),
          active#(add(X1, X2)) -> active#(X2)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {active#(if(X1, X2, X3)) -> active#(X1),
                  active#(s(X)) -> active#(X),
          active#(prod(X1, X2)) -> active#(X1),
          active#(prod(X1, X2)) -> active#(X2),
               active#(fact(X)) -> active#(X),
                  active#(p(X)) -> active#(X),
           active#(add(X1, X2)) -> active#(X1),
           active#(add(X1, X2)) -> active#(X2)}
      EDG:
       {(active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
        (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
        (active#(fact(X)) -> active#(X), active#(p(X)) -> active#(X))
        (active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
        (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
        (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
        (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> active#(X))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
        (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
        (active#(prod(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X))
        (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
        (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(p(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
        (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
        (active#(p(X)) -> active#(X), active#(fact(X)) -> active#(X))
        (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X))
        (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
        (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
        (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
        (active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(p(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
        (active#(prod(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
        (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
        (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
        (active#(prod(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X))
        (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
        (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))}
       SCCS:
        Scc:
         {active#(if(X1, X2, X3)) -> active#(X1),
                    active#(s(X)) -> active#(X),
            active#(prod(X1, X2)) -> active#(X1),
            active#(prod(X1, X2)) -> active#(X2),
                 active#(fact(X)) -> active#(X),
                    active#(p(X)) -> active#(X),
             active#(add(X1, X2)) -> active#(X1),
             active#(add(X1, X2)) -> active#(X2)}
        SCC:
         Strict:
          {active#(if(X1, X2, X3)) -> active#(X1),
                     active#(s(X)) -> active#(X),
             active#(prod(X1, X2)) -> active#(X1),
             active#(prod(X1, X2)) -> active#(X2),
                  active#(fact(X)) -> active#(X),
                     active#(p(X)) -> active#(X),
              active#(add(X1, X2)) -> active#(X1),
              active#(add(X1, X2)) -> active#(X2)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           {active#(if(X1, X2, X3)) -> active#(X1),
                      active#(s(X)) -> active#(X),
              active#(prod(X1, X2)) -> active#(X1),
              active#(prod(X1, X2)) -> active#(X2),
                   active#(fact(X)) -> active#(X),
                      active#(p(X)) -> active#(X),
               active#(add(X1, X2)) -> active#(X1)}
          EDG:
           {(active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> active#(X))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
            (active#(add(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X))
            (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
            (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
            (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
            (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(add(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
            (active#(fact(X)) -> active#(X), active#(p(X)) -> active#(X))
            (active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
            (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
            (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
            (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(p(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
            (active#(p(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
            (active#(p(X)) -> active#(X), active#(fact(X)) -> active#(X))
            (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X))
            (active#(p(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
            (active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(p(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
            (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
            (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
            (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
            (active#(prod(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X))
            (active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
            (active#(prod(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(prod(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
            (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
            (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
            (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
            (active#(prod(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X))
            (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))}
           SCCS:
            Scc:
             {active#(if(X1, X2, X3)) -> active#(X1),
                        active#(s(X)) -> active#(X),
                active#(prod(X1, X2)) -> active#(X1),
                active#(prod(X1, X2)) -> active#(X2),
                     active#(fact(X)) -> active#(X),
                        active#(p(X)) -> active#(X),
                 active#(add(X1, X2)) -> active#(X1)}
            SCC:
             Strict:
              {active#(if(X1, X2, X3)) -> active#(X1),
                         active#(s(X)) -> active#(X),
                 active#(prod(X1, X2)) -> active#(X1),
                 active#(prod(X1, X2)) -> active#(X2),
                      active#(fact(X)) -> active#(X),
                         active#(p(X)) -> active#(X),
                  active#(add(X1, X2)) -> active#(X1)}
             Weak:
             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                           zero(mark(X)) -> mark(zero(X)),
                             zero(ok(X)) -> ok(zero(X)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                           fact(mark(X)) -> mark(fact(X)),
                             fact(ok(X)) -> ok(fact(X)),
                              p(mark(X)) -> mark(p(X)),
                                p(ok(X)) -> ok(p(X)),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                         active(zero(X)) -> zero(active(X)),
                      active(zero(s(X))) -> mark(false()),
                       active(zero(0())) -> mark(true()),
                            active(s(X)) -> s(active(X)),
                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                    active(prod(X1, X2)) -> prod(active(X1), X2),
                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                    active(prod(0(), X)) -> mark(0()),
                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                         active(fact(X)) -> fact(active(X)),
                            active(p(X)) -> p(active(X)),
                         active(p(s(X))) -> mark(X),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(zero(X)) -> zero(proper(X)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                         proper(fact(X)) -> fact(proper(X)),
                            proper(p(X)) -> p(proper(X)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               {active#(if(X1, X2, X3)) -> active#(X1),
                          active#(s(X)) -> active#(X),
                  active#(prod(X1, X2)) -> active#(X1),
                  active#(prod(X1, X2)) -> active#(X2),
                       active#(fact(X)) -> active#(X),
                   active#(add(X1, X2)) -> active#(X1)}
              EDG:
               {(active#(prod(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
                (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
                (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
                (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
                (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                (active#(prod(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
                (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
                (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
                (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
                (active#(prod(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
                (active#(prod(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
                (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
                (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
                (active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
                (active#(fact(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
                (active#(add(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                (active#(add(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
                (active#(add(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
                (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
                (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
                (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
                (active#(if(X1, X2, X3)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))}
               SCCS:
                Scc:
                 {active#(if(X1, X2, X3)) -> active#(X1),
                            active#(s(X)) -> active#(X),
                    active#(prod(X1, X2)) -> active#(X1),
                    active#(prod(X1, X2)) -> active#(X2),
                         active#(fact(X)) -> active#(X),
                     active#(add(X1, X2)) -> active#(X1)}
                SCC:
                 Strict:
                  {active#(if(X1, X2, X3)) -> active#(X1),
                             active#(s(X)) -> active#(X),
                     active#(prod(X1, X2)) -> active#(X1),
                     active#(prod(X1, X2)) -> active#(X2),
                          active#(fact(X)) -> active#(X),
                      active#(add(X1, X2)) -> active#(X1)}
                 Weak:
                 {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                               zero(mark(X)) -> mark(zero(X)),
                                 zero(ok(X)) -> ok(zero(X)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                          prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                          prod(mark(X1), X2) -> mark(prod(X1, X2)),
                        prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                               fact(mark(X)) -> mark(fact(X)),
                                 fact(ok(X)) -> ok(fact(X)),
                                  p(mark(X)) -> mark(p(X)),
                                    p(ok(X)) -> ok(p(X)),
                      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                    active(if(true(), X, Y)) -> mark(X),
                   active(if(false(), X, Y)) -> mark(Y),
                             active(zero(X)) -> zero(active(X)),
                          active(zero(s(X))) -> mark(false()),
                           active(zero(0())) -> mark(true()),
                                active(s(X)) -> s(active(X)),
                        active(prod(X1, X2)) -> prod(X1, active(X2)),
                        active(prod(X1, X2)) -> prod(active(X1), X2),
                       active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                        active(prod(0(), X)) -> mark(0()),
                             active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                             active(fact(X)) -> fact(active(X)),
                                active(p(X)) -> p(active(X)),
                             active(p(s(X))) -> mark(X),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                             proper(zero(X)) -> zero(proper(X)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                        proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                             proper(fact(X)) -> fact(proper(X)),
                                proper(p(X)) -> p(proper(X)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(true()) -> ok(true()),
                             proper(false()) -> ok(false()),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(active#) = 0
                  Strict:
                   {active#(if(X1, X2, X3)) -> active#(X1),
                              active#(s(X)) -> active#(X),
                      active#(prod(X1, X2)) -> active#(X1),
                      active#(prod(X1, X2)) -> active#(X2),
                           active#(fact(X)) -> active#(X)}
                  EDG:
                   {(active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
                    (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
                    (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
                    (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                    (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
                    (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
                    (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                    (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                    (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                    (active#(prod(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
                    (active#(prod(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
                    (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X1))
                    (active#(prod(X1, X2)) -> active#(X2), active#(prod(X1, X2)) -> active#(X2))
                    (active#(prod(X1, X2)) -> active#(X2), active#(fact(X)) -> active#(X))
                    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                    (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
                    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                    (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X2))
                    (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
                    (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X2))
                    (active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))}
                   SCCS:
                    Scc:
                     {active#(if(X1, X2, X3)) -> active#(X1),
                                active#(s(X)) -> active#(X),
                        active#(prod(X1, X2)) -> active#(X1),
                        active#(prod(X1, X2)) -> active#(X2),
                             active#(fact(X)) -> active#(X)}
                    SCC:
                     Strict:
                      {active#(if(X1, X2, X3)) -> active#(X1),
                                 active#(s(X)) -> active#(X),
                         active#(prod(X1, X2)) -> active#(X1),
                         active#(prod(X1, X2)) -> active#(X2),
                              active#(fact(X)) -> active#(X)}
                     Weak:
                     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                   zero(mark(X)) -> mark(zero(X)),
                                     zero(ok(X)) -> ok(zero(X)),
                                      s(mark(X)) -> mark(s(X)),
                                        s(ok(X)) -> ok(s(X)),
                              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                              prod(mark(X1), X2) -> mark(prod(X1, X2)),
                            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                   fact(mark(X)) -> mark(fact(X)),
                                     fact(ok(X)) -> ok(fact(X)),
                                      p(mark(X)) -> mark(p(X)),
                                        p(ok(X)) -> ok(p(X)),
                          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                        active(if(true(), X, Y)) -> mark(X),
                       active(if(false(), X, Y)) -> mark(Y),
                                 active(zero(X)) -> zero(active(X)),
                              active(zero(s(X))) -> mark(false()),
                               active(zero(0())) -> mark(true()),
                                    active(s(X)) -> s(active(X)),
                            active(prod(X1, X2)) -> prod(X1, active(X2)),
                            active(prod(X1, X2)) -> prod(active(X1), X2),
                           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                            active(prod(0(), X)) -> mark(0()),
                                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                 active(fact(X)) -> fact(active(X)),
                                    active(p(X)) -> p(active(X)),
                                 active(p(s(X))) -> mark(X),
                             active(add(X1, X2)) -> add(X1, active(X2)),
                             active(add(X1, X2)) -> add(active(X1), X2),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                               add(mark(X1), X2) -> mark(add(X1, X2)),
                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                 proper(zero(X)) -> zero(proper(X)),
                                    proper(s(X)) -> s(proper(X)),
                                     proper(0()) -> ok(0()),
                            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                 proper(fact(X)) -> fact(proper(X)),
                                    proper(p(X)) -> p(proper(X)),
                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                  proper(true()) -> ok(true()),
                                 proper(false()) -> ok(false()),
                                    top(mark(X)) -> top(proper(X)),
                                      top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(active#) = 0
                      Strict:
                       {active#(if(X1, X2, X3)) -> active#(X1),
                                  active#(s(X)) -> active#(X),
                          active#(prod(X1, X2)) -> active#(X1),
                               active#(fact(X)) -> active#(X)}
                      EDG:
                       {(active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
                        (active#(fact(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
                        (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
                        (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                        (active#(prod(X1, X2)) -> active#(X1), active#(fact(X)) -> active#(X))
                        (active#(prod(X1, X2)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                        (active#(prod(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                        (active#(prod(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                        (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                        (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
                        (active#(if(X1, X2, X3)) -> active#(X1), active#(prod(X1, X2)) -> active#(X1))
                        (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
                        (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                        (active#(s(X)) -> active#(X), active#(prod(X1, X2)) -> active#(X1))
                        (active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))}
                       SCCS:
                        Scc:
                         {active#(if(X1, X2, X3)) -> active#(X1),
                                    active#(s(X)) -> active#(X),
                            active#(prod(X1, X2)) -> active#(X1),
                                 active#(fact(X)) -> active#(X)}
                        SCC:
                         Strict:
                          {active#(if(X1, X2, X3)) -> active#(X1),
                                     active#(s(X)) -> active#(X),
                             active#(prod(X1, X2)) -> active#(X1),
                                  active#(fact(X)) -> active#(X)}
                         Weak:
                         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                       zero(mark(X)) -> mark(zero(X)),
                                         zero(ok(X)) -> ok(zero(X)),
                                          s(mark(X)) -> mark(s(X)),
                                            s(ok(X)) -> ok(s(X)),
                                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                       fact(mark(X)) -> mark(fact(X)),
                                         fact(ok(X)) -> ok(fact(X)),
                                          p(mark(X)) -> mark(p(X)),
                                            p(ok(X)) -> ok(p(X)),
                              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                            active(if(true(), X, Y)) -> mark(X),
                           active(if(false(), X, Y)) -> mark(Y),
                                     active(zero(X)) -> zero(active(X)),
                                  active(zero(s(X))) -> mark(false()),
                                   active(zero(0())) -> mark(true()),
                                        active(s(X)) -> s(active(X)),
                                active(prod(X1, X2)) -> prod(X1, active(X2)),
                                active(prod(X1, X2)) -> prod(active(X1), X2),
                               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                active(prod(0(), X)) -> mark(0()),
                                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                     active(fact(X)) -> fact(active(X)),
                                        active(p(X)) -> p(active(X)),
                                     active(p(s(X))) -> mark(X),
                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                 active(add(X1, X2)) -> add(active(X1), X2),
                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                 active(add(0(), X)) -> mark(X),
                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                     proper(zero(X)) -> zero(proper(X)),
                                        proper(s(X)) -> s(proper(X)),
                                         proper(0()) -> ok(0()),
                                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                     proper(fact(X)) -> fact(proper(X)),
                                        proper(p(X)) -> p(proper(X)),
                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                      proper(true()) -> ok(true()),
                                     proper(false()) -> ok(false()),
                                        top(mark(X)) -> top(proper(X)),
                                          top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(active#) = 0
                          Strict:
                           {active#(if(X1, X2, X3)) -> active#(X1),
                                      active#(s(X)) -> active#(X),
                                   active#(fact(X)) -> active#(X)}
                          EDG:
                           {(active#(s(X)) -> active#(X), active#(fact(X)) -> active#(X))
                            (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                            (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                            (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                            (active#(fact(X)) -> active#(X), active#(s(X)) -> active#(X))
                            (active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))
                            (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                            (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X))
                            (active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))}
                           SCCS:
                            Scc:
                             {active#(if(X1, X2, X3)) -> active#(X1),
                                        active#(s(X)) -> active#(X),
                                     active#(fact(X)) -> active#(X)}
                            SCC:
                             Strict:
                              {active#(if(X1, X2, X3)) -> active#(X1),
                                         active#(s(X)) -> active#(X),
                                      active#(fact(X)) -> active#(X)}
                             Weak:
                             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                           zero(mark(X)) -> mark(zero(X)),
                                             zero(ok(X)) -> ok(zero(X)),
                                              s(mark(X)) -> mark(s(X)),
                                                s(ok(X)) -> ok(s(X)),
                                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                           fact(mark(X)) -> mark(fact(X)),
                                             fact(ok(X)) -> ok(fact(X)),
                                              p(mark(X)) -> mark(p(X)),
                                                p(ok(X)) -> ok(p(X)),
                                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                active(if(true(), X, Y)) -> mark(X),
                               active(if(false(), X, Y)) -> mark(Y),
                                         active(zero(X)) -> zero(active(X)),
                                      active(zero(s(X))) -> mark(false()),
                                       active(zero(0())) -> mark(true()),
                                            active(s(X)) -> s(active(X)),
                                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                                    active(prod(X1, X2)) -> prod(active(X1), X2),
                                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                    active(prod(0(), X)) -> mark(0()),
                                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                         active(fact(X)) -> fact(active(X)),
                                            active(p(X)) -> p(active(X)),
                                         active(p(s(X))) -> mark(X),
                                     active(add(X1, X2)) -> add(X1, active(X2)),
                                     active(add(X1, X2)) -> add(active(X1), X2),
                                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                     active(add(0(), X)) -> mark(X),
                                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                                       add(mark(X1), X2) -> mark(add(X1, X2)),
                                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                         proper(zero(X)) -> zero(proper(X)),
                                            proper(s(X)) -> s(proper(X)),
                                             proper(0()) -> ok(0()),
                                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                         proper(fact(X)) -> fact(proper(X)),
                                            proper(p(X)) -> p(proper(X)),
                                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                          proper(true()) -> ok(true()),
                                         proper(false()) -> ok(false()),
                                            top(mark(X)) -> top(proper(X)),
                                              top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(active#) = 0
                              Strict:
                               {active#(if(X1, X2, X3)) -> active#(X1),
                                       active#(fact(X)) -> active#(X)}
                              EDG:
                               {(active#(if(X1, X2, X3)) -> active#(X1), active#(fact(X)) -> active#(X))
                                (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
                                (active#(fact(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
                                (active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))}
                               SCCS:
                                Scc:
                                 {active#(if(X1, X2, X3)) -> active#(X1),
                                         active#(fact(X)) -> active#(X)}
                                SCC:
                                 Strict:
                                  {active#(if(X1, X2, X3)) -> active#(X1),
                                          active#(fact(X)) -> active#(X)}
                                 Weak:
                                 {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                               zero(mark(X)) -> mark(zero(X)),
                                                 zero(ok(X)) -> ok(zero(X)),
                                                  s(mark(X)) -> mark(s(X)),
                                                    s(ok(X)) -> ok(s(X)),
                                          prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                          prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                        prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                               fact(mark(X)) -> mark(fact(X)),
                                                 fact(ok(X)) -> ok(fact(X)),
                                                  p(mark(X)) -> mark(p(X)),
                                                    p(ok(X)) -> ok(p(X)),
                                      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                    active(if(true(), X, Y)) -> mark(X),
                                   active(if(false(), X, Y)) -> mark(Y),
                                             active(zero(X)) -> zero(active(X)),
                                          active(zero(s(X))) -> mark(false()),
                                           active(zero(0())) -> mark(true()),
                                                active(s(X)) -> s(active(X)),
                                        active(prod(X1, X2)) -> prod(X1, active(X2)),
                                        active(prod(X1, X2)) -> prod(active(X1), X2),
                                       active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                        active(prod(0(), X)) -> mark(0()),
                                             active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                             active(fact(X)) -> fact(active(X)),
                                                active(p(X)) -> p(active(X)),
                                             active(p(s(X))) -> mark(X),
                                         active(add(X1, X2)) -> add(X1, active(X2)),
                                         active(add(X1, X2)) -> add(active(X1), X2),
                                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                         active(add(0(), X)) -> mark(X),
                                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                                           add(mark(X1), X2) -> mark(add(X1, X2)),
                                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                             proper(zero(X)) -> zero(proper(X)),
                                                proper(s(X)) -> s(proper(X)),
                                                 proper(0()) -> ok(0()),
                                        proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                             proper(fact(X)) -> fact(proper(X)),
                                                proper(p(X)) -> p(proper(X)),
                                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                              proper(true()) -> ok(true()),
                                             proper(false()) -> ok(false()),
                                                top(mark(X)) -> top(proper(X)),
                                                  top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(active#) = 0
                                  Strict:
                                   {active#(fact(X)) -> active#(X)}
                                  EDG:
                                   {(active#(fact(X)) -> active#(X), active#(fact(X)) -> active#(X))}
                                   SCCS:
                                    Scc:
                                     {active#(fact(X)) -> active#(X)}
                                    SCC:
                                     Strict:
                                      {active#(fact(X)) -> active#(X)}
                                     Weak:
                                     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                   zero(mark(X)) -> mark(zero(X)),
                                                     zero(ok(X)) -> ok(zero(X)),
                                                      s(mark(X)) -> mark(s(X)),
                                                        s(ok(X)) -> ok(s(X)),
                                              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                                              prod(mark(X1), X2) -> mark(prod(X1, X2)),
                                            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                                                   fact(mark(X)) -> mark(fact(X)),
                                                     fact(ok(X)) -> ok(fact(X)),
                                                      p(mark(X)) -> mark(p(X)),
                                                        p(ok(X)) -> ok(p(X)),
                                          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                                        active(if(true(), X, Y)) -> mark(X),
                                       active(if(false(), X, Y)) -> mark(Y),
                                                 active(zero(X)) -> zero(active(X)),
                                              active(zero(s(X))) -> mark(false()),
                                               active(zero(0())) -> mark(true()),
                                                    active(s(X)) -> s(active(X)),
                                            active(prod(X1, X2)) -> prod(X1, active(X2)),
                                            active(prod(X1, X2)) -> prod(active(X1), X2),
                                           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                                            active(prod(0(), X)) -> mark(0()),
                                                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                                                 active(fact(X)) -> fact(active(X)),
                                                    active(p(X)) -> p(active(X)),
                                                 active(p(s(X))) -> mark(X),
                                             active(add(X1, X2)) -> add(X1, active(X2)),
                                             active(add(X1, X2)) -> add(active(X1), X2),
                                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                             active(add(0(), X)) -> mark(X),
                                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                                               add(mark(X1), X2) -> mark(add(X1, X2)),
                                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                 proper(zero(X)) -> zero(proper(X)),
                                                    proper(s(X)) -> s(proper(X)),
                                                     proper(0()) -> ok(0()),
                                            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                                                 proper(fact(X)) -> fact(proper(X)),
                                                    proper(p(X)) -> p(proper(X)),
                                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                  proper(true()) -> ok(true()),
                                                 proper(false()) -> ok(false()),
                                                    top(mark(X)) -> top(proper(X)),
                                                      top(ok(X)) -> top(active(X))}
                                     SPSC:
                                      Simple Projection:
                                       pi(active#) = 0
                                      Strict:
                                       {}
                                      Qed
    SCC:
     Strict:
      {p#(mark(X)) -> p#(X),
         p#(ok(X)) -> p#(X)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {p#(ok(X)) -> p#(X)}
      EDG:
       {(p#(ok(X)) -> p#(X), p#(ok(X)) -> p#(X))}
       SCCS:
        Scc:
         {p#(ok(X)) -> p#(X)}
        SCC:
         Strict:
          {p#(ok(X)) -> p#(X)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(p#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {fact#(mark(X)) -> fact#(X),
         fact#(ok(X)) -> fact#(X)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(fact#) = 0
      Strict:
       {fact#(ok(X)) -> fact#(X)}
      EDG:
       {(fact#(ok(X)) -> fact#(X), fact#(ok(X)) -> fact#(X))}
       SCCS:
        Scc:
         {fact#(ok(X)) -> fact#(X)}
        SCC:
         Strict:
          {fact#(ok(X)) -> fact#(X)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(fact#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  prod#(X1, mark(X2)) -> prod#(X1, X2),
         prod#(mark(X1), X2) -> prod#(X1, X2),
       prod#(ok(X1), ok(X2)) -> prod#(X1, X2)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(prod#) = 0
      Strict:
       {prod#(X1, mark(X2)) -> prod#(X1, X2),
        prod#(mark(X1), X2) -> prod#(X1, X2)}
      EDG:
       {(prod#(mark(X1), X2) -> prod#(X1, X2), prod#(mark(X1), X2) -> prod#(X1, X2))
        (prod#(mark(X1), X2) -> prod#(X1, X2), prod#(X1, mark(X2)) -> prod#(X1, X2))
        (prod#(X1, mark(X2)) -> prod#(X1, X2), prod#(X1, mark(X2)) -> prod#(X1, X2))
        (prod#(X1, mark(X2)) -> prod#(X1, X2), prod#(mark(X1), X2) -> prod#(X1, X2))}
       SCCS:
        Scc:
         {prod#(X1, mark(X2)) -> prod#(X1, X2),
          prod#(mark(X1), X2) -> prod#(X1, X2)}
        SCC:
         Strict:
          {prod#(X1, mark(X2)) -> prod#(X1, X2),
           prod#(mark(X1), X2) -> prod#(X1, X2)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(prod#) = 0
          Strict:
           {prod#(X1, mark(X2)) -> prod#(X1, X2)}
          EDG:
           {(prod#(X1, mark(X2)) -> prod#(X1, X2), prod#(X1, mark(X2)) -> prod#(X1, X2))}
           SCCS:
            Scc:
             {prod#(X1, mark(X2)) -> prod#(X1, X2)}
            SCC:
             Strict:
              {prod#(X1, mark(X2)) -> prod#(X1, X2)}
             Weak:
             {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                           zero(mark(X)) -> mark(zero(X)),
                             zero(ok(X)) -> ok(zero(X)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                      prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                      prod(mark(X1), X2) -> mark(prod(X1, X2)),
                    prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                           fact(mark(X)) -> mark(fact(X)),
                             fact(ok(X)) -> ok(fact(X)),
                              p(mark(X)) -> mark(p(X)),
                                p(ok(X)) -> ok(p(X)),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                         active(zero(X)) -> zero(active(X)),
                      active(zero(s(X))) -> mark(false()),
                       active(zero(0())) -> mark(true()),
                            active(s(X)) -> s(active(X)),
                    active(prod(X1, X2)) -> prod(X1, active(X2)),
                    active(prod(X1, X2)) -> prod(active(X1), X2),
                   active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                    active(prod(0(), X)) -> mark(0()),
                         active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                         active(fact(X)) -> fact(active(X)),
                            active(p(X)) -> p(active(X)),
                         active(p(s(X))) -> mark(X),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(zero(X)) -> zero(proper(X)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                    proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                         proper(fact(X)) -> fact(proper(X)),
                            proper(p(X)) -> p(proper(X)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(prod#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {s#(mark(X)) -> s#(X),
         s#(ok(X)) -> s#(X)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(ok(X)) -> s#(X)}
      EDG:
       {(s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(ok(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(ok(X)) -> s#(X)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {zero#(mark(X)) -> zero#(X),
         zero#(ok(X)) -> zero#(X)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(zero#) = 0
      Strict:
       {zero#(ok(X)) -> zero#(X)}
      EDG:
       {(zero#(ok(X)) -> zero#(X), zero#(ok(X)) -> zero#(X))}
       SCCS:
        Scc:
         {zero#(ok(X)) -> zero#(X)}
        SCC:
         Strict:
          {zero#(ok(X)) -> zero#(X)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(zero#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {      if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
       if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)}
     Weak:
     {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   zero(mark(X)) -> mark(zero(X)),
                     zero(ok(X)) -> ok(zero(X)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
              prod(X1, mark(X2)) -> mark(prod(X1, X2)),
              prod(mark(X1), X2) -> mark(prod(X1, X2)),
            prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                   fact(mark(X)) -> mark(fact(X)),
                     fact(ok(X)) -> ok(fact(X)),
                      p(mark(X)) -> mark(p(X)),
                        p(ok(X)) -> ok(p(X)),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                 active(zero(X)) -> zero(active(X)),
              active(zero(s(X))) -> mark(false()),
               active(zero(0())) -> mark(true()),
                    active(s(X)) -> s(active(X)),
            active(prod(X1, X2)) -> prod(X1, active(X2)),
            active(prod(X1, X2)) -> prod(active(X1), X2),
           active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
            active(prod(0(), X)) -> mark(0()),
                 active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                 active(fact(X)) -> fact(active(X)),
                    active(p(X)) -> p(active(X)),
                 active(p(s(X))) -> mark(X),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(zero(X)) -> zero(proper(X)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
            proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                 proper(fact(X)) -> fact(proper(X)),
                    proper(p(X)) -> p(proper(X)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(if#) = 0
      Strict:
       {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)}
      EDG:
       {(if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))}
       SCCS:
        Scc:
         {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)}
        SCC:
         Strict:
          {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)}
         Weak:
         {      if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                       zero(mark(X)) -> mark(zero(X)),
                         zero(ok(X)) -> ok(zero(X)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                  prod(X1, mark(X2)) -> mark(prod(X1, X2)),
                  prod(mark(X1), X2) -> mark(prod(X1, X2)),
                prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                       fact(mark(X)) -> mark(fact(X)),
                         fact(ok(X)) -> ok(fact(X)),
                          p(mark(X)) -> mark(p(X)),
                            p(ok(X)) -> ok(p(X)),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                     active(zero(X)) -> zero(active(X)),
                  active(zero(s(X))) -> mark(false()),
                   active(zero(0())) -> mark(true()),
                        active(s(X)) -> s(active(X)),
                active(prod(X1, X2)) -> prod(X1, active(X2)),
                active(prod(X1, X2)) -> prod(active(X1), X2),
               active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
                active(prod(0(), X)) -> mark(0()),
                     active(fact(X)) -> mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
                     active(fact(X)) -> fact(active(X)),
                        active(p(X)) -> p(active(X)),
                     active(p(s(X))) -> mark(X),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(zero(X)) -> zero(proper(X)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
                     proper(fact(X)) -> fact(proper(X)),
                        proper(p(X)) -> p(proper(X)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(if#) = 0
          Strict:
           {}
          Qed