MAYBE
Time: 0.470671
TRS:
 {            cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
                   recip mark X -> mark recip X,
                     recip ok X -> ok recip X,
                     sqr mark X -> mark sqr X,
                       sqr ok X -> ok sqr X,
                   terms mark X -> mark terms X,
                     terms ok X -> ok terms X,
                         s ok X -> ok s X,
            active cons(X1, X2) -> cons(active X1, X2),
                 active recip X -> recip active X,
                   active sqr X -> sqr active X,
                 active sqr s X -> mark s add(sqr X, dbl X),
                 active sqr 0() -> mark 0(),
                 active terms N -> mark cons(recip sqr N, terms s N),
                 active terms X -> terms active X,
             active add(X1, X2) -> add(X1, active X2),
             active add(X1, X2) -> add(active X1, X2),
             active add(s X, Y) -> mark s add(X, Y),
             active add(0(), X) -> mark X,
                   active dbl X -> dbl active X,
                 active dbl s X -> mark s s dbl X,
                 active dbl 0() -> mark 0(),
           active first(X1, X2) -> first(X1, active X2),
           active first(X1, X2) -> first(active X1, X2),
  active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
           active first(0(), X) -> mark nil(),
               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),
                     dbl mark X -> mark dbl X,
                       dbl ok X -> ok dbl X,
             first(X1, mark X2) -> mark first(X1, X2),
             first(mark X1, X2) -> mark first(X1, X2),
            first(ok X1, ok X2) -> ok first(X1, X2),
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper recip X -> recip proper X,
                   proper sqr X -> sqr proper X,
                 proper terms X -> terms proper X,
                     proper s X -> s proper X,
                     proper 0() -> ok 0(),
             proper add(X1, X2) -> add(proper X1, proper X2),
                   proper dbl X -> dbl proper X,
                   proper nil() -> ok nil(),
           proper first(X1, X2) -> first(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
 DP:
  DP:
   {            cons#(mark X1, X2) -> cons#(X1, X2),
               cons#(ok X1, ok X2) -> cons#(X1, X2),
                     recip# mark X -> recip# X,
                       recip# ok X -> recip# X,
                       sqr# mark X -> sqr# X,
                         sqr# ok X -> sqr# X,
                     terms# mark X -> terms# X,
                       terms# ok X -> terms# X,
                           s# ok X -> s# X,
              active# cons(X1, X2) -> cons#(active X1, X2),
              active# cons(X1, X2) -> active# X1,
                   active# recip X -> recip# active X,
                   active# recip X -> active# X,
                     active# sqr X -> sqr# active X,
                     active# sqr X -> active# X,
                   active# sqr s X -> sqr# X,
                   active# sqr s X -> s# add(sqr X, dbl X),
                   active# sqr s X -> add#(sqr X, dbl X),
                   active# sqr s X -> dbl# X,
                   active# terms N -> cons#(recip sqr N, terms s N),
                   active# terms N -> recip# sqr N,
                   active# terms N -> sqr# N,
                   active# terms N -> terms# s N,
                   active# terms N -> s# N,
                   active# terms X -> terms# active X,
                   active# terms X -> active# X,
               active# add(X1, X2) -> active# X1,
               active# add(X1, X2) -> active# X2,
               active# add(X1, X2) -> add#(X1, active X2),
               active# add(X1, X2) -> add#(active X1, X2),
               active# add(s X, Y) -> s# add(X, Y),
               active# add(s X, Y) -> add#(X, Y),
                     active# dbl X -> active# X,
                     active# dbl X -> dbl# active X,
                   active# dbl s X -> s# s dbl X,
                   active# dbl s X -> s# dbl X,
                   active# dbl s X -> dbl# X,
             active# first(X1, X2) -> active# X1,
             active# first(X1, X2) -> active# X2,
             active# first(X1, X2) -> first#(X1, active X2),
             active# first(X1, X2) -> first#(active X1, X2),
    active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)),
    active# first(s X, cons(Y, Z)) -> first#(X, Z),
                 add#(X1, mark X2) -> add#(X1, X2),
                 add#(mark X1, X2) -> add#(X1, X2),
                add#(ok X1, ok X2) -> add#(X1, X2),
                       dbl# mark X -> dbl# X,
                         dbl# ok X -> dbl# X,
               first#(X1, mark X2) -> first#(X1, X2),
               first#(mark X1, X2) -> first#(X1, X2),
              first#(ok X1, ok X2) -> first#(X1, X2),
              proper# cons(X1, X2) -> cons#(proper X1, proper X2),
              proper# cons(X1, X2) -> proper# X1,
              proper# cons(X1, X2) -> proper# X2,
                   proper# recip X -> recip# proper X,
                   proper# recip X -> proper# X,
                     proper# sqr X -> sqr# proper X,
                     proper# sqr X -> proper# X,
                   proper# terms X -> terms# proper X,
                   proper# terms X -> proper# X,
                       proper# s X -> s# proper X,
                       proper# s 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# dbl X -> dbl# proper X,
                     proper# dbl X -> proper# X,
             proper# first(X1, X2) -> first#(proper X1, proper X2),
             proper# first(X1, X2) -> proper# X1,
             proper# first(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}
  TRS:
  {            cons(mark X1, X2) -> mark cons(X1, X2),
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                    recip mark X -> mark recip X,
                      recip ok X -> ok recip X,
                      sqr mark X -> mark sqr X,
                        sqr ok X -> ok sqr X,
                    terms mark X -> mark terms X,
                      terms ok X -> ok terms X,
                          s ok X -> ok s X,
             active cons(X1, X2) -> cons(active X1, X2),
                  active recip X -> recip active X,
                    active sqr X -> sqr active X,
                  active sqr s X -> mark s add(sqr X, dbl X),
                  active sqr 0() -> mark 0(),
                  active terms N -> mark cons(recip sqr N, terms s N),
                  active terms X -> terms active X,
              active add(X1, X2) -> add(X1, active X2),
              active add(X1, X2) -> add(active X1, X2),
              active add(s X, Y) -> mark s add(X, Y),
              active add(0(), X) -> mark X,
                    active dbl X -> dbl active X,
                  active dbl s X -> mark s s dbl X,
                  active dbl 0() -> mark 0(),
            active first(X1, X2) -> first(X1, active X2),
            active first(X1, X2) -> first(active X1, X2),
   active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
            active first(0(), X) -> mark nil(),
                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),
                      dbl mark X -> mark dbl X,
                        dbl ok X -> ok dbl X,
              first(X1, mark X2) -> mark first(X1, X2),
              first(mark X1, X2) -> mark first(X1, X2),
             first(ok X1, ok X2) -> ok first(X1, X2),
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                  proper recip X -> recip proper X,
                    proper sqr X -> sqr proper X,
                  proper terms X -> terms proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
              proper add(X1, X2) -> add(proper X1, proper X2),
                    proper dbl X -> dbl proper X,
                    proper nil() -> ok nil(),
            proper first(X1, X2) -> first(proper X1, proper X2),
                      top mark X -> top proper X,
                        top ok X -> top active X}
  UR:
   {            cons(mark X1, X2) -> mark cons(X1, X2),
               cons(ok X1, ok X2) -> ok cons(X1, X2),
                     recip mark X -> mark recip X,
                       recip ok X -> ok recip X,
                       sqr mark X -> mark sqr X,
                         sqr ok X -> ok sqr X,
                     terms mark X -> mark terms X,
                       terms ok X -> ok terms X,
                           s ok X -> ok s X,
              active cons(X1, X2) -> cons(active X1, X2),
                   active recip X -> recip active X,
                     active sqr X -> sqr active X,
                   active sqr s X -> mark s add(sqr X, dbl X),
                   active sqr 0() -> mark 0(),
                   active terms N -> mark cons(recip sqr N, terms s N),
                   active terms X -> terms active X,
               active add(X1, X2) -> add(X1, active X2),
               active add(X1, X2) -> add(active X1, X2),
               active add(s X, Y) -> mark s add(X, Y),
               active add(0(), X) -> mark X,
                     active dbl X -> dbl active X,
                   active dbl s X -> mark s s dbl X,
                   active dbl 0() -> mark 0(),
             active first(X1, X2) -> first(X1, active X2),
             active first(X1, X2) -> first(active X1, X2),
    active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
             active first(0(), X) -> mark nil(),
                 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),
                       dbl mark X -> mark dbl X,
                         dbl ok X -> ok dbl X,
               first(X1, mark X2) -> mark first(X1, X2),
               first(mark X1, X2) -> mark first(X1, X2),
              first(ok X1, ok X2) -> ok first(X1, X2),
              proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper recip X -> recip proper X,
                     proper sqr X -> sqr proper X,
                   proper terms X -> terms proper X,
                       proper s X -> s proper X,
                       proper 0() -> ok 0(),
               proper add(X1, X2) -> add(proper X1, proper X2),
                     proper dbl X -> dbl proper X,
                     proper nil() -> ok nil(),
             proper first(X1, X2) -> first(proper X1, proper X2),
                          a(x, y) -> x,
                          a(x, y) -> y}
   EDG:
    {
     (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# dbl s X -> s# s dbl X, s# ok X -> s# X)
     (active# recip X -> recip# active X, recip# ok X -> recip# X)
     (active# recip X -> recip# active X, recip# mark X -> recip# X)
     (active# terms X -> terms# active X, terms# ok X -> terms# X)
     (active# terms X -> terms# active X, terms# mark X -> terms# X)
     (active# dbl s X -> s# dbl X, s# ok X -> s# X)
     (proper# sqr X -> sqr# proper X, sqr# ok X -> sqr# X)
     (proper# sqr X -> sqr# proper X, sqr# mark X -> sqr# X)
     (proper# s X -> s# proper X, s# ok X -> s# 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# terms N -> recip# sqr N, recip# ok X -> recip# X)
     (active# terms N -> recip# sqr N, recip# mark X -> recip# X)
     (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))
     (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
     (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
     (active# terms N -> cons#(recip sqr N, terms s N), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# terms N -> cons#(recip sqr N, terms s N), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
     (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
     (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
     (active# add(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
     (active# add(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
     (active# add(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# add(X1, X2) -> active# X1, active# dbl X -> active# X)
     (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X1, active# terms X -> active# X)
     (active# add(X1, X2) -> active# X1, active# terms X -> terms# active X)
     (active# add(X1, X2) -> active# X1, active# terms N -> s# N)
     (active# add(X1, X2) -> active# X1, active# terms N -> terms# s N)
     (active# add(X1, X2) -> active# X1, active# terms N -> sqr# N)
     (active# add(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
     (active# add(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
     (active# add(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
     (active# add(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
     (active# add(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
     (active# add(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
     (active# add(X1, X2) -> active# X1, active# sqr X -> active# X)
     (active# add(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
     (active# add(X1, X2) -> active# X1, active# recip X -> active# X)
     (active# add(X1, X2) -> active# X1, active# recip X -> recip# 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))
     (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# terms X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# recip X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# first(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# terms X -> proper# X)
     (proper# first(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
     (proper# first(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# recip X -> proper# X)
     (proper# first(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
     (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (recip# ok X -> recip# X, recip# ok X -> recip# X)
     (recip# ok X -> recip# X, recip# mark X -> recip# X)
     (sqr# ok X -> sqr# X, sqr# ok X -> sqr# X)
     (sqr# ok X -> sqr# X, sqr# mark X -> sqr# X)
     (terms# ok X -> terms# X, terms# ok X -> terms# X)
     (terms# ok X -> terms# X, terms# mark X -> terms# X)
     (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# recip X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (active# recip X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (active# recip X -> active# X, active# first(X1, X2) -> active# X2)
     (active# recip X -> active# X, active# first(X1, X2) -> active# X1)
     (active# recip X -> active# X, active# dbl s X -> dbl# X)
     (active# recip X -> active# X, active# dbl s X -> s# dbl X)
     (active# recip X -> active# X, active# dbl s X -> s# s dbl X)
     (active# recip X -> active# X, active# dbl X -> dbl# active X)
     (active# recip X -> active# X, active# dbl X -> active# X)
     (active# recip X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# recip X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# recip X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# recip X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# recip X -> active# X, active# add(X1, X2) -> active# X2)
     (active# recip X -> active# X, active# add(X1, X2) -> active# X1)
     (active# recip X -> active# X, active# terms X -> active# X)
     (active# recip X -> active# X, active# terms X -> terms# active X)
     (active# recip X -> active# X, active# terms N -> s# N)
     (active# recip X -> active# X, active# terms N -> terms# s N)
     (active# recip X -> active# X, active# terms N -> sqr# N)
     (active# recip X -> active# X, active# terms N -> recip# sqr N)
     (active# recip X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
     (active# recip X -> active# X, active# sqr s X -> dbl# X)
     (active# recip X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
     (active# recip X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
     (active# recip X -> active# X, active# sqr s X -> sqr# X)
     (active# recip X -> active# X, active# sqr X -> active# X)
     (active# recip X -> active# X, active# sqr X -> sqr# active X)
     (active# recip X -> active# X, active# recip X -> active# X)
     (active# recip X -> active# X, active# recip X -> recip# active X)
     (active# recip X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# recip X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# sqr s X -> sqr# X, sqr# ok X -> sqr# X)
     (active# sqr s X -> sqr# X, sqr# mark X -> sqr# X)
     (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# terms X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (active# terms X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (active# terms X -> active# X, active# first(X1, X2) -> active# X2)
     (active# terms X -> active# X, active# first(X1, X2) -> active# X1)
     (active# terms X -> active# X, active# dbl s X -> dbl# X)
     (active# terms X -> active# X, active# dbl s X -> s# dbl X)
     (active# terms X -> active# X, active# dbl s X -> s# s dbl X)
     (active# terms X -> active# X, active# dbl X -> dbl# active X)
     (active# terms X -> active# X, active# dbl X -> active# X)
     (active# terms X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# terms X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# terms X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# terms X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# terms X -> active# X, active# add(X1, X2) -> active# X2)
     (active# terms X -> active# X, active# add(X1, X2) -> active# X1)
     (active# terms X -> active# X, active# terms X -> active# X)
     (active# terms X -> active# X, active# terms X -> terms# active X)
     (active# terms X -> active# X, active# terms N -> s# N)
     (active# terms X -> active# X, active# terms N -> terms# s N)
     (active# terms X -> active# X, active# terms N -> sqr# N)
     (active# terms X -> active# X, active# terms N -> recip# sqr N)
     (active# terms X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
     (active# terms X -> active# X, active# sqr s X -> dbl# X)
     (active# terms X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
     (active# terms X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
     (active# terms X -> active# X, active# sqr s X -> sqr# X)
     (active# terms X -> active# X, active# sqr X -> active# X)
     (active# terms X -> active# X, active# sqr X -> sqr# active X)
     (active# terms X -> active# X, active# recip X -> active# X)
     (active# terms X -> active# X, active# recip X -> recip# active X)
     (active# terms X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# terms X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# dbl s X -> dbl# X, dbl# ok X -> dbl# X)
     (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
     (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
     (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
     (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# sqr X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# sqr X -> proper# X, proper# dbl X -> proper# X)
     (proper# sqr X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# sqr X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# sqr X -> proper# X, proper# s X -> proper# X)
     (proper# sqr X -> proper# X, proper# s X -> s# proper X)
     (proper# sqr X -> proper# X, proper# terms X -> proper# X)
     (proper# sqr X -> proper# X, proper# terms X -> terms# proper X)
     (proper# sqr X -> proper# X, proper# sqr X -> proper# X)
     (proper# sqr X -> proper# X, proper# sqr X -> sqr# proper X)
     (proper# sqr X -> proper# X, proper# recip X -> proper# X)
     (proper# sqr X -> proper# X, proper# recip X -> recip# proper X)
     (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# sqr X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# dbl X -> proper# X)
     (proper# s X -> proper# X, proper# dbl X -> dbl# 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# s X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# terms X -> proper# X)
     (proper# s X -> proper# X, proper# terms X -> terms# proper X)
     (proper# s X -> proper# X, proper# sqr X -> proper# X)
     (proper# s X -> proper# X, proper# sqr X -> sqr# proper X)
     (proper# s X -> proper# X, proper# recip X -> proper# X)
     (proper# s X -> proper# X, proper# recip X -> recip# 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))
     (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# dbl X -> proper# X)
     (top# mark X -> proper# X, proper# dbl X -> dbl# proper X)
     (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# terms X -> proper# X)
     (top# mark X -> proper# X, proper# terms X -> terms# proper X)
     (top# mark X -> proper# X, proper# sqr X -> proper# X)
     (top# mark X -> proper# X, proper# sqr X -> sqr# proper X)
     (top# mark X -> proper# X, proper# recip X -> proper# X)
     (top# mark X -> proper# X, proper# recip X -> recip# proper X)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
     (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(X1, active X2), add#(mark X1, X2) -> add#(X1, X2))
     (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
     (proper# 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))
     (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
     (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
     (active# terms N -> s# N, s# ok X -> s# X)
     (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
     (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
     (active# first(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
     (active# first(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
     (active# first(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
     (active# first(X1, X2) -> active# X2, active# dbl X -> active# X)
     (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
     (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
     (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
     (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
     (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
     (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X2, active# terms X -> active# X)
     (active# first(X1, X2) -> active# X2, active# terms X -> terms# active X)
     (active# first(X1, X2) -> active# X2, active# terms N -> s# N)
     (active# first(X1, X2) -> active# X2, active# terms N -> terms# s N)
     (active# first(X1, X2) -> active# X2, active# terms N -> sqr# N)
     (active# first(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
     (active# first(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
     (active# first(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
     (active# first(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
     (active# first(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
     (active# first(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
     (active# first(X1, X2) -> active# X2, active# sqr X -> active# X)
     (active# first(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
     (active# first(X1, X2) -> active# X2, active# recip X -> active# X)
     (active# first(X1, X2) -> active# X2, active# recip X -> recip# active X)
     (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
     (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (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# s X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# terms X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# recip X -> proper# X)
     (proper# add(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
     (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (active# sqr s X -> s# add(sqr X, dbl X), s# ok X -> s# X)
     (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# recip X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# terms X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# first(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (proper# first(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
     (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# recip X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# terms X -> proper# X)
     (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# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
     (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# recip X -> recip# active X)
     (active# add(X1, X2) -> active# X2, active# recip X -> active# X)
     (active# add(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
     (active# add(X1, X2) -> active# X2, active# sqr X -> active# X)
     (active# add(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
     (active# add(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
     (active# add(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
     (active# add(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
     (active# add(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
     (active# add(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
     (active# add(X1, X2) -> active# X2, active# terms N -> sqr# N)
     (active# add(X1, X2) -> active# X2, active# terms N -> terms# s N)
     (active# add(X1, X2) -> active# X2, active# terms N -> s# N)
     (active# add(X1, X2) -> active# X2, active# terms X -> terms# active X)
     (active# add(X1, X2) -> active# X2, active# terms X -> active# X)
     (active# add(X1, X2) -> active# X2, active# add(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) -> add#(X1, active X2))
     (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
     (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
     (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
     (active# add(X1, X2) -> active# X2, active# dbl X -> active# X)
     (active# add(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
     (active# add(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
     (active# add(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
     (active# add(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
     (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
     (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
     (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
     (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
     (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# terms N -> sqr# N, sqr# mark X -> sqr# X)
     (active# terms N -> sqr# N, sqr# ok X -> sqr# X)
     (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))
     (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (active# sqr s X -> add#(sqr X, dbl X), add#(X1, mark X2) -> add#(X1, X2))
     (active# sqr s X -> add#(sqr X, dbl X), add#(mark X1, X2) -> add#(X1, X2))
     (active# sqr s X -> add#(sqr X, dbl X), add#(ok X1, ok X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(ok X1, ok X2) -> add#(X1, X2))
     (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# recip X -> recip# active X)
     (top# ok X -> active# X, active# recip X -> active# X)
     (top# ok X -> active# X, active# sqr X -> sqr# active X)
     (top# ok X -> active# X, active# sqr X -> active# X)
     (top# ok X -> active# X, active# sqr s X -> sqr# X)
     (top# ok X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
     (top# ok X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
     (top# ok X -> active# X, active# sqr s X -> dbl# X)
     (top# ok X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
     (top# ok X -> active# X, active# terms N -> recip# sqr N)
     (top# ok X -> active# X, active# terms N -> sqr# N)
     (top# ok X -> active# X, active# terms N -> terms# s N)
     (top# ok X -> active# X, active# terms N -> s# N)
     (top# ok X -> active# X, active# terms X -> terms# active X)
     (top# ok X -> active# X, active# terms X -> active# X)
     (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))
     (top# ok X -> active# X, active# dbl X -> active# X)
     (top# ok X -> active# X, active# dbl X -> dbl# active X)
     (top# ok X -> active# X, active# dbl s X -> s# s dbl X)
     (top# ok X -> active# X, active# dbl s X -> s# dbl X)
     (top# ok X -> active# X, active# dbl s X -> dbl# X)
     (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# recip X -> recip# proper X)
     (proper# dbl X -> proper# X, proper# recip X -> proper# X)
     (proper# dbl X -> proper# X, proper# sqr X -> sqr# proper X)
     (proper# dbl X -> proper# X, proper# sqr X -> proper# X)
     (proper# dbl X -> proper# X, proper# terms X -> terms# proper X)
     (proper# dbl X -> proper# X, proper# terms X -> proper# X)
     (proper# dbl X -> proper# X, proper# s X -> s# proper X)
     (proper# dbl X -> proper# X, proper# s X -> proper# X)
     (proper# dbl X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
     (proper# dbl X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (proper# terms X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# terms X -> proper# X, proper# recip X -> recip# proper X)
     (proper# terms X -> proper# X, proper# recip X -> proper# X)
     (proper# terms X -> proper# X, proper# sqr X -> sqr# proper X)
     (proper# terms X -> proper# X, proper# sqr X -> proper# X)
     (proper# terms X -> proper# X, proper# terms X -> terms# proper X)
     (proper# terms X -> proper# X, proper# terms X -> proper# X)
     (proper# terms X -> proper# X, proper# s X -> s# proper X)
     (proper# terms X -> proper# X, proper# s X -> proper# X)
     (proper# terms X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# terms X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# terms X -> proper# X, proper# dbl X -> proper# X)
     (proper# terms X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (proper# recip X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# recip X -> proper# X, proper# recip X -> recip# proper X)
     (proper# recip X -> proper# X, proper# recip X -> proper# X)
     (proper# recip X -> proper# X, proper# sqr X -> sqr# proper X)
     (proper# recip X -> proper# X, proper# sqr X -> proper# X)
     (proper# recip X -> proper# X, proper# terms X -> terms# proper X)
     (proper# recip X -> proper# X, proper# terms X -> proper# X)
     (proper# recip X -> proper# X, proper# s X -> s# proper X)
     (proper# recip X -> proper# X, proper# s X -> proper# X)
     (proper# recip X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
     (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X1)
     (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X2)
     (proper# recip X -> proper# X, proper# dbl X -> dbl# proper X)
     (proper# recip X -> proper# X, proper# dbl X -> proper# X)
     (proper# recip X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X1)
     (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X2)
     (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
     (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
     (active# dbl X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# dbl X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# recip X -> recip# active X)
     (active# dbl X -> active# X, active# recip X -> active# X)
     (active# dbl X -> active# X, active# sqr X -> sqr# active X)
     (active# dbl X -> active# X, active# sqr X -> active# X)
     (active# dbl X -> active# X, active# sqr s X -> sqr# X)
     (active# dbl X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
     (active# dbl X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
     (active# dbl X -> active# X, active# sqr s X -> dbl# X)
     (active# dbl X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
     (active# dbl X -> active# X, active# terms N -> recip# sqr N)
     (active# dbl X -> active# X, active# terms N -> sqr# N)
     (active# dbl X -> active# X, active# terms N -> terms# s N)
     (active# dbl X -> active# X, active# terms N -> s# N)
     (active# dbl X -> active# X, active# terms X -> terms# active X)
     (active# dbl X -> active# X, active# terms X -> active# X)
     (active# dbl X -> active# X, active# add(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# add(X1, X2) -> active# X2)
     (active# dbl X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# dbl X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# dbl X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# dbl X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# dbl X -> active# X, active# dbl X -> active# X)
     (active# dbl X -> active# X, active# dbl X -> dbl# active X)
     (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
     (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
     (active# dbl X -> active# X, active# dbl s X -> dbl# X)
     (active# dbl X -> active# X, active# first(X1, X2) -> active# X1)
     (active# dbl X -> active# X, active# first(X1, X2) -> active# X2)
     (active# dbl X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (active# dbl X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# sqr s X -> dbl# X, dbl# mark X -> dbl# X)
     (active# sqr s X -> dbl# X, dbl# ok X -> dbl# X)
     (active# sqr X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# sqr X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# sqr X -> active# X, active# recip X -> recip# active X)
     (active# sqr X -> active# X, active# recip X -> active# X)
     (active# sqr X -> active# X, active# sqr X -> sqr# active X)
     (active# sqr X -> active# X, active# sqr X -> active# X)
     (active# sqr X -> active# X, active# sqr s X -> sqr# X)
     (active# sqr X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
     (active# sqr X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
     (active# sqr X -> active# X, active# sqr s X -> dbl# X)
     (active# sqr X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
     (active# sqr X -> active# X, active# terms N -> recip# sqr N)
     (active# sqr X -> active# X, active# terms N -> sqr# N)
     (active# sqr X -> active# X, active# terms N -> terms# s N)
     (active# sqr X -> active# X, active# terms N -> s# N)
     (active# sqr X -> active# X, active# terms X -> terms# active X)
     (active# sqr X -> active# X, active# terms X -> active# X)
     (active# sqr X -> active# X, active# add(X1, X2) -> active# X1)
     (active# sqr X -> active# X, active# add(X1, X2) -> active# X2)
     (active# sqr X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
     (active# sqr X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
     (active# sqr X -> active# X, active# add(s X, Y) -> s# add(X, Y))
     (active# sqr X -> active# X, active# add(s X, Y) -> add#(X, Y))
     (active# sqr X -> active# X, active# dbl X -> active# X)
     (active# sqr X -> active# X, active# dbl X -> dbl# active X)
     (active# sqr X -> active# X, active# dbl s X -> s# s dbl X)
     (active# sqr X -> active# X, active# dbl s X -> s# dbl X)
     (active# sqr X -> active# X, active# dbl s X -> dbl# X)
     (active# sqr X -> active# X, active# first(X1, X2) -> active# X1)
     (active# sqr X -> active# X, active# first(X1, X2) -> active# X2)
     (active# sqr X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
     (active# sqr X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
     (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (s# ok X -> s# X, s# ok X -> s# X)
     (terms# mark X -> terms# X, terms# mark X -> terms# X)
     (terms# mark X -> terms# X, terms# ok X -> terms# X)
     (sqr# mark X -> sqr# X, sqr# mark X -> sqr# X)
     (sqr# mark X -> sqr# X, sqr# ok X -> sqr# X)
     (recip# mark X -> recip# X, recip# mark X -> recip# X)
     (recip# mark X -> recip# X, recip# ok X -> recip# 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# recip X -> recip# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# recip X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# terms X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# 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# add(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
     (proper# add(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
     (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
     (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
     (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
     (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X1, active# recip X -> recip# active X)
     (active# first(X1, X2) -> active# X1, active# recip X -> active# X)
     (active# first(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
     (active# first(X1, X2) -> active# X1, active# sqr X -> active# X)
     (active# first(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
     (active# first(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
     (active# first(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
     (active# first(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
     (active# first(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
     (active# first(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
     (active# first(X1, X2) -> active# X1, active# terms N -> sqr# N)
     (active# first(X1, X2) -> active# X1, active# terms N -> terms# s N)
     (active# first(X1, X2) -> active# X1, active# terms N -> s# N)
     (active# first(X1, X2) -> active# X1, active# terms X -> terms# active X)
     (active# first(X1, X2) -> active# X1, active# terms X -> active# X)
     (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
     (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     (active# first(X1, X2) -> active# X1, active# dbl X -> active# X)
     (active# first(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# first(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
     (active# first(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
     (active# first(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
     (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
     (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (active# 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# recip X -> recip# active X)
     (active# cons(X1, X2) -> active# X1, active# recip X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
     (active# cons(X1, X2) -> active# X1, active# sqr X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
     (active# cons(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
     (active# cons(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
     (active# cons(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
     (active# cons(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
     (active# cons(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
     (active# cons(X1, X2) -> active# X1, active# terms N -> sqr# N)
     (active# cons(X1, X2) -> active# X1, active# terms N -> terms# s N)
     (active# cons(X1, X2) -> active# X1, active# terms N -> s# N)
     (active# cons(X1, X2) -> active# X1, active# terms X -> terms# active X)
     (active# cons(X1, X2) -> active# X1, active# terms X -> active# X)
     (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# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
     (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
     (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
     (active# cons(X1, X2) -> active# X1, active# dbl X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
     (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
     (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
     (active# cons(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
     (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
     (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
     (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
     (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
     (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
     (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
     (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (add#(mark X1, X2) -> add#(X1, X2), add#(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))
     (active# terms N -> terms# s N, terms# mark X -> terms# X)
     (active# terms N -> terms# s N, terms# ok X -> terms# X)
     (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# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
     (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# X)
     (proper# terms X -> terms# proper X, terms# mark X -> terms# X)
     (proper# terms X -> terms# proper X, terms# ok X -> terms# X)
     (proper# recip X -> recip# proper X, recip# mark X -> recip# X)
     (proper# recip X -> recip# proper X, recip# ok X -> recip# X)
     (active# dbl X -> dbl# active X, dbl# mark X -> dbl# X)
     (active# dbl X -> dbl# active X, dbl# ok X -> dbl# X)
     (active# sqr X -> sqr# active X, sqr# mark X -> sqr# X)
     (active# sqr X -> sqr# active X, sqr# ok X -> sqr# X)
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
     (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(ok X1, ok X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
     (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
     (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))
    }
    EDG:
     {
      (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# dbl s X -> s# s dbl X, s# ok X -> s# X)
      (active# recip X -> recip# active X, recip# ok X -> recip# X)
      (active# recip X -> recip# active X, recip# mark X -> recip# X)
      (active# terms X -> terms# active X, terms# ok X -> terms# X)
      (active# terms X -> terms# active X, terms# mark X -> terms# X)
      (active# dbl s X -> s# dbl X, s# ok X -> s# X)
      (proper# sqr X -> sqr# proper X, sqr# ok X -> sqr# X)
      (proper# sqr X -> sqr# proper X, sqr# mark X -> sqr# X)
      (proper# s X -> s# proper X, s# ok X -> s# 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# terms N -> recip# sqr N, recip# ok X -> recip# X)
      (active# terms N -> recip# sqr N, recip# mark X -> recip# X)
      (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))
      (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
      (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
      (active# terms N -> cons#(recip sqr N, terms s N), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (active# terms N -> cons#(recip sqr N, terms s N), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
      (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
      (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
      (active# add(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
      (active# add(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
      (active# add(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
      (active# add(X1, X2) -> active# X1, active# dbl X -> active# X)
      (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
      (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X1, active# terms X -> active# X)
      (active# add(X1, X2) -> active# X1, active# terms X -> terms# active X)
      (active# add(X1, X2) -> active# X1, active# terms N -> s# N)
      (active# add(X1, X2) -> active# X1, active# terms N -> terms# s N)
      (active# add(X1, X2) -> active# X1, active# terms N -> sqr# N)
      (active# add(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
      (active# add(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
      (active# add(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
      (active# add(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
      (active# add(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
      (active# add(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
      (active# add(X1, X2) -> active# X1, active# sqr X -> active# X)
      (active# add(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
      (active# add(X1, X2) -> active# X1, active# recip X -> active# X)
      (active# add(X1, X2) -> active# X1, active# recip X -> recip# 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))
      (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# terms X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# recip X -> proper# X)
      (proper# cons(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
      (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
      (proper# first(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# terms X -> proper# X)
      (proper# first(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
      (proper# first(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# recip X -> proper# X)
      (proper# first(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
      (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (recip# ok X -> recip# X, recip# ok X -> recip# X)
      (recip# ok X -> recip# X, recip# mark X -> recip# X)
      (sqr# ok X -> sqr# X, sqr# ok X -> sqr# X)
      (sqr# ok X -> sqr# X, sqr# mark X -> sqr# X)
      (terms# ok X -> terms# X, terms# ok X -> terms# X)
      (terms# ok X -> terms# X, terms# mark X -> terms# X)
      (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# recip X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (active# recip X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (active# recip X -> active# X, active# first(X1, X2) -> active# X2)
      (active# recip X -> active# X, active# first(X1, X2) -> active# X1)
      (active# recip X -> active# X, active# dbl s X -> dbl# X)
      (active# recip X -> active# X, active# dbl s X -> s# dbl X)
      (active# recip X -> active# X, active# dbl s X -> s# s dbl X)
      (active# recip X -> active# X, active# dbl X -> dbl# active X)
      (active# recip X -> active# X, active# dbl X -> active# X)
      (active# recip X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# recip X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# recip X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# recip X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# recip X -> active# X, active# add(X1, X2) -> active# X2)
      (active# recip X -> active# X, active# add(X1, X2) -> active# X1)
      (active# recip X -> active# X, active# terms X -> active# X)
      (active# recip X -> active# X, active# terms X -> terms# active X)
      (active# recip X -> active# X, active# terms N -> s# N)
      (active# recip X -> active# X, active# terms N -> terms# s N)
      (active# recip X -> active# X, active# terms N -> sqr# N)
      (active# recip X -> active# X, active# terms N -> recip# sqr N)
      (active# recip X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
      (active# recip X -> active# X, active# sqr s X -> dbl# X)
      (active# recip X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
      (active# recip X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
      (active# recip X -> active# X, active# sqr s X -> sqr# X)
      (active# recip X -> active# X, active# sqr X -> active# X)
      (active# recip X -> active# X, active# sqr X -> sqr# active X)
      (active# recip X -> active# X, active# recip X -> active# X)
      (active# recip X -> active# X, active# recip X -> recip# active X)
      (active# recip X -> active# X, active# cons(X1, X2) -> active# X1)
      (active# recip X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# sqr s X -> sqr# X, sqr# ok X -> sqr# X)
      (active# sqr s X -> sqr# X, sqr# mark X -> sqr# X)
      (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# terms X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (active# terms X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (active# terms X -> active# X, active# first(X1, X2) -> active# X2)
      (active# terms X -> active# X, active# first(X1, X2) -> active# X1)
      (active# terms X -> active# X, active# dbl s X -> dbl# X)
      (active# terms X -> active# X, active# dbl s X -> s# dbl X)
      (active# terms X -> active# X, active# dbl s X -> s# s dbl X)
      (active# terms X -> active# X, active# dbl X -> dbl# active X)
      (active# terms X -> active# X, active# dbl X -> active# X)
      (active# terms X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# terms X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# terms X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# terms X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# terms X -> active# X, active# add(X1, X2) -> active# X2)
      (active# terms X -> active# X, active# add(X1, X2) -> active# X1)
      (active# terms X -> active# X, active# terms X -> active# X)
      (active# terms X -> active# X, active# terms X -> terms# active X)
      (active# terms X -> active# X, active# terms N -> s# N)
      (active# terms X -> active# X, active# terms N -> terms# s N)
      (active# terms X -> active# X, active# terms N -> sqr# N)
      (active# terms X -> active# X, active# terms N -> recip# sqr N)
      (active# terms X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
      (active# terms X -> active# X, active# sqr s X -> dbl# X)
      (active# terms X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
      (active# terms X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
      (active# terms X -> active# X, active# sqr s X -> sqr# X)
      (active# terms X -> active# X, active# sqr X -> active# X)
      (active# terms X -> active# X, active# sqr X -> sqr# active X)
      (active# terms X -> active# X, active# recip X -> active# X)
      (active# terms X -> active# X, active# recip X -> recip# active X)
      (active# terms X -> active# X, active# cons(X1, X2) -> active# X1)
      (active# terms X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# dbl s X -> dbl# X, dbl# ok X -> dbl# X)
      (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
      (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
      (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
      (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# sqr X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# sqr X -> proper# X, proper# dbl X -> proper# X)
      (proper# sqr X -> proper# X, proper# dbl X -> dbl# proper X)
      (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# sqr X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# sqr X -> proper# X, proper# s X -> proper# X)
      (proper# sqr X -> proper# X, proper# s X -> s# proper X)
      (proper# sqr X -> proper# X, proper# terms X -> proper# X)
      (proper# sqr X -> proper# X, proper# terms X -> terms# proper X)
      (proper# sqr X -> proper# X, proper# sqr X -> proper# X)
      (proper# sqr X -> proper# X, proper# sqr X -> sqr# proper X)
      (proper# sqr X -> proper# X, proper# recip X -> proper# X)
      (proper# sqr X -> proper# X, proper# recip X -> recip# proper X)
      (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (proper# sqr X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# dbl X -> proper# X)
      (proper# s X -> proper# X, proper# dbl X -> dbl# 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# s X -> proper# X)
      (proper# s X -> proper# X, proper# s X -> s# proper X)
      (proper# s X -> proper# X, proper# terms X -> proper# X)
      (proper# s X -> proper# X, proper# terms X -> terms# proper X)
      (proper# s X -> proper# X, proper# sqr X -> proper# X)
      (proper# s X -> proper# X, proper# sqr X -> sqr# proper X)
      (proper# s X -> proper# X, proper# recip X -> proper# X)
      (proper# s X -> proper# X, proper# recip X -> recip# 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))
      (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# dbl X -> proper# X)
      (top# mark X -> proper# X, proper# dbl X -> dbl# proper X)
      (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# s X -> proper# X)
      (top# mark X -> proper# X, proper# s X -> s# proper X)
      (top# mark X -> proper# X, proper# terms X -> proper# X)
      (top# mark X -> proper# X, proper# terms X -> terms# proper X)
      (top# mark X -> proper# X, proper# sqr X -> proper# X)
      (top# mark X -> proper# X, proper# sqr X -> sqr# proper X)
      (top# mark X -> proper# X, proper# recip X -> proper# X)
      (top# mark X -> proper# X, proper# recip X -> recip# proper X)
      (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
      (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
      (active# add(X1, X2) -> add#(X1, active X2), add#(mark X1, X2) -> add#(X1, X2))
      (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
      (proper# 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))
      (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
      (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
      (active# terms N -> s# N, s# ok X -> s# X)
      (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
      (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
      (active# first(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
      (active# first(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
      (active# first(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
      (active# first(X1, X2) -> active# X2, active# dbl X -> active# X)
      (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
      (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
      (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
      (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
      (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
      (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X2, active# terms X -> active# X)
      (active# first(X1, X2) -> active# X2, active# terms X -> terms# active X)
      (active# first(X1, X2) -> active# X2, active# terms N -> s# N)
      (active# first(X1, X2) -> active# X2, active# terms N -> terms# s N)
      (active# first(X1, X2) -> active# X2, active# terms N -> sqr# N)
      (active# first(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
      (active# first(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
      (active# first(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
      (active# first(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
      (active# first(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
      (active# first(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
      (active# first(X1, X2) -> active# X2, active# sqr X -> active# X)
      (active# first(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
      (active# first(X1, X2) -> active# X2, active# recip X -> active# X)
      (active# first(X1, X2) -> active# X2, active# recip X -> recip# active X)
      (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
      (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
      (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# add(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
      (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# s X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# terms X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# recip X -> proper# X)
      (proper# add(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
      (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
      (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (active# sqr s X -> s# add(sqr X, dbl X), s# ok X -> s# X)
      (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# recip X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# terms X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
      (proper# first(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
      (proper# first(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
      (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
      (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
      (proper# cons(X1, X2) -> proper# X2, proper# recip X -> proper# X)
      (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
      (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
      (proper# cons(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
      (proper# cons(X1, X2) -> proper# X2, proper# terms X -> proper# X)
      (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# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
      (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
      (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
      (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
      (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
      (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# recip X -> recip# active X)
      (active# add(X1, X2) -> active# X2, active# recip X -> active# X)
      (active# add(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
      (active# add(X1, X2) -> active# X2, active# sqr X -> active# X)
      (active# add(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
      (active# add(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
      (active# add(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
      (active# add(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
      (active# add(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
      (active# add(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
      (active# add(X1, X2) -> active# X2, active# terms N -> sqr# N)
      (active# add(X1, X2) -> active# X2, active# terms N -> terms# s N)
      (active# add(X1, X2) -> active# X2, active# terms N -> s# N)
      (active# add(X1, X2) -> active# X2, active# terms X -> terms# active X)
      (active# add(X1, X2) -> active# X2, active# terms X -> active# X)
      (active# add(X1, X2) -> active# X2, active# add(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) -> add#(X1, active X2))
      (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
      (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
      (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
      (active# add(X1, X2) -> active# X2, active# dbl X -> active# X)
      (active# add(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
      (active# add(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
      (active# add(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
      (active# add(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
      (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
      (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
      (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
      (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
      (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# terms N -> sqr# N, sqr# mark X -> sqr# X)
      (active# terms N -> sqr# N, sqr# ok X -> sqr# X)
      (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))
      (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (active# sqr s X -> add#(sqr X, dbl X), add#(X1, mark X2) -> add#(X1, X2))
      (active# sqr s X -> add#(sqr X, dbl X), add#(mark X1, X2) -> add#(X1, X2))
      (active# sqr s X -> add#(sqr X, dbl X), add#(ok X1, ok X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(ok X1, ok X2) -> add#(X1, X2))
      (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# recip X -> recip# active X)
      (top# ok X -> active# X, active# recip X -> active# X)
      (top# ok X -> active# X, active# sqr X -> sqr# active X)
      (top# ok X -> active# X, active# sqr X -> active# X)
      (top# ok X -> active# X, active# sqr s X -> sqr# X)
      (top# ok X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
      (top# ok X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
      (top# ok X -> active# X, active# sqr s X -> dbl# X)
      (top# ok X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
      (top# ok X -> active# X, active# terms N -> recip# sqr N)
      (top# ok X -> active# X, active# terms N -> sqr# N)
      (top# ok X -> active# X, active# terms N -> terms# s N)
      (top# ok X -> active# X, active# terms N -> s# N)
      (top# ok X -> active# X, active# terms X -> terms# active X)
      (top# ok X -> active# X, active# terms X -> active# X)
      (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))
      (top# ok X -> active# X, active# dbl X -> active# X)
      (top# ok X -> active# X, active# dbl X -> dbl# active X)
      (top# ok X -> active# X, active# dbl s X -> s# s dbl X)
      (top# ok X -> active# X, active# dbl s X -> s# dbl X)
      (top# ok X -> active# X, active# dbl s X -> dbl# X)
      (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (proper# dbl X -> proper# X, proper# recip X -> recip# proper X)
      (proper# dbl X -> proper# X, proper# recip X -> proper# X)
      (proper# dbl X -> proper# X, proper# sqr X -> sqr# proper X)
      (proper# dbl X -> proper# X, proper# sqr X -> proper# X)
      (proper# dbl X -> proper# X, proper# terms X -> terms# proper X)
      (proper# dbl X -> proper# X, proper# terms X -> proper# X)
      (proper# dbl X -> proper# X, proper# s X -> s# proper X)
      (proper# dbl X -> proper# X, proper# s X -> proper# X)
      (proper# dbl X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
      (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
      (proper# dbl X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (proper# terms X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (proper# terms X -> proper# X, proper# recip X -> recip# proper X)
      (proper# terms X -> proper# X, proper# recip X -> proper# X)
      (proper# terms X -> proper# X, proper# sqr X -> sqr# proper X)
      (proper# terms X -> proper# X, proper# sqr X -> proper# X)
      (proper# terms X -> proper# X, proper# terms X -> terms# proper X)
      (proper# terms X -> proper# X, proper# terms X -> proper# X)
      (proper# terms X -> proper# X, proper# s X -> s# proper X)
      (proper# terms X -> proper# X, proper# s X -> proper# X)
      (proper# terms X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# terms X -> proper# X, proper# dbl X -> dbl# proper X)
      (proper# terms X -> proper# X, proper# dbl X -> proper# X)
      (proper# terms X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (proper# recip X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
      (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X1)
      (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X2)
      (proper# recip X -> proper# X, proper# recip X -> recip# proper X)
      (proper# recip X -> proper# X, proper# recip X -> proper# X)
      (proper# recip X -> proper# X, proper# sqr X -> sqr# proper X)
      (proper# recip X -> proper# X, proper# sqr X -> proper# X)
      (proper# recip X -> proper# X, proper# terms X -> terms# proper X)
      (proper# recip X -> proper# X, proper# terms X -> proper# X)
      (proper# recip X -> proper# X, proper# s X -> s# proper X)
      (proper# recip X -> proper# X, proper# s X -> proper# X)
      (proper# recip X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
      (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X1)
      (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X2)
      (proper# recip X -> proper# X, proper# dbl X -> dbl# proper X)
      (proper# recip X -> proper# X, proper# dbl X -> proper# X)
      (proper# recip X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X1)
      (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X2)
      (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
      (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
      (active# dbl X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# dbl X -> active# X, active# cons(X1, X2) -> active# X1)
      (active# dbl X -> active# X, active# recip X -> recip# active X)
      (active# dbl X -> active# X, active# recip X -> active# X)
      (active# dbl X -> active# X, active# sqr X -> sqr# active X)
      (active# dbl X -> active# X, active# sqr X -> active# X)
      (active# dbl X -> active# X, active# sqr s X -> sqr# X)
      (active# dbl X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
      (active# dbl X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
      (active# dbl X -> active# X, active# sqr s X -> dbl# X)
      (active# dbl X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
      (active# dbl X -> active# X, active# terms N -> recip# sqr N)
      (active# dbl X -> active# X, active# terms N -> sqr# N)
      (active# dbl X -> active# X, active# terms N -> terms# s N)
      (active# dbl X -> active# X, active# terms N -> s# N)
      (active# dbl X -> active# X, active# terms X -> terms# active X)
      (active# dbl X -> active# X, active# terms X -> active# X)
      (active# dbl X -> active# X, active# add(X1, X2) -> active# X1)
      (active# dbl X -> active# X, active# add(X1, X2) -> active# X2)
      (active# dbl X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# dbl X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# dbl X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# dbl X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# dbl X -> active# X, active# dbl X -> active# X)
      (active# dbl X -> active# X, active# dbl X -> dbl# active X)
      (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
      (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
      (active# dbl X -> active# X, active# dbl s X -> dbl# X)
      (active# dbl X -> active# X, active# first(X1, X2) -> active# X1)
      (active# dbl X -> active# X, active# first(X1, X2) -> active# X2)
      (active# dbl X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (active# dbl X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# sqr s X -> dbl# X, dbl# mark X -> dbl# X)
      (active# sqr s X -> dbl# X, dbl# ok X -> dbl# X)
      (active# sqr X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# sqr X -> active# X, active# cons(X1, X2) -> active# X1)
      (active# sqr X -> active# X, active# recip X -> recip# active X)
      (active# sqr X -> active# X, active# recip X -> active# X)
      (active# sqr X -> active# X, active# sqr X -> sqr# active X)
      (active# sqr X -> active# X, active# sqr X -> active# X)
      (active# sqr X -> active# X, active# sqr s X -> sqr# X)
      (active# sqr X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
      (active# sqr X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
      (active# sqr X -> active# X, active# sqr s X -> dbl# X)
      (active# sqr X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
      (active# sqr X -> active# X, active# terms N -> recip# sqr N)
      (active# sqr X -> active# X, active# terms N -> sqr# N)
      (active# sqr X -> active# X, active# terms N -> terms# s N)
      (active# sqr X -> active# X, active# terms N -> s# N)
      (active# sqr X -> active# X, active# terms X -> terms# active X)
      (active# sqr X -> active# X, active# terms X -> active# X)
      (active# sqr X -> active# X, active# add(X1, X2) -> active# X1)
      (active# sqr X -> active# X, active# add(X1, X2) -> active# X2)
      (active# sqr X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
      (active# sqr X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
      (active# sqr X -> active# X, active# add(s X, Y) -> s# add(X, Y))
      (active# sqr X -> active# X, active# add(s X, Y) -> add#(X, Y))
      (active# sqr X -> active# X, active# dbl X -> active# X)
      (active# sqr X -> active# X, active# dbl X -> dbl# active X)
      (active# sqr X -> active# X, active# dbl s X -> s# s dbl X)
      (active# sqr X -> active# X, active# dbl s X -> s# dbl X)
      (active# sqr X -> active# X, active# dbl s X -> dbl# X)
      (active# sqr X -> active# X, active# first(X1, X2) -> active# X1)
      (active# sqr X -> active# X, active# first(X1, X2) -> active# X2)
      (active# sqr X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
      (active# sqr X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
      (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (s# ok X -> s# X, s# ok X -> s# X)
      (terms# mark X -> terms# X, terms# mark X -> terms# X)
      (terms# mark X -> terms# X, terms# ok X -> terms# X)
      (sqr# mark X -> sqr# X, sqr# mark X -> sqr# X)
      (sqr# mark X -> sqr# X, sqr# ok X -> sqr# X)
      (recip# mark X -> recip# X, recip# mark X -> recip# X)
      (recip# mark X -> recip# X, recip# ok X -> recip# 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# recip X -> recip# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# recip X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# terms X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# 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# add(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
      (proper# add(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
      (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
      (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
      (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
      (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
      (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X1, active# recip X -> recip# active X)
      (active# first(X1, X2) -> active# X1, active# recip X -> active# X)
      (active# first(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
      (active# first(X1, X2) -> active# X1, active# sqr X -> active# X)
      (active# first(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
      (active# first(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
      (active# first(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
      (active# first(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
      (active# first(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
      (active# first(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
      (active# first(X1, X2) -> active# X1, active# terms N -> sqr# N)
      (active# first(X1, X2) -> active# X1, active# terms N -> terms# s N)
      (active# first(X1, X2) -> active# X1, active# terms N -> s# N)
      (active# first(X1, X2) -> active# X1, active# terms X -> terms# active X)
      (active# first(X1, X2) -> active# X1, active# terms X -> active# X)
      (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
      (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
      (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
      (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
      (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
      (active# first(X1, X2) -> active# X1, active# dbl X -> active# X)
      (active# first(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
      (active# first(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
      (active# first(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
      (active# first(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
      (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
      (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (active# 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# recip X -> recip# active X)
      (active# cons(X1, X2) -> active# X1, active# recip X -> active# X)
      (active# cons(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
      (active# cons(X1, X2) -> active# X1, active# sqr X -> active# X)
      (active# cons(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
      (active# cons(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
      (active# cons(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
      (active# cons(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
      (active# cons(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
      (active# cons(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
      (active# cons(X1, X2) -> active# X1, active# terms N -> sqr# N)
      (active# cons(X1, X2) -> active# X1, active# terms N -> terms# s N)
      (active# cons(X1, X2) -> active# X1, active# terms N -> s# N)
      (active# cons(X1, X2) -> active# X1, active# terms X -> terms# active X)
      (active# cons(X1, X2) -> active# X1, active# terms X -> active# X)
      (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# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
      (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
      (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
      (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
      (active# cons(X1, X2) -> active# X1, active# dbl X -> active# X)
      (active# cons(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
      (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
      (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
      (active# cons(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
      (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
      (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
      (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
      (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
      (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
      (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
      (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
      (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (add#(mark X1, X2) -> add#(X1, X2), add#(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))
      (active# terms N -> terms# s N, terms# mark X -> terms# X)
      (active# terms N -> terms# s N, terms# ok X -> terms# X)
      (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# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
      (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# X)
      (proper# terms X -> terms# proper X, terms# mark X -> terms# X)
      (proper# terms X -> terms# proper X, terms# ok X -> terms# X)
      (proper# recip X -> recip# proper X, recip# mark X -> recip# X)
      (proper# recip X -> recip# proper X, recip# ok X -> recip# X)
      (active# dbl X -> dbl# active X, dbl# mark X -> dbl# X)
      (active# dbl X -> dbl# active X, dbl# ok X -> dbl# X)
      (active# sqr X -> sqr# active X, sqr# mark X -> sqr# X)
      (active# sqr X -> sqr# active X, sqr# ok X -> sqr# X)
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
      (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(ok X1, ok X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
      (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
      (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))
     }
     EDG:
      {
       (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# dbl s X -> s# s dbl X, s# ok X -> s# X)
       (active# recip X -> recip# active X, recip# ok X -> recip# X)
       (active# recip X -> recip# active X, recip# mark X -> recip# X)
       (active# terms X -> terms# active X, terms# ok X -> terms# X)
       (active# terms X -> terms# active X, terms# mark X -> terms# X)
       (active# dbl s X -> s# dbl X, s# ok X -> s# X)
       (proper# sqr X -> sqr# proper X, sqr# ok X -> sqr# X)
       (proper# sqr X -> sqr# proper X, sqr# mark X -> sqr# X)
       (proper# s X -> s# proper X, s# ok X -> s# 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# terms N -> recip# sqr N, recip# ok X -> recip# X)
       (active# terms N -> recip# sqr N, recip# mark X -> recip# X)
       (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))
       (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
       (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
       (active# terms N -> cons#(recip sqr N, terms s N), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (active# terms N -> cons#(recip sqr N, terms s N), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
       (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
       (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
       (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
       (active# add(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
       (active# add(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
       (active# add(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
       (active# add(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
       (active# add(X1, X2) -> active# X1, active# dbl X -> active# X)
       (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
       (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
       (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
       (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
       (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
       (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
       (active# add(X1, X2) -> active# X1, active# terms X -> active# X)
       (active# add(X1, X2) -> active# X1, active# terms X -> terms# active X)
       (active# add(X1, X2) -> active# X1, active# terms N -> s# N)
       (active# add(X1, X2) -> active# X1, active# terms N -> terms# s N)
       (active# add(X1, X2) -> active# X1, active# terms N -> sqr# N)
       (active# add(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
       (active# add(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
       (active# add(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
       (active# add(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
       (active# add(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
       (active# add(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
       (active# add(X1, X2) -> active# X1, active# sqr X -> active# X)
       (active# add(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
       (active# add(X1, X2) -> active# X1, active# recip X -> active# X)
       (active# add(X1, X2) -> active# X1, active# recip X -> recip# 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))
       (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# terms X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# recip X -> proper# X)
       (proper# cons(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
       (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
       (proper# first(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
       (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# terms X -> proper# X)
       (proper# first(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
       (proper# first(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# recip X -> proper# X)
       (proper# first(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
       (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (recip# ok X -> recip# X, recip# ok X -> recip# X)
       (recip# ok X -> recip# X, recip# mark X -> recip# X)
       (sqr# ok X -> sqr# X, sqr# ok X -> sqr# X)
       (sqr# ok X -> sqr# X, sqr# mark X -> sqr# X)
       (terms# ok X -> terms# X, terms# ok X -> terms# X)
       (terms# ok X -> terms# X, terms# mark X -> terms# X)
       (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# recip X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (active# recip X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (active# recip X -> active# X, active# first(X1, X2) -> active# X2)
       (active# recip X -> active# X, active# first(X1, X2) -> active# X1)
       (active# recip X -> active# X, active# dbl s X -> dbl# X)
       (active# recip X -> active# X, active# dbl s X -> s# dbl X)
       (active# recip X -> active# X, active# dbl s X -> s# s dbl X)
       (active# recip X -> active# X, active# dbl X -> dbl# active X)
       (active# recip X -> active# X, active# dbl X -> active# X)
       (active# recip X -> active# X, active# add(s X, Y) -> add#(X, Y))
       (active# recip X -> active# X, active# add(s X, Y) -> s# add(X, Y))
       (active# recip X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
       (active# recip X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
       (active# recip X -> active# X, active# add(X1, X2) -> active# X2)
       (active# recip X -> active# X, active# add(X1, X2) -> active# X1)
       (active# recip X -> active# X, active# terms X -> active# X)
       (active# recip X -> active# X, active# terms X -> terms# active X)
       (active# recip X -> active# X, active# terms N -> s# N)
       (active# recip X -> active# X, active# terms N -> terms# s N)
       (active# recip X -> active# X, active# terms N -> sqr# N)
       (active# recip X -> active# X, active# terms N -> recip# sqr N)
       (active# recip X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
       (active# recip X -> active# X, active# sqr s X -> dbl# X)
       (active# recip X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
       (active# recip X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
       (active# recip X -> active# X, active# sqr s X -> sqr# X)
       (active# recip X -> active# X, active# sqr X -> active# X)
       (active# recip X -> active# X, active# sqr X -> sqr# active X)
       (active# recip X -> active# X, active# recip X -> active# X)
       (active# recip X -> active# X, active# recip X -> recip# active X)
       (active# recip X -> active# X, active# cons(X1, X2) -> active# X1)
       (active# recip X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# sqr s X -> sqr# X, sqr# ok X -> sqr# X)
       (active# sqr s X -> sqr# X, sqr# mark X -> sqr# X)
       (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# terms X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (active# terms X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (active# terms X -> active# X, active# first(X1, X2) -> active# X2)
       (active# terms X -> active# X, active# first(X1, X2) -> active# X1)
       (active# terms X -> active# X, active# dbl s X -> dbl# X)
       (active# terms X -> active# X, active# dbl s X -> s# dbl X)
       (active# terms X -> active# X, active# dbl s X -> s# s dbl X)
       (active# terms X -> active# X, active# dbl X -> dbl# active X)
       (active# terms X -> active# X, active# dbl X -> active# X)
       (active# terms X -> active# X, active# add(s X, Y) -> add#(X, Y))
       (active# terms X -> active# X, active# add(s X, Y) -> s# add(X, Y))
       (active# terms X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
       (active# terms X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
       (active# terms X -> active# X, active# add(X1, X2) -> active# X2)
       (active# terms X -> active# X, active# add(X1, X2) -> active# X1)
       (active# terms X -> active# X, active# terms X -> active# X)
       (active# terms X -> active# X, active# terms X -> terms# active X)
       (active# terms X -> active# X, active# terms N -> s# N)
       (active# terms X -> active# X, active# terms N -> terms# s N)
       (active# terms X -> active# X, active# terms N -> sqr# N)
       (active# terms X -> active# X, active# terms N -> recip# sqr N)
       (active# terms X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
       (active# terms X -> active# X, active# sqr s X -> dbl# X)
       (active# terms X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
       (active# terms X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
       (active# terms X -> active# X, active# sqr s X -> sqr# X)
       (active# terms X -> active# X, active# sqr X -> active# X)
       (active# terms X -> active# X, active# sqr X -> sqr# active X)
       (active# terms X -> active# X, active# recip X -> active# X)
       (active# terms X -> active# X, active# recip X -> recip# active X)
       (active# terms X -> active# X, active# cons(X1, X2) -> active# X1)
       (active# terms X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# dbl s X -> dbl# X, dbl# ok X -> dbl# X)
       (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
       (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
       (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
       (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# sqr X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# sqr X -> proper# X, proper# dbl X -> proper# X)
       (proper# sqr X -> proper# X, proper# dbl X -> dbl# proper X)
       (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X2)
       (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X1)
       (proper# sqr X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# sqr X -> proper# X, proper# s X -> proper# X)
       (proper# sqr X -> proper# X, proper# s X -> s# proper X)
       (proper# sqr X -> proper# X, proper# terms X -> proper# X)
       (proper# sqr X -> proper# X, proper# terms X -> terms# proper X)
       (proper# sqr X -> proper# X, proper# sqr X -> proper# X)
       (proper# sqr X -> proper# X, proper# sqr X -> sqr# proper X)
       (proper# sqr X -> proper# X, proper# recip X -> proper# X)
       (proper# sqr X -> proper# X, proper# recip X -> recip# proper X)
       (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (proper# sqr X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# s X -> proper# X, proper# dbl X -> proper# X)
       (proper# s X -> proper# X, proper# dbl X -> dbl# 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# s X -> proper# X)
       (proper# s X -> proper# X, proper# s X -> s# proper X)
       (proper# s X -> proper# X, proper# terms X -> proper# X)
       (proper# s X -> proper# X, proper# terms X -> terms# proper X)
       (proper# s X -> proper# X, proper# sqr X -> proper# X)
       (proper# s X -> proper# X, proper# sqr X -> sqr# proper X)
       (proper# s X -> proper# X, proper# recip X -> proper# X)
       (proper# s X -> proper# X, proper# recip X -> recip# 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))
       (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (top# mark X -> proper# X, proper# dbl X -> proper# X)
       (top# mark X -> proper# X, proper# dbl X -> dbl# proper X)
       (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
       (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
       (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (top# mark X -> proper# X, proper# s X -> proper# X)
       (top# mark X -> proper# X, proper# s X -> s# proper X)
       (top# mark X -> proper# X, proper# terms X -> proper# X)
       (top# mark X -> proper# X, proper# terms X -> terms# proper X)
       (top# mark X -> proper# X, proper# sqr X -> proper# X)
       (top# mark X -> proper# X, proper# sqr X -> sqr# proper X)
       (top# mark X -> proper# X, proper# recip X -> proper# X)
       (top# mark X -> proper# X, proper# recip X -> recip# proper X)
       (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
       (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
       (active# add(X1, X2) -> add#(X1, active X2), add#(mark X1, X2) -> add#(X1, X2))
       (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
       (proper# 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))
       (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
       (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
       (active# terms N -> s# N, s# ok X -> s# X)
       (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
       (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
       (active# first(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
       (active# first(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
       (active# first(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
       (active# first(X1, X2) -> active# X2, active# dbl X -> active# X)
       (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
       (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
       (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
       (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
       (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
       (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X2, active# terms X -> active# X)
       (active# first(X1, X2) -> active# X2, active# terms X -> terms# active X)
       (active# first(X1, X2) -> active# X2, active# terms N -> s# N)
       (active# first(X1, X2) -> active# X2, active# terms N -> terms# s N)
       (active# first(X1, X2) -> active# X2, active# terms N -> sqr# N)
       (active# first(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
       (active# first(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
       (active# first(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
       (active# first(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
       (active# first(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
       (active# first(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
       (active# first(X1, X2) -> active# X2, active# sqr X -> active# X)
       (active# first(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
       (active# first(X1, X2) -> active# X2, active# recip X -> active# X)
       (active# first(X1, X2) -> active# X2, active# recip X -> recip# active X)
       (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
       (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
       (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
       (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# add(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
       (proper# add(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
       (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# s X -> proper# X)
       (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
       (proper# add(X1, X2) -> proper# X2, proper# terms X -> proper# X)
       (proper# add(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
       (proper# add(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
       (proper# add(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
       (proper# add(X1, X2) -> proper# X2, proper# recip X -> proper# X)
       (proper# add(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
       (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
       (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
       (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (active# sqr s X -> s# add(sqr X, dbl X), s# ok X -> s# X)
       (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# recip X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# terms X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
       (proper# first(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
       (proper# first(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
       (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
       (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
       (proper# cons(X1, X2) -> proper# X2, proper# recip X -> proper# X)
       (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
       (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
       (proper# cons(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
       (proper# cons(X1, X2) -> proper# X2, proper# terms X -> proper# X)
       (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# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
       (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
       (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
       (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
       (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
       (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# recip X -> recip# active X)
       (active# add(X1, X2) -> active# X2, active# recip X -> active# X)
       (active# add(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
       (active# add(X1, X2) -> active# X2, active# sqr X -> active# X)
       (active# add(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
       (active# add(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
       (active# add(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
       (active# add(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
       (active# add(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
       (active# add(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
       (active# add(X1, X2) -> active# X2, active# terms N -> sqr# N)
       (active# add(X1, X2) -> active# X2, active# terms N -> terms# s N)
       (active# add(X1, X2) -> active# X2, active# terms N -> s# N)
       (active# add(X1, X2) -> active# X2, active# terms X -> terms# active X)
       (active# add(X1, X2) -> active# X2, active# terms X -> active# X)
       (active# add(X1, X2) -> active# X2, active# add(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) -> add#(X1, active X2))
       (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
       (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
       (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
       (active# add(X1, X2) -> active# X2, active# dbl X -> active# X)
       (active# add(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
       (active# add(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
       (active# add(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
       (active# add(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
       (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
       (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
       (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
       (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
       (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# terms N -> sqr# N, sqr# mark X -> sqr# X)
       (active# terms N -> sqr# N, sqr# ok X -> sqr# X)
       (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))
       (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (active# sqr s X -> add#(sqr X, dbl X), add#(X1, mark X2) -> add#(X1, X2))
       (active# sqr s X -> add#(sqr X, dbl X), add#(mark X1, X2) -> add#(X1, X2))
       (active# sqr s X -> add#(sqr X, dbl X), add#(ok X1, ok X2) -> add#(X1, X2))
       (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
       (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
       (active# add(s X, Y) -> add#(X, Y), add#(ok X1, ok X2) -> add#(X1, X2))
       (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# recip X -> recip# active X)
       (top# ok X -> active# X, active# recip X -> active# X)
       (top# ok X -> active# X, active# sqr X -> sqr# active X)
       (top# ok X -> active# X, active# sqr X -> active# X)
       (top# ok X -> active# X, active# sqr s X -> sqr# X)
       (top# ok X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
       (top# ok X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
       (top# ok X -> active# X, active# sqr s X -> dbl# X)
       (top# ok X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
       (top# ok X -> active# X, active# terms N -> recip# sqr N)
       (top# ok X -> active# X, active# terms N -> sqr# N)
       (top# ok X -> active# X, active# terms N -> terms# s N)
       (top# ok X -> active# X, active# terms N -> s# N)
       (top# ok X -> active# X, active# terms X -> terms# active X)
       (top# ok X -> active# X, active# terms X -> active# X)
       (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))
       (top# ok X -> active# X, active# dbl X -> active# X)
       (top# ok X -> active# X, active# dbl X -> dbl# active X)
       (top# ok X -> active# X, active# dbl s X -> s# s dbl X)
       (top# ok X -> active# X, active# dbl s X -> s# dbl X)
       (top# ok X -> active# X, active# dbl s X -> dbl# X)
       (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
       (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
       (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (proper# dbl X -> proper# X, proper# recip X -> recip# proper X)
       (proper# dbl X -> proper# X, proper# recip X -> proper# X)
       (proper# dbl X -> proper# X, proper# sqr X -> sqr# proper X)
       (proper# dbl X -> proper# X, proper# sqr X -> proper# X)
       (proper# dbl X -> proper# X, proper# terms X -> terms# proper X)
       (proper# dbl X -> proper# X, proper# terms X -> proper# X)
       (proper# dbl X -> proper# X, proper# s X -> s# proper X)
       (proper# dbl X -> proper# X, proper# s X -> proper# X)
       (proper# dbl X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X1)
       (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X2)
       (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
       (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
       (proper# dbl X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (proper# terms X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (proper# terms X -> proper# X, proper# recip X -> recip# proper X)
       (proper# terms X -> proper# X, proper# recip X -> proper# X)
       (proper# terms X -> proper# X, proper# sqr X -> sqr# proper X)
       (proper# terms X -> proper# X, proper# sqr X -> proper# X)
       (proper# terms X -> proper# X, proper# terms X -> terms# proper X)
       (proper# terms X -> proper# X, proper# terms X -> proper# X)
       (proper# terms X -> proper# X, proper# s X -> s# proper X)
       (proper# terms X -> proper# X, proper# s X -> proper# X)
       (proper# terms X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X1)
       (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X2)
       (proper# terms X -> proper# X, proper# dbl X -> dbl# proper X)
       (proper# terms X -> proper# X, proper# dbl X -> proper# X)
       (proper# terms X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (proper# recip X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
       (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X1)
       (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X2)
       (proper# recip X -> proper# X, proper# recip X -> recip# proper X)
       (proper# recip X -> proper# X, proper# recip X -> proper# X)
       (proper# recip X -> proper# X, proper# sqr X -> sqr# proper X)
       (proper# recip X -> proper# X, proper# sqr X -> proper# X)
       (proper# recip X -> proper# X, proper# terms X -> terms# proper X)
       (proper# recip X -> proper# X, proper# terms X -> proper# X)
       (proper# recip X -> proper# X, proper# s X -> s# proper X)
       (proper# recip X -> proper# X, proper# s X -> proper# X)
       (proper# recip X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
       (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X1)
       (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X2)
       (proper# recip X -> proper# X, proper# dbl X -> dbl# proper X)
       (proper# recip X -> proper# X, proper# dbl X -> proper# X)
       (proper# recip X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X1)
       (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X2)
       (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
       (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
       (active# dbl X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# dbl X -> active# X, active# cons(X1, X2) -> active# X1)
       (active# dbl X -> active# X, active# recip X -> recip# active X)
       (active# dbl X -> active# X, active# recip X -> active# X)
       (active# dbl X -> active# X, active# sqr X -> sqr# active X)
       (active# dbl X -> active# X, active# sqr X -> active# X)
       (active# dbl X -> active# X, active# sqr s X -> sqr# X)
       (active# dbl X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
       (active# dbl X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
       (active# dbl X -> active# X, active# sqr s X -> dbl# X)
       (active# dbl X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
       (active# dbl X -> active# X, active# terms N -> recip# sqr N)
       (active# dbl X -> active# X, active# terms N -> sqr# N)
       (active# dbl X -> active# X, active# terms N -> terms# s N)
       (active# dbl X -> active# X, active# terms N -> s# N)
       (active# dbl X -> active# X, active# terms X -> terms# active X)
       (active# dbl X -> active# X, active# terms X -> active# X)
       (active# dbl X -> active# X, active# add(X1, X2) -> active# X1)
       (active# dbl X -> active# X, active# add(X1, X2) -> active# X2)
       (active# dbl X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
       (active# dbl X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
       (active# dbl X -> active# X, active# add(s X, Y) -> s# add(X, Y))
       (active# dbl X -> active# X, active# add(s X, Y) -> add#(X, Y))
       (active# dbl X -> active# X, active# dbl X -> active# X)
       (active# dbl X -> active# X, active# dbl X -> dbl# active X)
       (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
       (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
       (active# dbl X -> active# X, active# dbl s X -> dbl# X)
       (active# dbl X -> active# X, active# first(X1, X2) -> active# X1)
       (active# dbl X -> active# X, active# first(X1, X2) -> active# X2)
       (active# dbl X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (active# dbl X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# sqr s X -> dbl# X, dbl# mark X -> dbl# X)
       (active# sqr s X -> dbl# X, dbl# ok X -> dbl# X)
       (active# sqr X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# sqr X -> active# X, active# cons(X1, X2) -> active# X1)
       (active# sqr X -> active# X, active# recip X -> recip# active X)
       (active# sqr X -> active# X, active# recip X -> active# X)
       (active# sqr X -> active# X, active# sqr X -> sqr# active X)
       (active# sqr X -> active# X, active# sqr X -> active# X)
       (active# sqr X -> active# X, active# sqr s X -> sqr# X)
       (active# sqr X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
       (active# sqr X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
       (active# sqr X -> active# X, active# sqr s X -> dbl# X)
       (active# sqr X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
       (active# sqr X -> active# X, active# terms N -> recip# sqr N)
       (active# sqr X -> active# X, active# terms N -> sqr# N)
       (active# sqr X -> active# X, active# terms N -> terms# s N)
       (active# sqr X -> active# X, active# terms N -> s# N)
       (active# sqr X -> active# X, active# terms X -> terms# active X)
       (active# sqr X -> active# X, active# terms X -> active# X)
       (active# sqr X -> active# X, active# add(X1, X2) -> active# X1)
       (active# sqr X -> active# X, active# add(X1, X2) -> active# X2)
       (active# sqr X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
       (active# sqr X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
       (active# sqr X -> active# X, active# add(s X, Y) -> s# add(X, Y))
       (active# sqr X -> active# X, active# add(s X, Y) -> add#(X, Y))
       (active# sqr X -> active# X, active# dbl X -> active# X)
       (active# sqr X -> active# X, active# dbl X -> dbl# active X)
       (active# sqr X -> active# X, active# dbl s X -> s# s dbl X)
       (active# sqr X -> active# X, active# dbl s X -> s# dbl X)
       (active# sqr X -> active# X, active# dbl s X -> dbl# X)
       (active# sqr X -> active# X, active# first(X1, X2) -> active# X1)
       (active# sqr X -> active# X, active# first(X1, X2) -> active# X2)
       (active# sqr X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
       (active# sqr X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
       (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (s# ok X -> s# X, s# ok X -> s# X)
       (terms# mark X -> terms# X, terms# mark X -> terms# X)
       (terms# mark X -> terms# X, terms# ok X -> terms# X)
       (sqr# mark X -> sqr# X, sqr# mark X -> sqr# X)
       (sqr# mark X -> sqr# X, sqr# ok X -> sqr# X)
       (recip# mark X -> recip# X, recip# mark X -> recip# X)
       (recip# mark X -> recip# X, recip# ok X -> recip# 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# recip X -> recip# proper X)
       (proper# add(X1, X2) -> proper# X1, proper# recip X -> proper# X)
       (proper# add(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
       (proper# add(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
       (proper# add(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
       (proper# add(X1, X2) -> proper# X1, proper# terms X -> proper# X)
       (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
       (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
       (proper# add(X1, X2) -> proper# X1, proper# 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# add(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
       (proper# add(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
       (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
       (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
       (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
       (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
       (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X1, active# recip X -> recip# active X)
       (active# first(X1, X2) -> active# X1, active# recip X -> active# X)
       (active# first(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
       (active# first(X1, X2) -> active# X1, active# sqr X -> active# X)
       (active# first(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
       (active# first(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
       (active# first(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
       (active# first(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
       (active# first(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
       (active# first(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
       (active# first(X1, X2) -> active# X1, active# terms N -> sqr# N)
       (active# first(X1, X2) -> active# X1, active# terms N -> terms# s N)
       (active# first(X1, X2) -> active# X1, active# terms N -> s# N)
       (active# first(X1, X2) -> active# X1, active# terms X -> terms# active X)
       (active# first(X1, X2) -> active# X1, active# terms X -> active# X)
       (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
       (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
       (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
       (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
       (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
       (active# first(X1, X2) -> active# X1, active# dbl X -> active# X)
       (active# first(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
       (active# first(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
       (active# first(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
       (active# first(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
       (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
       (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (active# 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# recip X -> recip# active X)
       (active# cons(X1, X2) -> active# X1, active# recip X -> active# X)
       (active# cons(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
       (active# cons(X1, X2) -> active# X1, active# sqr X -> active# X)
       (active# cons(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
       (active# cons(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
       (active# cons(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
       (active# cons(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
       (active# cons(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
       (active# cons(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
       (active# cons(X1, X2) -> active# X1, active# terms N -> sqr# N)
       (active# cons(X1, X2) -> active# X1, active# terms N -> terms# s N)
       (active# cons(X1, X2) -> active# X1, active# terms N -> s# N)
       (active# cons(X1, X2) -> active# X1, active# terms X -> terms# active X)
       (active# cons(X1, X2) -> active# X1, active# terms X -> active# X)
       (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# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
       (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
       (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
       (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
       (active# cons(X1, X2) -> active# X1, active# dbl X -> active# X)
       (active# cons(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
       (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
       (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
       (active# cons(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
       (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
       (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
       (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
       (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
       (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
       (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
       (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
       (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (add#(mark X1, X2) -> add#(X1, X2), add#(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))
       (active# terms N -> terms# s N, terms# ok X -> terms# X)
       (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# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
       (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# X)
       (proper# terms X -> terms# proper X, terms# mark X -> terms# X)
       (proper# terms X -> terms# proper X, terms# ok X -> terms# X)
       (proper# recip X -> recip# proper X, recip# mark X -> recip# X)
       (proper# recip X -> recip# proper X, recip# ok X -> recip# X)
       (active# dbl X -> dbl# active X, dbl# mark X -> dbl# X)
       (active# dbl X -> dbl# active X, dbl# ok X -> dbl# X)
       (active# sqr X -> sqr# active X, sqr# mark X -> sqr# X)
       (active# sqr X -> sqr# active X, sqr# ok X -> sqr# X)
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
       (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(ok X1, ok X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
       (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
       (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))
      }
      EDG:
       {
        (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# dbl s X -> s# s dbl X, s# ok X -> s# X)
        (active# recip X -> recip# active X, recip# ok X -> recip# X)
        (active# recip X -> recip# active X, recip# mark X -> recip# X)
        (active# terms X -> terms# active X, terms# ok X -> terms# X)
        (active# terms X -> terms# active X, terms# mark X -> terms# X)
        (active# dbl s X -> s# dbl X, s# ok X -> s# X)
        (proper# sqr X -> sqr# proper X, sqr# ok X -> sqr# X)
        (proper# sqr X -> sqr# proper X, sqr# mark X -> sqr# X)
        (proper# s X -> s# proper X, s# ok X -> s# 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# terms N -> recip# sqr N, recip# ok X -> recip# X)
        (active# terms N -> recip# sqr N, recip# mark X -> recip# X)
        (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))
        (first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
        (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
        (active# terms N -> cons#(recip sqr N, terms s N), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (active# terms N -> cons#(recip sqr N, terms s N), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# add(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
        (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
        (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
        (active# add(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
        (active# add(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
        (active# add(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
        (active# add(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
        (active# add(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
        (active# add(X1, X2) -> active# X1, active# dbl X -> active# X)
        (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
        (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
        (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
        (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
        (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
        (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
        (active# add(X1, X2) -> active# X1, active# terms X -> active# X)
        (active# add(X1, X2) -> active# X1, active# terms X -> terms# active X)
        (active# add(X1, X2) -> active# X1, active# terms N -> s# N)
        (active# add(X1, X2) -> active# X1, active# terms N -> terms# s N)
        (active# add(X1, X2) -> active# X1, active# terms N -> sqr# N)
        (active# add(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
        (active# add(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
        (active# add(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
        (active# add(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
        (active# add(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
        (active# add(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
        (active# add(X1, X2) -> active# X1, active# sqr X -> active# X)
        (active# add(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
        (active# add(X1, X2) -> active# X1, active# recip X -> active# X)
        (active# add(X1, X2) -> active# X1, active# recip X -> recip# 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))
        (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# terms X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# recip X -> proper# X)
        (proper# cons(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
        (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
        (proper# first(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
        (proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# terms X -> proper# X)
        (proper# first(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
        (proper# first(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# recip X -> proper# X)
        (proper# first(X1, X2) -> proper# X1, proper# recip X -> recip# proper X)
        (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (recip# ok X -> recip# X, recip# ok X -> recip# X)
        (recip# ok X -> recip# X, recip# mark X -> recip# X)
        (sqr# ok X -> sqr# X, sqr# ok X -> sqr# X)
        (sqr# ok X -> sqr# X, sqr# mark X -> sqr# X)
        (terms# ok X -> terms# X, terms# ok X -> terms# X)
        (terms# ok X -> terms# X, terms# mark X -> terms# X)
        (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# recip X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# recip X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (active# recip X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (active# recip X -> active# X, active# first(X1, X2) -> active# X2)
        (active# recip X -> active# X, active# first(X1, X2) -> active# X1)
        (active# recip X -> active# X, active# dbl s X -> dbl# X)
        (active# recip X -> active# X, active# dbl s X -> s# dbl X)
        (active# recip X -> active# X, active# dbl s X -> s# s dbl X)
        (active# recip X -> active# X, active# dbl X -> dbl# active X)
        (active# recip X -> active# X, active# dbl X -> active# X)
        (active# recip X -> active# X, active# add(s X, Y) -> add#(X, Y))
        (active# recip X -> active# X, active# add(s X, Y) -> s# add(X, Y))
        (active# recip X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
        (active# recip X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
        (active# recip X -> active# X, active# add(X1, X2) -> active# X2)
        (active# recip X -> active# X, active# add(X1, X2) -> active# X1)
        (active# recip X -> active# X, active# terms X -> active# X)
        (active# recip X -> active# X, active# terms X -> terms# active X)
        (active# recip X -> active# X, active# terms N -> s# N)
        (active# recip X -> active# X, active# terms N -> terms# s N)
        (active# recip X -> active# X, active# terms N -> sqr# N)
        (active# recip X -> active# X, active# terms N -> recip# sqr N)
        (active# recip X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
        (active# recip X -> active# X, active# sqr s X -> dbl# X)
        (active# recip X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
        (active# recip X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
        (active# recip X -> active# X, active# sqr s X -> sqr# X)
        (active# recip X -> active# X, active# sqr X -> active# X)
        (active# recip X -> active# X, active# sqr X -> sqr# active X)
        (active# recip X -> active# X, active# recip X -> active# X)
        (active# recip X -> active# X, active# recip X -> recip# active X)
        (active# recip X -> active# X, active# cons(X1, X2) -> active# X1)
        (active# recip X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# sqr s X -> sqr# X, sqr# ok X -> sqr# X)
        (active# sqr s X -> sqr# X, sqr# mark X -> sqr# X)
        (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# terms X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# terms X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (active# terms X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (active# terms X -> active# X, active# first(X1, X2) -> active# X2)
        (active# terms X -> active# X, active# first(X1, X2) -> active# X1)
        (active# terms X -> active# X, active# dbl s X -> dbl# X)
        (active# terms X -> active# X, active# dbl s X -> s# dbl X)
        (active# terms X -> active# X, active# dbl s X -> s# s dbl X)
        (active# terms X -> active# X, active# dbl X -> dbl# active X)
        (active# terms X -> active# X, active# dbl X -> active# X)
        (active# terms X -> active# X, active# add(s X, Y) -> add#(X, Y))
        (active# terms X -> active# X, active# add(s X, Y) -> s# add(X, Y))
        (active# terms X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
        (active# terms X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
        (active# terms X -> active# X, active# add(X1, X2) -> active# X2)
        (active# terms X -> active# X, active# add(X1, X2) -> active# X1)
        (active# terms X -> active# X, active# terms X -> active# X)
        (active# terms X -> active# X, active# terms X -> terms# active X)
        (active# terms X -> active# X, active# terms N -> s# N)
        (active# terms X -> active# X, active# terms N -> terms# s N)
        (active# terms X -> active# X, active# terms N -> sqr# N)
        (active# terms X -> active# X, active# terms N -> recip# sqr N)
        (active# terms X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
        (active# terms X -> active# X, active# sqr s X -> dbl# X)
        (active# terms X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
        (active# terms X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
        (active# terms X -> active# X, active# sqr s X -> sqr# X)
        (active# terms X -> active# X, active# sqr X -> active# X)
        (active# terms X -> active# X, active# sqr X -> sqr# active X)
        (active# terms X -> active# X, active# recip X -> active# X)
        (active# terms X -> active# X, active# recip X -> recip# active X)
        (active# terms X -> active# X, active# cons(X1, X2) -> active# X1)
        (active# terms X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# dbl s X -> dbl# X, dbl# ok X -> dbl# X)
        (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X)
        (dbl# ok X -> dbl# X, dbl# ok X -> dbl# X)
        (dbl# ok X -> dbl# X, dbl# mark X -> dbl# X)
        (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (proper# sqr X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# sqr X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# sqr X -> proper# X, proper# dbl X -> proper# X)
        (proper# sqr X -> proper# X, proper# dbl X -> dbl# proper X)
        (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X2)
        (proper# sqr X -> proper# X, proper# add(X1, X2) -> proper# X1)
        (proper# sqr X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# sqr X -> proper# X, proper# s X -> proper# X)
        (proper# sqr X -> proper# X, proper# s X -> s# proper X)
        (proper# sqr X -> proper# X, proper# terms X -> proper# X)
        (proper# sqr X -> proper# X, proper# terms X -> terms# proper X)
        (proper# sqr X -> proper# X, proper# sqr X -> proper# X)
        (proper# sqr X -> proper# X, proper# sqr X -> sqr# proper X)
        (proper# sqr X -> proper# X, proper# recip X -> proper# X)
        (proper# sqr X -> proper# X, proper# recip X -> recip# proper X)
        (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (proper# sqr X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (proper# sqr X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# s X -> proper# X, proper# dbl X -> proper# X)
        (proper# s X -> proper# X, proper# dbl X -> dbl# 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# s X -> proper# X)
        (proper# s X -> proper# X, proper# s X -> s# proper X)
        (proper# s X -> proper# X, proper# terms X -> proper# X)
        (proper# s X -> proper# X, proper# terms X -> terms# proper X)
        (proper# s X -> proper# X, proper# sqr X -> proper# X)
        (proper# s X -> proper# X, proper# sqr X -> sqr# proper X)
        (proper# s X -> proper# X, proper# recip X -> proper# X)
        (proper# s X -> proper# X, proper# recip X -> recip# 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))
        (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (top# mark X -> proper# X, proper# dbl X -> proper# X)
        (top# mark X -> proper# X, proper# dbl X -> dbl# proper X)
        (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
        (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
        (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (top# mark X -> proper# X, proper# s X -> proper# X)
        (top# mark X -> proper# X, proper# s X -> s# proper X)
        (top# mark X -> proper# X, proper# terms X -> proper# X)
        (top# mark X -> proper# X, proper# terms X -> terms# proper X)
        (top# mark X -> proper# X, proper# sqr X -> proper# X)
        (top# mark X -> proper# X, proper# sqr X -> sqr# proper X)
        (top# mark X -> proper# X, proper# recip X -> proper# X)
        (top# mark X -> proper# X, proper# recip X -> recip# proper X)
        (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
        (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
        (active# add(X1, X2) -> add#(X1, active X2), add#(mark X1, X2) -> add#(X1, X2))
        (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
        (proper# 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))
        (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
        (proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
        (active# terms N -> s# N, s# ok X -> s# X)
        (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
        (active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
        (active# first(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
        (active# first(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
        (active# first(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
        (active# first(X1, X2) -> active# X2, active# dbl X -> active# X)
        (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
        (active# first(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
        (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
        (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
        (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
        (active# first(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X2, active# terms X -> active# X)
        (active# first(X1, X2) -> active# X2, active# terms X -> terms# active X)
        (active# first(X1, X2) -> active# X2, active# terms N -> s# N)
        (active# first(X1, X2) -> active# X2, active# terms N -> terms# s N)
        (active# first(X1, X2) -> active# X2, active# terms N -> sqr# N)
        (active# first(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
        (active# first(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
        (active# first(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
        (active# first(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
        (active# first(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
        (active# first(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
        (active# first(X1, X2) -> active# X2, active# sqr X -> active# X)
        (active# first(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
        (active# first(X1, X2) -> active# X2, active# recip X -> active# X)
        (active# first(X1, X2) -> active# X2, active# recip X -> recip# active X)
        (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
        (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
        (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
        (proper# add(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# add(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
        (proper# add(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
        (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# s X -> proper# X)
        (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
        (proper# add(X1, X2) -> proper# X2, proper# terms X -> proper# X)
        (proper# add(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
        (proper# add(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
        (proper# add(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
        (proper# add(X1, X2) -> proper# X2, proper# recip X -> proper# X)
        (proper# add(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
        (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
        (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
        (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (active# sqr s X -> s# add(sqr X, dbl X), s# ok X -> s# X)
        (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# recip X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# terms X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
        (proper# first(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
        (proper# first(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
        (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
        (proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X2, proper# recip X -> recip# proper X)
        (proper# cons(X1, X2) -> proper# X2, proper# recip X -> proper# X)
        (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> sqr# proper X)
        (proper# cons(X1, X2) -> proper# X2, proper# sqr X -> proper# X)
        (proper# cons(X1, X2) -> proper# X2, proper# terms X -> terms# proper X)
        (proper# cons(X1, X2) -> proper# X2, proper# terms X -> proper# X)
        (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# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
        (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> dbl# proper X)
        (proper# cons(X1, X2) -> proper# X2, proper# dbl X -> proper# X)
        (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
        (proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
        (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# recip X -> recip# active X)
        (active# add(X1, X2) -> active# X2, active# recip X -> active# X)
        (active# add(X1, X2) -> active# X2, active# sqr X -> sqr# active X)
        (active# add(X1, X2) -> active# X2, active# sqr X -> active# X)
        (active# add(X1, X2) -> active# X2, active# sqr s X -> sqr# X)
        (active# add(X1, X2) -> active# X2, active# sqr s X -> s# add(sqr X, dbl X))
        (active# add(X1, X2) -> active# X2, active# sqr s X -> add#(sqr X, dbl X))
        (active# add(X1, X2) -> active# X2, active# sqr s X -> dbl# X)
        (active# add(X1, X2) -> active# X2, active# terms N -> cons#(recip sqr N, terms s N))
        (active# add(X1, X2) -> active# X2, active# terms N -> recip# sqr N)
        (active# add(X1, X2) -> active# X2, active# terms N -> sqr# N)
        (active# add(X1, X2) -> active# X2, active# terms N -> terms# s N)
        (active# add(X1, X2) -> active# X2, active# terms N -> s# N)
        (active# add(X1, X2) -> active# X2, active# terms X -> terms# active X)
        (active# add(X1, X2) -> active# X2, active# terms X -> active# X)
        (active# add(X1, X2) -> active# X2, active# add(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) -> add#(X1, active X2))
        (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
        (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
        (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
        (active# add(X1, X2) -> active# X2, active# dbl X -> active# X)
        (active# add(X1, X2) -> active# X2, active# dbl X -> dbl# active X)
        (active# add(X1, X2) -> active# X2, active# dbl s X -> s# s dbl X)
        (active# add(X1, X2) -> active# X2, active# dbl s X -> s# dbl X)
        (active# add(X1, X2) -> active# X2, active# dbl s X -> dbl# X)
        (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
        (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
        (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
        (active# add(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
        (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# add(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# terms N -> sqr# N, sqr# mark X -> sqr# X)
        (active# terms N -> sqr# N, sqr# ok X -> sqr# X)
        (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))
        (active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (active# sqr s X -> add#(sqr X, dbl X), add#(X1, mark X2) -> add#(X1, X2))
        (active# sqr s X -> add#(sqr X, dbl X), add#(mark X1, X2) -> add#(X1, X2))
        (active# sqr s X -> add#(sqr X, dbl X), add#(ok X1, ok X2) -> add#(X1, X2))
        (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2))
        (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2))
        (active# add(s X, Y) -> add#(X, Y), add#(ok X1, ok X2) -> add#(X1, X2))
        (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# recip X -> recip# active X)
        (top# ok X -> active# X, active# recip X -> active# X)
        (top# ok X -> active# X, active# sqr X -> sqr# active X)
        (top# ok X -> active# X, active# sqr X -> active# X)
        (top# ok X -> active# X, active# sqr s X -> sqr# X)
        (top# ok X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
        (top# ok X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
        (top# ok X -> active# X, active# sqr s X -> dbl# X)
        (top# ok X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
        (top# ok X -> active# X, active# terms N -> recip# sqr N)
        (top# ok X -> active# X, active# terms N -> sqr# N)
        (top# ok X -> active# X, active# terms N -> terms# s N)
        (top# ok X -> active# X, active# terms N -> s# N)
        (top# ok X -> active# X, active# terms X -> terms# active X)
        (top# ok X -> active# X, active# terms X -> active# X)
        (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))
        (top# ok X -> active# X, active# dbl X -> active# X)
        (top# ok X -> active# X, active# dbl X -> dbl# active X)
        (top# ok X -> active# X, active# dbl s X -> s# s dbl X)
        (top# ok X -> active# X, active# dbl s X -> s# dbl X)
        (top# ok X -> active# X, active# dbl s X -> dbl# X)
        (top# ok X -> active# X, active# first(X1, X2) -> active# X1)
        (top# ok X -> active# X, active# first(X1, X2) -> active# X2)
        (top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (proper# dbl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (proper# dbl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (proper# dbl X -> proper# X, proper# recip X -> recip# proper X)
        (proper# dbl X -> proper# X, proper# recip X -> proper# X)
        (proper# dbl X -> proper# X, proper# sqr X -> sqr# proper X)
        (proper# dbl X -> proper# X, proper# sqr X -> proper# X)
        (proper# dbl X -> proper# X, proper# terms X -> terms# proper X)
        (proper# dbl X -> proper# X, proper# terms X -> proper# X)
        (proper# dbl X -> proper# X, proper# s X -> s# proper X)
        (proper# dbl X -> proper# X, proper# s X -> proper# X)
        (proper# dbl X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X1)
        (proper# dbl X -> proper# X, proper# add(X1, X2) -> proper# X2)
        (proper# dbl X -> proper# X, proper# dbl X -> dbl# proper X)
        (proper# dbl X -> proper# X, proper# dbl X -> proper# X)
        (proper# dbl X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# dbl X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (proper# terms X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (proper# terms X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (proper# terms X -> proper# X, proper# recip X -> recip# proper X)
        (proper# terms X -> proper# X, proper# recip X -> proper# X)
        (proper# terms X -> proper# X, proper# sqr X -> sqr# proper X)
        (proper# terms X -> proper# X, proper# sqr X -> proper# X)
        (proper# terms X -> proper# X, proper# terms X -> terms# proper X)
        (proper# terms X -> proper# X, proper# terms X -> proper# X)
        (proper# terms X -> proper# X, proper# s X -> s# proper X)
        (proper# terms X -> proper# X, proper# s X -> proper# X)
        (proper# terms X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X1)
        (proper# terms X -> proper# X, proper# add(X1, X2) -> proper# X2)
        (proper# terms X -> proper# X, proper# dbl X -> dbl# proper X)
        (proper# terms X -> proper# X, proper# dbl X -> proper# X)
        (proper# terms X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# terms X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (proper# recip X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
        (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X1)
        (proper# recip X -> proper# X, proper# cons(X1, X2) -> proper# X2)
        (proper# recip X -> proper# X, proper# recip X -> recip# proper X)
        (proper# recip X -> proper# X, proper# recip X -> proper# X)
        (proper# recip X -> proper# X, proper# sqr X -> sqr# proper X)
        (proper# recip X -> proper# X, proper# sqr X -> proper# X)
        (proper# recip X -> proper# X, proper# terms X -> terms# proper X)
        (proper# recip X -> proper# X, proper# terms X -> proper# X)
        (proper# recip X -> proper# X, proper# s X -> s# proper X)
        (proper# recip X -> proper# X, proper# s X -> proper# X)
        (proper# recip X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
        (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X1)
        (proper# recip X -> proper# X, proper# add(X1, X2) -> proper# X2)
        (proper# recip X -> proper# X, proper# dbl X -> dbl# proper X)
        (proper# recip X -> proper# X, proper# dbl X -> proper# X)
        (proper# recip X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X1)
        (proper# recip X -> proper# X, proper# first(X1, X2) -> proper# X2)
        (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X)
        (dbl# mark X -> dbl# X, dbl# ok X -> dbl# X)
        (active# dbl X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# dbl X -> active# X, active# cons(X1, X2) -> active# X1)
        (active# dbl X -> active# X, active# recip X -> recip# active X)
        (active# dbl X -> active# X, active# recip X -> active# X)
        (active# dbl X -> active# X, active# sqr X -> sqr# active X)
        (active# dbl X -> active# X, active# sqr X -> active# X)
        (active# dbl X -> active# X, active# sqr s X -> sqr# X)
        (active# dbl X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
        (active# dbl X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
        (active# dbl X -> active# X, active# sqr s X -> dbl# X)
        (active# dbl X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
        (active# dbl X -> active# X, active# terms N -> recip# sqr N)
        (active# dbl X -> active# X, active# terms N -> sqr# N)
        (active# dbl X -> active# X, active# terms N -> terms# s N)
        (active# dbl X -> active# X, active# terms N -> s# N)
        (active# dbl X -> active# X, active# terms X -> terms# active X)
        (active# dbl X -> active# X, active# terms X -> active# X)
        (active# dbl X -> active# X, active# add(X1, X2) -> active# X1)
        (active# dbl X -> active# X, active# add(X1, X2) -> active# X2)
        (active# dbl X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
        (active# dbl X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
        (active# dbl X -> active# X, active# add(s X, Y) -> s# add(X, Y))
        (active# dbl X -> active# X, active# add(s X, Y) -> add#(X, Y))
        (active# dbl X -> active# X, active# dbl X -> active# X)
        (active# dbl X -> active# X, active# dbl X -> dbl# active X)
        (active# dbl X -> active# X, active# dbl s X -> s# s dbl X)
        (active# dbl X -> active# X, active# dbl s X -> s# dbl X)
        (active# dbl X -> active# X, active# dbl s X -> dbl# X)
        (active# dbl X -> active# X, active# first(X1, X2) -> active# X1)
        (active# dbl X -> active# X, active# first(X1, X2) -> active# X2)
        (active# dbl X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (active# dbl X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# dbl X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# sqr s X -> dbl# X, dbl# mark X -> dbl# X)
        (active# sqr s X -> dbl# X, dbl# ok X -> dbl# X)
        (active# sqr X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# sqr X -> active# X, active# cons(X1, X2) -> active# X1)
        (active# sqr X -> active# X, active# recip X -> recip# active X)
        (active# sqr X -> active# X, active# recip X -> active# X)
        (active# sqr X -> active# X, active# sqr X -> sqr# active X)
        (active# sqr X -> active# X, active# sqr X -> active# X)
        (active# sqr X -> active# X, active# sqr s X -> sqr# X)
        (active# sqr X -> active# X, active# sqr s X -> s# add(sqr X, dbl X))
        (active# sqr X -> active# X, active# sqr s X -> add#(sqr X, dbl X))
        (active# sqr X -> active# X, active# sqr s X -> dbl# X)
        (active# sqr X -> active# X, active# terms N -> cons#(recip sqr N, terms s N))
        (active# sqr X -> active# X, active# terms N -> recip# sqr N)
        (active# sqr X -> active# X, active# terms N -> sqr# N)
        (active# sqr X -> active# X, active# terms N -> terms# s N)
        (active# sqr X -> active# X, active# terms N -> s# N)
        (active# sqr X -> active# X, active# terms X -> terms# active X)
        (active# sqr X -> active# X, active# terms X -> active# X)
        (active# sqr X -> active# X, active# add(X1, X2) -> active# X1)
        (active# sqr X -> active# X, active# add(X1, X2) -> active# X2)
        (active# sqr X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
        (active# sqr X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
        (active# sqr X -> active# X, active# add(s X, Y) -> s# add(X, Y))
        (active# sqr X -> active# X, active# add(s X, Y) -> add#(X, Y))
        (active# sqr X -> active# X, active# dbl X -> active# X)
        (active# sqr X -> active# X, active# dbl X -> dbl# active X)
        (active# sqr X -> active# X, active# dbl s X -> s# s dbl X)
        (active# sqr X -> active# X, active# dbl s X -> s# dbl X)
        (active# sqr X -> active# X, active# dbl s X -> dbl# X)
        (active# sqr X -> active# X, active# first(X1, X2) -> active# X1)
        (active# sqr X -> active# X, active# first(X1, X2) -> active# X2)
        (active# sqr X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
        (active# sqr X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
        (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# sqr X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (s# ok X -> s# X, s# ok X -> s# X)
        (terms# mark X -> terms# X, terms# mark X -> terms# X)
        (terms# mark X -> terms# X, terms# ok X -> terms# X)
        (sqr# mark X -> sqr# X, sqr# mark X -> sqr# X)
        (sqr# mark X -> sqr# X, sqr# ok X -> sqr# X)
        (recip# mark X -> recip# X, recip# mark X -> recip# X)
        (recip# mark X -> recip# X, recip# ok X -> recip# 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# recip X -> recip# proper X)
        (proper# add(X1, X2) -> proper# X1, proper# recip X -> proper# X)
        (proper# add(X1, X2) -> proper# X1, proper# sqr X -> sqr# proper X)
        (proper# add(X1, X2) -> proper# X1, proper# sqr X -> proper# X)
        (proper# add(X1, X2) -> proper# X1, proper# terms X -> terms# proper X)
        (proper# add(X1, X2) -> proper# X1, proper# terms X -> proper# X)
        (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
        (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
        (proper# add(X1, X2) -> proper# X1, proper# 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# add(X1, X2) -> proper# X1, proper# dbl X -> dbl# proper X)
        (proper# add(X1, X2) -> proper# X1, proper# dbl X -> proper# X)
        (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
        (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
        (proper# add(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
        (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
        (active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X1, active# recip X -> recip# active X)
        (active# first(X1, X2) -> active# X1, active# recip X -> active# X)
        (active# first(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
        (active# first(X1, X2) -> active# X1, active# sqr X -> active# X)
        (active# first(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
        (active# first(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
        (active# first(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
        (active# first(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
        (active# first(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
        (active# first(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
        (active# first(X1, X2) -> active# X1, active# terms N -> sqr# N)
        (active# first(X1, X2) -> active# X1, active# terms N -> terms# s N)
        (active# first(X1, X2) -> active# X1, active# terms N -> s# N)
        (active# first(X1, X2) -> active# X1, active# terms X -> terms# active X)
        (active# first(X1, X2) -> active# X1, active# terms X -> active# X)
        (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
        (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
        (active# first(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
        (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
        (active# first(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
        (active# first(X1, X2) -> active# X1, active# dbl X -> active# X)
        (active# first(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
        (active# first(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
        (active# first(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
        (active# first(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
        (active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
        (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (active# 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# recip X -> recip# active X)
        (active# cons(X1, X2) -> active# X1, active# recip X -> active# X)
        (active# cons(X1, X2) -> active# X1, active# sqr X -> sqr# active X)
        (active# cons(X1, X2) -> active# X1, active# sqr X -> active# X)
        (active# cons(X1, X2) -> active# X1, active# sqr s X -> sqr# X)
        (active# cons(X1, X2) -> active# X1, active# sqr s X -> s# add(sqr X, dbl X))
        (active# cons(X1, X2) -> active# X1, active# sqr s X -> add#(sqr X, dbl X))
        (active# cons(X1, X2) -> active# X1, active# sqr s X -> dbl# X)
        (active# cons(X1, X2) -> active# X1, active# terms N -> cons#(recip sqr N, terms s N))
        (active# cons(X1, X2) -> active# X1, active# terms N -> recip# sqr N)
        (active# cons(X1, X2) -> active# X1, active# terms N -> sqr# N)
        (active# cons(X1, X2) -> active# X1, active# terms N -> terms# s N)
        (active# cons(X1, X2) -> active# X1, active# terms N -> s# N)
        (active# cons(X1, X2) -> active# X1, active# terms X -> terms# active X)
        (active# cons(X1, X2) -> active# X1, active# terms X -> active# X)
        (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# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
        (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
        (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
        (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
        (active# cons(X1, X2) -> active# X1, active# dbl X -> active# X)
        (active# cons(X1, X2) -> active# X1, active# dbl X -> dbl# active X)
        (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# s dbl X)
        (active# cons(X1, X2) -> active# X1, active# dbl s X -> s# dbl X)
        (active# cons(X1, X2) -> active# X1, active# dbl s X -> dbl# X)
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
        (active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
        (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
        (active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
        (first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
        (first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
        (first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
        (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
        (first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (add#(mark X1, X2) -> add#(X1, X2), add#(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))
        (active# terms N -> terms# s N, terms# ok X -> terms# X)
        (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# dbl X -> dbl# proper X, dbl# mark X -> dbl# X)
        (proper# dbl X -> dbl# proper X, dbl# ok X -> dbl# X)
        (proper# terms X -> terms# proper X, terms# mark X -> terms# X)
        (proper# terms X -> terms# proper X, terms# ok X -> terms# X)
        (proper# recip X -> recip# proper X, recip# mark X -> recip# X)
        (proper# recip X -> recip# proper X, recip# ok X -> recip# X)
        (active# dbl X -> dbl# active X, dbl# mark X -> dbl# X)
        (active# dbl X -> dbl# active X, dbl# ok X -> dbl# X)
        (active# sqr X -> sqr# active X, sqr# mark X -> sqr# X)
        (active# sqr X -> sqr# active X, sqr# ok X -> sqr# X)
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
        (active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(ok X1, ok X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
        (active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
        (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))
       }
       STATUS:
        arrows: 0.875274
        SCCS (11):
         Scc:
          {top# mark X -> top# proper X,
             top# ok X -> top# active X}
         Scc:
          { active# cons(X1, X2) -> active# X1,
                 active# recip X -> active# X,
                   active# sqr X -> active# X,
                 active# terms X -> active# X,
             active# add(X1, X2) -> active# X1,
             active# add(X1, X2) -> active# X2,
                   active# dbl X -> active# X,
           active# first(X1, X2) -> active# X1,
           active# first(X1, X2) -> active# X2}
         Scc:
          { proper# cons(X1, X2) -> proper# X1,
            proper# cons(X1, X2) -> proper# X2,
                 proper# recip X -> proper# X,
                   proper# sqr X -> proper# X,
                 proper# terms X -> proper# X,
                     proper# s X -> proper# X,
             proper# add(X1, X2) -> proper# X1,
             proper# add(X1, X2) -> proper# X2,
                   proper# dbl X -> proper# X,
           proper# first(X1, X2) -> proper# X1,
           proper# first(X1, X2) -> proper# X2}
         Scc:
          {dbl# mark X -> dbl# X,
             dbl# ok X -> dbl# X}
         Scc:
          {terms# mark X -> terms# X,
             terms# ok X -> terms# X}
         Scc:
          {sqr# mark X -> sqr# X,
             sqr# ok X -> sqr# X}
         Scc:
          {recip# mark X -> recip# X,
             recip# ok X -> recip# X}
         Scc:
          {s# ok X -> s# X}
         Scc:
          { first#(X1, mark X2) -> first#(X1, X2),
            first#(mark X1, X2) -> first#(X1, X2),
           first#(ok X1, ok X2) -> first#(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:
          { cons#(mark X1, X2) -> cons#(X1, X2),
           cons#(ok X1, ok X2) -> cons#(X1, X2)}
         
         SCC (2):
          Strict:
           {top# mark X -> top# proper X,
              top# ok X -> top# active X}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (9):
          Strict:
           { active# cons(X1, X2) -> active# X1,
                  active# recip X -> active# X,
                    active# sqr X -> active# X,
                  active# terms X -> active# X,
              active# add(X1, X2) -> active# X1,
              active# add(X1, X2) -> active# X2,
                    active# dbl X -> active# X,
            active# first(X1, X2) -> active# X1,
            active# first(X1, X2) -> active# X2}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         SCC (11):
          Strict:
           { proper# cons(X1, X2) -> proper# X1,
             proper# cons(X1, X2) -> proper# X2,
                  proper# recip X -> proper# X,
                    proper# sqr X -> proper# X,
                  proper# terms X -> proper# X,
                      proper# s X -> proper# X,
              proper# add(X1, X2) -> proper# X1,
              proper# add(X1, X2) -> proper# X2,
                    proper# dbl X -> proper# X,
            proper# first(X1, X2) -> proper# X1,
            proper# first(X1, X2) -> proper# X2}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         
         
         
         
         
         
         
         
         
         SCC (2):
          Strict:
           {dbl# mark X -> dbl# X,
              dbl# ok X -> dbl# X}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (2):
          Strict:
           {terms# mark X -> terms# X,
              terms# ok X -> terms# X}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (2):
          Strict:
           {sqr# mark X -> sqr# X,
              sqr# ok X -> sqr# X}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (2):
          Strict:
           {recip# mark X -> recip# X,
              recip# ok X -> recip# X}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         
         SCC (1):
          Strict:
           {s# ok X -> s# X}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open
         
         SCC (3):
          Strict:
           { first#(X1, mark X2) -> first#(X1, X2),
             first#(mark X1, X2) -> first#(X1, X2),
            first#(ok X1, ok X2) -> first#(X1, X2)}
          Weak:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              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:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              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:
          {            cons(mark X1, X2) -> mark cons(X1, X2),
                      cons(ok X1, ok X2) -> ok cons(X1, X2),
                            recip mark X -> mark recip X,
                              recip ok X -> ok recip X,
                              sqr mark X -> mark sqr X,
                                sqr ok X -> ok sqr X,
                            terms mark X -> mark terms X,
                              terms ok X -> ok terms X,
                                  s ok X -> ok s X,
                     active cons(X1, X2) -> cons(active X1, X2),
                          active recip X -> recip active X,
                            active sqr X -> sqr active X,
                          active sqr s X -> mark s add(sqr X, dbl X),
                          active sqr 0() -> mark 0(),
                          active terms N -> mark cons(recip sqr N, terms s N),
                          active terms X -> terms active X,
                      active add(X1, X2) -> add(X1, active X2),
                      active add(X1, X2) -> add(active X1, X2),
                      active add(s X, Y) -> mark s add(X, Y),
                      active add(0(), X) -> mark X,
                            active dbl X -> dbl active X,
                          active dbl s X -> mark s s dbl X,
                          active dbl 0() -> mark 0(),
                    active first(X1, X2) -> first(X1, active X2),
                    active first(X1, X2) -> first(active X1, X2),
           active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                    active first(0(), X) -> mark nil(),
                        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),
                              dbl mark X -> mark dbl X,
                                dbl ok X -> ok dbl X,
                      first(X1, mark X2) -> mark first(X1, X2),
                      first(mark X1, X2) -> mark first(X1, X2),
                     first(ok X1, ok X2) -> ok first(X1, X2),
                     proper cons(X1, X2) -> cons(proper X1, proper X2),
                          proper recip X -> recip proper X,
                            proper sqr X -> sqr proper X,
                          proper terms X -> terms proper X,
                              proper s X -> s proper X,
                              proper 0() -> ok 0(),
                      proper add(X1, X2) -> add(proper X1, proper X2),
                            proper dbl X -> dbl proper X,
                            proper nil() -> ok nil(),
                    proper first(X1, X2) -> first(proper X1, proper X2),
                              top mark X -> top proper X,
                                top ok X -> top active X}
          Open