MAYBE
Time: 1.268803
TRS:
 {               U12 mark X -> mark U12 X,
                   U12 ok X -> ok U12 X,
                 isNat ok X -> ok isNat X,
               active U12 X -> U12 active X,
            active U12 tt() -> mark tt(),
          active isNat s V1 -> mark U21 isNat V1,
  active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
           active isNat 0() -> mark tt(),
         active U11(X1, X2) -> U11(active X1, X2),
       active U11(tt(), V2) -> mark U12 isNat V2,
               active U21 X -> U21 active X,
            active U21 tt() -> mark tt(),
         active U31(X1, X2) -> U31(active X1, X2),
        active U31(tt(), N) -> mark N,
     active U42(X1, X2, X3) -> U42(active X1, X2, X3),
     active U42(tt(), M, N) -> mark s plus(N, M),
     active U41(X1, X2, X3) -> U41(active X1, X2, X3),
     active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                 active s X -> s active X,
        active plus(N, s M) -> mark U41(isNat M, M, N),
        active plus(N, 0()) -> mark U31(isNat N, N),
        active plus(X1, X2) -> plus(X1, active X2),
        active plus(X1, X2) -> plus(active X1, X2),
           U11(mark X1, X2) -> mark U11(X1, X2),
          U11(ok X1, ok X2) -> ok U11(X1, X2),
                 U21 mark X -> mark U21 X,
                   U21 ok X -> ok U21 X,
           U31(mark X1, X2) -> mark U31(X1, X2),
          U31(ok X1, ok X2) -> ok U31(X1, X2),
       U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
   U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
       U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
   U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                   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),
               proper U12 X -> U12 proper X,
             proper isNat X -> isNat proper X,
         proper U11(X1, X2) -> U11(proper X1, proper X2),
                proper tt() -> ok tt(),
               proper U21 X -> U21 proper X,
         proper U31(X1, X2) -> U31(proper X1, proper X2),
     proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
     proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                 proper s X -> s proper X,
        proper plus(X1, X2) -> plus(proper X1, proper X2),
                 proper 0() -> ok 0(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
 DP:
  DP:
   {               U12# mark X -> U12# X,
                     U12# ok X -> U12# X,
                   isNat# ok X -> isNat# X,
                 active# U12 X -> U12# active X,
                 active# U12 X -> active# X,
            active# isNat s V1 -> isNat# V1,
            active# isNat s V1 -> U21# isNat V1,
    active# isNat plus(V1, V2) -> isNat# V1,
    active# isNat plus(V1, V2) -> U11#(isNat V1, V2),
           active# U11(X1, X2) -> active# X1,
           active# U11(X1, X2) -> U11#(active X1, X2),
         active# U11(tt(), V2) -> U12# isNat V2,
         active# U11(tt(), V2) -> isNat# V2,
                 active# U21 X -> active# X,
                 active# U21 X -> U21# active X,
           active# U31(X1, X2) -> active# X1,
           active# U31(X1, X2) -> U31#(active X1, X2),
       active# U42(X1, X2, X3) -> active# X1,
       active# U42(X1, X2, X3) -> U42#(active X1, X2, X3),
       active# U42(tt(), M, N) -> s# plus(N, M),
       active# U42(tt(), M, N) -> plus#(N, M),
       active# U41(X1, X2, X3) -> active# X1,
       active# U41(X1, X2, X3) -> U41#(active X1, X2, X3),
       active# U41(tt(), M, N) -> isNat# N,
       active# U41(tt(), M, N) -> U42#(isNat N, M, N),
                   active# s X -> active# X,
                   active# s X -> s# active X,
          active# plus(N, s M) -> isNat# M,
          active# plus(N, s M) -> U41#(isNat M, M, N),
          active# plus(N, 0()) -> isNat# N,
          active# plus(N, 0()) -> U31#(isNat N, 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),
             U11#(mark X1, X2) -> U11#(X1, X2),
            U11#(ok X1, ok X2) -> U11#(X1, X2),
                   U21# mark X -> U21# X,
                     U21# ok X -> U21# X,
             U31#(mark X1, X2) -> U31#(X1, X2),
            U31#(ok X1, ok X2) -> U31#(X1, X2),
         U42#(mark X1, X2, X3) -> U42#(X1, X2, X3),
     U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3),
         U41#(mark X1, X2, X3) -> U41#(X1, X2, X3),
     U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3),
                     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),
                 proper# U12 X -> U12# proper X,
                 proper# U12 X -> proper# X,
               proper# isNat X -> isNat# proper X,
               proper# isNat X -> proper# X,
           proper# U11(X1, X2) -> U11#(proper X1, proper X2),
           proper# U11(X1, X2) -> proper# X1,
           proper# U11(X1, X2) -> proper# X2,
                 proper# U21 X -> U21# proper X,
                 proper# U21 X -> proper# X,
           proper# U31(X1, X2) -> U31#(proper X1, proper X2),
           proper# U31(X1, X2) -> proper# X1,
           proper# U31(X1, X2) -> proper# X2,
       proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3),
       proper# U42(X1, X2, X3) -> proper# X1,
       proper# U42(X1, X2, X3) -> proper# X2,
       proper# U42(X1, X2, X3) -> proper# X3,
       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# 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,
                   top# mark X -> proper# X,
                   top# mark X -> top# proper X,
                     top# ok X -> active# X,
                     top# ok X -> top# active X}
  TRS:
  {               U12 mark X -> mark U12 X,
                    U12 ok X -> ok U12 X,
                  isNat ok X -> ok isNat X,
                active U12 X -> U12 active X,
             active U12 tt() -> mark tt(),
           active isNat s V1 -> mark U21 isNat V1,
   active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
            active isNat 0() -> mark tt(),
          active U11(X1, X2) -> U11(active X1, X2),
        active U11(tt(), V2) -> mark U12 isNat V2,
                active U21 X -> U21 active X,
             active U21 tt() -> mark tt(),
          active U31(X1, X2) -> U31(active X1, X2),
         active U31(tt(), N) -> mark N,
      active U42(X1, X2, X3) -> U42(active X1, X2, X3),
      active U42(tt(), M, N) -> mark s plus(N, M),
      active U41(X1, X2, X3) -> U41(active X1, X2, X3),
      active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                  active s X -> s active X,
         active plus(N, s M) -> mark U41(isNat M, M, N),
         active plus(N, 0()) -> mark U31(isNat N, N),
         active plus(X1, X2) -> plus(X1, active X2),
         active plus(X1, X2) -> plus(active X1, X2),
            U11(mark X1, X2) -> mark U11(X1, X2),
           U11(ok X1, ok X2) -> ok U11(X1, X2),
                  U21 mark X -> mark U21 X,
                    U21 ok X -> ok U21 X,
            U31(mark X1, X2) -> mark U31(X1, X2),
           U31(ok X1, ok X2) -> ok U31(X1, X2),
        U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
    U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
        U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
    U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                    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),
                proper U12 X -> U12 proper X,
              proper isNat X -> isNat proper X,
          proper U11(X1, X2) -> U11(proper X1, proper X2),
                 proper tt() -> ok tt(),
                proper U21 X -> U21 proper X,
          proper U31(X1, X2) -> U31(proper X1, proper X2),
      proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
      proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                  proper s X -> s proper X,
         proper plus(X1, X2) -> plus(proper X1, proper X2),
                  proper 0() -> ok 0(),
                  top mark X -> top proper X,
                    top ok X -> top active X}
  UR:
   {               U12 mark X -> mark U12 X,
                     U12 ok X -> ok U12 X,
                   isNat ok X -> ok isNat X,
                 active U12 X -> U12 active X,
              active U12 tt() -> mark tt(),
            active isNat s V1 -> mark U21 isNat V1,
    active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
             active isNat 0() -> mark tt(),
           active U11(X1, X2) -> U11(active X1, X2),
         active U11(tt(), V2) -> mark U12 isNat V2,
                 active U21 X -> U21 active X,
              active U21 tt() -> mark tt(),
           active U31(X1, X2) -> U31(active X1, X2),
          active U31(tt(), N) -> mark N,
       active U42(X1, X2, X3) -> U42(active X1, X2, X3),
       active U42(tt(), M, N) -> mark s plus(N, M),
       active U41(X1, X2, X3) -> U41(active X1, X2, X3),
       active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                   active s X -> s active X,
          active plus(N, s M) -> mark U41(isNat M, M, N),
          active plus(N, 0()) -> mark U31(isNat N, N),
          active plus(X1, X2) -> plus(X1, active X2),
          active plus(X1, X2) -> plus(active X1, X2),
             U11(mark X1, X2) -> mark U11(X1, X2),
            U11(ok X1, ok X2) -> ok U11(X1, X2),
                   U21 mark X -> mark U21 X,
                     U21 ok X -> ok U21 X,
             U31(mark X1, X2) -> mark U31(X1, X2),
            U31(ok X1, ok X2) -> ok U31(X1, X2),
         U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
     U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
         U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
     U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                     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),
                 proper U12 X -> U12 proper X,
               proper isNat X -> isNat proper X,
           proper U11(X1, X2) -> U11(proper X1, proper X2),
                  proper tt() -> ok tt(),
                 proper U21 X -> U21 proper X,
           proper U31(X1, X2) -> U31(proper X1, proper X2),
       proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
       proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                   proper s X -> s proper X,
          proper plus(X1, X2) -> plus(proper X1, proper X2),
                   proper 0() -> ok 0()}
   EDG:
    {
     (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# 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# U42(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X2, proper# U21 X -> proper# X)
     (proper# U11(X1, X2) -> proper# X2, proper# U21 X -> U21# 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# 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# U12 X -> proper# X)
     (proper# U11(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U21 X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U21 X -> U21# proper X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X2, proper# isNat X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U12 X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X2, proper# U12 X -> U12# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (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# X1)
     (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# U42(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# U21 X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# U21 X -> U21# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# plus(X1, X2) -> proper# X2, proper# U12 X -> proper# X)
     (proper# plus(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
     (active# U41(tt(), M, N) -> isNat# N, isNat# ok X -> isNat# 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# plus(X1, X2) -> plus#(active X1, X2), plus#(ok X1, ok 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#(X1, mark X2) -> plus#(X1, X2))
     (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))
     (U31#(ok X1, ok X2) -> U31#(X1, X2), U31#(ok X1, ok X2) -> U31#(X1, X2))
     (U31#(ok X1, ok X2) -> U31#(X1, X2), U31#(mark X1, X2) -> U31#(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))
     (active# plus(N, 0()) -> U31#(isNat N, N), U31#(ok X1, ok X2) -> U31#(X1, X2))
     (active# plus(N, 0()) -> U31#(isNat N, N), U31#(mark X1, X2) -> U31#(X1, X2))
     (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U31(X1, X2) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, N))
     (active# U31(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# U31(X1, X2) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# U31(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# U31(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# U31(X1, X2) -> active# X1, active# s X -> active# X)
     (active# U31(X1, X2) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# U31(X1, X2) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
     (active# U31(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U31(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# U31(X1, X2) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
     (active# U31(X1, X2) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# U31(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# U31(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
     (active# U31(X1, X2) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# U31(X1, X2) -> active# X1, active# U31(X1, X2) -> active# X1)
     (active# U31(X1, X2) -> active# X1, active# U21 X -> U21# active X)
     (active# U31(X1, X2) -> active# X1, active# U21 X -> active# X)
     (active# U31(X1, X2) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
     (active# U31(X1, X2) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
     (active# U31(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U31(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# U31(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# U31(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U31(X1, X2) -> active# X1, active# isNat s V1 -> U21# isNat V1)
     (active# U31(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U31(X1, X2) -> active# X1, active# U12 X -> active# X)
     (active# U31(X1, X2) -> active# X1, active# U12 X -> U12# active X)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, 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) -> active# X2)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> U31#(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(N, s M) -> U41#(isNat M, M, N))
     (active# U41(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# U41(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U41(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U41(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# U41(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
     (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(X1, X2, X3) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
     (active# U41(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# U41(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# U41(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# U41(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# U21 X -> U21# active X)
     (active# U41(X1, X2, X3) -> active# X1, active# U21 X -> active# X)
     (active# U41(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
     (active# U41(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
     (active# U41(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U41(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat s V1 -> U21# isNat V1)
     (active# U41(X1, X2, X3) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U41(X1, X2, X3) -> active# X1, active# U12 X -> active# X)
     (active# U41(X1, X2, X3) -> active# X1, active# U12 X -> U12# active X)
     (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# U11(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (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# X1)
     (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# U42(X1, X2, X3) -> proper# X3)
     (proper# U11(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U11(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# U21 X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# U21 X -> U21# proper X)
     (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U11(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# U11(X1, X2) -> proper# X1, proper# U12 X -> proper# X)
     (proper# U11(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U21 X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U21 X -> U21# proper X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X1, proper# isNat X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U12 X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X1, proper# U12 X -> U12# proper X)
     (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# 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# U42(X1, X2, X3) -> proper# X3)
     (proper# plus(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# plus(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
     (proper# plus(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
     (proper# plus(X1, X2) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# plus(X1, X2) -> proper# X1, proper# U21 X -> proper# X)
     (proper# plus(X1, X2) -> proper# X1, proper# U21 X -> U21# 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# 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# U12 X -> proper# X)
     (proper# plus(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
     (proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
     (proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
     (active# isNat plus(V1, V2) -> U11#(isNat V1, V2), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (active# isNat plus(V1, V2) -> U11#(isNat V1, V2), U11#(mark X1, X2) -> U11#(X1, X2))
     (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# 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# U42(X1, X2, X3) -> proper# X3)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U21 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U21 X -> U21# 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))
     (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# U12 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X3, proper# U12 X -> U12# proper X)
     (active# isNat plus(V1, V2) -> isNat# V1, isNat# ok X -> isNat# X)
     (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
     (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(mark X1, X2) -> U11#(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))
     (active# plus(N, s M) -> U41#(isNat M, M, N), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (active# plus(N, s M) -> U41#(isNat M, M, N), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (active# U21 X -> U21# active X, U21# ok X -> U21# X)
     (active# U21 X -> U21# active X, U21# mark X -> U21# X)
     (proper# U12 X -> U12# proper X, U12# ok X -> U12# X)
     (proper# U12 X -> U12# proper X, U12# mark X -> U12# X)
     (proper# U21 X -> U21# proper X, U21# ok X -> U21# X)
     (proper# U21 X -> U21# proper X, U21# mark X -> U21# 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# isNat s V1 -> U21# isNat V1, U21# ok X -> U21# X)
     (active# isNat s V1 -> U21# isNat V1, U21# mark X -> U21# X)
     (U12# mark X -> U12# X, U12# ok X -> U12# X)
     (U12# mark X -> U12# X, U12# mark X -> U12# X)
     (isNat# ok X -> isNat# X, isNat# ok X -> isNat# X)
     (active# U21 X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U21 X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U21 X -> active# X, active# plus(X1, X2) -> active# X2)
     (active# U21 X -> active# X, active# plus(X1, X2) -> active# X1)
     (active# U21 X -> active# X, active# plus(N, 0()) -> U31#(isNat N, N))
     (active# U21 X -> active# X, active# plus(N, 0()) -> isNat# N)
     (active# U21 X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# U21 X -> active# X, active# plus(N, s M) -> isNat# M)
     (active# U21 X -> active# X, active# s X -> s# active X)
     (active# U21 X -> active# X, active# s X -> active# X)
     (active# U21 X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# U21 X -> active# X, active# U41(tt(), M, N) -> isNat# N)
     (active# U21 X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U21 X -> active# X, active# U41(X1, X2, X3) -> active# X1)
     (active# U21 X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
     (active# U21 X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# U21 X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# U21 X -> active# X, active# U42(X1, X2, X3) -> active# X1)
     (active# U21 X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# U21 X -> active# X, active# U31(X1, X2) -> active# X1)
     (active# U21 X -> active# X, active# U21 X -> U21# active X)
     (active# U21 X -> active# X, active# U21 X -> active# X)
     (active# U21 X -> active# X, active# U11(tt(), V2) -> isNat# V2)
     (active# U21 X -> active# X, active# U11(tt(), V2) -> U12# isNat V2)
     (active# U21 X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U21 X -> active# X, active# U11(X1, X2) -> active# X1)
     (active# U21 X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# U21 X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U21 X -> active# X, active# isNat s V1 -> U21# isNat V1)
     (active# U21 X -> active# X, active# isNat s V1 -> isNat# V1)
     (active# U21 X -> active# X, active# U12 X -> active# X)
     (active# U21 X -> active# X, active# U12 X -> U12# active X)
     (U21# mark X -> U21# X, U21# ok X -> U21# X)
     (U21# mark X -> U21# X, U21# mark X -> U21# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (proper# U12 X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# U12 X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# U12 X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U12 X -> proper# X, proper# s X -> proper# X)
     (proper# U12 X -> proper# X, proper# s X -> s# proper X)
     (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U12 X -> proper# X, proper# U31(X1, X2) -> proper# X2)
     (proper# U12 X -> proper# X, proper# U31(X1, X2) -> proper# X1)
     (proper# U12 X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U12 X -> proper# X, proper# U21 X -> proper# X)
     (proper# U12 X -> proper# X, proper# U21 X -> U21# proper X)
     (proper# U12 X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (proper# U12 X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# U12 X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U12 X -> proper# X, proper# isNat X -> proper# X)
     (proper# U12 X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# U12 X -> proper# X, proper# U12 X -> proper# X)
     (proper# U12 X -> proper# X, proper# U12 X -> U12# proper X)
     (proper# U21 X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# U21 X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# U21 X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U21 X -> proper# X, proper# s X -> proper# X)
     (proper# U21 X -> proper# X, proper# s X -> s# proper X)
     (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U21 X -> proper# X, proper# U31(X1, X2) -> proper# X2)
     (proper# U21 X -> proper# X, proper# U31(X1, X2) -> proper# X1)
     (proper# U21 X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U21 X -> proper# X, proper# U21 X -> proper# X)
     (proper# U21 X -> proper# X, proper# U21 X -> U21# proper X)
     (proper# U21 X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (proper# U21 X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# U21 X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U21 X -> proper# X, proper# isNat X -> proper# X)
     (proper# U21 X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# U21 X -> proper# X, proper# U12 X -> proper# X)
     (proper# U21 X -> proper# X, proper# U12 X -> U12# proper X)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# U31(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# U31(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# U21 X -> proper# X)
     (top# mark X -> proper# X, proper# U21 X -> U21# proper X)
     (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# isNat X -> proper# X)
     (top# mark X -> proper# X, proper# isNat X -> isNat# proper X)
     (top# mark X -> proper# X, proper# U12 X -> proper# X)
     (top# mark X -> proper# X, proper# U12 X -> U12# proper X)
     (active# plus(N, s M) -> isNat# M, isNat# ok X -> isNat# X)
     (active# U42(X1, X2, X3) -> U42#(active X1, X2, X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
     (active# U42(X1, X2, X3) -> U42#(active X1, X2, X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
     (U42#(mark X1, X2, X3) -> U42#(X1, X2, X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
     (U42#(mark X1, X2, X3) -> U42#(X1, X2, X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
     (U41#(mark X1, X2, 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), U41#(mark X1, X2, 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))
     (U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
     (U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
     (active# U41(X1, X2, X3) -> U41#(active X1, X2, X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (active# U41(X1, X2, X3) -> U41#(active X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (active# U42(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X)
     (active# U42(tt(), M, N) -> s# plus(N, M), s# ok X -> s# X)
     (top# ok X -> active# X, active# U12 X -> U12# active X)
     (top# ok X -> active# X, active# U12 X -> active# X)
     (top# ok X -> active# X, active# isNat s V1 -> isNat# V1)
     (top# ok X -> active# X, active# isNat s V1 -> U21# isNat V1)
     (top# ok X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (top# ok X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (top# ok X -> active# X, active# U11(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
     (top# ok X -> active# X, active# U11(tt(), V2) -> U12# isNat V2)
     (top# ok X -> active# X, active# U11(tt(), V2) -> isNat# V2)
     (top# ok X -> active# X, active# U21 X -> active# X)
     (top# ok X -> active# X, active# U21 X -> U21# active X)
     (top# ok X -> active# X, active# U31(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
     (top# ok X -> active# X, active# U42(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (top# ok X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
     (top# ok X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
     (top# ok X -> active# X, active# U41(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (top# ok X -> active# X, active# U41(tt(), M, N) -> isNat# N)
     (top# ok X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# plus(N, s M) -> isNat# M)
     (top# ok X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
     (top# ok X -> active# X, active# plus(N, 0()) -> isNat# N)
     (top# ok X -> active# X, active# plus(N, 0()) -> U31#(isNat N, N))
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (proper# s X -> proper# X, proper# U12 X -> U12# proper X)
     (proper# s X -> proper# X, proper# U12 X -> proper# X)
     (proper# s X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# s X -> proper# X, proper# isNat X -> proper# X)
     (proper# s X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# U21 X -> U21# proper X)
     (proper# s X -> proper# X, proper# U21 X -> proper# X)
     (proper# s X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# U31(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# U31(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U12 X -> U12# proper X)
     (proper# isNat X -> proper# X, proper# U12 X -> proper# X)
     (proper# isNat X -> proper# X, proper# isNat X -> isNat# proper X)
     (proper# isNat X -> proper# X, proper# isNat X -> proper# X)
     (proper# isNat X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# U11(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U11(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U21 X -> U21# proper X)
     (proper# isNat X -> proper# X, proper# U21 X -> proper# X)
     (proper# isNat X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# U31(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U31(X1, X2) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# isNat X -> proper# X, proper# s X -> s# proper X)
     (proper# isNat X -> proper# X, proper# s X -> proper# X)
     (proper# isNat X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# isNat X -> proper# X, proper# plus(X1, X2) -> proper# X1)
     (proper# isNat X -> proper# X, proper# plus(X1, X2) -> proper# X2)
     (s# ok X -> s# X, s# mark X -> s# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (U21# ok X -> U21# X, U21# mark X -> U21# X)
     (U21# ok X -> U21# X, U21# ok X -> U21# X)
     (active# s X -> active# X, active# U12 X -> U12# active X)
     (active# s X -> active# X, active# U12 X -> active# X)
     (active# s X -> active# X, active# isNat s V1 -> isNat# V1)
     (active# s X -> active# X, active# isNat s V1 -> U21# isNat V1)
     (active# s X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (active# s X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (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# U11(tt(), V2) -> U12# isNat V2)
     (active# s X -> active# X, active# U11(tt(), V2) -> isNat# V2)
     (active# s X -> active# X, active# U21 X -> active# X)
     (active# s X -> active# X, active# U21 X -> U21# active X)
     (active# s X -> active# X, active# U31(X1, X2) -> active# X1)
     (active# s X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# s X -> active# X, active# U42(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# s X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# s X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
     (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) -> isNat# N)
     (active# s X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (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) -> isNat# M)
     (active# s X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# s X -> active# X, active# plus(N, 0()) -> isNat# N)
     (active# s X -> active# X, active# plus(N, 0()) -> U31#(isNat N, 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# U12 X -> active# X, active# U12 X -> U12# active X)
     (active# U12 X -> active# X, active# U12 X -> active# X)
     (active# U12 X -> active# X, active# isNat s V1 -> isNat# V1)
     (active# U12 X -> active# X, active# isNat s V1 -> U21# isNat V1)
     (active# U12 X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U12 X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# U12 X -> active# X, active# U11(X1, X2) -> active# X1)
     (active# U12 X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U12 X -> active# X, active# U11(tt(), V2) -> U12# isNat V2)
     (active# U12 X -> active# X, active# U11(tt(), V2) -> isNat# V2)
     (active# U12 X -> active# X, active# U21 X -> active# X)
     (active# U12 X -> active# X, active# U21 X -> U21# active X)
     (active# U12 X -> active# X, active# U31(X1, X2) -> active# X1)
     (active# U12 X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# U12 X -> active# X, active# U42(X1, X2, X3) -> active# X1)
     (active# U12 X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# U12 X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# U12 X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
     (active# U12 X -> active# X, active# U41(X1, X2, X3) -> active# X1)
     (active# U12 X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U12 X -> active# X, active# U41(tt(), M, N) -> isNat# N)
     (active# U12 X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# U12 X -> active# X, active# s X -> active# X)
     (active# U12 X -> active# X, active# s X -> s# active X)
     (active# U12 X -> active# X, active# plus(N, s M) -> isNat# M)
     (active# U12 X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# U12 X -> active# X, active# plus(N, 0()) -> isNat# N)
     (active# U12 X -> active# X, active# plus(N, 0()) -> U31#(isNat N, N))
     (active# U12 X -> active# X, active# plus(X1, X2) -> active# X1)
     (active# U12 X -> active# X, active# plus(X1, X2) -> active# X2)
     (active# U12 X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U12 X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
     (U12# ok X -> U12# X, U12# mark X -> U12# X)
     (U12# ok X -> U12# X, U12# ok X -> U12# X)
     (active# U11(tt(), V2) -> U12# isNat V2, U12# mark X -> U12# X)
     (active# U11(tt(), V2) -> U12# isNat V2, U12# ok X -> U12# X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# isNat X -> isNat# proper X, isNat# ok X -> isNat# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# s X -> s# active X, s# ok X -> s# X)
     (active# U12 X -> U12# active X, U12# mark X -> U12# X)
     (active# U12 X -> U12# active X, U12# ok X -> U12# X)
     (active# U41(tt(), M, N) -> U42#(isNat N, M, N), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
     (active# U41(tt(), M, N) -> U42#(isNat N, M, N), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
     (proper# U31(X1, X2) -> U31#(proper X1, proper X2), U31#(mark X1, X2) -> U31#(X1, X2))
     (proper# U31(X1, X2) -> U31#(proper X1, proper X2), U31#(ok X1, ok X2) -> U31#(X1, X2))
     (active# plus(X1, X2) -> plus#(X1, active X2), plus#(X1, mark 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#(ok X1, ok X2) -> plus#(X1, X2))
     (active# isNat s V1 -> isNat# V1, isNat# ok X -> isNat# X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U12 X -> U12# proper X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U12 X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# isNat X -> isNat# proper X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# isNat X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U21 X -> U21# proper X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U21 X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U42(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
     (proper# U42(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
     (proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
     (active# U11(tt(), V2) -> isNat# V2, isNat# ok X -> isNat# X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U12 X -> U12# proper X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U12 X -> proper# X)
     (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# 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# U21 X -> U21# proper X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U21 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X3)
     (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# 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# U31(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
     (proper# U31(X1, X2) -> proper# X1, proper# U12 X -> proper# X)
     (proper# U31(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
     (proper# U31(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
     (proper# U31(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U31(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X1, proper# U21 X -> U21# proper X)
     (proper# U31(X1, X2) -> proper# X1, proper# U21 X -> proper# X)
     (proper# U31(X1, X2) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U31(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U31(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# U31(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# U31(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U31(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
     (active# plus(X1, X2) -> active# X1, active# U12 X -> U12# active X)
     (active# plus(X1, X2) -> active# X1, active# U12 X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# plus(X1, X2) -> active# X1, active# isNat s V1 -> U21# isNat V1)
     (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# plus(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
     (active# plus(X1, X2) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
     (active# plus(X1, X2) -> active# X1, active# U21 X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# U21 X -> U21# active X)
     (active# plus(X1, X2) -> active# X1, active# U31(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# plus(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
     (active# plus(X1, X2) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# plus(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# plus(X1, X2) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, N))
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
     (active# U42(X1, X2, X3) -> active# X1, active# U12 X -> U12# active X)
     (active# U42(X1, X2, X3) -> active# X1, active# U12 X -> active# X)
     (active# U42(X1, X2, X3) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U42(X1, X2, X3) -> active# X1, active# isNat s V1 -> U21# isNat V1)
     (active# U42(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U42(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# U42(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> active# X1)
     (active# U42(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# U42(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
     (active# U42(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
     (active# U42(X1, X2, X3) -> active# X1, active# U21 X -> active# X)
     (active# U42(X1, X2, X3) -> active# X1, active# U21 X -> U21# active X)
     (active# U42(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> active# X1)
     (active# U42(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# U42(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
     (active# U42(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# U42(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# U42(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
     (active# U42(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
     (active# U42(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# U42(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
     (active# U42(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# U42(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# U42(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# U42(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# M)
     (active# U42(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# U42(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# U42(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, N))
     (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
     (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
     (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
     (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
     (active# U11(X1, X2) -> active# X1, active# U12 X -> U12# active X)
     (active# U11(X1, X2) -> active# X1, active# U12 X -> active# X)
     (active# U11(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
     (active# U11(X1, X2) -> active# X1, active# isNat s V1 -> U21# isNat V1)
     (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
     (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, 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# U11(tt(), V2) -> U12# isNat V2)
     (active# U11(X1, X2) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
     (active# U11(X1, X2) -> active# X1, active# U21 X -> active# X)
     (active# U11(X1, X2) -> active# X1, active# U21 X -> U21# active X)
     (active# U11(X1, X2) -> active# X1, active# U31(X1, X2) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# U11(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
     (active# U11(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# U11(X1, X2) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# U11(X1, X2) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
     (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) -> isNat# N)
     (active# U11(X1, X2) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (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) -> isNat# M)
     (active# U11(X1, X2) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# U11(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
     (active# U11(X1, X2) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, 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))
     (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))
     (U31#(mark X1, X2) -> U31#(X1, X2), U31#(mark X1, X2) -> U31#(X1, X2))
     (U31#(mark X1, X2) -> U31#(X1, X2), U31#(ok X1, ok X2) -> U31#(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# U31(X1, X2) -> U31#(active X1, X2), U31#(mark X1, X2) -> U31#(X1, X2))
     (active# U31(X1, X2) -> U31#(active X1, X2), U31#(ok X1, ok X2) -> U31#(X1, X2))
     (active# plus(N, 0()) -> isNat# N, isNat# ok X -> isNat# X)
     (active# U42(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2))
     (active# U42(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2))
     (active# U42(tt(), M, N) -> plus#(N, M), plus#(ok X1, ok X2) -> plus#(X1, X2))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U12 X -> U12# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U12 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# isNat X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, 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) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U21 X -> U21# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U21 X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X3)
     (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# U41(X1, X2, X3) -> proper# X1)
     (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# X3)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# U41(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, 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) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
     (proper# U31(X1, X2) -> proper# X2, proper# U12 X -> proper# X)
     (proper# U31(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
     (proper# U31(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
     (proper# U31(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
     (proper# U31(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X2, proper# U21 X -> U21# proper X)
     (proper# U31(X1, X2) -> proper# X2, proper# U21 X -> proper# X)
     (proper# U31(X1, X2) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
     (proper# U31(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
     (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X3)
     (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
     (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
     (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
     (proper# U31(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# U31(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# U31(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
     (proper# U31(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
     (proper# U31(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
     (active# plus(X1, X2) -> active# X2, active# U12 X -> U12# active X)
     (active# plus(X1, X2) -> active# X2, active# U12 X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# isNat s V1 -> isNat# V1)
     (active# plus(X1, X2) -> active# X2, active# isNat s V1 -> U21# isNat V1)
     (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> isNat# V1)
     (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
     (active# plus(X1, X2) -> active# X2, active# U11(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U11(X1, X2) -> U11#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# U11(tt(), V2) -> U12# isNat V2)
     (active# plus(X1, X2) -> active# X2, active# U11(tt(), V2) -> isNat# V2)
     (active# plus(X1, X2) -> active# X2, active# U21 X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# U21 X -> U21# active X)
     (active# plus(X1, X2) -> active# X2, active# U31(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U31(X1, X2) -> U31#(active X1, X2))
     (active# plus(X1, X2) -> active# X2, active# U42(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U42(tt(), M, N) -> s# plus(N, M))
     (active# plus(X1, X2) -> active# X2, active# U42(tt(), M, N) -> plus#(N, M))
     (active# plus(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
     (active# plus(X1, X2) -> active# X2, active# U41(tt(), M, N) -> isNat# N)
     (active# plus(X1, X2) -> active# X2, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
     (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
     (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> isNat# M)
     (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> U41#(isNat M, M, N))
     (active# plus(X1, X2) -> active# X2, active# plus(N, 0()) -> isNat# N)
     (active# plus(X1, X2) -> active# X2, active# plus(N, 0()) -> U31#(isNat N, N))
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
     (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
    }
    EDG:
     {
      (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# 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# U42(X1, X2, X3) -> proper# X3)
      (proper# U11(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U11(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U11(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U11(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
      (proper# U11(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
      (proper# U11(X1, X2) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U11(X1, X2) -> proper# X2, proper# U21 X -> proper# X)
      (proper# U11(X1, X2) -> proper# X2, proper# U21 X -> U21# 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# 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# U12 X -> proper# X)
      (proper# U11(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U21 X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U21 X -> U21# proper X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X2, proper# isNat X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# isNat X -> isNat# proper X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U12 X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X2, proper# U12 X -> U12# proper X)
      (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
      (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# plus(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# plus(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# plus(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
      (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# X1)
      (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# U42(X1, X2, X3) -> proper# X3)
      (proper# plus(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# plus(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# plus(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
      (proper# plus(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# plus(X1, X2) -> proper# X2, proper# U21 X -> proper# X)
      (proper# plus(X1, X2) -> proper# X2, proper# U21 X -> U21# proper X)
      (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
      (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# plus(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
      (proper# plus(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
      (proper# plus(X1, X2) -> proper# X2, proper# U12 X -> proper# X)
      (proper# plus(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
      (active# U41(tt(), M, N) -> isNat# N, isNat# ok X -> isNat# 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# plus(X1, X2) -> plus#(active X1, X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
      (active# plus(X1, X2) -> plus#(active X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
      (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))
      (U31#(ok X1, ok X2) -> U31#(X1, X2), U31#(ok X1, ok X2) -> U31#(X1, X2))
      (U31#(ok X1, ok X2) -> U31#(X1, X2), U31#(mark X1, X2) -> U31#(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))
      (active# plus(N, 0()) -> U31#(isNat N, N), U31#(ok X1, ok X2) -> U31#(X1, X2))
      (active# plus(N, 0()) -> U31#(isNat N, N), U31#(mark X1, X2) -> U31#(X1, X2))
      (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
      (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
      (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X2)
      (active# U31(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# U31(X1, X2) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, N))
      (active# U31(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
      (active# U31(X1, X2) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# U31(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
      (active# U31(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# U31(X1, X2) -> active# X1, active# s X -> active# X)
      (active# U31(X1, X2) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# U31(X1, X2) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
      (active# U31(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (active# U31(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
      (active# U31(X1, X2) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
      (active# U31(X1, X2) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# U31(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# U31(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
      (active# U31(X1, X2) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# U31(X1, X2) -> active# X1, active# U31(X1, X2) -> active# X1)
      (active# U31(X1, X2) -> active# X1, active# U21 X -> U21# active X)
      (active# U31(X1, X2) -> active# X1, active# U21 X -> active# X)
      (active# U31(X1, X2) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
      (active# U31(X1, X2) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
      (active# U31(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# U31(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
      (active# U31(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# U31(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
      (active# U31(X1, X2) -> active# X1, active# isNat s V1 -> U21# isNat V1)
      (active# U31(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
      (active# U31(X1, X2) -> active# X1, active# U12 X -> active# X)
      (active# U31(X1, X2) -> active# X1, active# U12 X -> U12# active X)
      (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, 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) -> active# X2)
      (active# U41(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# U41(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> U31#(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(N, s M) -> U41#(isNat M, M, N))
      (active# U41(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# M)
      (active# U41(X1, X2, X3) -> active# X1, active# s X -> s# active X)
      (active# U41(X1, X2, X3) -> active# X1, active# s X -> active# X)
      (active# U41(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# U41(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
      (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(X1, X2, X3) -> active# X1)
      (active# U41(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
      (active# U41(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# U41(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# U41(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
      (active# U41(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# U41(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> active# X1)
      (active# U41(X1, X2, X3) -> active# X1, active# U21 X -> U21# active X)
      (active# U41(X1, X2, X3) -> active# X1, active# U21 X -> active# X)
      (active# U41(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
      (active# U41(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
      (active# U41(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# U41(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> active# X1)
      (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# U41(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
      (active# U41(X1, X2, X3) -> active# X1, active# isNat s V1 -> U21# isNat V1)
      (active# U41(X1, X2, X3) -> active# X1, active# isNat s V1 -> isNat# V1)
      (active# U41(X1, X2, X3) -> active# X1, active# U12 X -> active# X)
      (active# U41(X1, X2, X3) -> active# X1, active# U12 X -> U12# active X)
      (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
      (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
      (proper# U11(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U11(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# U11(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# U11(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
      (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# X1)
      (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# U42(X1, X2, X3) -> proper# X3)
      (proper# U11(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U11(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U11(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U11(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
      (proper# U11(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
      (proper# U11(X1, X2) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U11(X1, X2) -> proper# X1, proper# U21 X -> proper# X)
      (proper# U11(X1, X2) -> proper# X1, proper# U21 X -> U21# proper X)
      (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
      (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
      (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U11(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
      (proper# U11(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
      (proper# U11(X1, X2) -> proper# X1, proper# U12 X -> proper# X)
      (proper# U11(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U21 X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U21 X -> U21# proper X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X1, proper# isNat X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# isNat X -> isNat# proper X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U12 X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X1, proper# U12 X -> U12# proper X)
      (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# 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# U42(X1, X2, X3) -> proper# X3)
      (proper# plus(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# plus(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# plus(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
      (proper# plus(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
      (proper# plus(X1, X2) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# plus(X1, X2) -> proper# X1, proper# U21 X -> proper# X)
      (proper# plus(X1, X2) -> proper# X1, proper# U21 X -> U21# 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# 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# U12 X -> proper# X)
      (proper# plus(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
      (proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
      (proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
      (active# isNat plus(V1, V2) -> U11#(isNat V1, V2), U11#(ok X1, ok X2) -> U11#(X1, X2))
      (active# isNat plus(V1, V2) -> U11#(isNat V1, V2), U11#(mark X1, X2) -> U11#(X1, X2))
      (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# 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# U42(X1, X2, X3) -> proper# X3)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X1)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U21 X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U21 X -> U21# 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))
      (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# U12 X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X3, proper# U12 X -> U12# proper X)
      (active# isNat plus(V1, V2) -> isNat# V1, isNat# ok X -> isNat# X)
      (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
      (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(mark X1, X2) -> U11#(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))
      (active# plus(N, s M) -> U41#(isNat M, M, N), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
      (active# U21 X -> U21# active X, U21# ok X -> U21# X)
      (active# U21 X -> U21# active X, U21# mark X -> U21# X)
      (proper# U12 X -> U12# proper X, U12# ok X -> U12# X)
      (proper# U12 X -> U12# proper X, U12# mark X -> U12# X)
      (proper# U21 X -> U21# proper X, U21# ok X -> U21# X)
      (proper# U21 X -> U21# proper X, U21# mark X -> U21# 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# isNat s V1 -> U21# isNat V1, U21# ok X -> U21# X)
      (active# isNat s V1 -> U21# isNat V1, U21# mark X -> U21# X)
      (U12# mark X -> U12# X, U12# ok X -> U12# X)
      (U12# mark X -> U12# X, U12# mark X -> U12# X)
      (isNat# ok X -> isNat# X, isNat# ok X -> isNat# X)
      (active# U21 X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
      (active# U21 X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
      (active# U21 X -> active# X, active# plus(X1, X2) -> active# X2)
      (active# U21 X -> active# X, active# plus(X1, X2) -> active# X1)
      (active# U21 X -> active# X, active# plus(N, 0()) -> U31#(isNat N, N))
      (active# U21 X -> active# X, active# plus(N, 0()) -> isNat# N)
      (active# U21 X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# U21 X -> active# X, active# plus(N, s M) -> isNat# M)
      (active# U21 X -> active# X, active# s X -> s# active X)
      (active# U21 X -> active# X, active# s X -> active# X)
      (active# U21 X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# U21 X -> active# X, active# U41(tt(), M, N) -> isNat# N)
      (active# U21 X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (active# U21 X -> active# X, active# U41(X1, X2, X3) -> active# X1)
      (active# U21 X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
      (active# U21 X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# U21 X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# U21 X -> active# X, active# U42(X1, X2, X3) -> active# X1)
      (active# U21 X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# U21 X -> active# X, active# U31(X1, X2) -> active# X1)
      (active# U21 X -> active# X, active# U21 X -> U21# active X)
      (active# U21 X -> active# X, active# U21 X -> active# X)
      (active# U21 X -> active# X, active# U11(tt(), V2) -> isNat# V2)
      (active# U21 X -> active# X, active# U11(tt(), V2) -> U12# isNat V2)
      (active# U21 X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# U21 X -> active# X, active# U11(X1, X2) -> active# X1)
      (active# U21 X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# U21 X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
      (active# U21 X -> active# X, active# isNat s V1 -> U21# isNat V1)
      (active# U21 X -> active# X, active# isNat s V1 -> isNat# V1)
      (active# U21 X -> active# X, active# U12 X -> active# X)
      (active# U21 X -> active# X, active# U12 X -> U12# active X)
      (U21# mark X -> U21# X, U21# ok X -> U21# X)
      (U21# mark X -> U21# X, U21# mark X -> U21# X)
      (s# mark X -> s# X, s# ok X -> s# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (proper# U12 X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (proper# U12 X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (proper# U12 X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U12 X -> proper# X, proper# s X -> proper# X)
      (proper# U12 X -> proper# X, proper# s X -> s# proper X)
      (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U12 X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U12 X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U12 X -> proper# X, proper# U31(X1, X2) -> proper# X2)
      (proper# U12 X -> proper# X, proper# U31(X1, X2) -> proper# X1)
      (proper# U12 X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U12 X -> proper# X, proper# U21 X -> proper# X)
      (proper# U12 X -> proper# X, proper# U21 X -> U21# proper X)
      (proper# U12 X -> proper# X, proper# U11(X1, X2) -> proper# X2)
      (proper# U12 X -> proper# X, proper# U11(X1, X2) -> proper# X1)
      (proper# U12 X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U12 X -> proper# X, proper# isNat X -> proper# X)
      (proper# U12 X -> proper# X, proper# isNat X -> isNat# proper X)
      (proper# U12 X -> proper# X, proper# U12 X -> proper# X)
      (proper# U12 X -> proper# X, proper# U12 X -> U12# proper X)
      (proper# U21 X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (proper# U21 X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (proper# U21 X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U21 X -> proper# X, proper# s X -> proper# X)
      (proper# U21 X -> proper# X, proper# s X -> s# proper X)
      (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U21 X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U21 X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U21 X -> proper# X, proper# U31(X1, X2) -> proper# X2)
      (proper# U21 X -> proper# X, proper# U31(X1, X2) -> proper# X1)
      (proper# U21 X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U21 X -> proper# X, proper# U21 X -> proper# X)
      (proper# U21 X -> proper# X, proper# U21 X -> U21# proper X)
      (proper# U21 X -> proper# X, proper# U11(X1, X2) -> proper# X2)
      (proper# U21 X -> proper# X, proper# U11(X1, X2) -> proper# X1)
      (proper# U21 X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U21 X -> proper# X, proper# isNat X -> proper# X)
      (proper# U21 X -> proper# X, proper# isNat X -> isNat# proper X)
      (proper# U21 X -> proper# X, proper# U12 X -> proper# X)
      (proper# U21 X -> proper# X, proper# U12 X -> U12# proper X)
      (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# s X -> proper# X)
      (top# mark X -> proper# X, proper# s X -> s# proper X)
      (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
      (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
      (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
      (top# mark X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
      (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
      (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
      (top# mark X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (top# mark X -> proper# X, proper# U31(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# U31(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# U21 X -> proper# X)
      (top# mark X -> proper# X, proper# U21 X -> U21# proper X)
      (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# isNat X -> proper# X)
      (top# mark X -> proper# X, proper# isNat X -> isNat# proper X)
      (top# mark X -> proper# X, proper# U12 X -> proper# X)
      (top# mark X -> proper# X, proper# U12 X -> U12# proper X)
      (active# U42(X1, X2, X3) -> U42#(active X1, X2, X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
      (active# U42(X1, X2, X3) -> U42#(active X1, X2, X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
      (U42#(mark X1, X2, X3) -> U42#(X1, X2, X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
      (U42#(mark X1, X2, X3) -> U42#(X1, X2, X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
      (U41#(mark X1, X2, 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), U41#(mark X1, X2, 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))
      (U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
      (U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
      (U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
      (active# U41(X1, X2, X3) -> U41#(active X1, X2, X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
      (active# U41(X1, X2, X3) -> U41#(active X1, X2, X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
      (active# U42(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X)
      (active# U42(tt(), M, N) -> s# plus(N, M), s# ok X -> s# X)
      (top# ok X -> active# X, active# U12 X -> U12# active X)
      (top# ok X -> active# X, active# U12 X -> active# X)
      (top# ok X -> active# X, active# isNat s V1 -> isNat# V1)
      (top# ok X -> active# X, active# isNat s V1 -> U21# isNat V1)
      (top# ok X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
      (top# ok X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (top# ok X -> active# X, active# U11(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
      (top# ok X -> active# X, active# U11(tt(), V2) -> U12# isNat V2)
      (top# ok X -> active# X, active# U11(tt(), V2) -> isNat# V2)
      (top# ok X -> active# X, active# U21 X -> active# X)
      (top# ok X -> active# X, active# U21 X -> U21# active X)
      (top# ok X -> active# X, active# U31(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
      (top# ok X -> active# X, active# U42(X1, X2, X3) -> active# X1)
      (top# ok X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (top# ok X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
      (top# ok X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
      (top# ok X -> active# X, active# U41(X1, X2, X3) -> active# X1)
      (top# ok X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (top# ok X -> active# X, active# U41(tt(), M, N) -> isNat# N)
      (top# ok X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (top# ok X -> active# X, active# s X -> active# X)
      (top# ok X -> active# X, active# s X -> s# active X)
      (top# ok X -> active# X, active# plus(N, s M) -> isNat# M)
      (top# ok X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
      (top# ok X -> active# X, active# plus(N, 0()) -> isNat# N)
      (top# ok X -> active# X, active# plus(N, 0()) -> U31#(isNat N, N))
      (top# ok X -> active# X, active# plus(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# plus(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
      (top# ok X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
      (proper# s X -> proper# X, proper# U12 X -> U12# proper X)
      (proper# s X -> proper# X, proper# U12 X -> proper# X)
      (proper# s X -> proper# X, proper# isNat X -> isNat# proper X)
      (proper# s X -> proper# X, proper# isNat X -> proper# X)
      (proper# s X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# U11(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# U11(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# U21 X -> U21# proper X)
      (proper# s X -> proper# X, proper# U21 X -> proper# X)
      (proper# s X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# U31(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# U31(X1, X2) -> proper# X2)
      (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# s X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# s X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# s X -> proper# X, proper# s X -> s# proper X)
      (proper# s X -> proper# X, proper# s X -> proper# X)
      (proper# s X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (proper# s X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (proper# isNat X -> proper# X, proper# U12 X -> U12# proper X)
      (proper# isNat X -> proper# X, proper# U12 X -> proper# X)
      (proper# isNat X -> proper# X, proper# isNat X -> isNat# proper X)
      (proper# isNat X -> proper# X, proper# isNat X -> proper# X)
      (proper# isNat X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# isNat X -> proper# X, proper# U11(X1, X2) -> proper# X1)
      (proper# isNat X -> proper# X, proper# U11(X1, X2) -> proper# X2)
      (proper# isNat X -> proper# X, proper# U21 X -> U21# proper X)
      (proper# isNat X -> proper# X, proper# U21 X -> proper# X)
      (proper# isNat X -> proper# X, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# isNat X -> proper# X, proper# U31(X1, X2) -> proper# X1)
      (proper# isNat X -> proper# X, proper# U31(X1, X2) -> proper# X2)
      (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# isNat X -> proper# X, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# isNat X -> proper# X, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# isNat X -> proper# X, proper# s X -> s# proper X)
      (proper# isNat X -> proper# X, proper# s X -> proper# X)
      (proper# isNat X -> proper# X, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# isNat X -> proper# X, proper# plus(X1, X2) -> proper# X1)
      (proper# isNat X -> proper# X, proper# plus(X1, X2) -> proper# X2)
      (s# ok X -> s# X, s# mark X -> s# X)
      (s# ok X -> s# X, s# ok X -> s# X)
      (U21# ok X -> U21# X, U21# mark X -> U21# X)
      (U21# ok X -> U21# X, U21# ok X -> U21# X)
      (active# s X -> active# X, active# U12 X -> U12# active X)
      (active# s X -> active# X, active# U12 X -> active# X)
      (active# s X -> active# X, active# isNat s V1 -> isNat# V1)
      (active# s X -> active# X, active# isNat s V1 -> U21# isNat V1)
      (active# s X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
      (active# s X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (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# U11(tt(), V2) -> U12# isNat V2)
      (active# s X -> active# X, active# U11(tt(), V2) -> isNat# V2)
      (active# s X -> active# X, active# U21 X -> active# X)
      (active# s X -> active# X, active# U21 X -> U21# active X)
      (active# s X -> active# X, active# U31(X1, X2) -> active# X1)
      (active# s X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# s X -> active# X, active# U42(X1, X2, X3) -> active# X1)
      (active# s X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# s X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# s X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
      (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) -> isNat# N)
      (active# s X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (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) -> isNat# M)
      (active# s X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# s X -> active# X, active# plus(N, 0()) -> isNat# N)
      (active# s X -> active# X, active# plus(N, 0()) -> U31#(isNat N, 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# U12 X -> active# X, active# U12 X -> U12# active X)
      (active# U12 X -> active# X, active# U12 X -> active# X)
      (active# U12 X -> active# X, active# isNat s V1 -> isNat# V1)
      (active# U12 X -> active# X, active# isNat s V1 -> U21# isNat V1)
      (active# U12 X -> active# X, active# isNat plus(V1, V2) -> isNat# V1)
      (active# U12 X -> active# X, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# U12 X -> active# X, active# U11(X1, X2) -> active# X1)
      (active# U12 X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# U12 X -> active# X, active# U11(tt(), V2) -> U12# isNat V2)
      (active# U12 X -> active# X, active# U11(tt(), V2) -> isNat# V2)
      (active# U12 X -> active# X, active# U21 X -> active# X)
      (active# U12 X -> active# X, active# U21 X -> U21# active X)
      (active# U12 X -> active# X, active# U31(X1, X2) -> active# X1)
      (active# U12 X -> active# X, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# U12 X -> active# X, active# U42(X1, X2, X3) -> active# X1)
      (active# U12 X -> active# X, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# U12 X -> active# X, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# U12 X -> active# X, active# U42(tt(), M, N) -> plus#(N, M))
      (active# U12 X -> active# X, active# U41(X1, X2, X3) -> active# X1)
      (active# U12 X -> active# X, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (active# U12 X -> active# X, active# U41(tt(), M, N) -> isNat# N)
      (active# U12 X -> active# X, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# U12 X -> active# X, active# s X -> active# X)
      (active# U12 X -> active# X, active# s X -> s# active X)
      (active# U12 X -> active# X, active# plus(N, s M) -> isNat# M)
      (active# U12 X -> active# X, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# U12 X -> active# X, active# plus(N, 0()) -> isNat# N)
      (active# U12 X -> active# X, active# plus(N, 0()) -> U31#(isNat N, N))
      (active# U12 X -> active# X, active# plus(X1, X2) -> active# X1)
      (active# U12 X -> active# X, active# plus(X1, X2) -> active# X2)
      (active# U12 X -> active# X, active# plus(X1, X2) -> plus#(X1, active X2))
      (active# U12 X -> active# X, active# plus(X1, X2) -> plus#(active X1, X2))
      (U12# ok X -> U12# X, U12# mark X -> U12# X)
      (U12# ok X -> U12# X, U12# ok X -> U12# X)
      (active# U11(tt(), V2) -> U12# isNat V2, U12# mark X -> U12# X)
      (active# U11(tt(), V2) -> U12# isNat V2, U12# ok X -> U12# X)
      (top# ok X -> top# active X, top# mark X -> proper# X)
      (top# ok X -> top# active X, top# mark X -> top# proper X)
      (top# ok X -> top# active X, top# ok X -> active# X)
      (top# ok X -> top# active X, top# ok X -> top# active X)
      (proper# s X -> s# proper X, s# mark X -> s# X)
      (proper# s X -> s# proper X, s# ok X -> s# X)
      (proper# isNat X -> isNat# proper X, isNat# ok X -> isNat# X)
      (active# s X -> s# active X, s# mark X -> s# X)
      (active# s X -> s# active X, s# ok X -> s# X)
      (active# U12 X -> U12# active X, U12# mark X -> U12# X)
      (active# U12 X -> U12# active X, U12# ok X -> U12# X)
      (active# U41(tt(), M, N) -> U42#(isNat N, M, N), U42#(mark X1, X2, X3) -> U42#(X1, X2, X3))
      (active# U41(tt(), M, N) -> U42#(isNat N, M, N), U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3))
      (proper# U31(X1, X2) -> U31#(proper X1, proper X2), U31#(mark X1, X2) -> U31#(X1, X2))
      (proper# U31(X1, X2) -> U31#(proper X1, proper X2), U31#(ok X1, ok X2) -> U31#(X1, X2))
      (active# plus(X1, X2) -> plus#(X1, active X2), plus#(X1, mark X2) -> plus#(X1, X2))
      (active# plus(X1, X2) -> plus#(X1, active X2), plus#(ok X1, ok X2) -> plus#(X1, X2))
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U12 X -> U12# proper X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U12 X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# isNat X -> isNat# proper X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# isNat X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U11(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U21 X -> U21# proper X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U21 X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U31(X1, X2) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U42(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X1)
      (proper# U42(X1, X2, X3) -> proper# X3, proper# plus(X1, X2) -> proper# X2)
      (proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3), U41#(mark X1, X2, X3) -> U41#(X1, X2, X3))
      (proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3), U41#(ok X1, ok X2, ok X3) -> U41#(X1, X2, X3))
      (active# U11(tt(), V2) -> isNat# V2, isNat# ok X -> isNat# X)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U12 X -> U12# proper X)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U12 X -> proper# X)
      (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# 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# U21 X -> U21# proper X)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U21 X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X3)
      (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# 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# U31(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
      (proper# U31(X1, X2) -> proper# X1, proper# U12 X -> proper# X)
      (proper# U31(X1, X2) -> proper# X1, proper# isNat X -> isNat# proper X)
      (proper# U31(X1, X2) -> proper# X1, proper# isNat X -> proper# X)
      (proper# U31(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U31(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X1, proper# U21 X -> U21# proper X)
      (proper# U31(X1, X2) -> proper# X1, proper# U21 X -> proper# X)
      (proper# U31(X1, X2) -> proper# X1, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U31(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X1, proper# U31(X1, X2) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X1, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X1, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U31(X1, X2) -> proper# X1, proper# s X -> s# proper X)
      (proper# U31(X1, X2) -> proper# X1, proper# s X -> proper# X)
      (proper# U31(X1, X2) -> proper# X1, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U31(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X1, proper# plus(X1, X2) -> proper# X2)
      (active# plus(X1, X2) -> active# X1, active# U12 X -> U12# active X)
      (active# plus(X1, X2) -> active# X1, active# U12 X -> active# X)
      (active# plus(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
      (active# plus(X1, X2) -> active# X1, active# isNat s V1 -> U21# isNat V1)
      (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
      (active# plus(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# plus(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# plus(X1, X2) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
      (active# plus(X1, X2) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
      (active# plus(X1, X2) -> active# X1, active# U21 X -> active# X)
      (active# plus(X1, X2) -> active# X1, active# U21 X -> U21# active X)
      (active# plus(X1, X2) -> active# X1, active# U31(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# plus(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# plus(X1, X2) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# plus(X1, X2) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
      (active# plus(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (active# plus(X1, X2) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
      (active# plus(X1, X2) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# plus(X1, X2) -> active# X1, active# s X -> active# X)
      (active# plus(X1, X2) -> active# X1, active# s X -> s# active X)
      (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> isNat# M)
      (active# plus(X1, X2) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# plus(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
      (active# plus(X1, X2) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, N))
      (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X1, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
      (active# U42(X1, X2, X3) -> active# X1, active# U12 X -> U12# active X)
      (active# U42(X1, X2, X3) -> active# X1, active# U12 X -> active# X)
      (active# U42(X1, X2, X3) -> active# X1, active# isNat s V1 -> isNat# V1)
      (active# U42(X1, X2, X3) -> active# X1, active# isNat s V1 -> U21# isNat V1)
      (active# U42(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
      (active# U42(X1, X2, X3) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# U42(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> active# X1)
      (active# U42(X1, X2, X3) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# U42(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> U12# isNat V2)
      (active# U42(X1, X2, X3) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
      (active# U42(X1, X2, X3) -> active# X1, active# U21 X -> active# X)
      (active# U42(X1, X2, X3) -> active# X1, active# U21 X -> U21# active X)
      (active# U42(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> active# X1)
      (active# U42(X1, X2, X3) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# U42(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
      (active# U42(X1, X2, X3) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# U42(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# U42(X1, X2, X3) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
      (active# U42(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> active# X1)
      (active# U42(X1, X2, X3) -> active# X1, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (active# U42(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> isNat# N)
      (active# U42(X1, X2, X3) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# U42(X1, X2, X3) -> active# X1, active# s X -> active# X)
      (active# U42(X1, X2, X3) -> active# X1, active# s X -> s# active X)
      (active# U42(X1, X2, X3) -> active# X1, active# plus(N, s M) -> isNat# M)
      (active# U42(X1, X2, X3) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# U42(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> isNat# N)
      (active# U42(X1, X2, X3) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, N))
      (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X1)
      (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> active# X2)
      (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(X1, active X2))
      (active# U42(X1, X2, X3) -> active# X1, active# plus(X1, X2) -> plus#(active X1, X2))
      (active# U11(X1, X2) -> active# X1, active# U12 X -> U12# active X)
      (active# U11(X1, X2) -> active# X1, active# U12 X -> active# X)
      (active# U11(X1, X2) -> active# X1, active# isNat s V1 -> isNat# V1)
      (active# U11(X1, X2) -> active# X1, active# isNat s V1 -> U21# isNat V1)
      (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> isNat# V1)
      (active# U11(X1, X2) -> active# X1, active# isNat plus(V1, V2) -> U11#(isNat V1, 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# U11(tt(), V2) -> U12# isNat V2)
      (active# U11(X1, X2) -> active# X1, active# U11(tt(), V2) -> isNat# V2)
      (active# U11(X1, X2) -> active# X1, active# U21 X -> active# X)
      (active# U11(X1, X2) -> active# X1, active# U21 X -> U21# active X)
      (active# U11(X1, X2) -> active# X1, active# U31(X1, X2) -> active# X1)
      (active# U11(X1, X2) -> active# X1, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# U11(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> active# X1)
      (active# U11(X1, X2) -> active# X1, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# U11(X1, X2) -> active# X1, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# U11(X1, X2) -> active# X1, active# U42(tt(), M, N) -> plus#(N, M))
      (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) -> isNat# N)
      (active# U11(X1, X2) -> active# X1, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (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) -> isNat# M)
      (active# U11(X1, X2) -> active# X1, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# U11(X1, X2) -> active# X1, active# plus(N, 0()) -> isNat# N)
      (active# U11(X1, X2) -> active# X1, active# plus(N, 0()) -> U31#(isNat N, 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))
      (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))
      (U31#(mark X1, X2) -> U31#(X1, X2), U31#(mark X1, X2) -> U31#(X1, X2))
      (U31#(mark X1, X2) -> U31#(X1, X2), U31#(ok X1, ok X2) -> U31#(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# U31(X1, X2) -> U31#(active X1, X2), U31#(mark X1, X2) -> U31#(X1, X2))
      (active# U31(X1, X2) -> U31#(active X1, X2), U31#(ok X1, ok X2) -> U31#(X1, X2))
      (active# plus(N, 0()) -> isNat# N, isNat# ok X -> isNat# X)
      (active# U42(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2))
      (active# U42(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2))
      (active# U42(tt(), M, N) -> plus#(N, M), plus#(ok X1, ok X2) -> plus#(X1, X2))
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U12 X -> U12# proper X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U12 X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# isNat X -> isNat# proper X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# isNat X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, 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) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U21 X -> U21# proper X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U21 X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X3)
      (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# U41(X1, X2, X3) -> proper# X1)
      (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# X3)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
      (proper# U41(X1, X2, X3) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, 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) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
      (proper# U31(X1, X2) -> proper# X2, proper# U12 X -> proper# X)
      (proper# U31(X1, X2) -> proper# X2, proper# isNat X -> isNat# proper X)
      (proper# U31(X1, X2) -> proper# X2, proper# isNat X -> proper# X)
      (proper# U31(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
      (proper# U31(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X2, proper# U21 X -> U21# proper X)
      (proper# U31(X1, X2) -> proper# X2, proper# U21 X -> proper# X)
      (proper# U31(X1, X2) -> proper# X2, proper# U31(X1, X2) -> U31#(proper X1, proper X2))
      (proper# U31(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X2, proper# U31(X1, X2) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> U42#(proper X1, proper X2, proper X3))
      (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X2, proper# U42(X1, X2, X3) -> proper# X3)
      (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> U41#(proper X1, proper X2, proper X3))
      (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X2)
      (proper# U31(X1, X2) -> proper# X2, proper# U41(X1, X2, X3) -> proper# X3)
      (proper# U31(X1, X2) -> proper# X2, proper# s X -> s# proper X)
      (proper# U31(X1, X2) -> proper# X2, proper# s X -> proper# X)
      (proper# U31(X1, X2) -> proper# X2, proper# plus(X1, X2) -> plus#(proper X1, proper X2))
      (proper# U31(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X1)
      (proper# U31(X1, X2) -> proper# X2, proper# plus(X1, X2) -> proper# X2)
      (active# plus(X1, X2) -> active# X2, active# U12 X -> U12# active X)
      (active# plus(X1, X2) -> active# X2, active# U12 X -> active# X)
      (active# plus(X1, X2) -> active# X2, active# isNat s V1 -> isNat# V1)
      (active# plus(X1, X2) -> active# X2, active# isNat s V1 -> U21# isNat V1)
      (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> isNat# V1)
      (active# plus(X1, X2) -> active# X2, active# isNat plus(V1, V2) -> U11#(isNat V1, V2))
      (active# plus(X1, X2) -> active# X2, active# U11(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# U11(X1, X2) -> U11#(active X1, X2))
      (active# plus(X1, X2) -> active# X2, active# U11(tt(), V2) -> U12# isNat V2)
      (active# plus(X1, X2) -> active# X2, active# U11(tt(), V2) -> isNat# V2)
      (active# plus(X1, X2) -> active# X2, active# U21 X -> active# X)
      (active# plus(X1, X2) -> active# X2, active# U21 X -> U21# active X)
      (active# plus(X1, X2) -> active# X2, active# U31(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# U31(X1, X2) -> U31#(active X1, X2))
      (active# plus(X1, X2) -> active# X2, active# U42(X1, X2, X3) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# U42(X1, X2, X3) -> U42#(active X1, X2, X3))
      (active# plus(X1, X2) -> active# X2, active# U42(tt(), M, N) -> s# plus(N, M))
      (active# plus(X1, X2) -> active# X2, active# U42(tt(), M, N) -> plus#(N, M))
      (active# plus(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# U41(X1, X2, X3) -> U41#(active X1, X2, X3))
      (active# plus(X1, X2) -> active# X2, active# U41(tt(), M, N) -> isNat# N)
      (active# plus(X1, X2) -> active# X2, active# U41(tt(), M, N) -> U42#(isNat N, M, N))
      (active# plus(X1, X2) -> active# X2, active# s X -> active# X)
      (active# plus(X1, X2) -> active# X2, active# s X -> s# active X)
      (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> isNat# M)
      (active# plus(X1, X2) -> active# X2, active# plus(N, s M) -> U41#(isNat M, M, N))
      (active# plus(X1, X2) -> active# X2, active# plus(N, 0()) -> isNat# N)
      (active# plus(X1, X2) -> active# X2, active# plus(N, 0()) -> U31#(isNat N, N))
      (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# X1)
      (active# plus(X1, X2) -> active# X2, active# plus(X1, X2) -> active# 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) -> plus#(active X1, X2))
     }
     STATUS:
      arrows: 0.864285
      SCCS (12):
       Scc:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Scc:
        {          proper# U12 X -> proper# X,
                 proper# isNat X -> proper# X,
             proper# U11(X1, X2) -> proper# X1,
             proper# U11(X1, X2) -> proper# X2,
                   proper# U21 X -> proper# X,
             proper# U31(X1, X2) -> proper# X1,
             proper# U31(X1, X2) -> proper# X2,
         proper# U42(X1, X2, X3) -> proper# X1,
         proper# U42(X1, X2, X3) -> proper# X2,
         proper# U42(X1, X2, X3) -> proper# X3,
         proper# U41(X1, X2, X3) -> proper# X1,
         proper# U41(X1, X2, X3) -> proper# X2,
         proper# U41(X1, X2, X3) -> proper# X3,
                     proper# s X -> proper# X,
            proper# plus(X1, X2) -> proper# X1,
            proper# plus(X1, X2) -> proper# X2}
       Scc:
        {          active# U12 X -> active# X,
             active# U11(X1, X2) -> active# X1,
                   active# U21 X -> active# X,
             active# U31(X1, X2) -> active# X1,
         active# U42(X1, X2, X3) -> active# X1,
         active# U41(X1, X2, X3) -> active# X1,
                     active# s X -> active# X,
            active# plus(X1, X2) -> active# X1,
            active# plus(X1, X2) -> active# X2}
       Scc:
        {    U41#(mark X1, X2, X3) -> U41#(X1, X2, X3),
         U41#(ok X1, ok X2, ok X3) -> U41#(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:
        {s# mark X -> s# X,
           s# ok X -> s# X}
       Scc:
        {    U42#(mark X1, X2, X3) -> U42#(X1, X2, X3),
         U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3)}
       Scc:
        { U31#(mark X1, X2) -> U31#(X1, X2),
         U31#(ok X1, ok X2) -> U31#(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:
        {U21# mark X -> U21# X,
           U21# ok X -> U21# X}
       Scc:
        {U12# mark X -> U12# X,
           U12# ok X -> U12# X}
       
       SCC (2):
        Strict:
         {top# mark X -> top# proper X,
            top# ok X -> top# active X}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       
       SCC (16):
        Strict:
         {          proper# U12 X -> proper# X,
                  proper# isNat X -> proper# X,
              proper# U11(X1, X2) -> proper# X1,
              proper# U11(X1, X2) -> proper# X2,
                    proper# U21 X -> proper# X,
              proper# U31(X1, X2) -> proper# X1,
              proper# U31(X1, X2) -> proper# X2,
          proper# U42(X1, X2, X3) -> proper# X1,
          proper# U42(X1, X2, X3) -> proper# X2,
          proper# U42(X1, X2, X3) -> proper# X3,
          proper# U41(X1, X2, X3) -> proper# X1,
          proper# U41(X1, X2, X3) -> proper# X2,
          proper# U41(X1, X2, X3) -> proper# X3,
                      proper# s X -> proper# X,
             proper# plus(X1, X2) -> proper# X1,
             proper# plus(X1, X2) -> proper# X2}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       
       
       
       
       
       
       
       
       SCC (9):
        Strict:
         {          active# U12 X -> active# X,
              active# U11(X1, X2) -> active# X1,
                    active# U21 X -> active# X,
              active# U31(X1, X2) -> active# X1,
          active# U42(X1, X2, X3) -> active# X1,
          active# U41(X1, X2, X3) -> active# X1,
                      active# s X -> active# X,
             active# plus(X1, X2) -> active# X1,
             active# plus(X1, X2) -> active# X2}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        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:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        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:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        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:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {    U42#(mark X1, X2, X3) -> U42#(X1, X2, X3),
          U42#(ok X1, ok X2, ok X3) -> U42#(X1, X2, X3)}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         { U31#(mark X1, X2) -> U31#(X1, X2),
          U31#(ok X1, ok X2) -> U31#(X1, X2)}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        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:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       SCC (1):
        Strict:
         {isNat# ok X -> isNat# X}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       SCC (2):
        Strict:
         {U21# mark X -> U21# X,
            U21# ok X -> U21# X}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open
       
       
       SCC (2):
        Strict:
         {U12# mark X -> U12# X,
            U12# ok X -> U12# X}
        Weak:
        {               U12 mark X -> mark U12 X,
                          U12 ok X -> ok U12 X,
                        isNat ok X -> ok isNat X,
                      active U12 X -> U12 active X,
                   active U12 tt() -> mark tt(),
                 active isNat s V1 -> mark U21 isNat V1,
         active isNat plus(V1, V2) -> mark U11(isNat V1, V2),
                  active isNat 0() -> mark tt(),
                active U11(X1, X2) -> U11(active X1, X2),
              active U11(tt(), V2) -> mark U12 isNat V2,
                      active U21 X -> U21 active X,
                   active U21 tt() -> mark tt(),
                active U31(X1, X2) -> U31(active X1, X2),
               active U31(tt(), N) -> mark N,
            active U42(X1, X2, X3) -> U42(active X1, X2, X3),
            active U42(tt(), M, N) -> mark s plus(N, M),
            active U41(X1, X2, X3) -> U41(active X1, X2, X3),
            active U41(tt(), M, N) -> mark U42(isNat N, M, N),
                        active s X -> s active X,
               active plus(N, s M) -> mark U41(isNat M, M, N),
               active plus(N, 0()) -> mark U31(isNat N, N),
               active plus(X1, X2) -> plus(X1, active X2),
               active plus(X1, X2) -> plus(active X1, X2),
                  U11(mark X1, X2) -> mark U11(X1, X2),
                 U11(ok X1, ok X2) -> ok U11(X1, X2),
                        U21 mark X -> mark U21 X,
                          U21 ok X -> ok U21 X,
                  U31(mark X1, X2) -> mark U31(X1, X2),
                 U31(ok X1, ok X2) -> ok U31(X1, X2),
              U42(mark X1, X2, X3) -> mark U42(X1, X2, X3),
          U42(ok X1, ok X2, ok X3) -> ok U42(X1, X2, X3),
              U41(mark X1, X2, X3) -> mark U41(X1, X2, X3),
          U41(ok X1, ok X2, ok X3) -> ok U41(X1, X2, X3),
                          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),
                      proper U12 X -> U12 proper X,
                    proper isNat X -> isNat proper X,
                proper U11(X1, X2) -> U11(proper X1, proper X2),
                       proper tt() -> ok tt(),
                      proper U21 X -> U21 proper X,
                proper U31(X1, X2) -> U31(proper X1, proper X2),
            proper U42(X1, X2, X3) -> U42(proper X1, proper X2, proper X3),
            proper U41(X1, X2, X3) -> U41(proper X1, proper X2, proper X3),
                        proper s X -> s proper X,
               proper plus(X1, X2) -> plus(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
        Open