MAYBE
Time: 0.078308
TRS:
 {         active fst(X1, X2) -> fst(X1, active X2),
           active fst(X1, X2) -> fst(active X1, X2),
           active fst(0(), Z) -> mark nil(),
  active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
          active cons(X1, X2) -> cons(active X1, X2),
                active from X -> mark cons(X, from s X),
                active from X -> from active X,
           active add(X1, X2) -> add(X1, active X2),
           active add(X1, X2) -> add(active X1, X2),
           active add(0(), X) -> mark X,
           active add(s X, Y) -> mark s add(X, Y),
                 active len X -> len active X,
             active len nil() -> mark 0(),
        active len cons(X, Z) -> mark s len Z,
             fst(X1, mark X2) -> mark fst(X1, X2),
             fst(mark X1, X2) -> mark fst(X1, X2),
            fst(ok X1, ok X2) -> ok fst(X1, X2),
            cons(mark X1, X2) -> mark cons(X1, X2),
           cons(ok X1, ok X2) -> ok cons(X1, X2),
                       s ok X -> ok s X,
                  from mark X -> mark from X,
                    from ok X -> ok from X,
             add(X1, mark X2) -> mark add(X1, X2),
             add(mark X1, X2) -> mark add(X1, X2),
            add(ok X1, ok X2) -> ok add(X1, X2),
                   len mark X -> mark len X,
                     len ok X -> ok len X,
                 proper nil() -> ok nil(),
           proper fst(X1, X2) -> fst(proper X1, proper X2),
                   proper 0() -> ok 0(),
          proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper s X -> s proper X,
                proper from X -> from proper X,
           proper add(X1, X2) -> add(proper X1, proper X2),
                 proper len X -> len proper X,
                   top mark X -> top proper X,
                     top ok X -> top active X}
 DP:
  DP:
   {         active# fst(X1, X2) -> active# X1,
             active# fst(X1, X2) -> active# X2,
             active# fst(X1, X2) -> fst#(X1, active X2),
             active# fst(X1, X2) -> fst#(active X1, X2),
    active# fst(s X, cons(Y, Z)) -> fst#(X, Z),
    active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)),
            active# cons(X1, X2) -> active# X1,
            active# cons(X1, X2) -> cons#(active X1, X2),
                  active# from X -> active# X,
                  active# from X -> cons#(X, from s X),
                  active# from X -> s# X,
                  active# from X -> from# active X,
                  active# from X -> from# s X,
             active# add(X1, X2) -> active# X1,
             active# add(X1, X2) -> active# X2,
             active# add(X1, X2) -> add#(X1, active X2),
             active# add(X1, X2) -> add#(active X1, X2),
             active# add(s X, Y) -> s# add(X, Y),
             active# add(s X, Y) -> add#(X, Y),
                   active# len X -> active# X,
                   active# len X -> len# active X,
          active# len cons(X, Z) -> s# len Z,
          active# len cons(X, Z) -> len# Z,
               fst#(X1, mark X2) -> fst#(X1, X2),
               fst#(mark X1, X2) -> fst#(X1, X2),
              fst#(ok X1, ok X2) -> fst#(X1, X2),
              cons#(mark X1, X2) -> cons#(X1, X2),
             cons#(ok X1, ok X2) -> cons#(X1, X2),
                         s# ok X -> s# X,
                    from# mark X -> from# X,
                      from# ok X -> from# X,
               add#(X1, mark X2) -> add#(X1, X2),
               add#(mark X1, X2) -> add#(X1, X2),
              add#(ok X1, ok X2) -> add#(X1, X2),
                     len# mark X -> len# X,
                       len# ok X -> len# X,
             proper# fst(X1, X2) -> fst#(proper X1, proper X2),
             proper# fst(X1, X2) -> proper# X1,
             proper# fst(X1, X2) -> proper# X2,
            proper# cons(X1, X2) -> cons#(proper X1, proper X2),
            proper# cons(X1, X2) -> proper# X1,
            proper# cons(X1, X2) -> proper# X2,
                     proper# s X -> s# proper X,
                     proper# s X -> proper# X,
                  proper# from X -> from# proper X,
                  proper# from X -> proper# X,
             proper# add(X1, X2) -> add#(proper X1, proper X2),
             proper# add(X1, X2) -> proper# X1,
             proper# add(X1, X2) -> proper# X2,
                   proper# len X -> len# proper X,
                   proper# len X -> proper# X,
                     top# mark X -> proper# X,
                     top# mark X -> top# proper X,
                       top# ok X -> active# X,
                       top# ok X -> top# active X}
  TRS:
  {         active fst(X1, X2) -> fst(X1, active X2),
            active fst(X1, X2) -> fst(active X1, X2),
            active fst(0(), Z) -> mark nil(),
   active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
           active cons(X1, X2) -> cons(active X1, X2),
                 active from X -> mark cons(X, from s X),
                 active from X -> from active X,
            active add(X1, X2) -> add(X1, active X2),
            active add(X1, X2) -> add(active X1, X2),
            active add(0(), X) -> mark X,
            active add(s X, Y) -> mark s add(X, Y),
                  active len X -> len active X,
              active len nil() -> mark 0(),
         active len cons(X, Z) -> mark s len Z,
              fst(X1, mark X2) -> mark fst(X1, X2),
              fst(mark X1, X2) -> mark fst(X1, X2),
             fst(ok X1, ok X2) -> ok fst(X1, X2),
             cons(mark X1, X2) -> mark cons(X1, X2),
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   from mark X -> mark from X,
                     from ok X -> ok from X,
              add(X1, mark X2) -> mark add(X1, X2),
              add(mark X1, X2) -> mark add(X1, X2),
             add(ok X1, ok X2) -> ok add(X1, X2),
                    len mark X -> mark len X,
                      len ok X -> ok len X,
                  proper nil() -> ok nil(),
            proper fst(X1, X2) -> fst(proper X1, proper X2),
                    proper 0() -> ok 0(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper s X -> s proper X,
                 proper from X -> from proper X,
            proper add(X1, X2) -> add(proper X1, proper X2),
                  proper len X -> len proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
  UR:
   {         active fst(X1, X2) -> fst(X1, active X2),
             active fst(X1, X2) -> fst(active X1, X2),
             active fst(0(), Z) -> mark nil(),
    active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
            active cons(X1, X2) -> cons(active X1, X2),
                  active from X -> mark cons(X, from s X),
                  active from X -> from active X,
             active add(X1, X2) -> add(X1, active X2),
             active add(X1, X2) -> add(active X1, X2),
             active add(0(), X) -> mark X,
             active add(s X, Y) -> mark s add(X, Y),
                   active len X -> len active X,
               active len nil() -> mark 0(),
          active len cons(X, Z) -> mark s len Z,
               fst(X1, mark X2) -> mark fst(X1, X2),
               fst(mark X1, X2) -> mark fst(X1, X2),
              fst(ok X1, ok X2) -> ok fst(X1, X2),
              cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
                         s ok X -> ok s X,
                    from mark X -> mark from X,
                      from ok X -> ok from X,
               add(X1, mark X2) -> mark add(X1, X2),
               add(mark X1, X2) -> mark add(X1, X2),
              add(ok X1, ok X2) -> ok add(X1, X2),
                     len mark X -> mark len X,
                       len ok X -> ok len X,
                   proper nil() -> ok nil(),
             proper fst(X1, X2) -> fst(proper X1, proper X2),
                     proper 0() -> ok 0(),
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper s X -> s proper X,
                  proper from X -> from proper X,
             proper add(X1, X2) -> add(proper X1, proper X2),
                   proper len X -> len proper X}
   EDG:
    {
     (active# fst(X1, X2) -> fst#(X1, active X2), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (active# fst(X1, X2) -> fst#(X1, active X2), fst#(mark X1, X2) -> fst#(X1, X2))
     (active# fst(X1, X2) -> fst#(X1, active X2), fst#(X1, mark X2) -> fst#(X1, X2))
     (proper# fst(X1, X2) -> fst#(proper X1, proper X2), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (proper# fst(X1, X2) -> fst#(proper X1, proper X2), fst#(mark X1, X2) -> fst#(X1, X2))
     (proper# fst(X1, X2) -> fst#(proper X1, proper X2), fst#(X1, mark X2) -> fst#(X1, X2))
     (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(mark X1, X2) -> add#(X1, X2))
     (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(X1, mark X2) -> add#(X1, X2))
     (active# fst(X1, X2) -> fst#(active X1, X2), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (active# fst(X1, X2) -> fst#(active X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
     (active# fst(X1, X2) -> fst#(active X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
     (active# add(X1, X2) -> add#(active X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(active X1, X2), add#(mark X1, X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(active X1, X2), add#(X1, mark X2) -> add#(X1, X2))
     (active# 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# from X -> active# X, active# len cons(X, Z) -> len# Z)
     (active# from X -> active# X, active# len cons(X, Z) -> s# len Z)
     (active# from X -> active# X, active# len X -> len# active X)
     (active# from X -> active# X, active# len X -> active# X)
     (active# from X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# from X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# from X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# from X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# from X -> active# X, active# add(X1, X2) -> active# X2)
     (active# from X -> active# X, active# add(X1, X2) -> active# X1)
     (active# from X -> active# X, active# from X -> from# s X)
     (active# from X -> active# X, active# from X -> from# active X)
     (active# from X -> active# X, active# from X -> s# X)
     (active# from X -> active# X, active# from X -> cons#(X, from s X))
     (active# from X -> active# X, active# from X -> active# X)
     (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# from X -> active# X, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (active# from X -> active# X, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# from X -> active# X, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# from X -> active# X, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# from X -> active# X, active# fst(X1, X2) -> active# X2)
     (active# from X -> active# X, active# fst(X1, X2) -> active# X1)
     (active# len X -> active# X, active# len cons(X, Z) -> len# Z)
     (active# len X -> active# X, active# len cons(X, Z) -> s# len Z)
     (active# len X -> active# X, active# len X -> len# active X)
     (active# len X -> active# X, active# len X -> active# X)
     (active# len X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# len X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# len X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# len X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# len X -> active# X, active# add(X1, X2) -> active# X2)
     (active# len X -> active# X, active# add(X1, X2) -> active# X1)
     (active# len X -> active# X, active# from X -> from# s X)
     (active# len X -> active# X, active# from X -> from# active X)
     (active# len X -> active# X, active# from X -> s# X)
     (active# len X -> active# X, active# from X -> cons#(X, from s X))
     (active# len X -> active# X, active# from X -> active# X)
     (active# len X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# len X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# len X -> active# X, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (active# len X -> active# X, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# len X -> active# X, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# len X -> active# X, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# len X -> active# X, active# fst(X1, X2) -> active# X2)
     (active# len X -> active# X, active# fst(X1, X2) -> active# X1)
     (from# mark X -> from# X, from# ok X -> from# X)
     (from# mark X -> from# X, from# mark X -> from# X)
     (len# mark X -> len# X, len# ok X -> len# X)
     (len# mark X -> len# X, len# mark X -> len# X)
     (proper# s X -> proper# X, proper# len X -> proper# X)
     (proper# s X -> proper# X, proper# len X -> len# proper X)
     (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# from X -> proper# X)
     (proper# s X -> proper# X, proper# from X -> from# 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# 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# fst(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# fst(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (proper# len X -> proper# X, proper# len X -> proper# X)
     (proper# len X -> proper# X, proper# len X -> len# proper X)
     (proper# len X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# len X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# len X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# len X -> proper# X, proper# from X -> proper# X)
     (proper# len X -> proper# X, proper# from X -> from# proper X)
     (proper# len X -> proper# X, proper# s X -> proper# X)
     (proper# len X -> proper# X, proper# s X -> s# proper X)
     (proper# len X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# len X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# len X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# len X -> proper# X, proper# fst(X1, X2) -> proper# X2)
     (proper# len X -> proper# X, proper# fst(X1, X2) -> proper# X1)
     (proper# len X -> proper# X, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (top# ok X -> active# X, active# len cons(X, Z) -> len# Z)
     (top# ok X -> active# X, active# len cons(X, Z) -> s# len Z)
     (top# ok X -> active# X, active# len X -> len# active X)
     (top# ok X -> active# X, active# len X -> active# X)
     (top# ok X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (top# ok X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (top# ok X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (top# ok X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (top# ok X -> active# X, active# add(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# add(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# from X -> from# s X)
     (top# ok X -> active# X, active# from X -> from# active X)
     (top# ok X -> active# X, active# from X -> s# X)
     (top# ok X -> active# X, active# from X -> cons#(X, from s X))
     (top# ok X -> active# X, active# from X -> active# X)
     (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (top# ok X -> active# X, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (top# ok X -> active# X, active# fst(X1, X2) -> fst#(active X1, X2))
     (top# ok X -> active# X, active# fst(X1, X2) -> fst#(X1, active X2))
     (top# ok X -> active# X, active# fst(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# fst(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# len cons(X, Z) -> len# Z)
     (active# cons(X1, X2) -> active# X1, active# len cons(X, Z) -> s# len Z)
     (active# cons(X1, X2) -> active# X1, active# len X -> len# active X)
     (active# cons(X1, X2) -> active# X1, active# len X -> active# X)
     (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# from X -> from# s X)
     (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
     (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
     (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# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (active# cons(X1, X2) -> active# X1, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# cons(X1, X2) -> active# X1, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# cons(X1, X2) -> active# X1, active# fst(X1, X2) -> active# X2)
     (active# cons(X1, X2) -> active# X1, active# fst(X1, X2) -> active# X1)
     (proper# fst(X1, X2) -> proper# X1, proper# len X -> proper# X)
     (proper# fst(X1, X2) -> proper# X1, proper# len X -> len# proper X)
     (proper# fst(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# fst(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# fst(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# fst(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# fst(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# fst(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# fst(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# fst(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# fst(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# fst(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# fst(X1, X2) -> proper# X1, proper# fst(X1, X2) -> proper# X2)
     (proper# fst(X1, X2) -> proper# X1, proper# fst(X1, X2) -> proper# X1)
     (proper# fst(X1, X2) -> proper# X1, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X1, proper# len X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# len X -> len# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X1, proper# fst(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X1, proper# fst(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (active# add(X1, X2) -> active# X2, active# len cons(X, Z) -> len# Z)
     (active# add(X1, X2) -> active# X2, active# len cons(X, Z) -> s# len Z)
     (active# add(X1, X2) -> active# X2, active# len X -> len# active X)
     (active# add(X1, X2) -> active# X2, active# len X -> active# X)
     (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# from X -> from# s X)
     (active# add(X1, X2) -> active# X2, active# from X -> from# active X)
     (active# add(X1, X2) -> active# X2, active# from X -> s# X)
     (active# add(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
     (active# add(X1, X2) -> active# X2, active# from X -> active# X)
     (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# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (active# add(X1, X2) -> active# X2, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# add(X1, X2) -> active# X2, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# add(X1, X2) -> active# X2, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# add(X1, X2) -> active# X2, active# fst(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X2, active# fst(X1, X2) -> active# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# len X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# len X -> len# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# fst(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# fst(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (active# from X -> from# active X, from# ok X -> from# X)
     (active# from X -> from# active X, from# mark X -> from# X)
     (active# len X -> len# active X, len# ok X -> len# X)
     (active# len X -> len# active X, len# mark X -> len# X)
     (proper# from X -> from# proper X, from# ok X -> from# X)
     (proper# from X -> from# proper X, from# mark X -> from# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (active# len cons(X, Z) -> s# len Z, s# ok X -> s# X)
     (fst#(mark X1, X2) -> fst#(X1, X2), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (fst#(mark X1, X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
     (fst#(mark X1, X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(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# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(X1, mark X2) -> fst#(X1, X2))
     (active# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(mark X1, X2) -> fst#(X1, X2))
     (active# fst(s X, cons(Y, Z)) -> fst#(X, Z), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (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))
     (fst#(ok X1, ok X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
     (fst#(ok X1, ok X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
     (fst#(ok X1, ok X2) -> fst#(X1, X2), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (fst#(X1, mark X2) -> fst#(X1, X2), fst#(X1, mark X2) -> fst#(X1, X2))
     (fst#(X1, mark X2) -> fst#(X1, X2), fst#(mark X1, X2) -> fst#(X1, X2))
     (fst#(X1, mark X2) -> fst#(X1, X2), fst#(ok X1, ok X2) -> fst#(X1, X2))
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (proper# len X -> len# proper X, len# mark X -> len# X)
     (proper# len X -> len# proper X, len# ok X -> len# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (active# from X -> from# s X, from# mark X -> from# X)
     (active# from X -> from# s X, from# ok X -> from# X)
     (proper# add(X1, X2) -> proper# X2, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X2, proper# fst(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# fst(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# len X -> len# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# len X -> proper# X)
     (proper# fst(X1, X2) -> proper# X2, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (proper# fst(X1, X2) -> proper# X2, proper# fst(X1, X2) -> proper# X1)
     (proper# fst(X1, X2) -> proper# X2, proper# fst(X1, X2) -> proper# X2)
     (proper# fst(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# fst(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# fst(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# fst(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# fst(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# fst(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# fst(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# fst(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# fst(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# fst(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# fst(X1, X2) -> proper# X2, proper# len X -> len# proper X)
     (proper# fst(X1, X2) -> proper# X2, proper# len X -> proper# X)
     (active# fst(X1, X2) -> active# X2, active# fst(X1, X2) -> active# X1)
     (active# fst(X1, X2) -> active# X2, active# fst(X1, X2) -> active# X2)
     (active# fst(X1, X2) -> active# X2, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# fst(X1, X2) -> active# X2, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# fst(X1, X2) -> active# X2, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# fst(X1, X2) -> active# X2, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (active# fst(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
     (active# fst(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# fst(X1, X2) -> active# X2, active# from X -> active# X)
     (active# fst(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
     (active# fst(X1, X2) -> active# X2, active# from X -> s# X)
     (active# fst(X1, X2) -> active# X2, active# from X -> from# active X)
     (active# fst(X1, X2) -> active# X2, active# from X -> from# s X)
     (active# fst(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
     (active# fst(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
     (active# fst(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
     (active# fst(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
     (active# fst(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
     (active# fst(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
     (active# fst(X1, X2) -> active# X2, active# len X -> active# X)
     (active# fst(X1, X2) -> active# X2, active# len X -> len# active X)
     (active# fst(X1, X2) -> active# X2, active# len cons(X, Z) -> s# len Z)
     (active# fst(X1, X2) -> active# X2, active# len cons(X, Z) -> len# Z)
     (proper# cons(X1, X2) -> proper# X1, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# fst(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# fst(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# len X -> len# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# len X -> proper# X)
     (active# add(X1, X2) -> active# X1, active# fst(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X1, active# fst(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X1, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# add(X1, X2) -> active# X1, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# add(X1, X2) -> active# X1, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# add(X1, X2) -> active# X1, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (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# from X -> active# X)
     (active# add(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# add(X1, X2) -> active# X1, active# from X -> s# X)
     (active# add(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# add(X1, X2) -> active# X1, active# from X -> from# s X)
     (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# add(X1, X2) -> active# X1, active# len X -> active# X)
     (active# add(X1, X2) -> active# X1, active# len X -> len# active X)
     (active# add(X1, X2) -> active# X1, active# len cons(X, Z) -> s# len Z)
     (active# add(X1, X2) -> active# X1, active# len cons(X, Z) -> len# Z)
     (active# fst(X1, X2) -> active# X1, active# fst(X1, X2) -> active# X1)
     (active# fst(X1, X2) -> active# X1, active# fst(X1, X2) -> active# X2)
     (active# fst(X1, X2) -> active# X1, active# fst(X1, X2) -> fst#(X1, active X2))
     (active# fst(X1, X2) -> active# X1, active# fst(X1, X2) -> fst#(active X1, X2))
     (active# fst(X1, X2) -> active# X1, active# fst(s X, cons(Y, Z)) -> fst#(X, Z))
     (active# fst(X1, X2) -> active# X1, active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)))
     (active# fst(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# fst(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# fst(X1, X2) -> active# X1, active# from X -> active# X)
     (active# fst(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# fst(X1, X2) -> active# X1, active# from X -> s# X)
     (active# fst(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# fst(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# fst(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
     (active# fst(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
     (active# fst(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# fst(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# fst(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# fst(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     (active# fst(X1, X2) -> active# X1, active# len X -> active# X)
     (active# fst(X1, X2) -> active# X1, active# len X -> len# active X)
     (active# fst(X1, X2) -> active# X1, active# len cons(X, Z) -> s# len Z)
     (active# fst(X1, X2) -> active# X1, active# len cons(X, Z) -> len# Z)
     (top# mark X -> proper# X, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# fst(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# fst(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# from X -> from# proper X)
     (top# mark X -> proper# X, proper# from X -> proper# X)
     (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# len X -> len# proper X)
     (top# mark X -> proper# X, proper# len X -> proper# X)
     (proper# from X -> proper# X, proper# fst(X1, X2) -> fst#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# fst(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# fst(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# from X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# len X -> len# proper X)
     (proper# from X -> proper# X, proper# len X -> proper# X)
     (len# ok X -> len# X, len# mark X -> len# X)
     (len# ok X -> len# X, len# ok X -> len# X)
     (from# ok X -> from# X, from# mark X -> from# X)
     (from# ok X -> from# X, from# ok X -> from# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (active# from X -> s# X, s# ok X -> s# X)
     (active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# fst(s X, cons(Y, Z)) -> cons#(Y, fst(X, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# len cons(X, Z) -> len# Z, len# mark X -> len# X)
     (active# len cons(X, Z) -> len# Z, len# ok X -> len# X)
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(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# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
    }
    STATUS:
     arrows: 0.860826
     SCCS (9):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       { proper# fst(X1, X2) -> proper# X1,
         proper# fst(X1, X2) -> proper# X2,
        proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
                 proper# s X -> proper# X,
              proper# from X -> proper# X,
         proper# add(X1, X2) -> proper# X1,
         proper# add(X1, X2) -> proper# X2,
               proper# len X -> proper# X}
      Scc:
       { active# fst(X1, X2) -> active# X1,
         active# fst(X1, X2) -> active# X2,
        active# cons(X1, X2) -> active# X1,
              active# from X -> active# X,
         active# add(X1, X2) -> active# X1,
         active# add(X1, X2) -> active# X2,
               active# len X -> active# X}
      Scc:
       {from# mark X -> from# X,
          from# ok X -> from# X}
      Scc:
       {len# mark X -> len# X,
          len# ok X -> len# X}
      Scc:
       { cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(ok X1, ok X2) -> cons#(X1, 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:
       { fst#(X1, mark X2) -> fst#(X1, X2),
         fst#(mark X1, X2) -> fst#(X1, X2),
        fst#(ok X1, ok X2) -> fst#(X1, X2)}
      Scc:
       {s# ok X -> s# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      SCC (9):
       Strict:
        { proper# fst(X1, X2) -> proper# X1,
          proper# fst(X1, X2) -> proper# X2,
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
                  proper# s X -> proper# X,
               proper# from X -> proper# X,
          proper# add(X1, X2) -> proper# X1,
          proper# add(X1, X2) -> proper# X2,
                proper# len X -> proper# X}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      
      SCC (7):
       Strict:
        { active# fst(X1, X2) -> active# X1,
          active# fst(X1, X2) -> active# X2,
         active# cons(X1, X2) -> active# X1,
               active# from X -> active# X,
          active# add(X1, X2) -> active# X1,
          active# add(X1, X2) -> active# X2,
                active# len X -> active# X}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      
      
      SCC (2):
       Strict:
        {from# mark X -> from# X,
           from# ok X -> from# X}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      
      
      
      SCC (2):
       Strict:
        {len# mark X -> len# X,
           len# ok X -> len# X}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      
      
      
      
      SCC (2):
       Strict:
        { cons#(mark X1, X2) -> cons#(X1, X2),
         cons#(ok X1, ok X2) -> cons#(X1, X2)}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      
      SCC (3):
       Strict:
        { add#(X1, mark X2) -> add#(X1, X2),
          add#(mark X1, X2) -> add#(X1, X2),
         add#(ok X1, ok X2) -> add#(X1, X2)}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { fst#(X1, mark X2) -> fst#(X1, X2),
          fst#(mark X1, X2) -> fst#(X1, X2),
         fst#(ok X1, ok X2) -> fst#(X1, X2)}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {s# ok X -> s# X}
       Weak:
       {         active fst(X1, X2) -> fst(X1, active X2),
                 active fst(X1, X2) -> fst(active X1, X2),
                 active fst(0(), Z) -> mark nil(),
        active fst(s X, cons(Y, Z)) -> mark cons(Y, fst(X, Z)),
                active cons(X1, X2) -> cons(active X1, X2),
                      active from X -> mark cons(X, from s X),
                      active from X -> from active X,
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(0(), X) -> mark X,
                 active add(s X, Y) -> mark s add(X, Y),
                       active len X -> len active X,
                   active len nil() -> mark 0(),
              active len cons(X, Z) -> mark s len Z,
                   fst(X1, mark X2) -> mark fst(X1, X2),
                   fst(mark X1, X2) -> mark fst(X1, X2),
                  fst(ok X1, ok X2) -> ok fst(X1, X2),
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                             s ok X -> ok s X,
                        from mark X -> mark from X,
                          from ok X -> ok from X,
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                         len mark X -> mark len X,
                           len ok X -> ok len X,
                       proper nil() -> ok nil(),
                 proper fst(X1, X2) -> fst(proper X1, proper X2),
                         proper 0() -> ok 0(),
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper s X -> s proper X,
                      proper from X -> from proper X,
                 proper add(X1, X2) -> add(proper X1, proper X2),
                       proper len X -> len proper X,
                         top mark X -> top proper X,
                           top ok X -> top active X}
       Open