YES
TRS:
 {            active(and(X1, X2)) -> and(active(X1), X2),
           active(and(true(), X)) -> mark(X),
          active(and(false(), Y)) -> mark(false()),
           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(add(X1, X2)) -> add(active(X1), X2),
              active(add(0(), X)) -> mark(X),
             active(add(s(X), Y)) -> mark(s(add(X, Y))),
            active(first(X1, X2)) -> first(X1, active(X2)),
            active(first(X1, X2)) -> first(active(X1), X2),
            active(first(0(), X)) -> mark(nil()),
  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                  active(from(X)) -> mark(cons(X, from(s(X)))),
                and(mark(X1), X2) -> mark(and(X1, X2)),
              and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
             if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
       if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                add(mark(X1), X2) -> mark(add(X1, X2)),
              add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                         s(ok(X)) -> ok(s(X)),
              first(X1, mark(X2)) -> mark(first(X1, X2)),
              first(mark(X1), X2) -> mark(first(X1, X2)),
            first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
             cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      from(ok(X)) -> ok(from(X)),
              proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                   proper(true()) -> ok(true()),
                  proper(false()) -> ok(false()),
           proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
              proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                      proper(0()) -> ok(0()),
                     proper(s(X)) -> s(proper(X)),
                    proper(nil()) -> ok(nil()),
            proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(from(X)) -> from(proper(X)),
                     top(mark(X)) -> top(proper(X)),
                       top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {            active#(and(X1, X2)) -> active#(X1),
                active#(and(X1, X2)) -> and#(active(X1), X2),
             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(X1, X2)) -> add#(active(X1), X2),
               active#(add(s(X), Y)) -> add#(X, Y),
               active#(add(s(X), Y)) -> s#(add(X, Y)),
              active#(first(X1, X2)) -> active#(X1),
              active#(first(X1, X2)) -> active#(X2),
              active#(first(X1, X2)) -> first#(X1, active(X2)),
              active#(first(X1, X2)) -> first#(active(X1), X2),
    active#(first(s(X), cons(Y, Z))) -> first#(X, Z),
    active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)),
                    active#(from(X)) -> s#(X),
                    active#(from(X)) -> cons#(X, from(s(X))),
                    active#(from(X)) -> from#(s(X)),
                  and#(mark(X1), X2) -> and#(X1, X2),
                and#(ok(X1), ok(X2)) -> and#(X1, X2),
               if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
         if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3),
                  add#(mark(X1), X2) -> add#(X1, X2),
                add#(ok(X1), ok(X2)) -> add#(X1, X2),
                           s#(ok(X)) -> s#(X),
                first#(X1, mark(X2)) -> first#(X1, X2),
                first#(mark(X1), X2) -> first#(X1, X2),
              first#(ok(X1), ok(X2)) -> first#(X1, X2),
               cons#(ok(X1), ok(X2)) -> cons#(X1, X2),
                        from#(ok(X)) -> from#(X),
                proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)),
                proper#(and(X1, X2)) -> proper#(X1),
                proper#(and(X1, X2)) -> proper#(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#(add(X1, X2)) -> add#(proper(X1), proper(X2)),
                proper#(add(X1, X2)) -> proper#(X1),
                proper#(add(X1, X2)) -> proper#(X2),
                       proper#(s(X)) -> s#(proper(X)),
                       proper#(s(X)) -> proper#(X),
              proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)),
              proper#(first(X1, X2)) -> proper#(X1),
              proper#(first(X1, X2)) -> proper#(X2),
               proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)),
               proper#(cons(X1, X2)) -> proper#(X1),
               proper#(cons(X1, X2)) -> proper#(X2),
                    proper#(from(X)) -> from#(proper(X)),
                    proper#(from(X)) -> proper#(X),
                       top#(mark(X)) -> proper#(X),
                       top#(mark(X)) -> top#(proper(X)),
                         top#(ok(X)) -> active#(X),
                         top#(ok(X)) -> top#(active(X))}
  Weak:
  {            active(and(X1, X2)) -> and(active(X1), X2),
            active(and(true(), X)) -> mark(X),
           active(and(false(), Y)) -> mark(false()),
            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(add(X1, X2)) -> add(active(X1), X2),
               active(add(0(), X)) -> mark(X),
              active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(first(X1, X2)) -> first(X1, active(X2)),
             active(first(X1, X2)) -> first(active(X1), X2),
             active(first(0(), X)) -> mark(nil()),
   active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                   active(from(X)) -> mark(cons(X, from(s(X)))),
                 and(mark(X1), X2) -> mark(and(X1, X2)),
               and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
              if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
        if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                 add(mark(X1), X2) -> mark(add(X1, X2)),
               add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                          s(ok(X)) -> ok(s(X)),
               first(X1, mark(X2)) -> mark(first(X1, X2)),
               first(mark(X1), X2) -> mark(first(X1, X2)),
             first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       from(ok(X)) -> ok(from(X)),
               proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                    proper(true()) -> ok(true()),
                   proper(false()) -> ok(false()),
            proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
               proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                       proper(0()) -> ok(0()),
                      proper(s(X)) -> s(proper(X)),
                     proper(nil()) -> ok(nil()),
             proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                   proper(from(X)) -> from(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
  EDG:
   {
    (active#(and(X1, X2)) -> and#(active(X1), X2), and#(ok(X1), ok(X2)) -> and#(X1, X2))
    (active#(and(X1, X2)) -> and#(active(X1), X2), and#(mark(X1), X2) -> and#(X1, X2))
    (active#(first(X1, X2)) -> first#(active(X1), X2), first#(ok(X1), ok(X2)) -> first#(X1, X2))
    (active#(first(X1, X2)) -> first#(active(X1), X2), first#(mark(X1), X2) -> first#(X1, X2))
    (active#(first(X1, X2)) -> first#(active(X1), X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(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#(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#(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#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (top#(mark(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (and#(ok(X1), ok(X2)) -> and#(X1, X2), and#(ok(X1), ok(X2)) -> and#(X1, X2))
    (and#(ok(X1), ok(X2)) -> and#(X1, X2), and#(mark(X1), X2) -> and#(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))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(first(X1, X2)) -> active#(X1))
    (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(s(X), Y)) -> 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)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(and(X1, X2)) -> and#(active(X1), X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (active#(first(X1, X2)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(first(X1, X2)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(first(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (active#(first(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2))
    (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2)))
    (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
    (active#(first(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(first(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(first(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(first(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> and#(active(X1), X2))
    (active#(first(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (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#(X1))
    (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#(and(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(first(X1, X2)) -> active#(X2), active#(from(X)) -> from#(s(X)))
    (active#(first(X1, X2)) -> active#(X2), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(first(X1, X2)) -> active#(X2), active#(from(X)) -> s#(X))
    (active#(first(X1, X2)) -> active#(X2), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (active#(first(X1, X2)) -> active#(X2), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(active(X1), X2))
    (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> first#(X1, active(X2)))
    (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2))
    (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(first(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(first(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(first(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> and#(active(X1), X2))
    (active#(first(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (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#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (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#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (active#(first(X1, X2)) -> first#(X1, active(X2)), first#(ok(X1), ok(X2)) -> first#(X1, X2))
    (active#(first(X1, X2)) -> first#(X1, active(X2)), first#(mark(X1), X2) -> first#(X1, X2))
    (active#(first(X1, X2)) -> first#(X1, active(X2)), first#(X1, mark(X2)) -> first#(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#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(from(X)) -> from#(s(X)), from#(ok(X)) -> from#(X))
    (proper#(from(X)) -> from#(proper(X)), from#(ok(X)) -> from#(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))
    (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))
    (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))
    (active#(if(X1, X2, X3)) -> if#(active(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))
    (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#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (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)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> add#(proper(X1), 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)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> s#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> from#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
    (proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), first#(X1, mark(X2)) -> first#(X1, X2))
    (proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), first#(mark(X1), X2) -> first#(X1, X2))
    (proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)), first#(ok(X1), ok(X2)) -> first#(X1, X2))
    (proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)), and#(mark(X1), X2) -> and#(X1, X2))
    (proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)), and#(ok(X1), ok(X2)) -> and#(X1, X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
    (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#(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#(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#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(and(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(ok(X)) -> s#(X))
    (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)) -> if#(proper(X1), proper(X2), proper(X3)), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(first(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(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#(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))
    (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#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(add(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> and#(active(X1), X2))
    (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))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (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#(first(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (active#(add(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (active#(add(X1, X2)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(add(X1, X2)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
    (active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> and#(active(X1), X2))
    (active#(and(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(and(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(and(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(and(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(and(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(and(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X1))
    (active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
    (active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(X1, active(X2)))
    (active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> first#(active(X1), X2))
    (active#(and(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (active#(and(X1, X2)) -> active#(X1), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (active#(and(X1, X2)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(and(X1, X2)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(and(X1, X2)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (first#(ok(X1), ok(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (first#(ok(X1), ok(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(ok(X1), ok(X2)) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(X1, X2))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(ok(X1), ok(X2)) -> first#(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))
    (and#(mark(X1), X2) -> and#(X1, X2), and#(mark(X1), X2) -> and#(X1, X2))
    (and#(mark(X1), X2) -> and#(X1, X2), and#(ok(X1), ok(X2)) -> and#(X1, X2))
    (top#(ok(X)) -> active#(X), active#(and(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(and(X1, X2)) -> and#(active(X1), X2))
    (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))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (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#(first(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> first#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(first(X1, X2)) -> first#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (top#(ok(X)) -> active#(X), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> s#(X))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> and#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(from(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> first#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (from#(ok(X)) -> from#(X), from#(ok(X)) -> from#(X))
    (active#(from(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(X1, mark(X2)) -> first#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(mark(X1), X2) -> first#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(ok(X1), ok(X2)) -> first#(X1, X2))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {   proper#(and(X1, X2)) -> proper#(X1),
         proper#(and(X1, X2)) -> proper#(X2),
      proper#(if(X1, X2, X3)) -> proper#(X1),
      proper#(if(X1, X2, X3)) -> proper#(X2),
      proper#(if(X1, X2, X3)) -> proper#(X3),
         proper#(add(X1, X2)) -> proper#(X1),
         proper#(add(X1, X2)) -> proper#(X2),
                proper#(s(X)) -> proper#(X),
       proper#(first(X1, X2)) -> proper#(X1),
       proper#(first(X1, X2)) -> proper#(X2),
        proper#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
             proper#(from(X)) -> proper#(X)}
    Scc:
     {from#(ok(X)) -> from#(X)}
    Scc:
     {cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
    Scc:
     {  first#(X1, mark(X2)) -> first#(X1, X2),
        first#(mark(X1), X2) -> first#(X1, X2),
      first#(ok(X1), ok(X2)) -> first#(X1, X2)}
    Scc:
     {s#(ok(X)) -> s#(X)}
    Scc:
     {  add#(mark(X1), X2) -> add#(X1, X2),
      add#(ok(X1), ok(X2)) -> add#(X1, X2)}
    Scc:
     {      if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
      if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)}
    Scc:
     {  and#(mark(X1), X2) -> and#(X1, X2),
      and#(ok(X1), ok(X2)) -> and#(X1, X2)}
    Scc:
     {   active#(and(X1, X2)) -> active#(X1),
      active#(if(X1, X2, X3)) -> active#(X1),
         active#(add(X1, X2)) -> active#(X1),
       active#(first(X1, X2)) -> active#(X1),
       active#(first(X1, X2)) -> active#(X2)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     POLY:
      Argument Filtering:
       pi(top#) = 0, pi(top) = [], pi(ok) = 0, pi(proper) = 0, pi(from) = [], pi(cons) = [], pi(first) = [0,1], pi(nil) = [], pi(s) = [], pi(0) = [], pi(add) = [0,1], pi(if) = [0,1,2], pi(false) = [], pi(true) = [], pi(and) = [0,1], pi(active) = 0, pi(mark) = [0]
      Usable Rules:
       {}
      Interpretation:
       [mark](x0) = x0 + 1
      Strict:
       {top#(ok(X)) -> top#(active(X))}
      Weak:
       {            active(and(X1, X2)) -> and(active(X1), X2),
                 active(and(true(), X)) -> mark(X),
                active(and(false(), Y)) -> mark(false()),
                 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(add(X1, X2)) -> add(active(X1), X2),
                    active(add(0(), X)) -> mark(X),
                   active(add(s(X), Y)) -> mark(s(add(X, Y))),
                  active(first(X1, X2)) -> first(X1, active(X2)),
                  active(first(X1, X2)) -> first(active(X1), X2),
                  active(first(0(), X)) -> mark(nil()),
        active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                        active(from(X)) -> mark(cons(X, from(s(X)))),
                      and(mark(X1), X2) -> mark(and(X1, X2)),
                    and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                   if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
             if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                      add(mark(X1), X2) -> mark(add(X1, X2)),
                    add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                               s(ok(X)) -> ok(s(X)),
                    first(X1, mark(X2)) -> mark(first(X1, X2)),
                    first(mark(X1), X2) -> mark(first(X1, X2)),
                  first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                   cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                            from(ok(X)) -> ok(from(X)),
                    proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                         proper(true()) -> ok(true()),
                        proper(false()) -> ok(false()),
                 proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                    proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            proper(0()) -> ok(0()),
                           proper(s(X)) -> s(proper(X)),
                          proper(nil()) -> ok(nil()),
                  proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                   proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(from(X)) -> from(proper(X)),
                           top(mark(X)) -> top(proper(X)),
                             top(ok(X)) -> top(active(X))}
      EDG:
       {(top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))}
       SCCS:
        Scc:
         {top#(ok(X)) -> top#(active(X))}
        SCC:
         Strict:
          {top#(ok(X)) -> top#(active(X))}
         Weak:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         POLY:
          Argument Filtering:
           pi(top#) = 0, pi(top) = [], pi(ok) = [0], pi(proper) = [], pi(from) = [], pi(cons) = [], pi(first) = [0], pi(nil) = [], pi(s) = [], pi(0) = [], pi(add) = [1], pi(if) = [2], pi(false) = [], pi(true) = [], pi(and) = [0], pi(active) = 0, pi(mark) = []
          Usable Rules:
           {}
          Interpretation:
           [ok](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {            active(and(X1, X2)) -> and(active(X1), X2),
                     active(and(true(), X)) -> mark(X),
                    active(and(false(), Y)) -> mark(false()),
                     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(add(X1, X2)) -> add(active(X1), X2),
                        active(add(0(), X)) -> mark(X),
                       active(add(s(X), Y)) -> mark(s(add(X, Y))),
                      active(first(X1, X2)) -> first(X1, active(X2)),
                      active(first(X1, X2)) -> first(active(X1), X2),
                      active(first(0(), X)) -> mark(nil()),
            active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                            active(from(X)) -> mark(cons(X, from(s(X)))),
                          and(mark(X1), X2) -> mark(and(X1, X2)),
                        and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                       if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                 if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                          add(mark(X1), X2) -> mark(add(X1, X2)),
                        add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                   s(ok(X)) -> ok(s(X)),
                        first(X1, mark(X2)) -> mark(first(X1, X2)),
                        first(mark(X1), X2) -> mark(first(X1, X2)),
                      first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                       cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                from(ok(X)) -> ok(from(X)),
                        proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                             proper(true()) -> ok(true()),
                            proper(false()) -> ok(false()),
                     proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                        proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                proper(0()) -> ok(0()),
                               proper(s(X)) -> s(proper(X)),
                              proper(nil()) -> ok(nil()),
                      proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                       proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                            proper(from(X)) -> from(proper(X)),
                               top(mark(X)) -> top(proper(X)),
                                 top(ok(X)) -> top(active(X))}
          Qed
    SCC:
     Strict:
      {   proper#(and(X1, X2)) -> proper#(X1),
          proper#(and(X1, X2)) -> proper#(X2),
       proper#(if(X1, X2, X3)) -> proper#(X1),
       proper#(if(X1, X2, X3)) -> proper#(X2),
       proper#(if(X1, X2, X3)) -> proper#(X3),
          proper#(add(X1, X2)) -> proper#(X1),
          proper#(add(X1, X2)) -> proper#(X2),
                 proper#(s(X)) -> proper#(X),
        proper#(first(X1, X2)) -> proper#(X1),
        proper#(first(X1, X2)) -> proper#(X2),
         proper#(cons(X1, X2)) -> proper#(X1),
         proper#(cons(X1, X2)) -> proper#(X2),
              proper#(from(X)) -> proper#(X)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {   proper#(and(X1, X2)) -> proper#(X1),
           proper#(and(X1, X2)) -> proper#(X2),
        proper#(if(X1, X2, X3)) -> proper#(X1),
        proper#(if(X1, X2, X3)) -> proper#(X2),
        proper#(if(X1, X2, X3)) -> proper#(X3),
           proper#(add(X1, X2)) -> proper#(X2),
                  proper#(s(X)) -> proper#(X),
         proper#(first(X1, X2)) -> proper#(X1),
         proper#(first(X1, X2)) -> proper#(X2),
          proper#(cons(X1, X2)) -> proper#(X1),
          proper#(cons(X1, X2)) -> proper#(X2),
               proper#(from(X)) -> proper#(X)}
      EDG:
       {
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
        (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#(X2), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (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#(and(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(first(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> proper#(X2))
        (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#(and(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
        (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(from(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(and(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
       }
       SCCS:
        Scc:
         {   proper#(and(X1, X2)) -> proper#(X1),
             proper#(and(X1, X2)) -> proper#(X2),
          proper#(if(X1, X2, X3)) -> proper#(X1),
          proper#(if(X1, X2, X3)) -> proper#(X2),
          proper#(if(X1, X2, X3)) -> proper#(X3),
             proper#(add(X1, X2)) -> proper#(X2),
                    proper#(s(X)) -> proper#(X),
           proper#(first(X1, X2)) -> proper#(X1),
           proper#(first(X1, X2)) -> proper#(X2),
            proper#(cons(X1, X2)) -> proper#(X1),
            proper#(cons(X1, X2)) -> proper#(X2),
                 proper#(from(X)) -> proper#(X)}
        SCC:
         Strict:
          {   proper#(and(X1, X2)) -> proper#(X1),
              proper#(and(X1, X2)) -> proper#(X2),
           proper#(if(X1, X2, X3)) -> proper#(X1),
           proper#(if(X1, X2, X3)) -> proper#(X2),
           proper#(if(X1, X2, X3)) -> proper#(X3),
              proper#(add(X1, X2)) -> proper#(X2),
                     proper#(s(X)) -> proper#(X),
            proper#(first(X1, X2)) -> proper#(X1),
            proper#(first(X1, X2)) -> proper#(X2),
             proper#(cons(X1, X2)) -> proper#(X1),
             proper#(cons(X1, X2)) -> proper#(X2),
                  proper#(from(X)) -> proper#(X)}
         Weak:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {   proper#(and(X1, X2)) -> proper#(X1),
               proper#(and(X1, X2)) -> proper#(X2),
            proper#(if(X1, X2, X3)) -> proper#(X1),
            proper#(if(X1, X2, X3)) -> proper#(X2),
            proper#(if(X1, X2, X3)) -> proper#(X3),
               proper#(add(X1, X2)) -> proper#(X2),
                      proper#(s(X)) -> proper#(X),
             proper#(first(X1, X2)) -> proper#(X2),
              proper#(cons(X1, X2)) -> proper#(X1),
              proper#(cons(X1, X2)) -> proper#(X2),
                   proper#(from(X)) -> proper#(X)}
          EDG:
           {(proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
            (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(from(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
            (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#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
            (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#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
            (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#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> 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)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
            (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#(first(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
            (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#(first(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))}
           SCCS:
            Scc:
             {   proper#(and(X1, X2)) -> proper#(X1),
                 proper#(and(X1, X2)) -> proper#(X2),
              proper#(if(X1, X2, X3)) -> proper#(X1),
              proper#(if(X1, X2, X3)) -> proper#(X2),
              proper#(if(X1, X2, X3)) -> proper#(X3),
                 proper#(add(X1, X2)) -> proper#(X2),
                        proper#(s(X)) -> proper#(X),
               proper#(first(X1, X2)) -> proper#(X2),
                proper#(cons(X1, X2)) -> proper#(X1),
                proper#(cons(X1, X2)) -> proper#(X2),
                     proper#(from(X)) -> proper#(X)}
            SCC:
             Strict:
              {   proper#(and(X1, X2)) -> proper#(X1),
                  proper#(and(X1, X2)) -> proper#(X2),
               proper#(if(X1, X2, X3)) -> proper#(X1),
               proper#(if(X1, X2, X3)) -> proper#(X2),
               proper#(if(X1, X2, X3)) -> proper#(X3),
                  proper#(add(X1, X2)) -> proper#(X2),
                         proper#(s(X)) -> proper#(X),
                proper#(first(X1, X2)) -> proper#(X2),
                 proper#(cons(X1, X2)) -> proper#(X1),
                 proper#(cons(X1, X2)) -> proper#(X2),
                      proper#(from(X)) -> proper#(X)}
             Weak:
             {            active(and(X1, X2)) -> and(active(X1), X2),
                       active(and(true(), X)) -> mark(X),
                      active(and(false(), Y)) -> mark(false()),
                       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(add(X1, X2)) -> add(active(X1), X2),
                          active(add(0(), X)) -> mark(X),
                         active(add(s(X), Y)) -> mark(s(add(X, Y))),
                        active(first(X1, X2)) -> first(X1, active(X2)),
                        active(first(X1, X2)) -> first(active(X1), X2),
                        active(first(0(), X)) -> mark(nil()),
              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                              active(from(X)) -> mark(cons(X, from(s(X)))),
                            and(mark(X1), X2) -> mark(and(X1, X2)),
                          and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                         if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                            add(mark(X1), X2) -> mark(add(X1, X2)),
                          add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                     s(ok(X)) -> ok(s(X)),
                          first(X1, mark(X2)) -> mark(first(X1, X2)),
                          first(mark(X1), X2) -> mark(first(X1, X2)),
                        first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                         cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                  from(ok(X)) -> ok(from(X)),
                          proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                               proper(true()) -> ok(true()),
                              proper(false()) -> ok(false()),
                       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                          proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                                 proper(s(X)) -> s(proper(X)),
                                proper(nil()) -> ok(nil()),
                        proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {   proper#(and(X1, X2)) -> proper#(X1),
                   proper#(and(X1, X2)) -> proper#(X2),
                proper#(if(X1, X2, X3)) -> proper#(X1),
                proper#(if(X1, X2, X3)) -> proper#(X2),
                proper#(if(X1, X2, X3)) -> proper#(X3),
                   proper#(add(X1, X2)) -> proper#(X2),
                          proper#(s(X)) -> proper#(X),
                 proper#(first(X1, X2)) -> proper#(X2),
                  proper#(cons(X1, X2)) -> proper#(X1),
                       proper#(from(X)) -> proper#(X)}
              EDG:
               {(proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(from(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                (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#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                (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#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                (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#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(add(X1, X2)) -> proper#(X2))
                (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#(and(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
                (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#(first(X1, X2)) -> proper#(X2))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
                (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#(first(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))}
               SCCS:
                Scc:
                 {   proper#(and(X1, X2)) -> proper#(X1),
                     proper#(and(X1, X2)) -> proper#(X2),
                  proper#(if(X1, X2, X3)) -> proper#(X1),
                  proper#(if(X1, X2, X3)) -> proper#(X2),
                  proper#(if(X1, X2, X3)) -> proper#(X3),
                     proper#(add(X1, X2)) -> proper#(X2),
                            proper#(s(X)) -> proper#(X),
                   proper#(first(X1, X2)) -> proper#(X2),
                    proper#(cons(X1, X2)) -> proper#(X1),
                         proper#(from(X)) -> proper#(X)}
                SCC:
                 Strict:
                  {   proper#(and(X1, X2)) -> proper#(X1),
                      proper#(and(X1, X2)) -> proper#(X2),
                   proper#(if(X1, X2, X3)) -> proper#(X1),
                   proper#(if(X1, X2, X3)) -> proper#(X2),
                   proper#(if(X1, X2, X3)) -> proper#(X3),
                      proper#(add(X1, X2)) -> proper#(X2),
                             proper#(s(X)) -> proper#(X),
                    proper#(first(X1, X2)) -> proper#(X2),
                     proper#(cons(X1, X2)) -> proper#(X1),
                          proper#(from(X)) -> proper#(X)}
                 Weak:
                 {            active(and(X1, X2)) -> and(active(X1), X2),
                           active(and(true(), X)) -> mark(X),
                          active(and(false(), Y)) -> mark(false()),
                           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(add(X1, X2)) -> add(active(X1), X2),
                              active(add(0(), X)) -> mark(X),
                             active(add(s(X), Y)) -> mark(s(add(X, Y))),
                            active(first(X1, X2)) -> first(X1, active(X2)),
                            active(first(X1, X2)) -> first(active(X1), X2),
                            active(first(0(), X)) -> mark(nil()),
                  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                  active(from(X)) -> mark(cons(X, from(s(X)))),
                                and(mark(X1), X2) -> mark(and(X1, X2)),
                              and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                             if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                       if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                add(mark(X1), X2) -> mark(add(X1, X2)),
                              add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                         s(ok(X)) -> ok(s(X)),
                              first(X1, mark(X2)) -> mark(first(X1, X2)),
                              first(mark(X1), X2) -> mark(first(X1, X2)),
                            first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                             cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                      from(ok(X)) -> ok(from(X)),
                              proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                   proper(true()) -> ok(true()),
                                  proper(false()) -> ok(false()),
                           proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                              proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                      proper(0()) -> ok(0()),
                                     proper(s(X)) -> s(proper(X)),
                                    proper(nil()) -> ok(nil()),
                            proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                  proper(from(X)) -> from(proper(X)),
                                     top(mark(X)) -> top(proper(X)),
                                       top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {   proper#(and(X1, X2)) -> proper#(X1),
                       proper#(and(X1, X2)) -> proper#(X2),
                    proper#(if(X1, X2, X3)) -> proper#(X1),
                    proper#(if(X1, X2, X3)) -> proper#(X2),
                    proper#(if(X1, X2, X3)) -> proper#(X3),
                              proper#(s(X)) -> proper#(X),
                     proper#(first(X1, X2)) -> proper#(X2),
                      proper#(cons(X1, X2)) -> proper#(X1),
                           proper#(from(X)) -> proper#(X)}
                  EDG:
                   {(proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (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#(X2), proper#(and(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
                    (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X2))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X2))
                    (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> 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)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(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#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X2))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(and(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))}
                   SCCS:
                    Scc:
                     {   proper#(and(X1, X2)) -> proper#(X1),
                         proper#(and(X1, X2)) -> proper#(X2),
                      proper#(if(X1, X2, X3)) -> proper#(X1),
                      proper#(if(X1, X2, X3)) -> proper#(X2),
                      proper#(if(X1, X2, X3)) -> proper#(X3),
                                proper#(s(X)) -> proper#(X),
                       proper#(first(X1, X2)) -> proper#(X2),
                        proper#(cons(X1, X2)) -> proper#(X1),
                             proper#(from(X)) -> proper#(X)}
                    SCC:
                     Strict:
                      {   proper#(and(X1, X2)) -> proper#(X1),
                          proper#(and(X1, X2)) -> proper#(X2),
                       proper#(if(X1, X2, X3)) -> proper#(X1),
                       proper#(if(X1, X2, X3)) -> proper#(X2),
                       proper#(if(X1, X2, X3)) -> proper#(X3),
                                 proper#(s(X)) -> proper#(X),
                        proper#(first(X1, X2)) -> proper#(X2),
                         proper#(cons(X1, X2)) -> proper#(X1),
                              proper#(from(X)) -> proper#(X)}
                     Weak:
                     {            active(and(X1, X2)) -> and(active(X1), X2),
                               active(and(true(), X)) -> mark(X),
                              active(and(false(), Y)) -> mark(false()),
                               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(add(X1, X2)) -> add(active(X1), X2),
                                  active(add(0(), X)) -> mark(X),
                                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                active(first(X1, X2)) -> first(X1, active(X2)),
                                active(first(X1, X2)) -> first(active(X1), X2),
                                active(first(0(), X)) -> mark(nil()),
                      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                      active(from(X)) -> mark(cons(X, from(s(X)))),
                                    and(mark(X1), X2) -> mark(and(X1, X2)),
                                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                    add(mark(X1), X2) -> mark(add(X1, X2)),
                                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                             s(ok(X)) -> ok(s(X)),
                                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                                  first(mark(X1), X2) -> mark(first(X1, X2)),
                                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                          from(ok(X)) -> ok(from(X)),
                                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                       proper(true()) -> ok(true()),
                                      proper(false()) -> ok(false()),
                               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                          proper(0()) -> ok(0()),
                                         proper(s(X)) -> s(proper(X)),
                                        proper(nil()) -> ok(nil()),
                                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                      proper(from(X)) -> from(proper(X)),
                                         top(mark(X)) -> top(proper(X)),
                                           top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(proper#) = 0
                      Strict:
                       {   proper#(and(X1, X2)) -> proper#(X1),
                        proper#(if(X1, X2, X3)) -> proper#(X1),
                        proper#(if(X1, X2, X3)) -> proper#(X2),
                        proper#(if(X1, X2, X3)) -> proper#(X3),
                                  proper#(s(X)) -> proper#(X),
                         proper#(first(X1, X2)) -> proper#(X2),
                          proper#(cons(X1, X2)) -> proper#(X1),
                               proper#(from(X)) -> proper#(X)}
                      EDG:
                       {(proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                        (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#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> 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#(and(X1, X2)) -> proper#(X1))
                        (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                        (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                        (proper#(s(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                        (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#(if(X1, X2, X3)) -> proper#(X3))
                        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> 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#(if(X1, X2, X3)) -> proper#(X3))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))}
                       SCCS:
                        Scc:
                         {   proper#(and(X1, X2)) -> proper#(X1),
                          proper#(if(X1, X2, X3)) -> proper#(X1),
                          proper#(if(X1, X2, X3)) -> proper#(X2),
                          proper#(if(X1, X2, X3)) -> proper#(X3),
                                    proper#(s(X)) -> proper#(X),
                           proper#(first(X1, X2)) -> proper#(X2),
                            proper#(cons(X1, X2)) -> proper#(X1),
                                 proper#(from(X)) -> proper#(X)}
                        SCC:
                         Strict:
                          {   proper#(and(X1, X2)) -> proper#(X1),
                           proper#(if(X1, X2, X3)) -> proper#(X1),
                           proper#(if(X1, X2, X3)) -> proper#(X2),
                           proper#(if(X1, X2, X3)) -> proper#(X3),
                                     proper#(s(X)) -> proper#(X),
                            proper#(first(X1, X2)) -> proper#(X2),
                             proper#(cons(X1, X2)) -> proper#(X1),
                                  proper#(from(X)) -> proper#(X)}
                         Weak:
                         {            active(and(X1, X2)) -> and(active(X1), X2),
                                   active(and(true(), X)) -> mark(X),
                                  active(and(false(), Y)) -> mark(false()),
                                   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(add(X1, X2)) -> add(active(X1), X2),
                                      active(add(0(), X)) -> mark(X),
                                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                    active(first(X1, X2)) -> first(X1, active(X2)),
                                    active(first(X1, X2)) -> first(active(X1), X2),
                                    active(first(0(), X)) -> mark(nil()),
                          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                          active(from(X)) -> mark(cons(X, from(s(X)))),
                                        and(mark(X1), X2) -> mark(and(X1, X2)),
                                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                        add(mark(X1), X2) -> mark(add(X1, X2)),
                                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                 s(ok(X)) -> ok(s(X)),
                                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                                      first(mark(X1), X2) -> mark(first(X1, X2)),
                                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                              from(ok(X)) -> ok(from(X)),
                                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                           proper(true()) -> ok(true()),
                                          proper(false()) -> ok(false()),
                                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                              proper(0()) -> ok(0()),
                                             proper(s(X)) -> s(proper(X)),
                                            proper(nil()) -> ok(nil()),
                                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                          proper(from(X)) -> from(proper(X)),
                                             top(mark(X)) -> top(proper(X)),
                                               top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(proper#) = 0
                          Strict:
                           {   proper#(and(X1, X2)) -> proper#(X1),
                            proper#(if(X1, X2, X3)) -> proper#(X1),
                            proper#(if(X1, X2, X3)) -> proper#(X2),
                            proper#(if(X1, X2, X3)) -> proper#(X3),
                                      proper#(s(X)) -> proper#(X),
                             proper#(first(X1, X2)) -> proper#(X2),
                                   proper#(from(X)) -> proper#(X)}
                          EDG:
                           {(proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                            (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#(X2), proper#(and(X1, X2)) -> proper#(X1))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                            (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                            (proper#(s(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> 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#(and(X1, X2)) -> proper#(X1))
                            (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                            (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                            (proper#(from(X)) -> proper#(X), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> 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#(if(X1, X2, X3)) -> proper#(X3))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(and(X1, X2)) -> proper#(X1))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(first(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
                            (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)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
                            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X))
                            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(first(X1, X2)) -> proper#(X2))
                            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))}
                           SCCS:
                            Scc:
                             {   proper#(and(X1, X2)) -> proper#(X1),
                              proper#(if(X1, X2, X3)) -> proper#(X1),
                              proper#(if(X1, X2, X3)) -> proper#(X2),
                              proper#(if(X1, X2, X3)) -> proper#(X3),
                                        proper#(s(X)) -> proper#(X),
                               proper#(first(X1, X2)) -> proper#(X2),
                                     proper#(from(X)) -> proper#(X)}
                            SCC:
                             Strict:
                              {   proper#(and(X1, X2)) -> proper#(X1),
                               proper#(if(X1, X2, X3)) -> proper#(X1),
                               proper#(if(X1, X2, X3)) -> proper#(X2),
                               proper#(if(X1, X2, X3)) -> proper#(X3),
                                         proper#(s(X)) -> proper#(X),
                                proper#(first(X1, X2)) -> proper#(X2),
                                      proper#(from(X)) -> proper#(X)}
                             Weak:
                             {            active(and(X1, X2)) -> and(active(X1), X2),
                                       active(and(true(), X)) -> mark(X),
                                      active(and(false(), Y)) -> mark(false()),
                                       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(add(X1, X2)) -> add(active(X1), X2),
                                          active(add(0(), X)) -> mark(X),
                                         active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                        active(first(X1, X2)) -> first(X1, active(X2)),
                                        active(first(X1, X2)) -> first(active(X1), X2),
                                        active(first(0(), X)) -> mark(nil()),
                              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                              active(from(X)) -> mark(cons(X, from(s(X)))),
                                            and(mark(X1), X2) -> mark(and(X1, X2)),
                                          and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                         if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                            add(mark(X1), X2) -> mark(add(X1, X2)),
                                          add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                     s(ok(X)) -> ok(s(X)),
                                          first(X1, mark(X2)) -> mark(first(X1, X2)),
                                          first(mark(X1), X2) -> mark(first(X1, X2)),
                                        first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                         cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                  from(ok(X)) -> ok(from(X)),
                                          proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                               proper(true()) -> ok(true()),
                                              proper(false()) -> ok(false()),
                                       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                          proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                  proper(0()) -> ok(0()),
                                                 proper(s(X)) -> s(proper(X)),
                                                proper(nil()) -> ok(nil()),
                                        proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                              proper(from(X)) -> from(proper(X)),
                                                 top(mark(X)) -> top(proper(X)),
                                                   top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(proper#) = 0
                              Strict:
                               {   proper#(and(X1, X2)) -> proper#(X1),
                                proper#(if(X1, X2, X3)) -> proper#(X1),
                                proper#(if(X1, X2, X3)) -> proper#(X2),
                                proper#(if(X1, X2, X3)) -> proper#(X3),
                                          proper#(s(X)) -> proper#(X),
                                       proper#(from(X)) -> proper#(X)}
                              EDG:
                               {(proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                                (proper#(s(X)) -> proper#(X), proper#(s(X)) -> 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#(and(X1, X2)) -> proper#(X1))
                                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> 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#(and(X1, X2)) -> proper#(X1))
                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                                (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#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                                (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                                (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                                (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                                (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                                (proper#(and(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                                (proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                                (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                                (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                                (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(and(X1, X2)) -> 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#(if(X1, X2, X3)) -> proper#(X3))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                                (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))}
                               SCCS:
                                Scc:
                                 {   proper#(and(X1, X2)) -> proper#(X1),
                                  proper#(if(X1, X2, X3)) -> proper#(X1),
                                  proper#(if(X1, X2, X3)) -> proper#(X2),
                                  proper#(if(X1, X2, X3)) -> proper#(X3),
                                            proper#(s(X)) -> proper#(X),
                                         proper#(from(X)) -> proper#(X)}
                                SCC:
                                 Strict:
                                  {   proper#(and(X1, X2)) -> proper#(X1),
                                   proper#(if(X1, X2, X3)) -> proper#(X1),
                                   proper#(if(X1, X2, X3)) -> proper#(X2),
                                   proper#(if(X1, X2, X3)) -> proper#(X3),
                                             proper#(s(X)) -> proper#(X),
                                          proper#(from(X)) -> proper#(X)}
                                 Weak:
                                 {            active(and(X1, X2)) -> and(active(X1), X2),
                                           active(and(true(), X)) -> mark(X),
                                          active(and(false(), Y)) -> mark(false()),
                                           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(add(X1, X2)) -> add(active(X1), X2),
                                              active(add(0(), X)) -> mark(X),
                                             active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                            active(first(X1, X2)) -> first(X1, active(X2)),
                                            active(first(X1, X2)) -> first(active(X1), X2),
                                            active(first(0(), X)) -> mark(nil()),
                                  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                                  active(from(X)) -> mark(cons(X, from(s(X)))),
                                                and(mark(X1), X2) -> mark(and(X1, X2)),
                                              and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                             if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                       if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                add(mark(X1), X2) -> mark(add(X1, X2)),
                                              add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                         s(ok(X)) -> ok(s(X)),
                                              first(X1, mark(X2)) -> mark(first(X1, X2)),
                                              first(mark(X1), X2) -> mark(first(X1, X2)),
                                            first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                             cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                      from(ok(X)) -> ok(from(X)),
                                              proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                                   proper(true()) -> ok(true()),
                                                  proper(false()) -> ok(false()),
                                           proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                              proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                      proper(0()) -> ok(0()),
                                                     proper(s(X)) -> s(proper(X)),
                                                    proper(nil()) -> ok(nil()),
                                            proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                  proper(from(X)) -> from(proper(X)),
                                                     top(mark(X)) -> top(proper(X)),
                                                       top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(proper#) = 0
                                  Strict:
                                   {   proper#(and(X1, X2)) -> proper#(X1),
                                    proper#(if(X1, X2, X3)) -> proper#(X1),
                                    proper#(if(X1, X2, X3)) -> proper#(X2),
                                    proper#(if(X1, X2, X3)) -> proper#(X3),
                                           proper#(from(X)) -> proper#(X)}
                                  EDG:
                                   {(proper#(and(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                                    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                                    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
                                    (proper#(and(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                                    (proper#(and(X1, X2)) -> proper#(X1), proper#(and(X1, X2)) -> proper#(X1))
                                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                                    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
                                    (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#(X2), proper#(and(X1, X2)) -> proper#(X1))
                                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(and(X1, X2)) -> proper#(X1))
                                    (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)) -> proper#(X2))
                                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
                                    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> proper#(X))
                                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(and(X1, X2)) -> 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#(if(X1, X2, X3)) -> proper#(X3))
                                    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                                    (proper#(from(X)) -> proper#(X), proper#(and(X1, X2)) -> proper#(X1))
                                    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                                    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                                    (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                                    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))}
                                   SCCS:
                                    Scc:
                                     {   proper#(and(X1, X2)) -> proper#(X1),
                                      proper#(if(X1, X2, X3)) -> proper#(X1),
                                      proper#(if(X1, X2, X3)) -> proper#(X2),
                                      proper#(if(X1, X2, X3)) -> proper#(X3),
                                             proper#(from(X)) -> proper#(X)}
                                    SCC:
                                     Strict:
                                      {   proper#(and(X1, X2)) -> proper#(X1),
                                       proper#(if(X1, X2, X3)) -> proper#(X1),
                                       proper#(if(X1, X2, X3)) -> proper#(X2),
                                       proper#(if(X1, X2, X3)) -> proper#(X3),
                                              proper#(from(X)) -> proper#(X)}
                                     Weak:
                                     {            active(and(X1, X2)) -> and(active(X1), X2),
                                               active(and(true(), X)) -> mark(X),
                                              active(and(false(), Y)) -> mark(false()),
                                               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(add(X1, X2)) -> add(active(X1), X2),
                                                  active(add(0(), X)) -> mark(X),
                                                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                active(first(X1, X2)) -> first(X1, active(X2)),
                                                active(first(X1, X2)) -> first(active(X1), X2),
                                                active(first(0(), X)) -> mark(nil()),
                                      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                                      active(from(X)) -> mark(cons(X, from(s(X)))),
                                                    and(mark(X1), X2) -> mark(and(X1, X2)),
                                                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                    add(mark(X1), X2) -> mark(add(X1, X2)),
                                                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                             s(ok(X)) -> ok(s(X)),
                                                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                                                  first(mark(X1), X2) -> mark(first(X1, X2)),
                                                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                          from(ok(X)) -> ok(from(X)),
                                                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                                       proper(true()) -> ok(true()),
                                                      proper(false()) -> ok(false()),
                                               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                          proper(0()) -> ok(0()),
                                                         proper(s(X)) -> s(proper(X)),
                                                        proper(nil()) -> ok(nil()),
                                                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                      proper(from(X)) -> from(proper(X)),
                                                         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#(if(X1, X2, X3)) -> proper#(X3),
                                               proper#(from(X)) -> proper#(X)}
                                      EDG:
                                       {(proper#(if(X1, X2, X3)) -> proper#(X3), proper#(from(X)) -> 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#(X1), proper#(from(X)) -> proper#(X))
                                        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
                                        (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#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                                        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                                        (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
                                        (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                                        (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#(from(X)) -> proper#(X))}
                                       SCCS:
                                        Scc:
                                         {proper#(if(X1, X2, X3)) -> proper#(X1),
                                          proper#(if(X1, X2, X3)) -> proper#(X2),
                                          proper#(if(X1, X2, X3)) -> proper#(X3),
                                                 proper#(from(X)) -> proper#(X)}
                                        SCC:
                                         Strict:
                                          {proper#(if(X1, X2, X3)) -> proper#(X1),
                                           proper#(if(X1, X2, X3)) -> proper#(X2),
                                           proper#(if(X1, X2, X3)) -> proper#(X3),
                                                  proper#(from(X)) -> proper#(X)}
                                         Weak:
                                         {            active(and(X1, X2)) -> and(active(X1), X2),
                                                   active(and(true(), X)) -> mark(X),
                                                  active(and(false(), Y)) -> mark(false()),
                                                   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(add(X1, X2)) -> add(active(X1), X2),
                                                      active(add(0(), X)) -> mark(X),
                                                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                    active(first(X1, X2)) -> first(X1, active(X2)),
                                                    active(first(X1, X2)) -> first(active(X1), X2),
                                                    active(first(0(), X)) -> mark(nil()),
                                          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                                          active(from(X)) -> mark(cons(X, from(s(X)))),
                                                        and(mark(X1), X2) -> mark(and(X1, X2)),
                                                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                        add(mark(X1), X2) -> mark(add(X1, X2)),
                                                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                                 s(ok(X)) -> ok(s(X)),
                                                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                                                      first(mark(X1), X2) -> mark(first(X1, X2)),
                                                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                              from(ok(X)) -> ok(from(X)),
                                                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                                           proper(true()) -> ok(true()),
                                                          proper(false()) -> ok(false()),
                                                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                              proper(0()) -> ok(0()),
                                                             proper(s(X)) -> s(proper(X)),
                                                            proper(nil()) -> ok(nil()),
                                                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                          proper(from(X)) -> from(proper(X)),
                                                             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#(from(X)) -> proper#(X)}
                                          EDG:
                                           {(proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(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#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                                            (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
                                            (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                                            (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#(from(X)) -> proper#(X))}
                                           SCCS:
                                            Scc:
                                             {proper#(if(X1, X2, X3)) -> proper#(X1),
                                              proper#(if(X1, X2, X3)) -> proper#(X2),
                                                     proper#(from(X)) -> proper#(X)}
                                            SCC:
                                             Strict:
                                              {proper#(if(X1, X2, X3)) -> proper#(X1),
                                               proper#(if(X1, X2, X3)) -> proper#(X2),
                                                      proper#(from(X)) -> proper#(X)}
                                             Weak:
                                             {            active(and(X1, X2)) -> and(active(X1), X2),
                                                       active(and(true(), X)) -> mark(X),
                                                      active(and(false(), Y)) -> mark(false()),
                                                       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(add(X1, X2)) -> add(active(X1), X2),
                                                          active(add(0(), X)) -> mark(X),
                                                         active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                        active(first(X1, X2)) -> first(X1, active(X2)),
                                                        active(first(X1, X2)) -> first(active(X1), X2),
                                                        active(first(0(), X)) -> mark(nil()),
                                              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                                              active(from(X)) -> mark(cons(X, from(s(X)))),
                                                            and(mark(X1), X2) -> mark(and(X1, X2)),
                                                          and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                                         if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                                   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                            add(mark(X1), X2) -> mark(add(X1, X2)),
                                                          add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                                     s(ok(X)) -> ok(s(X)),
                                                          first(X1, mark(X2)) -> mark(first(X1, X2)),
                                                          first(mark(X1), X2) -> mark(first(X1, X2)),
                                                        first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                                         cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                                  from(ok(X)) -> ok(from(X)),
                                                          proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                                               proper(true()) -> ok(true()),
                                                              proper(false()) -> ok(false()),
                                                       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                          proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                                  proper(0()) -> ok(0()),
                                                                 proper(s(X)) -> s(proper(X)),
                                                                proper(nil()) -> ok(nil()),
                                                        proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                              proper(from(X)) -> from(proper(X)),
                                                                 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#(from(X)) -> proper#(X)}
                                              EDG:
                                               {(proper#(if(X1, X2, X3)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                                                (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
                                                (proper#(from(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
                                                (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))}
                                               SCCS:
                                                Scc:
                                                 {proper#(if(X1, X2, X3)) -> proper#(X1),
                                                         proper#(from(X)) -> proper#(X)}
                                                SCC:
                                                 Strict:
                                                  {proper#(if(X1, X2, X3)) -> proper#(X1),
                                                          proper#(from(X)) -> proper#(X)}
                                                 Weak:
                                                 {            active(and(X1, X2)) -> and(active(X1), X2),
                                                           active(and(true(), X)) -> mark(X),
                                                          active(and(false(), Y)) -> mark(false()),
                                                           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(add(X1, X2)) -> add(active(X1), X2),
                                                              active(add(0(), X)) -> mark(X),
                                                             active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                            active(first(X1, X2)) -> first(X1, active(X2)),
                                                            active(first(X1, X2)) -> first(active(X1), X2),
                                                            active(first(0(), X)) -> mark(nil()),
                                                  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                                                  active(from(X)) -> mark(cons(X, from(s(X)))),
                                                                and(mark(X1), X2) -> mark(and(X1, X2)),
                                                              and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                                             if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                                       if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                                add(mark(X1), X2) -> mark(add(X1, X2)),
                                                              add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                                         s(ok(X)) -> ok(s(X)),
                                                              first(X1, mark(X2)) -> mark(first(X1, X2)),
                                                              first(mark(X1), X2) -> mark(first(X1, X2)),
                                                            first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                                             cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                                      from(ok(X)) -> ok(from(X)),
                                                              proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                                                   proper(true()) -> ok(true()),
                                                                  proper(false()) -> ok(false()),
                                                           proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                              proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                                      proper(0()) -> ok(0()),
                                                                     proper(s(X)) -> s(proper(X)),
                                                                    proper(nil()) -> ok(nil()),
                                                            proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                                  proper(from(X)) -> from(proper(X)),
                                                                     top(mark(X)) -> top(proper(X)),
                                                                       top(ok(X)) -> top(active(X))}
                                                 SPSC:
                                                  Simple Projection:
                                                   pi(proper#) = 0
                                                  Strict:
                                                   {proper#(from(X)) -> proper#(X)}
                                                  EDG:
                                                   {(proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))}
                                                   SCCS:
                                                    Scc:
                                                     {proper#(from(X)) -> proper#(X)}
                                                    SCC:
                                                     Strict:
                                                      {proper#(from(X)) -> proper#(X)}
                                                     Weak:
                                                     {            active(and(X1, X2)) -> and(active(X1), X2),
                                                               active(and(true(), X)) -> mark(X),
                                                              active(and(false(), Y)) -> mark(false()),
                                                               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(add(X1, X2)) -> add(active(X1), X2),
                                                                  active(add(0(), X)) -> mark(X),
                                                                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                                active(first(X1, X2)) -> first(X1, active(X2)),
                                                                active(first(X1, X2)) -> first(active(X1), X2),
                                                                active(first(0(), X)) -> mark(nil()),
                                                      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                                                      active(from(X)) -> mark(cons(X, from(s(X)))),
                                                                    and(mark(X1), X2) -> mark(and(X1, X2)),
                                                                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                                                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                                                           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                                                    add(mark(X1), X2) -> mark(add(X1, X2)),
                                                                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                                             s(ok(X)) -> ok(s(X)),
                                                                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                                                                  first(mark(X1), X2) -> mark(first(X1, X2)),
                                                                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                                                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                                          from(ok(X)) -> ok(from(X)),
                                                                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                                                       proper(true()) -> ok(true()),
                                                                      proper(false()) -> ok(false()),
                                                               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                                                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                                          proper(0()) -> ok(0()),
                                                                         proper(s(X)) -> s(proper(X)),
                                                                        proper(nil()) -> ok(nil()),
                                                                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                                      proper(from(X)) -> from(proper(X)),
                                                                         top(mark(X)) -> top(proper(X)),
                                                                           top(ok(X)) -> top(active(X))}
                                                     SPSC:
                                                      Simple Projection:
                                                       pi(proper#) = 0
                                                      Strict:
                                                       {}
                                                      Qed
    SCC:
     Strict:
      {from#(ok(X)) -> from#(X)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(from#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(cons#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {  first#(X1, mark(X2)) -> first#(X1, X2),
         first#(mark(X1), X2) -> first#(X1, X2),
       first#(ok(X1), ok(X2)) -> first#(X1, X2)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(first#) = 0
      Strict:
       {first#(X1, mark(X2)) -> first#(X1, X2),
        first#(mark(X1), X2) -> first#(X1, X2)}
      EDG:
       {(first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
        (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
        (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
        (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))}
       SCCS:
        Scc:
         {first#(X1, mark(X2)) -> first#(X1, X2),
          first#(mark(X1), X2) -> first#(X1, X2)}
        SCC:
         Strict:
          {first#(X1, mark(X2)) -> first#(X1, X2),
           first#(mark(X1), X2) -> first#(X1, X2)}
         Weak:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(first#) = 0
          Strict:
           {first#(X1, mark(X2)) -> first#(X1, X2)}
          EDG:
           {(first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))}
           SCCS:
            Scc:
             {first#(X1, mark(X2)) -> first#(X1, X2)}
            SCC:
             Strict:
              {first#(X1, mark(X2)) -> first#(X1, X2)}
             Weak:
             {            active(and(X1, X2)) -> and(active(X1), X2),
                       active(and(true(), X)) -> mark(X),
                      active(and(false(), Y)) -> mark(false()),
                       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(add(X1, X2)) -> add(active(X1), X2),
                          active(add(0(), X)) -> mark(X),
                         active(add(s(X), Y)) -> mark(s(add(X, Y))),
                        active(first(X1, X2)) -> first(X1, active(X2)),
                        active(first(X1, X2)) -> first(active(X1), X2),
                        active(first(0(), X)) -> mark(nil()),
              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                              active(from(X)) -> mark(cons(X, from(s(X)))),
                            and(mark(X1), X2) -> mark(and(X1, X2)),
                          and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                         if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                            add(mark(X1), X2) -> mark(add(X1, X2)),
                          add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                     s(ok(X)) -> ok(s(X)),
                          first(X1, mark(X2)) -> mark(first(X1, X2)),
                          first(mark(X1), X2) -> mark(first(X1, X2)),
                        first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                         cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                  from(ok(X)) -> ok(from(X)),
                          proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                               proper(true()) -> ok(true()),
                              proper(false()) -> ok(false()),
                       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                          proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                                 proper(s(X)) -> s(proper(X)),
                                proper(nil()) -> ok(nil()),
                        proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(first#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {s#(ok(X)) -> s#(X)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {  add#(mark(X1), X2) -> add#(X1, X2),
       add#(ok(X1), ok(X2)) -> add#(X1, X2)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {add#(mark(X1), X2) -> add#(X1, X2)}
      EDG:
       {(add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))}
       SCCS:
        Scc:
         {add#(mark(X1), X2) -> add#(X1, X2)}
        SCC:
         Strict:
          {add#(mark(X1), X2) -> add#(X1, X2)}
         Weak:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(add#) = 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:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         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:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(if#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  and#(mark(X1), X2) -> and#(X1, X2),
       and#(ok(X1), ok(X2)) -> and#(X1, X2)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(and#) = 0
      Strict:
       {and#(mark(X1), X2) -> and#(X1, X2)}
      EDG:
       {(and#(mark(X1), X2) -> and#(X1, X2), and#(mark(X1), X2) -> and#(X1, X2))}
       SCCS:
        Scc:
         {and#(mark(X1), X2) -> and#(X1, X2)}
        SCC:
         Strict:
          {and#(mark(X1), X2) -> and#(X1, X2)}
         Weak:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(and#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {   active#(and(X1, X2)) -> active#(X1),
       active#(if(X1, X2, X3)) -> active#(X1),
          active#(add(X1, X2)) -> active#(X1),
        active#(first(X1, X2)) -> active#(X1),
        active#(first(X1, X2)) -> active#(X2)}
     Weak:
     {            active(and(X1, X2)) -> and(active(X1), X2),
               active(and(true(), X)) -> mark(X),
              active(and(false(), Y)) -> mark(false()),
               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(add(X1, X2)) -> add(active(X1), X2),
                  active(add(0(), X)) -> mark(X),
                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(first(X1, X2)) -> first(X1, active(X2)),
                active(first(X1, X2)) -> first(active(X1), X2),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                    and(mark(X1), X2) -> mark(and(X1, X2)),
                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                    add(mark(X1), X2) -> mark(add(X1, X2)),
                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             s(ok(X)) -> ok(s(X)),
                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                  first(mark(X1), X2) -> mark(first(X1, X2)),
                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          from(ok(X)) -> ok(from(X)),
                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                       proper(true()) -> ok(true()),
                      proper(false()) -> ok(false()),
               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                         proper(s(X)) -> s(proper(X)),
                        proper(nil()) -> ok(nil()),
                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {   active#(and(X1, X2)) -> active#(X1),
        active#(if(X1, X2, X3)) -> active#(X1),
           active#(add(X1, X2)) -> active#(X1),
         active#(first(X1, X2)) -> active#(X2)}
      EDG:
       {(active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
        (active#(and(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(and(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X1), 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#(and(X1, X2)) -> active#(X1))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(and(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#(add(X1, X2)) -> active#(X1))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
        (active#(first(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1))
        (active#(first(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(first(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
        (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2))}
       SCCS:
        Scc:
         {   active#(and(X1, X2)) -> active#(X1),
          active#(if(X1, X2, X3)) -> active#(X1),
             active#(add(X1, X2)) -> active#(X1),
           active#(first(X1, X2)) -> active#(X2)}
        SCC:
         Strict:
          {   active#(and(X1, X2)) -> active#(X1),
           active#(if(X1, X2, X3)) -> active#(X1),
              active#(add(X1, X2)) -> active#(X1),
            active#(first(X1, X2)) -> active#(X2)}
         Weak:
         {            active(and(X1, X2)) -> and(active(X1), X2),
                   active(and(true(), X)) -> mark(X),
                  active(and(false(), Y)) -> mark(false()),
                   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(add(X1, X2)) -> add(active(X1), X2),
                      active(add(0(), X)) -> mark(X),
                     active(add(s(X), Y)) -> mark(s(add(X, Y))),
                    active(first(X1, X2)) -> first(X1, active(X2)),
                    active(first(X1, X2)) -> first(active(X1), X2),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                        and(mark(X1), X2) -> mark(and(X1, X2)),
                      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                     if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
               if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                        add(mark(X1), X2) -> mark(add(X1, X2)),
                      add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 s(ok(X)) -> ok(s(X)),
                      first(X1, mark(X2)) -> mark(first(X1, X2)),
                      first(mark(X1), X2) -> mark(first(X1, X2)),
                    first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                     cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              from(ok(X)) -> ok(from(X)),
                      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                           proper(true()) -> ok(true()),
                          proper(false()) -> ok(false()),
                   proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                      proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                             proper(s(X)) -> s(proper(X)),
                            proper(nil()) -> ok(nil()),
                    proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           {   active#(and(X1, X2)) -> active#(X1),
            active#(if(X1, X2, X3)) -> active#(X1),
             active#(first(X1, X2)) -> active#(X2)}
          EDG:
           {(active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
            (active#(and(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
            (active#(if(X1, X2, X3)) -> active#(X1), active#(and(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#(first(X1, X2)) -> active#(X2))
            (active#(first(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1))
            (active#(first(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
            (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2))}
           SCCS:
            Scc:
             {   active#(and(X1, X2)) -> active#(X1),
              active#(if(X1, X2, X3)) -> active#(X1),
               active#(first(X1, X2)) -> active#(X2)}
            SCC:
             Strict:
              {   active#(and(X1, X2)) -> active#(X1),
               active#(if(X1, X2, X3)) -> active#(X1),
                active#(first(X1, X2)) -> active#(X2)}
             Weak:
             {            active(and(X1, X2)) -> and(active(X1), X2),
                       active(and(true(), X)) -> mark(X),
                      active(and(false(), Y)) -> mark(false()),
                       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(add(X1, X2)) -> add(active(X1), X2),
                          active(add(0(), X)) -> mark(X),
                         active(add(s(X), Y)) -> mark(s(add(X, Y))),
                        active(first(X1, X2)) -> first(X1, active(X2)),
                        active(first(X1, X2)) -> first(active(X1), X2),
                        active(first(0(), X)) -> mark(nil()),
              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                              active(from(X)) -> mark(cons(X, from(s(X)))),
                            and(mark(X1), X2) -> mark(and(X1, X2)),
                          and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                         if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                            add(mark(X1), X2) -> mark(add(X1, X2)),
                          add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                     s(ok(X)) -> ok(s(X)),
                          first(X1, mark(X2)) -> mark(first(X1, X2)),
                          first(mark(X1), X2) -> mark(first(X1, X2)),
                        first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                         cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                  from(ok(X)) -> ok(from(X)),
                          proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                               proper(true()) -> ok(true()),
                              proper(false()) -> ok(false()),
                       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                          proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                                 proper(s(X)) -> s(proper(X)),
                                proper(nil()) -> ok(nil()),
                        proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               {  active#(and(X1, X2)) -> active#(X1),
                active#(first(X1, X2)) -> active#(X2)}
              EDG:
               {(active#(and(X1, X2)) -> active#(X1), active#(first(X1, X2)) -> active#(X2))
                (active#(and(X1, X2)) -> active#(X1), active#(and(X1, X2)) -> active#(X1))
                (active#(first(X1, X2)) -> active#(X2), active#(and(X1, X2)) -> active#(X1))
                (active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2))}
               SCCS:
                Scc:
                 {  active#(and(X1, X2)) -> active#(X1),
                  active#(first(X1, X2)) -> active#(X2)}
                SCC:
                 Strict:
                  {  active#(and(X1, X2)) -> active#(X1),
                   active#(first(X1, X2)) -> active#(X2)}
                 Weak:
                 {            active(and(X1, X2)) -> and(active(X1), X2),
                           active(and(true(), X)) -> mark(X),
                          active(and(false(), Y)) -> mark(false()),
                           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(add(X1, X2)) -> add(active(X1), X2),
                              active(add(0(), X)) -> mark(X),
                             active(add(s(X), Y)) -> mark(s(add(X, Y))),
                            active(first(X1, X2)) -> first(X1, active(X2)),
                            active(first(X1, X2)) -> first(active(X1), X2),
                            active(first(0(), X)) -> mark(nil()),
                  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                  active(from(X)) -> mark(cons(X, from(s(X)))),
                                and(mark(X1), X2) -> mark(and(X1, X2)),
                              and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                             if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                       if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                add(mark(X1), X2) -> mark(add(X1, X2)),
                              add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                         s(ok(X)) -> ok(s(X)),
                              first(X1, mark(X2)) -> mark(first(X1, X2)),
                              first(mark(X1), X2) -> mark(first(X1, X2)),
                            first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                             cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                      from(ok(X)) -> ok(from(X)),
                              proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                   proper(true()) -> ok(true()),
                                  proper(false()) -> ok(false()),
                           proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                              proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                      proper(0()) -> ok(0()),
                                     proper(s(X)) -> s(proper(X)),
                                    proper(nil()) -> ok(nil()),
                            proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                  proper(from(X)) -> from(proper(X)),
                                     top(mark(X)) -> top(proper(X)),
                                       top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(active#) = 0
                  Strict:
                   {active#(first(X1, X2)) -> active#(X2)}
                  EDG:
                   {(active#(first(X1, X2)) -> active#(X2), active#(first(X1, X2)) -> active#(X2))}
                   SCCS:
                    Scc:
                     {active#(first(X1, X2)) -> active#(X2)}
                    SCC:
                     Strict:
                      {active#(first(X1, X2)) -> active#(X2)}
                     Weak:
                     {            active(and(X1, X2)) -> and(active(X1), X2),
                               active(and(true(), X)) -> mark(X),
                              active(and(false(), Y)) -> mark(false()),
                               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(add(X1, X2)) -> add(active(X1), X2),
                                  active(add(0(), X)) -> mark(X),
                                 active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                active(first(X1, X2)) -> first(X1, active(X2)),
                                active(first(X1, X2)) -> first(active(X1), X2),
                                active(first(0(), X)) -> mark(nil()),
                      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                      active(from(X)) -> mark(cons(X, from(s(X)))),
                                    and(mark(X1), X2) -> mark(and(X1, X2)),
                                  and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                                 if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                           if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                    add(mark(X1), X2) -> mark(add(X1, X2)),
                                  add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                             s(ok(X)) -> ok(s(X)),
                                  first(X1, mark(X2)) -> mark(first(X1, X2)),
                                  first(mark(X1), X2) -> mark(first(X1, X2)),
                                first(ok(X1), ok(X2)) -> ok(first(X1, X2)),
                                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                          from(ok(X)) -> ok(from(X)),
                                  proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                                       proper(true()) -> ok(true()),
                                      proper(false()) -> ok(false()),
                               proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                  proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                          proper(0()) -> ok(0()),
                                         proper(s(X)) -> s(proper(X)),
                                        proper(nil()) -> ok(nil()),
                                proper(first(X1, X2)) -> first(proper(X1), proper(X2)),
                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                      proper(from(X)) -> from(proper(X)),
                                         top(mark(X)) -> top(proper(X)),
                                           top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(active#) = 0
                      Strict:
                       {}
                      Qed