MAYBE
Time: 0.128136
TRS:
 {       active U11(X1, X2) -> U11(active X1, X2),
        active U11(tt(), N) -> mark N,
                 active s X -> s active X,
        active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
        active plus(N, 0()) -> mark U11(isNat N, N),
        active plus(X1, X2) -> plus(X1, active X2),
        active plus(X1, X2) -> plus(active X1, X2),
     active U21(X1, X2, X3) -> U21(active X1, X2, X3),
     active U21(tt(), M, N) -> mark s plus(N, M),
               active U31 X -> U31 active X,
            active U31 tt() -> mark 0(),
           active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
           active x(N, 0()) -> mark U31 isNat N,
           active x(X1, X2) -> x(X1, active X2),
           active x(X1, X2) -> x(active X1, X2),
     active U41(X1, X2, X3) -> U41(active X1, X2, X3),
     active U41(tt(), M, N) -> mark plus(x(N, M), N),
         active and(X1, X2) -> and(active X1, X2),
        active and(tt(), X) -> mark X,
          active isNat s V1 -> mark isNat V1,
  active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
           active isNat 0() -> mark tt(),
     active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
           U11(mark X1, X2) -> mark U11(X1, X2),
          U11(ok X1, ok X2) -> ok U11(X1, X2),
                   s mark X -> mark s X,
                     s ok X -> ok s X,
          plus(X1, mark X2) -> mark plus(X1, X2),
          plus(mark X1, X2) -> mark plus(X1, X2),
         plus(ok X1, ok X2) -> ok plus(X1, X2),
       U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
   U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                 U31 mark X -> mark U31 X,
                   U31 ok X -> ok U31 X,
             x(X1, mark X2) -> mark x(X1, X2),
             x(mark X1, X2) -> mark x(X1, X2),
            x(ok X1, ok X2) -> ok x(X1, X2),
       U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
   U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
           and(mark X1, X2) -> mark and(X1, X2),
          and(ok X1, ok X2) -> ok and(X1, X2),
                 isNat ok X -> ok isNat X,
         proper U11(X1, X2) -> U11(proper X1, proper X2),
                proper tt() -> ok tt(),
                 proper s X -> s proper X,
        proper plus(X1, X2) -> plus(proper X1, proper X2),
     proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                 proper 0() -> ok 0(),
               proper U31 X -> U31 proper X,
           proper x(X1, X2) -> x(proper X1, proper X2),
     proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
         proper and(X1, X2) -> and(proper X1, proper X2),
             proper isNat X -> isNat proper X,
                 top mark X -> top proper X,
                   top ok X -> top active X}
 DP:
  DP:
   {       active# U11(X1, X2) -> active# X1,
           active# U11(X1, X2) -> U11#(active X1, X2),
                   active# s X -> active# X,
                   active# s X -> s# active X,
          active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N),
          active# plus(N, s M) -> and#(isNat M, isNat N),
          active# plus(N, s M) -> isNat# N,
          active# plus(N, s M) -> isNat# M,
          active# plus(N, 0()) -> U11#(isNat N, N),
          active# plus(N, 0()) -> isNat# N,
          active# plus(X1, X2) -> active# X1,
          active# plus(X1, X2) -> active# X2,
          active# plus(X1, X2) -> plus#(X1, active X2),
          active# plus(X1, X2) -> plus#(active X1, X2),
       active# U21(X1, X2, X3) -> active# X1,
       active# U21(X1, X2, X3) -> U21#(active X1, X2, X3),
       active# U21(tt(), M, N) -> s# plus(N, M),
       active# U21(tt(), M, N) -> plus#(N, M),
                 active# U31 X -> active# X,
                 active# U31 X -> U31# active X,
             active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N),
             active# x(N, s M) -> and#(isNat M, isNat N),
             active# x(N, s M) -> isNat# N,
             active# x(N, s M) -> isNat# M,
             active# x(N, 0()) -> U31# isNat N,
             active# x(N, 0()) -> isNat# N,
             active# x(X1, X2) -> active# X1,
             active# x(X1, X2) -> active# X2,
             active# x(X1, X2) -> x#(X1, active X2),
             active# x(X1, X2) -> x#(active X1, X2),
       active# U41(X1, X2, X3) -> active# X1,
       active# U41(X1, X2, X3) -> U41#(active X1, X2, X3),
       active# U41(tt(), M, N) -> plus#(x(N, M), N),
       active# U41(tt(), M, N) -> x#(N, M),
           active# and(X1, X2) -> active# X1,
           active# and(X1, X2) -> and#(active X1, X2),
            active# isNat s V1 -> isNat# V1,
    active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2),
    active# isNat plus(V1, V2) -> isNat# V1,
    active# isNat plus(V1, V2) -> isNat# V2,
       active# isNat x(V1, V2) -> and#(isNat V1, isNat V2),
       active# isNat x(V1, V2) -> isNat# V1,
       active# isNat x(V1, V2) -> isNat# V2,
             U11#(mark X1, X2) -> U11#(X1, X2),
            U11#(ok X1, ok X2) -> U11#(X1, X2),
                     s# mark X -> s# X,
                       s# ok X -> s# X,
            plus#(X1, mark X2) -> plus#(X1, X2),
            plus#(mark X1, X2) -> plus#(X1, X2),
           plus#(ok X1, ok X2) -> plus#(X1, X2),
         U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
     U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3),
                   U31# mark X -> U31# X,
                     U31# ok X -> U31# X,
               x#(X1, mark X2) -> x#(X1, X2),
               x#(mark X1, X2) -> x#(X1, X2),
              x#(ok X1, ok X2) -> x#(X1, X2),
         U41#(mark X1, X2, X3) -> U41#(X1, X2, X3),
     U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3),
             and#(mark X1, X2) -> and#(X1, X2),
            and#(ok X1, ok X2) -> and#(X1, X2),
                   isNat# ok X -> isNat# X,
           proper# U11(X1, X2) -> U11#(proper X1, proper X2),
           proper# U11(X1, X2) -> proper# X1,
           proper# U11(X1, X2) -> proper# X2,
                   proper# s X -> s# proper X,
                   proper# s X -> proper# X,
          proper# plus(X1, X2) -> plus#(proper X1, proper X2),
          proper# plus(X1, X2) -> proper# X1,
          proper# plus(X1, X2) -> proper# X2,
       proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3),
       proper# U21(X1, X2, X3) -> proper# X1,
       proper# U21(X1, X2, X3) -> proper# X2,
       proper# U21(X1, X2, X3) -> proper# X3,
                 proper# U31 X -> U31# proper X,
                 proper# U31 X -> proper# X,
             proper# x(X1, X2) -> x#(proper X1, proper X2),
             proper# x(X1, X2) -> proper# X1,
             proper# x(X1, X2) -> proper# X2,
       proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3),
       proper# U41(X1, X2, X3) -> proper# X1,
       proper# U41(X1, X2, X3) -> proper# X2,
       proper# U41(X1, X2, X3) -> proper# X3,
           proper# and(X1, X2) -> and#(proper X1, proper X2),
           proper# and(X1, X2) -> proper# X1,
           proper# and(X1, X2) -> proper# X2,
               proper# isNat X -> isNat# proper X,
               proper# isNat X -> proper# X,
                   top# mark X -> proper# X,
                   top# mark X -> top# proper X,
                     top# ok X -> active# X,
                     top# ok X -> top# active X}
  TRS:
  {       active U11(X1, X2) -> U11(active X1, X2),
         active U11(tt(), N) -> mark N,
                  active s X -> s active X,
         active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
         active plus(N, 0()) -> mark U11(isNat N, N),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
      active U21(X1, X2, X3) -> U21(active X1, X2, X3),
      active U21(tt(), M, N) -> mark s plus(N, M),
                active U31 X -> U31 active X,
             active U31 tt() -> mark 0(),
            active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
            active x(N, 0()) -> mark U31 isNat N,
            active x(X1, X2) -> x(X1, active X2),
            active x(X1, X2) -> x(active X1, X2),
      active U41(X1, X2, X3) -> U41(active X1, X2, X3),
      active U41(tt(), M, N) -> mark plus(x(N, M), N),
          active and(X1, X2) -> and(active X1, X2),
         active and(tt(), X) -> mark X,
           active isNat s V1 -> mark isNat V1,
   active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
            active isNat 0() -> mark tt(),
      active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
            U11(mark X1, X2) -> mark U11(X1, X2),
           U11(ok X1, ok X2) -> ok U11(X1, X2),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
           plus(X1, mark X2) -> mark plus(X1, X2),
           plus(mark X1, X2) -> mark plus(X1, X2),
          plus(ok X1, ok X2) -> ok plus(X1, X2),
        U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
    U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                  U31 mark X -> mark U31 X,
                    U31 ok X -> ok U31 X,
              x(X1, mark X2) -> mark x(X1, X2),
              x(mark X1, X2) -> mark x(X1, X2),
             x(ok X1, ok X2) -> ok x(X1, X2),
        U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
    U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
            and(mark X1, X2) -> mark and(X1, X2),
           and(ok X1, ok X2) -> ok and(X1, X2),
                  isNat ok X -> ok isNat X,
          proper U11(X1, X2) -> U11(proper X1, proper X2),
                 proper tt() -> ok tt(),
                  proper s X -> s proper X,
         proper plus(X1, X2) -> plus(proper X1, proper X2),
      proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                  proper 0() -> ok 0(),
                proper U31 X -> U31 proper X,
            proper x(X1, X2) -> x(proper X1, proper X2),
      proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
          proper and(X1, X2) -> and(proper X1, proper X2),
              proper isNat X -> isNat proper X,
                  top mark X -> top proper X,
                    top ok X -> top active X}
  UR:
   {       active U11(X1, X2) -> U11(active X1, X2),
          active U11(tt(), N) -> mark N,
                   active s X -> s active X,
          active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
          active plus(N, 0()) -> mark U11(isNat N, N),
          active plus(X1, X2) -> plus(X1, active X2),
          active plus(X1, X2) -> plus(active X1, X2),
       active U21(X1, X2, X3) -> U21(active X1, X2, X3),
       active U21(tt(), M, N) -> mark s plus(N, M),
                 active U31 X -> U31 active X,
              active U31 tt() -> mark 0(),
             active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
             active x(N, 0()) -> mark U31 isNat N,
             active x(X1, X2) -> x(X1, active X2),
             active x(X1, X2) -> x(active X1, X2),
       active U41(X1, X2, X3) -> U41(active X1, X2, X3),
       active U41(tt(), M, N) -> mark plus(x(N, M), N),
           active and(X1, X2) -> and(active X1, X2),
          active and(tt(), X) -> mark X,
            active isNat s V1 -> mark isNat V1,
    active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
             active isNat 0() -> mark tt(),
       active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
             U11(mark X1, X2) -> mark U11(X1, X2),
            U11(ok X1, ok X2) -> ok U11(X1, X2),
                     s mark X -> mark s X,
                       s ok X -> ok s X,
            plus(X1, mark X2) -> mark plus(X1, X2),
            plus(mark X1, X2) -> mark plus(X1, X2),
           plus(ok X1, ok X2) -> ok plus(X1, X2),
         U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
     U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                   U31 mark X -> mark U31 X,
                     U31 ok X -> ok U31 X,
               x(X1, mark X2) -> mark x(X1, X2),
               x(mark X1, X2) -> mark x(X1, X2),
              x(ok X1, ok X2) -> ok x(X1, X2),
         U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
     U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
             and(mark X1, X2) -> mark and(X1, X2),
            and(ok X1, ok X2) -> ok and(X1, X2),
                   isNat ok X -> ok isNat X,
           proper U11(X1, X2) -> U11(proper X1, proper X2),
                  proper tt() -> ok tt(),
                   proper s X -> s proper X,
          proper plus(X1, X2) -> plus(proper X1, proper X2),
       proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                   proper 0() -> ok 0(),
                 proper U31 X -> U31 proper X,
             proper x(X1, X2) -> x(proper X1, proper X2),
       proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
           proper and(X1, X2) -> and(proper X1, proper X2),
               proper isNat X -> isNat proper X,
                      a(x, y) -> x,
                      a(x, y) -> y}
   EDG:
    {
     (active# U31 X -> U31# active X, U31# ok X -> U31# X)
     (active# U31 X -> U31# active X, U31# mark X -> U31# X)
     (proper# U31 X -> U31# proper X, U31# ok X -> U31# X)
     (proper# U31 X -> U31# proper X, U31# mark X -> U31# 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# U11(X1, X2) -> U11#(active X1, X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (active# U11(X1, X2) -> U11#(active X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (active# x(N, 0()) -> U31# isNat N, U31# ok X -> U31# X)
     (active# x(N, 0()) -> U31# isNat N, U31# mark X -> U31# X)
     (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# U41(X1, X2, X3) -> U41#(active X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (active# U41(X1, X2, X3) -> U41#(active X1, X2, X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (active# isNat x(V1, V2) -> isNat# V2, isNat# ok X -> isNat# X)
     (U11#(ok X1, ok X2) -> U11#(X1, X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (U11#(ok X1, ok X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (x#(X1, mark X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (x#(X1, mark X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (x#(X1, mark X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (x#(ok X1, ok X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (x#(ok X1, ok X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (x#(ok X1, ok X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# x(N, s M) -> isNat# M, isNat# ok X -> isNat# X)
     (active# plus(X1, X2) -> active# X2, active# isNat x(V1, V2) -> isNat# V2)
     (active# plus(X1, X2) -> active# X2, active# isNat x(V1, V2) -> isNat# V1)
     (active# plus(X1, X2) -> active# X2, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> isNat# V2)
     (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> isNat# V1)
     (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# plus(X1, X2) -> active# X2, active# isNat s V1 -> isNat# V1)
     (active# plus(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U41(tt(), M, N) -> x#(N, M))
     (active# plus(X1, X2) -> active# X2, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# plus(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> x#(X1, active X2))
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# x(N, 0()) -> isNat# N)
     (active# plus(X1, X2) -> active# X2, active# x(N, 0()) -> U31# isNat N)
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> isNat# M)
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> isNat# N)
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# plus(X1, X2) -> active# X2, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# plus(X1, X2) -> active# X2, active# U31 X -> U31# active X)
     (active# plus(X1, X2) -> active# X2, active# U31 X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# U21(tt(), M, N) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X2, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# plus(N, 0()) -> isNat# N)
     (active# plus(X1, X2) -> active# X2, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> isNat# M)
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> isNat# N)
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# U11(X1, X2) -> active# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
     (proper# U11(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# U11(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X2, proper# U31 X -> proper# X)
     (proper# U11(X1, X2) -> proper# X2, proper# U31 X -> U31# proper X)
     (proper# U11(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# U11(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# U11(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# isNat X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U31 X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U31 X -> U31# proper X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# isNat X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U31 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U31 X -> U31# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (active# isNat s V1 -> isNat# V1, isNat# ok X -> isNat# X)
     (active# isNat x(V1, V2) -> isNat# V1, isNat# ok X -> isNat# X)
     (active# plus(X1, X2) -> plus#(X1, active X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(X1, active X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(X1, active X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (active# x(X1, X2) -> x#(X1, active X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(X1, active X2), x#(mark X1, X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(X1, active X2), x#(X1, mark X2) -> x#(X1, X2))
     (active# isNat x(V1, V2) -> and#(isNat V1, isNat V2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# isNat x(V1, V2) -> and#(isNat V1, isNat V2), and#(mark X1, X2) -> and#(X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (proper# plus(X1, X2) -> plus#(proper X1, proper X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# plus(N, 0()) -> isNat# N, isNat# ok X -> isNat# X)
     (active# x(N, 0()) -> isNat# N, isNat# ok X -> isNat# X)
     (active# plus(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V2)
     (active# plus(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V1)
     (active# plus(X1, X2) -> active# X1, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V2)
     (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# plus(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# plus(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U41(tt(), M, N) -> x#(N, M))
     (active# plus(X1, X2) -> active# X1, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# plus(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# x(N, 0()) -> isNat# N)
     (active# plus(X1, X2) -> active# X1, active# x(N, 0()) -> U31# isNat N)
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> isNat# M)
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> isNat# N)
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# plus(X1, X2) -> active# X1, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# plus(X1, X2) -> active# X1, active# U31 X -> U31# active X)
     (active# plus(X1, X2) -> active# X1, active# U31 X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# U21(tt(), M, N) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X1, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# plus(X1, X2) -> active# X1, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# N)
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V2)
     (active# x(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V1)
     (active# x(X1, X2) -> active# X1, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# x(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V2)
     (active# x(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# x(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# x(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# x(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# U41(tt(), M, N) -> x#(N, M))
     (active# x(X1, X2) -> active# X1, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# x(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# x(N, 0()) -> isNat# N)
     (active# x(X1, X2) -> active# X1, active# x(N, 0()) -> U31# isNat N)
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> isNat# M)
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> isNat# N)
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# x(X1, X2) -> active# X1, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# x(X1, X2) -> active# X1, active# U31 X -> U31# active X)
     (active# x(X1, X2) -> active# X1, active# U31 X -> active# X)
     (active# x(X1, X2) -> active# X1, active# U21(tt(), M, N) -> plus#(N, M))
     (active# x(X1, X2) -> active# X1, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# x(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# x(X1, X2) -> active# X1, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# N)
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# x(X1, X2) -> active# X1, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# x(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# x(X1, X2) -> active# X1, active# s X -> active# X)
     (active# x(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# x(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V2)
     (active# and(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V1)
     (active# and(X1, X2) -> active# X1, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# and(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V2)
     (active# and(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# and(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# and(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# U41(tt(), M, N) -> x#(N, M))
     (active# and(X1, X2) -> active# X1, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# and(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# and(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# and(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# x(N, 0()) -> isNat# N)
     (active# and(X1, X2) -> active# X1, active# x(N, 0()) -> U31# isNat N)
     (active# and(X1, X2) -> active# X1, active# x(N, s M) -> isNat# M)
     (active# and(X1, X2) -> active# X1, active# x(N, s M) -> isNat# N)
     (active# and(X1, X2) -> active# X1, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# and(X1, X2) -> active# X1, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# and(X1, X2) -> active# X1, active# U31 X -> U31# active X)
     (active# and(X1, X2) -> active# X1, active# U31 X -> active# X)
     (active# and(X1, X2) -> active# X1, active# U21(tt(), M, N) -> plus#(N, M))
     (active# and(X1, X2) -> active# X1, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# and(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# and(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# and(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# and(X1, X2) -> active# X1, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# N)
     (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# and(X1, X2) -> active# X1, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# and(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# and(X1, X2) -> active# X1, active# s X -> active# X)
     (active# and(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
     (proper# plus(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# U31 X -> proper# X)
     (proper# plus(X1, X2) -> proper# X1, proper# U31 X -> U31# proper X)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# plus(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
     (proper# x(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X1, proper# U31 X -> proper# X)
     (proper# x(X1, X2) -> proper# X1, proper# U31 X -> U31# proper X)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# x(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# and(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# U31 X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# U31 X -> U31# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# and(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (active# U41(tt(), M, N) -> plus#(x(N, M), N), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (active# U41(tt(), M, N) -> plus#(x(N, M), N), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# U41(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2))
     (proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (active# U31 X -> active# X, active# isNat x(V1, V2) -> isNat# V2)
     (active# U31 X -> active# X, active# isNat x(V1, V2) -> isNat# V1)
     (active# U31 X -> active# X, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U31 X -> active# X, active# isNat plus(V1, V2) -> isNat# V2)
     (active# U31 X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U31 X -> active# X, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U31 X -> active# X, active# isNat s V1 -> isNat# V1)
     (active# U31 X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
     (active# U31 X -> active# X, active# and(X1, X2) -> active# X1)
     (active# U31 X -> active# X, active# U41(tt(), M, N) -> x#(N, M))
     (active# U31 X -> active# X, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# U31 X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U31 X -> active# X, active# U41(X1, X2, X3) -> active# X1)
     (active# U31 X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
     (active# U31 X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
     (active# U31 X -> active# X, active# x(X1, X2) -> active# X2)
     (active# U31 X -> active# X, active# x(X1, X2) -> active# X1)
     (active# U31 X -> active# X, active# x(N, 0()) -> isNat# N)
     (active# U31 X -> active# X, active# x(N, 0()) -> U31# isNat N)
     (active# U31 X -> active# X, active# x(N, s M) -> isNat# M)
     (active# U31 X -> active# X, active# x(N, s M) -> isNat# N)
     (active# U31 X -> active# X, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# U31 X -> active# X, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# U31 X -> active# X, active# U31 X -> U31# active X)
     (active# U31 X -> active# X, active# U31 X -> active# X)
     (active# U31 X -> active# X, active# U21(tt(), M, N) -> plus#(N, M))
     (active# U31 X -> active# X, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# U31 X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U31 X -> active# X, active# U21(X1, X2, X3) -> active# X1)
     (active# U31 X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U31 X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U31 X -> active# X, active# plus(X1, X2) -> active# X2)
     (active# U31 X -> active# X, active# plus(X1, X2) -> active# X1)
     (active# U31 X -> active# X, active# plus(N, 0()) -> isNat# N)
     (active# U31 X -> active# X, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# U31 X -> active# X, active# plus(N, s M) -> isNat# M)
     (active# U31 X -> active# X, active# plus(N, s M) -> isNat# N)
     (active# U31 X -> active# X, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# U31 X -> active# X, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# U31 X -> active# X, active# s X -> s# active X)
     (active# U31 X -> active# X, active# s X -> active# X)
     (active# U31 X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U31 X -> active# X, active# U11(X1, X2) -> active# X1)
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (U31# ok X -> U31# X, U31# ok X -> U31# X)
     (U31# ok X -> U31# X, U31# mark X -> U31# X)
     (proper# s X -> proper# X, proper# isNat X -> proper# X)
     (proper# s X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# U31 X -> proper# X)
     (proper# s X -> proper# X, proper# U31 X -> U31# proper X)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(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# U11(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# isNat X -> proper# X)
     (proper# isNat X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# isNat X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# isNat X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# U31 X -> proper# X)
     (proper# isNat X -> proper# X, proper# U31 X -> U31# proper X)
     (proper# isNat X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# isNat X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# isNat X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# s X -> proper# X)
     (proper# isNat X -> proper# X, proper# s X -> s# proper X)
     (proper# isNat X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (top# ok X -> active# X, active# isNat x(V1, V2) -> isNat# V2)
     (top# ok X -> active# X, active# isNat x(V1, V2) -> isNat# V1)
     (top# ok X -> active# X, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (top# ok X -> active# X, active# isNat plus(V1, V2) -> isNat# V2)
     (top# ok X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (top# ok X -> active# X, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (top# ok X -> active# X, active# isNat s V1 -> isNat# V1)
     (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
     (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# U41(tt(), M, N) -> x#(N, M))
     (top# ok X -> active# X, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (top# ok X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (top# ok X -> active# X, active# U41(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
     (top# ok X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
     (top# ok X -> active# X, active# x(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# x(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# x(N, 0()) -> isNat# N)
     (top# ok X -> active# X, active# x(N, 0()) -> U31# isNat N)
     (top# ok X -> active# X, active# x(N, s M) -> isNat# M)
     (top# ok X -> active# X, active# x(N, s M) -> isNat# N)
     (top# ok X -> active# X, active# x(N, s M) -> and#(isNat M, isNat N))
     (top# ok X -> active# X, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (top# ok X -> active# X, active# U31 X -> U31# active X)
     (top# ok X -> active# X, active# U31 X -> active# X)
     (top# ok X -> active# X, active# U21(tt(), M, N) -> plus#(N, M))
     (top# ok X -> active# X, active# U21(tt(), M, N) -> s# plus(N, M))
     (top# ok X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (top# ok X -> active# X, active# U21(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# plus(N, 0()) -> isNat# N)
     (top# ok X -> active# X, active# plus(N, 0()) -> U11#(isNat N, N))
     (top# ok X -> active# X, active# plus(N, s M) -> isNat# M)
     (top# ok X -> active# X, active# plus(N, s M) -> isNat# N)
     (top# ok X -> active# X, active# plus(N, s M) -> and#(isNat M, isNat N))
     (top# ok X -> active# X, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
     (top# ok X -> active# X, active# U11(X1, X2) -> active# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# isNat X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# isNat X -> isNat# proper X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# and(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# and(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U31 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U31 X -> U31# proper X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (active# U41(tt(), M, N) -> x#(N, M), x#(ok X1, ok X2) -> x#(X1, X2))
     (active# U41(tt(), M, N) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2))
     (active# U41(tt(), M, N) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2))
     (active# U21(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2))
     (active# U21(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# U21(tt(), M, N) -> plus#(N, M), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U31 X -> U31# proper X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U31 X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# x(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X3, proper# and(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# and(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# isNat X -> isNat# proper X)
     (proper# U21(X1, X2, X3) -> proper# X3, proper# isNat X -> proper# X)
     (top# mark X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# U31 X -> U31# proper X)
     (top# mark X -> proper# X, proper# U31 X -> proper# X)
     (top# mark X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# isNat X -> isNat# proper X)
     (top# mark X -> proper# X, proper# isNat X -> proper# X)
     (proper# U31 X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U31 X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# U31 X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (proper# U31 X -> proper# X, proper# s X -> s# proper X)
     (proper# U31 X -> proper# X, proper# s X -> proper# X)
     (proper# U31 X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U31 X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# U31 X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# U31 X -> proper# X, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U31 X -> proper# X, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U31 X -> proper# X, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U31 X -> proper# X, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U31 X -> proper# X, proper# U31 X -> U31# proper X)
     (proper# U31 X -> proper# X, proper# U31 X -> proper# X)
     (proper# U31 X -> proper# X, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U31 X -> proper# X, proper# x(X1, X2) -> proper# X1)
     (proper# U31 X -> proper# X, proper# x(X1, X2) -> proper# X2)
     (proper# U31 X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U31 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U31 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U31 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U31 X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U31 X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# U31 X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# U31 X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# U31 X -> proper# X, proper# isNat X -> proper# X)
     (isNat# ok X -> isNat# X, isNat# ok X -> isNat# X)
     (U31# mark X -> U31# X, U31# mark X -> U31# X)
     (U31# mark X -> U31# X, U31# ok X -> U31# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (active# s X -> active# X, active# U11(X1, X2) -> active# X1)
     (active# s X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# s X -> active# X, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# s X -> active# X, active# plus(N, s M) -> isNat# N)
     (active# s X -> active# X, active# plus(N, s M) -> isNat# M)
     (active# s X -> active# X, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# s X -> active# X, active# plus(N, 0()) -> isNat# N)
     (active# s X -> active# X, active# plus(X1, X2) -> active# X1)
     (active# s X -> active# X, active# plus(X1, X2) -> active# X2)
     (active# s X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# s X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# s X -> active# X, active# U21(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# s X -> active# X, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# s X -> active# X, active# U21(tt(), M, N) -> plus#(N, M))
     (active# s X -> active# X, active# U31 X -> active# X)
     (active# s X -> active# X, active# U31 X -> U31# active X)
     (active# s X -> active# X, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# s X -> active# X, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# s X -> active# X, active# x(N, s M) -> isNat# N)
     (active# s X -> active# X, active# x(N, s M) -> isNat# M)
     (active# s X -> active# X, active# x(N, 0()) -> U31# isNat N)
     (active# s X -> active# X, active# x(N, 0()) -> isNat# N)
     (active# s X -> active# X, active# x(X1, X2) -> active# X1)
     (active# s X -> active# X, active# x(X1, X2) -> active# X2)
     (active# s X -> active# X, active# x(X1, X2) -> x#(X1, active X2))
     (active# s X -> active# X, active# x(X1, X2) -> x#(active X1, X2))
     (active# s X -> active# X, active# U41(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# s X -> active# X, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# s X -> active# X, active# U41(tt(), M, N) -> x#(N, M))
     (active# s X -> active# X, active# and(X1, X2) -> active# X1)
     (active# s X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
     (active# s X -> active# X, active# isNat s V1 -> isNat# V1)
     (active# s X -> active# X, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# s X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (active# s X -> active# X, active# isNat plus(V1, V2) -> isNat# V2)
     (active# s X -> active# X, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# s X -> active# X, active# isNat x(V1, V2) -> isNat# V1)
     (active# s X -> active# X, active# isNat x(V1, V2) -> isNat# V2)
     (proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (active# plus(N, 0()) -> U11#(isNat N, N), U11#(mark X1, X2) -> U11#(X1, X2))
     (active# plus(N, 0()) -> U11#(isNat N, N), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U31 X -> U31# proper X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U31 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# isNat X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U31 X -> U31# proper X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U31 X -> proper# X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U21(X1, X2, X3) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# U21(X1, X2, X3) -> proper# X1, proper# isNat X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# U11(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2) -> proper# X1, proper# U31 X -> U31# proper X)
     (proper# U11(X1, X2) -> proper# X1, proper# U31 X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# x(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# U11(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
     (active# U41(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U41(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U41(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# N)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U41(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U41(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# U41(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> plus#(N, M))
     (active# U41(X1, X2, X3) -> active# X1, active# U31 X -> active# X)
     (active# U41(X1, X2, X3) -> active# X1, active# U31 X -> U31# active X)
     (active# U41(X1, X2, X3) -> active# X1, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# U41(X1, X2, X3) -> active# X1, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# U41(X1, X2, X3) -> active# X1, active# x(N, s M) -> isNat# N)
     (active# U41(X1, X2, X3) -> active# X1, active# x(N, s M) -> isNat# M)
     (active# U41(X1, X2, X3) -> active# X1, active# x(N, 0()) -> U31# isNat N)
     (active# U41(X1, X2, X3) -> active# X1, active# x(N, 0()) -> isNat# N)
     (active# U41(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U41(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U41(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# U41(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U41(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# U41(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> x#(N, M))
     (active# U41(X1, X2, X3) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# U41(X1, X2, X3) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V2)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U41(X1, X2, X3) -> active# X1, active# isNat x(V1, V2) -> isNat# V1)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat x(V1, V2) -> isNat# V2)
     (active# U21(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U21(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U21(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# N)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# U21(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U21(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U21(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U21(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# U21(X1, X2, X3) -> active# X1, active# U21(tt(), M, N) -> plus#(N, M))
     (active# U21(X1, X2, X3) -> active# X1, active# U31 X -> active# X)
     (active# U21(X1, X2, X3) -> active# X1, active# U31 X -> U31# active X)
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, s M) -> isNat# N)
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, s M) -> isNat# M)
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, 0()) -> U31# isNat N)
     (active# U21(X1, X2, X3) -> active# X1, active# x(N, 0()) -> isNat# N)
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U21(X1, X2, X3) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# U21(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U21(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# U21(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> x#(N, M))
     (active# U21(X1, X2, X3) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# U21(X1, X2, X3) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# U21(X1, X2, X3) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U21(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U21(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U21(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V2)
     (active# U21(X1, X2, X3) -> active# X1, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U21(X1, X2, X3) -> active# X1, active# isNat x(V1, V2) -> isNat# V1)
     (active# U21(X1, X2, X3) -> active# X1, active# isNat x(V1, V2) -> isNat# V2)
     (active# U11(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U11(X1, X2) -> active# X1, active# s X -> active# X)
     (active# U11(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# U11(X1, X2) -> active# X1, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# U11(X1, X2) -> active# X1, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# U11(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# N)
     (active# U11(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# U11(X1, X2) -> active# X1, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# U11(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# U11(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U11(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U11(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U11(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# U11(X1, X2) -> active# X1, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# U11(X1, X2) -> active# X1, active# U21(tt(), M, N) -> plus#(N, M))
     (active# U11(X1, X2) -> active# X1, active# U31 X -> active# X)
     (active# U11(X1, X2) -> active# X1, active# U31 X -> U31# active X)
     (active# U11(X1, X2) -> active# X1, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# U11(X1, X2) -> active# X1, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# U11(X1, X2) -> active# X1, active# x(N, s M) -> isNat# N)
     (active# U11(X1, X2) -> active# X1, active# x(N, s M) -> isNat# M)
     (active# U11(X1, X2) -> active# X1, active# x(N, 0()) -> U31# isNat N)
     (active# U11(X1, X2) -> active# X1, active# x(N, 0()) -> isNat# N)
     (active# U11(X1, X2) -> active# X1, active# x(X1, X2) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# x(X1, X2) -> active# X2)
     (active# U11(X1, X2) -> active# X1, active# x(X1, X2) -> x#(X1, active X2))
     (active# U11(X1, X2) -> active# X1, active# x(X1, X2) -> x#(active X1, X2))
     (active# U11(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U11(X1, X2) -> active# X1, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# U11(X1, X2) -> active# X1, active# U41(tt(), M, N) -> x#(N, M))
     (active# U11(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# U11(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V2)
     (active# U11(X1, X2) -> active# X1, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# U11(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V1)
     (active# U11(X1, X2) -> active# X1, active# isNat x(V1, V2) -> isNat# V2)
     (active# x(N, s M) -> isNat# N, isNat# ok X -> isNat# X)
     (active# plus(N, s M) -> isNat# N, isNat# ok X -> isNat# X)
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(X1, mark X2) -> x#(X1, X2))
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(mark X1, X2) -> x#(X1, X2))
     (proper# x(X1, X2) -> x#(proper X1, proper X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# x(N, s M) -> and#(isNat M, isNat N), and#(mark X1, X2) -> and#(X1, X2))
     (active# x(N, s M) -> and#(isNat M, isNat N), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# plus(N, s M) -> and#(isNat M, isNat N), and#(mark X1, X2) -> and#(X1, X2))
     (active# plus(N, s M) -> and#(isNat M, isNat N), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# isNat plus(V1, V2) -> isNat# V1, isNat# ok X -> isNat# X)
     (proper# and(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# and(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# and(X1, X2) -> proper# X2, proper# U31 X -> U31# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# U31 X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# and(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# x(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X2, proper# U31 X -> U31# proper X)
     (proper# x(X1, X2) -> proper# X2, proper# U31 X -> proper# X)
     (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# x(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# x(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# x(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# x(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> U21#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U21(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# U31 X -> U31# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# U31 X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> x#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# x(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
     (active# x(X1, X2) -> active# X2, active# U11(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# s X -> active# X)
     (active# x(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> and#(isNat M, isNat N))
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> isNat# N)
     (active# x(X1, X2) -> active# X2, active# plus(N, s M) -> isNat# M)
     (active# x(X1, X2) -> active# X2, active# plus(N, 0()) -> U11#(isNat N, N))
     (active# x(X1, X2) -> active# X2, active# plus(N, 0()) -> isNat# N)
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# x(X1, X2) -> active# X2, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# U21(X1, X2, X3) -> U21#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X2, active# U21(tt(), M, N) -> s# plus(N, M))
     (active# x(X1, X2) -> active# X2, active# U21(tt(), M, N) -> plus#(N, M))
     (active# x(X1, X2) -> active# X2, active# U31 X -> active# X)
     (active# x(X1, X2) -> active# X2, active# U31 X -> U31# active X)
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> U41#(and(isNat M, isNat N), M, N))
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> and#(isNat M, isNat N))
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> isNat# N)
     (active# x(X1, X2) -> active# X2, active# x(N, s M) -> isNat# M)
     (active# x(X1, X2) -> active# X2, active# x(N, 0()) -> U31# isNat N)
     (active# x(X1, X2) -> active# X2, active# x(N, 0()) -> isNat# N)
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> active# X2)
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> x#(X1, active X2))
     (active# x(X1, X2) -> active# X2, active# x(X1, X2) -> x#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# x(X1, X2) -> active# X2, active# U41(tt(), M, N) -> plus#(x(N, M), N))
     (active# x(X1, X2) -> active# X2, active# U41(tt(), M, N) -> x#(N, M))
     (active# x(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
     (active# x(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
     (active# x(X1, X2) -> active# X2, active# isNat s V1 -> isNat# V1)
     (active# x(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (active# x(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> isNat# V1)
     (active# x(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> isNat# V2)
     (active# x(X1, X2) -> active# X2, active# isNat x(V1, V2) -> and#(isNat V1, isNat V2))
     (active# x(X1, X2) -> active# X2, active# isNat x(V1, V2) -> isNat# V1)
     (active# x(X1, X2) -> active# X2, active# isNat x(V1, V2) -> isNat# V2)
     (active# U21(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X)
     (active# U21(tt(), M, N) -> s# plus(N, M), s# ok X -> s# X)
     (active# plus(N, s M) -> isNat# M, isNat# ok X -> isNat# X)
     (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (x#(mark X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (x#(mark X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (x#(mark X1, X2) -> x#(X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(ok X1, ok X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (U11#(mark X1, X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (U11#(mark X1, X2) -> U11#(X1, X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (active# isNat plus(V1, V2) -> isNat# V2, isNat# ok X -> isNat# X)
     (U41#(mark X1, X2, X3) -> U41#(X1, X2, X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (U41#(mark X1, X2, X3) -> U41#(X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (active# U21(X1, X2, X3) -> U21#(active X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (active# U21(X1, X2, X3) -> U21#(active X1, X2, X3), U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3))
     (active# x(X1, X2) -> x#(active X1, X2), x#(X1, mark X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(active X1, X2), x#(mark X1, X2) -> x#(X1, X2))
     (active# x(X1, X2) -> x#(active X1, X2), x#(ok X1, ok X2) -> x#(X1, X2))
     (active# plus(X1, X2) -> plus#(active X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(active X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# plus(X1, X2) -> plus#(active X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (proper# isNat X -> isNat# proper X, isNat# ok X -> isNat# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# s X -> s# active X, s# ok X -> s# X)
    }
    STATUS:
     arrows: 0.873228
     SCCS (12):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {    active# U11(X1, X2) -> active# X1,
                    active# s X -> active# X,
           active# plus(X1, X2) -> active# X1,
           active# plus(X1, X2) -> active# X2,
        active# U21(X1, X2, X3) -> active# X1,
                  active# U31 X -> active# X,
              active# x(X1, X2) -> active# X1,
              active# x(X1, X2) -> active# X2,
        active# U41(X1, X2, X3) -> active# X1,
            active# and(X1, X2) -> active# X1}
      Scc:
       {    proper# U11(X1, X2) -> proper# X1,
            proper# U11(X1, X2) -> proper# X2,
                    proper# s X -> proper# X,
           proper# plus(X1, X2) -> proper# X1,
           proper# plus(X1, X2) -> proper# X2,
        proper# U21(X1, X2, X3) -> proper# X1,
        proper# U21(X1, X2, X3) -> proper# X2,
        proper# U21(X1, X2, X3) -> proper# X3,
                  proper# U31 X -> proper# X,
              proper# x(X1, X2) -> proper# X1,
              proper# x(X1, X2) -> proper# X2,
        proper# U41(X1, X2, X3) -> proper# X1,
        proper# U41(X1, X2, X3) -> proper# X2,
        proper# U41(X1, X2, X3) -> proper# X3,
            proper# and(X1, X2) -> proper# X1,
            proper# and(X1, X2) -> proper# X2,
                proper# isNat X -> proper# X}
      Scc:
       { and#(mark X1, X2) -> and#(X1, X2),
        and#(ok X1, ok X2) -> and#(X1, X2)}
      Scc:
       {    U41#(mark X1, X2, X3) -> U41#(X1, X2, X3),
        U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3)}
      Scc:
       { x#(X1, mark X2) -> x#(X1, X2),
         x#(mark X1, X2) -> x#(X1, X2),
        x#(ok X1, ok X2) -> x#(X1, X2)}
      Scc:
       {    U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
        U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3)}
      Scc:
       { plus#(X1, mark X2) -> plus#(X1, X2),
         plus#(mark X1, X2) -> plus#(X1, X2),
        plus#(ok X1, ok X2) -> plus#(X1, X2)}
      Scc:
       { U11#(mark X1, X2) -> U11#(X1, X2),
        U11#(ok X1, ok X2) -> U11#(X1, X2)}
      Scc:
       {isNat# ok X -> isNat# X}
      Scc:
       {U31# mark X -> U31# X,
          U31# ok X -> U31# X}
      Scc:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (10):
       Strict:
        {    active# U11(X1, X2) -> active# X1,
                     active# s X -> active# X,
            active# plus(X1, X2) -> active# X1,
            active# plus(X1, X2) -> active# X2,
         active# U21(X1, X2, X3) -> active# X1,
                   active# U31 X -> active# X,
               active# x(X1, X2) -> active# X1,
               active# x(X1, X2) -> active# X2,
         active# U41(X1, X2, X3) -> active# X1,
             active# and(X1, X2) -> active# X1}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      
      SCC (17):
       Strict:
        {    proper# U11(X1, X2) -> proper# X1,
             proper# U11(X1, X2) -> proper# X2,
                     proper# s X -> proper# X,
            proper# plus(X1, X2) -> proper# X1,
            proper# plus(X1, X2) -> proper# X2,
         proper# U21(X1, X2, X3) -> proper# X1,
         proper# U21(X1, X2, X3) -> proper# X2,
         proper# U21(X1, X2, X3) -> proper# X3,
                   proper# U31 X -> proper# X,
               proper# x(X1, X2) -> proper# X1,
               proper# x(X1, X2) -> proper# X2,
         proper# U41(X1, X2, X3) -> proper# X1,
         proper# U41(X1, X2, X3) -> proper# X2,
         proper# U41(X1, X2, X3) -> proper# X3,
             proper# and(X1, X2) -> proper# X1,
             proper# and(X1, X2) -> proper# X2,
                 proper# isNat X -> proper# X}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        { and#(mark X1, X2) -> and#(X1, X2),
         and#(ok X1, ok X2) -> and#(X1, X2)}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {    U41#(mark X1, X2, X3) -> U41#(X1, X2, X3),
         U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3)}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { x#(X1, mark X2) -> x#(X1, X2),
          x#(mark X1, X2) -> x#(X1, X2),
         x#(ok X1, ok X2) -> x#(X1, X2)}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {    U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
         U21#(ok X1, ok X2, ok X3) -> U21#(X1, X2, X3)}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        { plus#(X1, mark X2) -> plus#(X1, X2),
          plus#(mark X1, X2) -> plus#(X1, X2),
         plus#(ok X1, ok X2) -> plus#(X1, X2)}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        { U11#(mark X1, X2) -> U11#(X1, X2),
         U11#(ok X1, ok X2) -> U11#(X1, X2)}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {isNat# ok X -> isNat# X}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      
      
      SCC (2):
       Strict:
        {U31# mark X -> U31# X,
           U31# ok X -> U31# X}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {s# mark X -> s# X,
           s# ok X -> s# X}
       Weak:
       {       active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), N) -> mark N,
                       active s X -> s active X,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
              active plus(X1, X2) -> plus(X1, active X2),
              active plus(X1, X2) -> plus(active X1, X2),
           active U21(X1, X2, X3) -> U21(active X1, X2, X3),
           active U21(tt(), M, N) -> mark s plus(N, M),
                     active U31 X -> U31 active X,
                  active U31 tt() -> mark 0(),
                 active x(N, s M) -> mark U41(and(isNat M, isNat N), M, N),
                 active x(N, 0()) -> mark U31 isNat N,
                 active x(X1, X2) -> x(X1, active X2),
                 active x(X1, X2) -> x(active X1, X2),
           active U41(X1, X2, X3) -> U41(active X1, X2, X3),
           active U41(tt(), M, N) -> mark plus(x(N, M), N),
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
           active isNat x(V1, V2) -> mark and(isNat V1, isNat V2),
                 U11(mark X1, X2) -> mark U11(X1, X2),
                U11(ok X1, ok X2) -> ok U11(X1, X2),
                         s mark X -> mark s X,
                           s ok X -> ok s X,
                plus(X1, mark X2) -> mark plus(X1, X2),
                plus(mark X1, X2) -> mark plus(X1, X2),
               plus(ok X1, ok X2) -> ok plus(X1, X2),
             U21(mark X1, X2, X3) -> mark U21(X1, X2, X3),
         U21(ok X1, ok X2, ok X3) -> ok U21(X1, X2, X3),
                       U31 mark X -> mark U31 X,
                         U31 ok X -> ok U31 X,
                   x(X1, mark X2) -> mark x(X1, X2),
                   x(mark X1, X2) -> mark x(X1, X2),
                  x(ok X1, ok X2) -> ok x(X1, X2),
             U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
         U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                       isNat ok X -> ok isNat X,
               proper U11(X1, X2) -> U11(proper X1, proper X2),
                      proper tt() -> ok tt(),
                       proper s X -> s proper X,
              proper plus(X1, X2) -> plus(proper X1, proper X2),
           proper U21(X1, X2, X3) -> U21(proper X1, proper X2, proper X3),
                       proper 0() -> ok 0(),
                     proper U31 X -> U31 proper X,
                 proper x(X1, X2) -> x(proper X1, proper X2),
           proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
               proper and(X1, X2) -> and(proper X1, proper X2),
                   proper isNat X -> isNat proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
       Open