MAYBE
TRS:
 {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
               sel(mark(X1), X2) -> mark(sel(X1, X2)),
             sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
              fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
              fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
            fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                      s(mark(X)) -> mark(s(X)),
                        s(ok(X)) -> ok(s(X)),
             active(sel(X1, X2)) -> sel(X1, active(X2)),
             active(sel(X1, X2)) -> sel(active(X1), X2),
  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
   active(sel(0(), cons(X, XS))) -> mark(X),
              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
            active(fib1(X1, X2)) -> fib1(X1, active(X2)),
            active(fib1(X1, X2)) -> fib1(active(X1), X2),
                    active(s(X)) -> s(active(X)),
                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                  active(fib(X)) -> fib(active(X)),
            active(cons(X1, X2)) -> cons(active(X1), X2),
             active(add(X1, X2)) -> add(X1, active(X2)),
             active(add(X1, X2)) -> add(active(X1), X2),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
                    fib(mark(X)) -> mark(fib(X)),
                      fib(ok(X)) -> ok(fib(X)),
              cons(mark(X1), X2) -> mark(cons(X1, X2)),
            cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
               add(X1, mark(X2)) -> mark(add(X1, X2)),
               add(mark(X1), X2) -> mark(add(X1, X2)),
             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
             proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
            proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                    proper(s(X)) -> s(proper(X)),
                     proper(0()) -> ok(0()),
                  proper(fib(X)) -> fib(proper(X)),
            proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {             sel#(X1, mark(X2)) -> sel#(X1, X2),
                 sel#(mark(X1), X2) -> sel#(X1, X2),
               sel#(ok(X1), ok(X2)) -> sel#(X1, X2),
                fib1#(X1, mark(X2)) -> fib1#(X1, X2),
                fib1#(mark(X1), X2) -> fib1#(X1, X2),
              fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2),
                        s#(mark(X)) -> s#(X),
                          s#(ok(X)) -> s#(X),
               active#(sel(X1, X2)) -> sel#(X1, active(X2)),
               active#(sel(X1, X2)) -> sel#(active(X1), X2),
               active#(sel(X1, X2)) -> active#(X1),
               active#(sel(X1, X2)) -> active#(X2),
    active#(sel(s(N), cons(X, XS))) -> sel#(N, XS),
                active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)),
                active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))),
                active#(fib1(X, Y)) -> add#(X, Y),
              active#(fib1(X1, X2)) -> fib1#(X1, active(X2)),
              active#(fib1(X1, X2)) -> fib1#(active(X1), X2),
              active#(fib1(X1, X2)) -> active#(X1),
              active#(fib1(X1, X2)) -> active#(X2),
                      active#(s(X)) -> s#(active(X)),
                      active#(s(X)) -> active#(X),
                    active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))),
                    active#(fib(N)) -> fib1#(s(0()), s(0())),
                    active#(fib(N)) -> s#(0()),
                    active#(fib(X)) -> active#(X),
                    active#(fib(X)) -> fib#(active(X)),
              active#(cons(X1, X2)) -> active#(X1),
              active#(cons(X1, X2)) -> cons#(active(X1), X2),
               active#(add(X1, X2)) -> active#(X1),
               active#(add(X1, X2)) -> active#(X2),
               active#(add(X1, X2)) -> add#(X1, active(X2)),
               active#(add(X1, X2)) -> add#(active(X1), X2),
              active#(add(s(X), Y)) -> s#(add(X, Y)),
              active#(add(s(X), Y)) -> add#(X, Y),
                      fib#(mark(X)) -> fib#(X),
                        fib#(ok(X)) -> fib#(X),
                cons#(mark(X1), X2) -> cons#(X1, X2),
              cons#(ok(X1), ok(X2)) -> cons#(X1, X2),
                 add#(X1, mark(X2)) -> add#(X1, X2),
                 add#(mark(X1), X2) -> add#(X1, X2),
               add#(ok(X1), ok(X2)) -> add#(X1, X2),
               proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)),
               proper#(sel(X1, X2)) -> proper#(X1),
               proper#(sel(X1, X2)) -> proper#(X2),
              proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)),
              proper#(fib1(X1, X2)) -> proper#(X1),
              proper#(fib1(X1, X2)) -> proper#(X2),
                      proper#(s(X)) -> s#(proper(X)),
                      proper#(s(X)) -> proper#(X),
                    proper#(fib(X)) -> fib#(proper(X)),
                    proper#(fib(X)) -> proper#(X),
              proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)),
              proper#(cons(X1, X2)) -> proper#(X1),
              proper#(cons(X1, X2)) -> proper#(X2),
               proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)),
               proper#(add(X1, X2)) -> proper#(X1),
               proper#(add(X1, X2)) -> proper#(X2),
                      top#(mark(X)) -> proper#(X),
                      top#(mark(X)) -> top#(proper(X)),
                        top#(ok(X)) -> active#(X),
                        top#(ok(X)) -> top#(active(X))}
  Weak:
  {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                sel(mark(X1), X2) -> mark(sel(X1, X2)),
              sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
               fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
               fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
             fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                       s(mark(X)) -> mark(s(X)),
                         s(ok(X)) -> ok(s(X)),
              active(sel(X1, X2)) -> sel(X1, active(X2)),
              active(sel(X1, X2)) -> sel(active(X1), X2),
   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
    active(sel(0(), cons(X, XS))) -> mark(X),
               active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
             active(fib1(X1, X2)) -> fib1(X1, active(X2)),
             active(fib1(X1, X2)) -> fib1(active(X1), X2),
                     active(s(X)) -> s(active(X)),
                   active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                   active(fib(X)) -> fib(active(X)),
             active(cons(X1, X2)) -> cons(active(X1), X2),
              active(add(X1, X2)) -> add(X1, active(X2)),
              active(add(X1, X2)) -> add(active(X1), X2),
             active(add(s(X), Y)) -> mark(s(add(X, Y))),
              active(add(0(), X)) -> mark(X),
                     fib(mark(X)) -> mark(fib(X)),
                       fib(ok(X)) -> ok(fib(X)),
               cons(mark(X1), X2) -> mark(cons(X1, X2)),
             cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                add(X1, mark(X2)) -> mark(add(X1, X2)),
                add(mark(X1), X2) -> mark(add(X1, X2)),
              add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
              proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
             proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                     proper(s(X)) -> s(proper(X)),
                      proper(0()) -> ok(0()),
                   proper(fib(X)) -> fib(proper(X)),
             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
              proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                     top(mark(X)) -> top(proper(X)),
                       top(ok(X)) -> top(active(X))}
  EDG:
   {
    (active#(fib1(X1, X2)) -> fib1#(X1, active(X2)), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (active#(fib1(X1, X2)) -> fib1#(X1, active(X2)), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (active#(fib1(X1, X2)) -> fib1#(X1, active(X2)), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)), sel#(mark(X1), X2) -> sel#(X1, X2))
    (proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(sel(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib(X)) -> fib#(active(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib(N)) -> s#(0()))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(cons(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(cons(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib(X)) -> fib#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib(N)) -> s#(0()))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (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#(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#(fib(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib(X)) -> fib#(proper(X)))
    (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#(fib1(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(X1, mark(X2)) -> fib1#(X1, 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#(add(s(X), Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(active(X1), X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(active(X1), X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(active(X1), X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(s(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(s(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(fib(X)) -> fib#(active(X)))
    (active#(s(X)) -> active#(X), active#(fib(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(fib(N)) -> s#(0()))
    (active#(s(X)) -> active#(X), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(s(X)) -> active#(X), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(s(X)) -> active#(X), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(s(X)) -> active#(X), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(s(X)) -> active#(X), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(s(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (fib#(mark(X)) -> fib#(X), fib#(ok(X)) -> fib#(X))
    (fib#(mark(X)) -> fib#(X), fib#(mark(X)) -> fib#(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#(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#(fib(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(fib(X)) -> fib#(proper(X)))
    (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#(fib1(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (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#(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#(fib(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(fib(X)) -> fib#(proper(X)))
    (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#(fib1(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (active#(sel(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(sel(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(sel(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib(X)) -> fib#(active(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib(N)) -> s#(0()))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(sel(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(sel(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(add(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(fib(X)) -> fib#(active(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(fib(N)) -> s#(0()))
    (active#(add(X1, X2)) -> active#(X2), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(add(X1, X2)) -> active#(X2), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(add(X1, X2)) -> active#(X2), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (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#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(ok(X1), ok(X2)) -> sel#(X1, X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (sel#(ok(X1), ok(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(ok(X1), ok(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (add#(X1, mark(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(ok(X1), ok(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(ok(X)) -> s#(X))
    (active#(add(s(X), Y)) -> s#(add(X, Y)), s#(mark(X)) -> s#(X))
    (active#(fib(X)) -> fib#(active(X)), fib#(ok(X)) -> fib#(X))
    (active#(fib(X)) -> fib#(active(X)), fib#(mark(X)) -> fib#(X))
    (proper#(fib(X)) -> fib#(proper(X)), fib#(ok(X)) -> fib#(X))
    (proper#(fib(X)) -> fib#(proper(X)), fib#(mark(X)) -> fib#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (active#(s(X)) -> s#(active(X)), s#(mark(X)) -> s#(X))
    (active#(s(X)) -> s#(active(X)), s#(ok(X)) -> s#(X))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(fib1(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#(fib(X)) -> fib#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
    (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#(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#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib(N)) -> s#(0()))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
    (active#(fib1(X1, X2)) -> active#(X2), active#(fib(X)) -> fib#(active(X)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(fib1(X1, X2)) -> active#(X2), active#(add(s(X), Y)) -> add#(X, Y))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (top#(ok(X)) -> active#(X), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (top#(ok(X)) -> active#(X), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (top#(ok(X)) -> active#(X), active#(fib1(X, Y)) -> add#(X, Y))
    (top#(ok(X)) -> active#(X), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (top#(ok(X)) -> active#(X), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (top#(ok(X)) -> active#(X), active#(fib(N)) -> s#(0()))
    (top#(ok(X)) -> active#(X), active#(fib(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(fib(X)) -> fib#(active(X)))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (top#(ok(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
    (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
    (fib#(ok(X)) -> fib#(X), fib#(mark(X)) -> fib#(X))
    (fib#(ok(X)) -> fib#(X), fib#(ok(X)) -> fib#(X))
    (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (active#(fib(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(fib(X)) -> active#(X), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(fib(X)) -> active#(X), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(fib(X)) -> active#(X), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
    (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
    (active#(fib(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(fib(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(fib(X)) -> active#(X), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(fib(X)) -> active#(X), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(fib(X)) -> active#(X), active#(fib(N)) -> s#(0()))
    (active#(fib(X)) -> active#(X), active#(fib(X)) -> active#(X))
    (active#(fib(X)) -> active#(X), active#(fib(X)) -> fib#(active(X)))
    (active#(fib(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(fib(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
    (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
    (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(fib(X)) -> active#(X), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(fib(X)) -> active#(X), active#(add(s(X), Y)) -> add#(X, Y))
    (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(active(X1), X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(fib1(X1, X2)) -> fib1#(active(X1), X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (active#(fib1(X1, X2)) -> fib1#(active(X1), X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (active#(fib1(X1, X2)) -> fib1#(active(X1), X2), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(add(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib(X)) -> fib#(proper(X)))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X1))
    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(add(X1, X2)) -> active#(X1), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(add(X1, X2)) -> active#(X1), active#(fib(N)) -> s#(0()))
    (active#(add(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
    (active#(add(X1, X2)) -> active#(X1), active#(fib(X)) -> fib#(active(X)))
    (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(add(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(add(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X, Y)) -> add#(X, Y))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(X1, active(X2)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> fib1#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib(N)) -> s#(0()))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
    (active#(fib1(X1, X2)) -> active#(X1), active#(fib(X)) -> fib#(active(X)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
    (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(X1, active(X2)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> add#(active(X1), X2))
    (active#(fib1(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (active#(fib1(X1, X2)) -> active#(X1), active#(add(s(X), Y)) -> add#(X, Y))
    (active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))), sel#(mark(X1), X2) -> sel#(X1, X2))
    (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(X1, mark(X2)) -> add#(X1, X2))
    (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(mark(X1), X2) -> add#(X1, X2))
    (proper#(add(X1, X2)) -> add#(proper(X1), proper(X2)), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (proper#(fib1(X1, X2)) -> fib1#(proper(X1), proper(X2)), fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2))
    (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(X1, X2)) -> add#(X1, active(X2)), add#(ok(X1), ok(X2)) -> add#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(X1, active(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(X1, active(X2)), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(X1, active(X2)), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     { proper#(sel(X1, X2)) -> proper#(X1),
       proper#(sel(X1, X2)) -> proper#(X2),
      proper#(fib1(X1, X2)) -> proper#(X1),
      proper#(fib1(X1, X2)) -> proper#(X2),
              proper#(s(X)) -> proper#(X),
            proper#(fib(X)) -> proper#(X),
      proper#(cons(X1, X2)) -> proper#(X1),
      proper#(cons(X1, X2)) -> proper#(X2),
       proper#(add(X1, X2)) -> proper#(X1),
       proper#(add(X1, X2)) -> proper#(X2)}
    Scc:
     {  add#(X1, mark(X2)) -> add#(X1, X2),
        add#(mark(X1), X2) -> add#(X1, X2),
      add#(ok(X1), ok(X2)) -> add#(X1, X2)}
    Scc:
     {  cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
    Scc:
     {fib#(mark(X)) -> fib#(X),
        fib#(ok(X)) -> fib#(X)}
    Scc:
     { active#(sel(X1, X2)) -> active#(X1),
       active#(sel(X1, X2)) -> active#(X2),
      active#(fib1(X1, X2)) -> active#(X1),
      active#(fib1(X1, X2)) -> active#(X2),
              active#(s(X)) -> active#(X),
            active#(fib(X)) -> active#(X),
      active#(cons(X1, X2)) -> active#(X1),
       active#(add(X1, X2)) -> active#(X1),
       active#(add(X1, X2)) -> active#(X2)}
    Scc:
     {s#(mark(X)) -> s#(X),
        s#(ok(X)) -> s#(X)}
    Scc:
     {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
        fib1#(mark(X1), X2) -> fib1#(X1, X2),
      fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2)}
    Scc:
     {  sel#(X1, mark(X2)) -> sel#(X1, X2),
        sel#(mark(X1), X2) -> sel#(X1, X2),
      sel#(ok(X1), ok(X2)) -> sel#(X1, X2)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      { proper#(sel(X1, X2)) -> proper#(X1),
        proper#(sel(X1, X2)) -> proper#(X2),
       proper#(fib1(X1, X2)) -> proper#(X1),
       proper#(fib1(X1, X2)) -> proper#(X2),
               proper#(s(X)) -> proper#(X),
             proper#(fib(X)) -> proper#(X),
       proper#(cons(X1, X2)) -> proper#(X1),
       proper#(cons(X1, X2)) -> proper#(X2),
        proper#(add(X1, X2)) -> proper#(X1),
        proper#(add(X1, X2)) -> proper#(X2)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       { proper#(sel(X1, X2)) -> proper#(X1),
         proper#(sel(X1, X2)) -> proper#(X2),
        proper#(fib1(X1, X2)) -> proper#(X1),
        proper#(fib1(X1, X2)) -> proper#(X2),
                proper#(s(X)) -> proper#(X),
              proper#(fib(X)) -> proper#(X),
        proper#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
         proper#(add(X1, X2)) -> proper#(X2)}
      EDG:
       {(proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (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#(fib(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (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#(fib(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
        (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#(add(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
        (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
        (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#(add(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
       SCCS:
        Scc:
         { proper#(sel(X1, X2)) -> proper#(X1),
           proper#(sel(X1, X2)) -> proper#(X2),
          proper#(fib1(X1, X2)) -> proper#(X1),
          proper#(fib1(X1, X2)) -> proper#(X2),
                  proper#(s(X)) -> proper#(X),
                proper#(fib(X)) -> proper#(X),
          proper#(cons(X1, X2)) -> proper#(X1),
          proper#(cons(X1, X2)) -> proper#(X2),
           proper#(add(X1, X2)) -> proper#(X2)}
        SCC:
         Strict:
          { proper#(sel(X1, X2)) -> proper#(X1),
            proper#(sel(X1, X2)) -> proper#(X2),
           proper#(fib1(X1, X2)) -> proper#(X1),
           proper#(fib1(X1, X2)) -> proper#(X2),
                   proper#(s(X)) -> proper#(X),
                 proper#(fib(X)) -> proper#(X),
           proper#(cons(X1, X2)) -> proper#(X1),
           proper#(cons(X1, X2)) -> proper#(X2),
            proper#(add(X1, X2)) -> proper#(X2)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           { proper#(sel(X1, X2)) -> proper#(X1),
             proper#(sel(X1, X2)) -> proper#(X2),
            proper#(fib1(X1, X2)) -> proper#(X1),
            proper#(fib1(X1, X2)) -> proper#(X2),
                    proper#(s(X)) -> proper#(X),
                  proper#(fib(X)) -> proper#(X),
            proper#(cons(X1, X2)) -> proper#(X1),
             proper#(add(X1, X2)) -> proper#(X2)}
          EDG:
           {(proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
            (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
           SCCS:
            Scc:
             { proper#(sel(X1, X2)) -> proper#(X1),
               proper#(sel(X1, X2)) -> proper#(X2),
              proper#(fib1(X1, X2)) -> proper#(X1),
              proper#(fib1(X1, X2)) -> proper#(X2),
                      proper#(s(X)) -> proper#(X),
                    proper#(fib(X)) -> proper#(X),
              proper#(cons(X1, X2)) -> proper#(X1),
               proper#(add(X1, X2)) -> proper#(X2)}
            SCC:
             Strict:
              { proper#(sel(X1, X2)) -> proper#(X1),
                proper#(sel(X1, X2)) -> proper#(X2),
               proper#(fib1(X1, X2)) -> proper#(X1),
               proper#(fib1(X1, X2)) -> proper#(X2),
                       proper#(s(X)) -> proper#(X),
                     proper#(fib(X)) -> proper#(X),
               proper#(cons(X1, X2)) -> proper#(X1),
                proper#(add(X1, X2)) -> proper#(X2)}
             Weak:
             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                         active(sel(X1, X2)) -> sel(active(X1), X2),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                active(s(X)) -> s(active(X)),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                              active(fib(X)) -> fib(active(X)),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> mark(fib(X)),
                                  fib(ok(X)) -> ok(fib(X)),
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                              proper(fib(X)) -> fib(proper(X)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               { proper#(sel(X1, X2)) -> proper#(X1),
                proper#(fib1(X1, X2)) -> proper#(X1),
                proper#(fib1(X1, X2)) -> proper#(X2),
                        proper#(s(X)) -> proper#(X),
                      proper#(fib(X)) -> proper#(X),
                proper#(cons(X1, X2)) -> proper#(X1),
                 proper#(add(X1, X2)) -> proper#(X2)}
              EDG:
               {(proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
                (proper#(fib(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))}
               SCCS:
                Scc:
                 { proper#(sel(X1, X2)) -> proper#(X1),
                  proper#(fib1(X1, X2)) -> proper#(X1),
                  proper#(fib1(X1, X2)) -> proper#(X2),
                          proper#(s(X)) -> proper#(X),
                        proper#(fib(X)) -> proper#(X),
                  proper#(cons(X1, X2)) -> proper#(X1),
                   proper#(add(X1, X2)) -> proper#(X2)}
                SCC:
                 Strict:
                  { proper#(sel(X1, X2)) -> proper#(X1),
                   proper#(fib1(X1, X2)) -> proper#(X1),
                   proper#(fib1(X1, X2)) -> proper#(X2),
                           proper#(s(X)) -> proper#(X),
                         proper#(fib(X)) -> proper#(X),
                   proper#(cons(X1, X2)) -> proper#(X1),
                    proper#(add(X1, X2)) -> proper#(X2)}
                 Weak:
                 {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                               sel(mark(X1), X2) -> mark(sel(X1, X2)),
                             sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                              fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                              fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                            fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                      s(mark(X)) -> mark(s(X)),
                                        s(ok(X)) -> ok(s(X)),
                             active(sel(X1, X2)) -> sel(X1, active(X2)),
                             active(sel(X1, X2)) -> sel(active(X1), X2),
                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                   active(sel(0(), cons(X, XS))) -> mark(X),
                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                            active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                            active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                    active(s(X)) -> s(active(X)),
                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                  active(fib(X)) -> fib(active(X)),
                            active(cons(X1, X2)) -> cons(active(X1), X2),
                             active(add(X1, X2)) -> add(X1, active(X2)),
                             active(add(X1, X2)) -> add(active(X1), X2),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                                    fib(mark(X)) -> mark(fib(X)),
                                      fib(ok(X)) -> ok(fib(X)),
                              cons(mark(X1), X2) -> mark(cons(X1, X2)),
                            cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                               add(mark(X1), X2) -> mark(add(X1, X2)),
                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                            proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                    proper(s(X)) -> s(proper(X)),
                                     proper(0()) -> ok(0()),
                                  proper(fib(X)) -> fib(proper(X)),
                            proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                    top(mark(X)) -> top(proper(X)),
                                      top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   { proper#(sel(X1, X2)) -> proper#(X1),
                    proper#(fib1(X1, X2)) -> proper#(X1),
                    proper#(fib1(X1, X2)) -> proper#(X2),
                            proper#(s(X)) -> proper#(X),
                          proper#(fib(X)) -> proper#(X),
                     proper#(add(X1, X2)) -> proper#(X2)}
                  EDG:
                   {(proper#(fib1(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
                    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
                    (proper#(fib1(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
                    (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                    (proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
                    (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
                    (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
                    (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
                    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X1))
                    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
                    (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X1))
                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
                   SCCS:
                    Scc:
                     { proper#(sel(X1, X2)) -> proper#(X1),
                      proper#(fib1(X1, X2)) -> proper#(X1),
                      proper#(fib1(X1, X2)) -> proper#(X2),
                              proper#(s(X)) -> proper#(X),
                            proper#(fib(X)) -> proper#(X),
                       proper#(add(X1, X2)) -> proper#(X2)}
                    SCC:
                     Strict:
                      { proper#(sel(X1, X2)) -> proper#(X1),
                       proper#(fib1(X1, X2)) -> proper#(X1),
                       proper#(fib1(X1, X2)) -> proper#(X2),
                               proper#(s(X)) -> proper#(X),
                             proper#(fib(X)) -> proper#(X),
                        proper#(add(X1, X2)) -> proper#(X2)}
                     Weak:
                     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                          s(mark(X)) -> mark(s(X)),
                                            s(ok(X)) -> ok(s(X)),
                                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                                 active(sel(X1, X2)) -> sel(active(X1), X2),
                      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                       active(sel(0(), cons(X, XS))) -> mark(X),
                                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                        active(s(X)) -> s(active(X)),
                                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                      active(fib(X)) -> fib(active(X)),
                                active(cons(X1, X2)) -> cons(active(X1), X2),
                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                 active(add(X1, X2)) -> add(active(X1), X2),
                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                 active(add(0(), X)) -> mark(X),
                                        fib(mark(X)) -> mark(fib(X)),
                                          fib(ok(X)) -> ok(fib(X)),
                                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                        proper(s(X)) -> s(proper(X)),
                                         proper(0()) -> ok(0()),
                                      proper(fib(X)) -> fib(proper(X)),
                                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                        top(mark(X)) -> top(proper(X)),
                                          top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(proper#) = 0
                      Strict:
                       { proper#(sel(X1, X2)) -> proper#(X1),
                        proper#(fib1(X1, X2)) -> proper#(X2),
                                proper#(s(X)) -> proper#(X),
                              proper#(fib(X)) -> proper#(X),
                         proper#(add(X1, X2)) -> proper#(X2)}
                      EDG:
                       {(proper#(fib(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(fib(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
                        (proper#(fib(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(fib(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
                        (proper#(fib(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
                        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                        (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(fib(X)) -> proper#(X))
                        (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                        (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                        (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib(X)) -> proper#(X))
                        (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))
                        (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                        (proper#(s(X)) -> proper#(X), proper#(fib1(X1, X2)) -> proper#(X2))
                        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(fib(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(add(X1, X2)) -> proper#(X2))}
                       SCCS:
                        Scc:
                         { proper#(sel(X1, X2)) -> proper#(X1),
                          proper#(fib1(X1, X2)) -> proper#(X2),
                                  proper#(s(X)) -> proper#(X),
                                proper#(fib(X)) -> proper#(X),
                           proper#(add(X1, X2)) -> proper#(X2)}
                        SCC:
                         Strict:
                          { proper#(sel(X1, X2)) -> proper#(X1),
                           proper#(fib1(X1, X2)) -> proper#(X2),
                                   proper#(s(X)) -> proper#(X),
                                 proper#(fib(X)) -> proper#(X),
                            proper#(add(X1, X2)) -> proper#(X2)}
                         Weak:
                         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                              s(mark(X)) -> mark(s(X)),
                                                s(ok(X)) -> ok(s(X)),
                                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                                     active(sel(X1, X2)) -> sel(active(X1), X2),
                          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                           active(sel(0(), cons(X, XS))) -> mark(X),
                                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                            active(s(X)) -> s(active(X)),
                                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                          active(fib(X)) -> fib(active(X)),
                                    active(cons(X1, X2)) -> cons(active(X1), X2),
                                     active(add(X1, X2)) -> add(X1, active(X2)),
                                     active(add(X1, X2)) -> add(active(X1), X2),
                                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                     active(add(0(), X)) -> mark(X),
                                            fib(mark(X)) -> mark(fib(X)),
                                              fib(ok(X)) -> ok(fib(X)),
                                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                                       add(mark(X1), X2) -> mark(add(X1, X2)),
                                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                            proper(s(X)) -> s(proper(X)),
                                             proper(0()) -> ok(0()),
                                          proper(fib(X)) -> fib(proper(X)),
                                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                            top(mark(X)) -> top(proper(X)),
                                              top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(proper#) = 0
                          Strict:
                           { proper#(sel(X1, X2)) -> proper#(X1),
                            proper#(fib1(X1, X2)) -> proper#(X2),
                                    proper#(s(X)) -> proper#(X),
                             proper#(add(X1, X2)) -> proper#(X2)}
                          EDG:
                           {(proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                            (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                            (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#(fib1(X1, X2)) -> proper#(X2))
                            (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                            (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(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#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                            (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                            (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                            (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
                           SCCS:
                            Scc:
                             { proper#(sel(X1, X2)) -> proper#(X1),
                              proper#(fib1(X1, X2)) -> proper#(X2),
                                      proper#(s(X)) -> proper#(X),
                               proper#(add(X1, X2)) -> proper#(X2)}
                            SCC:
                             Strict:
                              { proper#(sel(X1, X2)) -> proper#(X1),
                               proper#(fib1(X1, X2)) -> proper#(X2),
                                       proper#(s(X)) -> proper#(X),
                                proper#(add(X1, X2)) -> proper#(X2)}
                             Weak:
                             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                  s(mark(X)) -> mark(s(X)),
                                                    s(ok(X)) -> ok(s(X)),
                                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                                         active(sel(X1, X2)) -> sel(active(X1), X2),
                              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                               active(sel(0(), cons(X, XS))) -> mark(X),
                                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                active(s(X)) -> s(active(X)),
                                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                              active(fib(X)) -> fib(active(X)),
                                        active(cons(X1, X2)) -> cons(active(X1), X2),
                                         active(add(X1, X2)) -> add(X1, active(X2)),
                                         active(add(X1, X2)) -> add(active(X1), X2),
                                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                         active(add(0(), X)) -> mark(X),
                                                fib(mark(X)) -> mark(fib(X)),
                                                  fib(ok(X)) -> ok(fib(X)),
                                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                                           add(mark(X1), X2) -> mark(add(X1, X2)),
                                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                proper(s(X)) -> s(proper(X)),
                                                 proper(0()) -> ok(0()),
                                              proper(fib(X)) -> fib(proper(X)),
                                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                top(mark(X)) -> top(proper(X)),
                                                  top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(proper#) = 0
                              Strict:
                               { proper#(sel(X1, X2)) -> proper#(X1),
                                proper#(fib1(X1, X2)) -> proper#(X2),
                                 proper#(add(X1, X2)) -> proper#(X2)}
                              EDG:
                               {(proper#(fib1(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                                (proper#(fib1(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(fib1(X1, X2)) -> proper#(X2))
                                (proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                                (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                                (proper#(sel(X1, X2)) -> proper#(X1), proper#(fib1(X1, X2)) -> proper#(X2))
                                (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
                               SCCS:
                                Scc:
                                 { proper#(sel(X1, X2)) -> proper#(X1),
                                  proper#(fib1(X1, X2)) -> proper#(X2),
                                   proper#(add(X1, X2)) -> proper#(X2)}
                                SCC:
                                 Strict:
                                  { proper#(sel(X1, X2)) -> proper#(X1),
                                   proper#(fib1(X1, X2)) -> proper#(X2),
                                    proper#(add(X1, X2)) -> proper#(X2)}
                                 Weak:
                                 {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                               sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                             sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                              fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                              fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                            fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                      s(mark(X)) -> mark(s(X)),
                                                        s(ok(X)) -> ok(s(X)),
                                             active(sel(X1, X2)) -> sel(X1, active(X2)),
                                             active(sel(X1, X2)) -> sel(active(X1), X2),
                                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                   active(sel(0(), cons(X, XS))) -> mark(X),
                                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                            active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                            active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                    active(s(X)) -> s(active(X)),
                                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                                  active(fib(X)) -> fib(active(X)),
                                            active(cons(X1, X2)) -> cons(active(X1), X2),
                                             active(add(X1, X2)) -> add(X1, active(X2)),
                                             active(add(X1, X2)) -> add(active(X1), X2),
                                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                             active(add(0(), X)) -> mark(X),
                                                    fib(mark(X)) -> mark(fib(X)),
                                                      fib(ok(X)) -> ok(fib(X)),
                                              cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                            cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                                               add(mark(X1), X2) -> mark(add(X1, X2)),
                                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                             proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                            proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                    proper(s(X)) -> s(proper(X)),
                                                     proper(0()) -> ok(0()),
                                                  proper(fib(X)) -> fib(proper(X)),
                                            proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                    top(mark(X)) -> top(proper(X)),
                                                      top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(proper#) = 0
                                  Strict:
                                   {proper#(sel(X1, X2)) -> proper#(X1),
                                    proper#(add(X1, X2)) -> proper#(X2)}
                                  EDG:
                                   {(proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))
                                    (proper#(add(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
                                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
                                    (proper#(sel(X1, X2)) -> proper#(X1), proper#(add(X1, X2)) -> proper#(X2))}
                                   SCCS:
                                    Scc:
                                     {proper#(sel(X1, X2)) -> proper#(X1),
                                      proper#(add(X1, X2)) -> proper#(X2)}
                                    SCC:
                                     Strict:
                                      {proper#(sel(X1, X2)) -> proper#(X1),
                                       proper#(add(X1, X2)) -> proper#(X2)}
                                     Weak:
                                     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                          s(mark(X)) -> mark(s(X)),
                                                            s(ok(X)) -> ok(s(X)),
                                                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                                                 active(sel(X1, X2)) -> sel(active(X1), X2),
                                      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                       active(sel(0(), cons(X, XS))) -> mark(X),
                                                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                        active(s(X)) -> s(active(X)),
                                                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                                      active(fib(X)) -> fib(active(X)),
                                                active(cons(X1, X2)) -> cons(active(X1), X2),
                                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                                 active(add(X1, X2)) -> add(active(X1), X2),
                                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                 active(add(0(), X)) -> mark(X),
                                                        fib(mark(X)) -> mark(fib(X)),
                                                          fib(ok(X)) -> ok(fib(X)),
                                                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                        proper(s(X)) -> s(proper(X)),
                                                         proper(0()) -> ok(0()),
                                                      proper(fib(X)) -> fib(proper(X)),
                                                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                        top(mark(X)) -> top(proper(X)),
                                                          top(ok(X)) -> top(active(X))}
                                     SPSC:
                                      Simple Projection:
                                       pi(proper#) = 0
                                      Strict:
                                       {proper#(add(X1, X2)) -> proper#(X2)}
                                      EDG:
                                       {(proper#(add(X1, X2)) -> proper#(X2), proper#(add(X1, X2)) -> proper#(X2))}
                                       SCCS:
                                        Scc:
                                         {proper#(add(X1, X2)) -> proper#(X2)}
                                        SCC:
                                         Strict:
                                          {proper#(add(X1, X2)) -> proper#(X2)}
                                         Weak:
                                         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                              s(mark(X)) -> mark(s(X)),
                                                                s(ok(X)) -> ok(s(X)),
                                                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                                                     active(sel(X1, X2)) -> sel(active(X1), X2),
                                          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                           active(sel(0(), cons(X, XS))) -> mark(X),
                                                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                            active(s(X)) -> s(active(X)),
                                                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                                          active(fib(X)) -> fib(active(X)),
                                                    active(cons(X1, X2)) -> cons(active(X1), X2),
                                                     active(add(X1, X2)) -> add(X1, active(X2)),
                                                     active(add(X1, X2)) -> add(active(X1), X2),
                                                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                     active(add(0(), X)) -> mark(X),
                                                            fib(mark(X)) -> mark(fib(X)),
                                                              fib(ok(X)) -> ok(fib(X)),
                                                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                                                       add(mark(X1), X2) -> mark(add(X1, X2)),
                                                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                            proper(s(X)) -> s(proper(X)),
                                                             proper(0()) -> ok(0()),
                                                          proper(fib(X)) -> fib(proper(X)),
                                                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                            top(mark(X)) -> top(proper(X)),
                                                              top(ok(X)) -> top(active(X))}
                                         SPSC:
                                          Simple Projection:
                                           pi(proper#) = 0
                                          Strict:
                                           {}
                                          Qed
    SCC:
     Strict:
      {  add#(X1, mark(X2)) -> add#(X1, X2),
         add#(mark(X1), X2) -> add#(X1, X2),
       add#(ok(X1), ok(X2)) -> add#(X1, X2)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {  add#(X1, mark(X2)) -> add#(X1, X2),
        add#(ok(X1), ok(X2)) -> add#(X1, X2)}
      EDG:
       {(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#(X1, mark(X2)) -> add#(X1, X2))
        (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
        (add#(X1, mark(X2)) -> add#(X1, X2), add#(ok(X1), ok(X2)) -> add#(X1, X2))}
       SCCS:
        Scc:
         {  add#(X1, mark(X2)) -> add#(X1, X2),
          add#(ok(X1), ok(X2)) -> add#(X1, X2)}
        SCC:
         Strict:
          {  add#(X1, mark(X2)) -> add#(X1, X2),
           add#(ok(X1), ok(X2)) -> add#(X1, X2)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(add#) = 0
          Strict:
           {add#(X1, mark(X2)) -> add#(X1, X2)}
          EDG:
           {(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))}
           SCCS:
            Scc:
             {add#(X1, mark(X2)) -> add#(X1, X2)}
            SCC:
             Strict:
              {add#(X1, mark(X2)) -> add#(X1, X2)}
             Weak:
             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                         active(sel(X1, X2)) -> sel(active(X1), X2),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                active(s(X)) -> s(active(X)),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                              active(fib(X)) -> fib(active(X)),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> mark(fib(X)),
                                  fib(ok(X)) -> ok(fib(X)),
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                              proper(fib(X)) -> fib(proper(X)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(add#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {  cons#(mark(X1), X2) -> cons#(X1, X2),
       cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(cons#) = 0
      Strict:
       {cons#(mark(X1), X2) -> cons#(X1, X2)}
      EDG:
       {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
       SCCS:
        Scc:
         {cons#(mark(X1), X2) -> cons#(X1, X2)}
        SCC:
         Strict:
          {cons#(mark(X1), X2) -> cons#(X1, X2)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(cons#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {fib#(mark(X)) -> fib#(X),
         fib#(ok(X)) -> fib#(X)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(fib#) = 0
      Strict:
       {fib#(ok(X)) -> fib#(X)}
      EDG:
       {(fib#(ok(X)) -> fib#(X), fib#(ok(X)) -> fib#(X))}
       SCCS:
        Scc:
         {fib#(ok(X)) -> fib#(X)}
        SCC:
         Strict:
          {fib#(ok(X)) -> fib#(X)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(fib#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      { active#(sel(X1, X2)) -> active#(X1),
        active#(sel(X1, X2)) -> active#(X2),
       active#(fib1(X1, X2)) -> active#(X1),
       active#(fib1(X1, X2)) -> active#(X2),
               active#(s(X)) -> active#(X),
             active#(fib(X)) -> active#(X),
       active#(cons(X1, X2)) -> active#(X1),
        active#(add(X1, X2)) -> active#(X1),
        active#(add(X1, X2)) -> active#(X2)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       { active#(sel(X1, X2)) -> active#(X1),
        active#(fib1(X1, X2)) -> active#(X1),
        active#(fib1(X1, X2)) -> active#(X2),
                active#(s(X)) -> active#(X),
              active#(fib(X)) -> active#(X),
        active#(cons(X1, X2)) -> active#(X1),
         active#(add(X1, X2)) -> active#(X1),
         active#(add(X1, X2)) -> active#(X2)}
      EDG:
       {(active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
        (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
        (active#(fib1(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
        (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
        (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
        (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
        (active#(fib(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(fib(X)) -> active#(X), active#(fib(X)) -> active#(X))
        (active#(fib(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
        (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
        (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
        (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
        (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
        (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
        (active#(fib1(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
        (active#(fib1(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
        (active#(fib1(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X1))
        (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
        (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(fib(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
        (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
        (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
        (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
        (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))}
       SCCS:
        Scc:
         { active#(sel(X1, X2)) -> active#(X1),
          active#(fib1(X1, X2)) -> active#(X1),
          active#(fib1(X1, X2)) -> active#(X2),
                  active#(s(X)) -> active#(X),
                active#(fib(X)) -> active#(X),
          active#(cons(X1, X2)) -> active#(X1),
           active#(add(X1, X2)) -> active#(X1),
           active#(add(X1, X2)) -> active#(X2)}
        SCC:
         Strict:
          { active#(sel(X1, X2)) -> active#(X1),
           active#(fib1(X1, X2)) -> active#(X1),
           active#(fib1(X1, X2)) -> active#(X2),
                   active#(s(X)) -> active#(X),
                 active#(fib(X)) -> active#(X),
           active#(cons(X1, X2)) -> active#(X1),
            active#(add(X1, X2)) -> active#(X1),
            active#(add(X1, X2)) -> active#(X2)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           { active#(sel(X1, X2)) -> active#(X1),
            active#(fib1(X1, X2)) -> active#(X1),
            active#(fib1(X1, X2)) -> active#(X2),
                    active#(s(X)) -> active#(X),
                  active#(fib(X)) -> active#(X),
            active#(cons(X1, X2)) -> active#(X1),
             active#(add(X1, X2)) -> active#(X2)}
          EDG:
           {(active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
            (active#(add(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
            (active#(add(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
            (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
            (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
            (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
            (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
            (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
            (active#(fib1(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
            (active#(fib1(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
            (active#(fib1(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
            (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
            (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
            (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(fib(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
            (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
            (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
            (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
            (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
            (active#(fib(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(fib(X)) -> active#(X), active#(fib(X)) -> active#(X))
            (active#(fib(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
            (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
            (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
            (active#(cons(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
            (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
            (active#(cons(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
            (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
            (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
            (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
            (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(sel(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
            (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
            (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
            (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
            (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
            (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
            (active#(fib1(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
            (active#(fib1(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
            (active#(fib1(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
            (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))}
           SCCS:
            Scc:
             { active#(sel(X1, X2)) -> active#(X1),
              active#(fib1(X1, X2)) -> active#(X1),
              active#(fib1(X1, X2)) -> active#(X2),
                      active#(s(X)) -> active#(X),
                    active#(fib(X)) -> active#(X),
              active#(cons(X1, X2)) -> active#(X1),
               active#(add(X1, X2)) -> active#(X2)}
            SCC:
             Strict:
              { active#(sel(X1, X2)) -> active#(X1),
               active#(fib1(X1, X2)) -> active#(X1),
               active#(fib1(X1, X2)) -> active#(X2),
                       active#(s(X)) -> active#(X),
                     active#(fib(X)) -> active#(X),
               active#(cons(X1, X2)) -> active#(X1),
                active#(add(X1, X2)) -> active#(X2)}
             Weak:
             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                         active(sel(X1, X2)) -> sel(active(X1), X2),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                active(s(X)) -> s(active(X)),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                              active(fib(X)) -> fib(active(X)),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> mark(fib(X)),
                                  fib(ok(X)) -> ok(fib(X)),
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                              proper(fib(X)) -> fib(proper(X)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               { active#(sel(X1, X2)) -> active#(X1),
                active#(fib1(X1, X2)) -> active#(X1),
                active#(fib1(X1, X2)) -> active#(X2),
                        active#(s(X)) -> active#(X),
                      active#(fib(X)) -> active#(X),
                 active#(add(X1, X2)) -> active#(X2)}
              EDG:
               {(active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
                (active#(fib1(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
                (active#(fib1(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
                (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                (active#(add(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
                (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
                (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
                (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                (active#(fib(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
                (active#(fib(X)) -> active#(X), active#(fib(X)) -> active#(X))
                (active#(fib(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
                (active#(fib(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
                (active#(fib(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
                (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(fib(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))
                (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
                (active#(fib1(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
                (active#(fib1(X1, X2)) -> active#(X2), active#(fib(X)) -> active#(X))
                (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
                (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(sel(X1, X2)) -> active#(X1), active#(fib(X)) -> active#(X))
                (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))}
               SCCS:
                Scc:
                 { active#(sel(X1, X2)) -> active#(X1),
                  active#(fib1(X1, X2)) -> active#(X1),
                  active#(fib1(X1, X2)) -> active#(X2),
                          active#(s(X)) -> active#(X),
                        active#(fib(X)) -> active#(X),
                   active#(add(X1, X2)) -> active#(X2)}
                SCC:
                 Strict:
                  { active#(sel(X1, X2)) -> active#(X1),
                   active#(fib1(X1, X2)) -> active#(X1),
                   active#(fib1(X1, X2)) -> active#(X2),
                           active#(s(X)) -> active#(X),
                         active#(fib(X)) -> active#(X),
                    active#(add(X1, X2)) -> active#(X2)}
                 Weak:
                 {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                               sel(mark(X1), X2) -> mark(sel(X1, X2)),
                             sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                              fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                              fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                            fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                      s(mark(X)) -> mark(s(X)),
                                        s(ok(X)) -> ok(s(X)),
                             active(sel(X1, X2)) -> sel(X1, active(X2)),
                             active(sel(X1, X2)) -> sel(active(X1), X2),
                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                   active(sel(0(), cons(X, XS))) -> mark(X),
                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                            active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                            active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                    active(s(X)) -> s(active(X)),
                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                  active(fib(X)) -> fib(active(X)),
                            active(cons(X1, X2)) -> cons(active(X1), X2),
                             active(add(X1, X2)) -> add(X1, active(X2)),
                             active(add(X1, X2)) -> add(active(X1), X2),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                                    fib(mark(X)) -> mark(fib(X)),
                                      fib(ok(X)) -> ok(fib(X)),
                              cons(mark(X1), X2) -> mark(cons(X1, X2)),
                            cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                               add(mark(X1), X2) -> mark(add(X1, X2)),
                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                             proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                            proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                    proper(s(X)) -> s(proper(X)),
                                     proper(0()) -> ok(0()),
                                  proper(fib(X)) -> fib(proper(X)),
                            proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                    top(mark(X)) -> top(proper(X)),
                                      top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(active#) = 0
                  Strict:
                   { active#(sel(X1, X2)) -> active#(X1),
                    active#(fib1(X1, X2)) -> active#(X1),
                    active#(fib1(X1, X2)) -> active#(X2),
                            active#(s(X)) -> active#(X),
                     active#(add(X1, X2)) -> active#(X2)}
                  EDG:
                   {(active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
                    (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
                    (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                    (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                    (active#(fib1(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
                    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
                    (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                    (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                    (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                    (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
                    (active#(add(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
                    (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                    (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                    (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
                    (active#(fib1(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                    (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
                    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
                    (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X1))
                    (active#(s(X)) -> active#(X), active#(fib1(X1, X2)) -> active#(X2))
                    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(add(X1, X2)) -> active#(X2))}
                   SCCS:
                    Scc:
                     { active#(sel(X1, X2)) -> active#(X1),
                      active#(fib1(X1, X2)) -> active#(X1),
                      active#(fib1(X1, X2)) -> active#(X2),
                              active#(s(X)) -> active#(X),
                       active#(add(X1, X2)) -> active#(X2)}
                    SCC:
                     Strict:
                      { active#(sel(X1, X2)) -> active#(X1),
                       active#(fib1(X1, X2)) -> active#(X1),
                       active#(fib1(X1, X2)) -> active#(X2),
                               active#(s(X)) -> active#(X),
                        active#(add(X1, X2)) -> active#(X2)}
                     Weak:
                     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                          s(mark(X)) -> mark(s(X)),
                                            s(ok(X)) -> ok(s(X)),
                                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                                 active(sel(X1, X2)) -> sel(active(X1), X2),
                      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                       active(sel(0(), cons(X, XS))) -> mark(X),
                                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                        active(s(X)) -> s(active(X)),
                                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                      active(fib(X)) -> fib(active(X)),
                                active(cons(X1, X2)) -> cons(active(X1), X2),
                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                 active(add(X1, X2)) -> add(active(X1), X2),
                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                 active(add(0(), X)) -> mark(X),
                                        fib(mark(X)) -> mark(fib(X)),
                                          fib(ok(X)) -> ok(fib(X)),
                                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                        proper(s(X)) -> s(proper(X)),
                                         proper(0()) -> ok(0()),
                                      proper(fib(X)) -> fib(proper(X)),
                                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                        top(mark(X)) -> top(proper(X)),
                                          top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(active#) = 0
                      Strict:
                       { active#(sel(X1, X2)) -> active#(X1),
                        active#(fib1(X1, X2)) -> active#(X1),
                        active#(fib1(X1, X2)) -> active#(X2),
                         active#(add(X1, X2)) -> active#(X2)}
                      EDG:
                       {(active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
                        (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
                        (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                        (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                        (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                        (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
                        (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                        (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                        (active#(fib1(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                        (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                        (active#(fib1(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X2))
                        (active#(fib1(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                        (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                        (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                        (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X2))
                        (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))}
                       SCCS:
                        Scc:
                         { active#(sel(X1, X2)) -> active#(X1),
                          active#(fib1(X1, X2)) -> active#(X1),
                          active#(fib1(X1, X2)) -> active#(X2),
                           active#(add(X1, X2)) -> active#(X2)}
                        SCC:
                         Strict:
                          { active#(sel(X1, X2)) -> active#(X1),
                           active#(fib1(X1, X2)) -> active#(X1),
                           active#(fib1(X1, X2)) -> active#(X2),
                            active#(add(X1, X2)) -> active#(X2)}
                         Weak:
                         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                              s(mark(X)) -> mark(s(X)),
                                                s(ok(X)) -> ok(s(X)),
                                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                                     active(sel(X1, X2)) -> sel(active(X1), X2),
                          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                           active(sel(0(), cons(X, XS))) -> mark(X),
                                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                            active(s(X)) -> s(active(X)),
                                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                          active(fib(X)) -> fib(active(X)),
                                    active(cons(X1, X2)) -> cons(active(X1), X2),
                                     active(add(X1, X2)) -> add(X1, active(X2)),
                                     active(add(X1, X2)) -> add(active(X1), X2),
                                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                     active(add(0(), X)) -> mark(X),
                                            fib(mark(X)) -> mark(fib(X)),
                                              fib(ok(X)) -> ok(fib(X)),
                                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                                       add(mark(X1), X2) -> mark(add(X1, X2)),
                                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                            proper(s(X)) -> s(proper(X)),
                                             proper(0()) -> ok(0()),
                                          proper(fib(X)) -> fib(proper(X)),
                                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                            top(mark(X)) -> top(proper(X)),
                                              top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(active#) = 0
                          Strict:
                           { active#(sel(X1, X2)) -> active#(X1),
                            active#(fib1(X1, X2)) -> active#(X1),
                             active#(add(X1, X2)) -> active#(X2)}
                          EDG:
                           {(active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))
                            (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                            (active#(fib1(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                            (active#(add(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
                            (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                            (active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                            (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                            (active#(sel(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                            (active#(sel(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))}
                           SCCS:
                            Scc:
                             { active#(sel(X1, X2)) -> active#(X1),
                              active#(fib1(X1, X2)) -> active#(X1),
                               active#(add(X1, X2)) -> active#(X2)}
                            SCC:
                             Strict:
                              { active#(sel(X1, X2)) -> active#(X1),
                               active#(fib1(X1, X2)) -> active#(X1),
                                active#(add(X1, X2)) -> active#(X2)}
                             Weak:
                             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                  s(mark(X)) -> mark(s(X)),
                                                    s(ok(X)) -> ok(s(X)),
                                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                                         active(sel(X1, X2)) -> sel(active(X1), X2),
                              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                               active(sel(0(), cons(X, XS))) -> mark(X),
                                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                active(s(X)) -> s(active(X)),
                                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                              active(fib(X)) -> fib(active(X)),
                                        active(cons(X1, X2)) -> cons(active(X1), X2),
                                         active(add(X1, X2)) -> add(X1, active(X2)),
                                         active(add(X1, X2)) -> add(active(X1), X2),
                                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                         active(add(0(), X)) -> mark(X),
                                                fib(mark(X)) -> mark(fib(X)),
                                                  fib(ok(X)) -> ok(fib(X)),
                                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                                           add(mark(X1), X2) -> mark(add(X1, X2)),
                                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                proper(s(X)) -> s(proper(X)),
                                                 proper(0()) -> ok(0()),
                                              proper(fib(X)) -> fib(proper(X)),
                                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                top(mark(X)) -> top(proper(X)),
                                                  top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(active#) = 0
                              Strict:
                               {active#(fib1(X1, X2)) -> active#(X1),
                                 active#(add(X1, X2)) -> active#(X2)}
                              EDG:
                               {(active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))
                                (active#(add(X1, X2)) -> active#(X2), active#(fib1(X1, X2)) -> active#(X1))
                                (active#(fib1(X1, X2)) -> active#(X1), active#(fib1(X1, X2)) -> active#(X1))
                                (active#(fib1(X1, X2)) -> active#(X1), active#(add(X1, X2)) -> active#(X2))}
                               SCCS:
                                Scc:
                                 {active#(fib1(X1, X2)) -> active#(X1),
                                   active#(add(X1, X2)) -> active#(X2)}
                                SCC:
                                 Strict:
                                  {active#(fib1(X1, X2)) -> active#(X1),
                                    active#(add(X1, X2)) -> active#(X2)}
                                 Weak:
                                 {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                               sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                             sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                              fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                              fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                            fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                      s(mark(X)) -> mark(s(X)),
                                                        s(ok(X)) -> ok(s(X)),
                                             active(sel(X1, X2)) -> sel(X1, active(X2)),
                                             active(sel(X1, X2)) -> sel(active(X1), X2),
                                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                   active(sel(0(), cons(X, XS))) -> mark(X),
                                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                            active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                            active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                    active(s(X)) -> s(active(X)),
                                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                                  active(fib(X)) -> fib(active(X)),
                                            active(cons(X1, X2)) -> cons(active(X1), X2),
                                             active(add(X1, X2)) -> add(X1, active(X2)),
                                             active(add(X1, X2)) -> add(active(X1), X2),
                                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                             active(add(0(), X)) -> mark(X),
                                                    fib(mark(X)) -> mark(fib(X)),
                                                      fib(ok(X)) -> ok(fib(X)),
                                              cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                            cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                               add(X1, mark(X2)) -> mark(add(X1, X2)),
                                               add(mark(X1), X2) -> mark(add(X1, X2)),
                                             add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                             proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                            proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                    proper(s(X)) -> s(proper(X)),
                                                     proper(0()) -> ok(0()),
                                                  proper(fib(X)) -> fib(proper(X)),
                                            proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                             proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                    top(mark(X)) -> top(proper(X)),
                                                      top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(active#) = 0
                                  Strict:
                                   {active#(add(X1, X2)) -> active#(X2)}
                                  EDG:
                                   {(active#(add(X1, X2)) -> active#(X2), active#(add(X1, X2)) -> active#(X2))}
                                   SCCS:
                                    Scc:
                                     {active#(add(X1, X2)) -> active#(X2)}
                                    SCC:
                                     Strict:
                                      {active#(add(X1, X2)) -> active#(X2)}
                                     Weak:
                                     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                                                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                                                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                                          s(mark(X)) -> mark(s(X)),
                                                            s(ok(X)) -> ok(s(X)),
                                                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                                                 active(sel(X1, X2)) -> sel(active(X1), X2),
                                      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                       active(sel(0(), cons(X, XS))) -> mark(X),
                                                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                                                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                                        active(s(X)) -> s(active(X)),
                                                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                                                      active(fib(X)) -> fib(active(X)),
                                                active(cons(X1, X2)) -> cons(active(X1), X2),
                                                 active(add(X1, X2)) -> add(X1, active(X2)),
                                                 active(add(X1, X2)) -> add(active(X1), X2),
                                                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                                                 active(add(0(), X)) -> mark(X),
                                                        fib(mark(X)) -> mark(fib(X)),
                                                          fib(ok(X)) -> ok(fib(X)),
                                                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                                                   add(mark(X1), X2) -> mark(add(X1, X2)),
                                                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                                                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                                        proper(s(X)) -> s(proper(X)),
                                                         proper(0()) -> ok(0()),
                                                      proper(fib(X)) -> fib(proper(X)),
                                                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                                        top(mark(X)) -> top(proper(X)),
                                                          top(ok(X)) -> top(active(X))}
                                     SPSC:
                                      Simple Projection:
                                       pi(active#) = 0
                                      Strict:
                                       {}
                                      Qed
    SCC:
     Strict:
      {s#(mark(X)) -> s#(X),
         s#(ok(X)) -> s#(X)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(ok(X)) -> s#(X)}
      EDG:
       {(s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(ok(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(ok(X)) -> s#(X)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
         fib1#(mark(X1), X2) -> fib1#(X1, X2),
       fib1#(ok(X1), ok(X2)) -> fib1#(X1, X2)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(fib1#) = 0
      Strict:
       {fib1#(X1, mark(X2)) -> fib1#(X1, X2),
        fib1#(mark(X1), X2) -> fib1#(X1, X2)}
      EDG:
       {(fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
        (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
        (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
        (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))}
       SCCS:
        Scc:
         {fib1#(X1, mark(X2)) -> fib1#(X1, X2),
          fib1#(mark(X1), X2) -> fib1#(X1, X2)}
        SCC:
         Strict:
          {fib1#(X1, mark(X2)) -> fib1#(X1, X2),
           fib1#(mark(X1), X2) -> fib1#(X1, X2)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(fib1#) = 0
          Strict:
           {fib1#(X1, mark(X2)) -> fib1#(X1, X2)}
          EDG:
           {(fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))}
           SCCS:
            Scc:
             {fib1#(X1, mark(X2)) -> fib1#(X1, X2)}
            SCC:
             Strict:
              {fib1#(X1, mark(X2)) -> fib1#(X1, X2)}
             Weak:
             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                         active(sel(X1, X2)) -> sel(active(X1), X2),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                active(s(X)) -> s(active(X)),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                              active(fib(X)) -> fib(active(X)),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> mark(fib(X)),
                                  fib(ok(X)) -> ok(fib(X)),
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                              proper(fib(X)) -> fib(proper(X)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(fib1#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {  sel#(X1, mark(X2)) -> sel#(X1, X2),
         sel#(mark(X1), X2) -> sel#(X1, X2),
       sel#(ok(X1), ok(X2)) -> sel#(X1, X2)}
     Weak:
     {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                   sel(mark(X1), X2) -> mark(sel(X1, X2)),
                 sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                  fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                          s(mark(X)) -> mark(s(X)),
                            s(ok(X)) -> ok(s(X)),
                 active(sel(X1, X2)) -> sel(X1, active(X2)),
                 active(sel(X1, X2)) -> sel(active(X1), X2),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                active(fib1(X1, X2)) -> fib1(active(X1), X2),
                        active(s(X)) -> s(active(X)),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                      active(fib(X)) -> fib(active(X)),
                active(cons(X1, X2)) -> cons(active(X1), X2),
                 active(add(X1, X2)) -> add(X1, active(X2)),
                 active(add(X1, X2)) -> add(active(X1), X2),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> mark(fib(X)),
                          fib(ok(X)) -> ok(fib(X)),
                  cons(mark(X1), X2) -> mark(cons(X1, X2)),
                cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   add(X1, mark(X2)) -> mark(add(X1, X2)),
                   add(mark(X1), X2) -> mark(add(X1, X2)),
                 add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                 proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                        proper(s(X)) -> s(proper(X)),
                         proper(0()) -> ok(0()),
                      proper(fib(X)) -> fib(proper(X)),
                proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(sel#) = 1
      Strict:
       {sel#(X1, mark(X2)) -> sel#(X1, X2),
        sel#(mark(X1), X2) -> sel#(X1, X2)}
      EDG:
       {(sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
        (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))}
       SCCS:
        Scc:
         {sel#(X1, mark(X2)) -> sel#(X1, X2),
          sel#(mark(X1), X2) -> sel#(X1, X2)}
        SCC:
         Strict:
          {sel#(X1, mark(X2)) -> sel#(X1, X2),
           sel#(mark(X1), X2) -> sel#(X1, X2)}
         Weak:
         {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                      fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                      fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                    fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                    active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                    active(fib1(X1, X2)) -> fib1(active(X1), X2),
                            active(s(X)) -> s(active(X)),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                          active(fib(X)) -> fib(active(X)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(add(X1, X2)) -> add(X1, active(X2)),
                     active(add(X1, X2)) -> add(active(X1), X2),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> mark(fib(X)),
                              fib(ok(X)) -> ok(fib(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       add(X1, mark(X2)) -> mark(add(X1, X2)),
                       add(mark(X1), X2) -> mark(add(X1, X2)),
                     add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                    proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                             proper(0()) -> ok(0()),
                          proper(fib(X)) -> fib(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(sel#) = 1
          Strict:
           {sel#(mark(X1), X2) -> sel#(X1, X2)}
          EDG:
           {(sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))}
           SCCS:
            Scc:
             {sel#(mark(X1), X2) -> sel#(X1, X2)}
            SCC:
             Strict:
              {sel#(mark(X1), X2) -> sel#(X1, X2)}
             Weak:
             {             sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                          fib1(X1, mark(X2)) -> mark(fib1(X1, X2)),
                          fib1(mark(X1), X2) -> mark(fib1(X1, X2)),
                        fib1(ok(X1), ok(X2)) -> ok(fib1(X1, X2)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                         active(sel(X1, X2)) -> sel(active(X1), X2),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                        active(fib1(X1, X2)) -> fib1(X1, active(X2)),
                        active(fib1(X1, X2)) -> fib1(active(X1), X2),
                                active(s(X)) -> s(active(X)),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                              active(fib(X)) -> fib(active(X)),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(add(X1, X2)) -> add(X1, active(X2)),
                         active(add(X1, X2)) -> add(active(X1), X2),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> mark(fib(X)),
                                  fib(ok(X)) -> ok(fib(X)),
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                           add(X1, mark(X2)) -> mark(add(X1, X2)),
                           add(mark(X1), X2) -> mark(add(X1, X2)),
                         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                        proper(fib1(X1, X2)) -> fib1(proper(X1), proper(X2)),
                                proper(s(X)) -> s(proper(X)),
                                 proper(0()) -> ok(0()),
                              proper(fib(X)) -> fib(proper(X)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(sel#) = 0
              Strict:
               {}
              Qed