MAYBE
Time: 4.162782
TRS:
 {            mark tt() -> tt(),
               mark s X -> s mark X,
               mark 0() -> 0(),
           mark isNat X -> a__isNat X,
      mark plus(X1, X2) -> a__plus(mark X1, mark X2),
       mark U11(X1, X2) -> a__U11(mark X1, X2),
   mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3),
       mark and(X1, X2) -> a__and(mark X1, X2),
         a__U11(X1, X2) -> U11(X1, X2),
        a__U11(tt(), N) -> mark N,
        a__plus(N, s M) -> a__U21(a__and(a__isNat M, isNat N), M, N),
        a__plus(N, 0()) -> a__U11(a__isNat N, N),
        a__plus(X1, X2) -> plus(X1, X2),
     a__U21(X1, X2, X3) -> U21(X1, X2, X3),
     a__U21(tt(), M, N) -> s a__plus(mark N, mark M),
         a__and(X1, X2) -> and(X1, X2),
        a__and(tt(), X) -> mark X,
             a__isNat X -> isNat X,
          a__isNat s V1 -> a__isNat V1,
           a__isNat 0() -> tt(),
  a__isNat plus(V1, V2) -> a__and(a__isNat V1, isNat V2)}
 DP:
  DP:
   {             mark# s X -> mark# X,
             mark# isNat X -> a__isNat# X,
        mark# plus(X1, X2) -> mark# X1,
        mark# plus(X1, X2) -> mark# X2,
        mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
         mark# U11(X1, X2) -> mark# X1,
         mark# U11(X1, X2) -> a__U11#(mark X1, X2),
     mark# U21(X1, X2, X3) -> mark# X1,
     mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3),
         mark# and(X1, X2) -> mark# X1,
         mark# and(X1, X2) -> a__and#(mark X1, X2),
          a__U11#(tt(), N) -> mark# N,
          a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N),
          a__plus#(N, s M) -> a__and#(a__isNat M, isNat N),
          a__plus#(N, s M) -> a__isNat# M,
          a__plus#(N, 0()) -> a__U11#(a__isNat N, N),
          a__plus#(N, 0()) -> a__isNat# N,
       a__U21#(tt(), M, N) -> mark# N,
       a__U21#(tt(), M, N) -> mark# M,
       a__U21#(tt(), M, N) -> a__plus#(mark N, mark M),
          a__and#(tt(), X) -> mark# X,
            a__isNat# s V1 -> a__isNat# V1,
    a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2),
    a__isNat# plus(V1, V2) -> a__isNat# V1}
  TRS:
  {            mark tt() -> tt(),
                mark s X -> s mark X,
                mark 0() -> 0(),
            mark isNat X -> a__isNat X,
       mark plus(X1, X2) -> a__plus(mark X1, mark X2),
        mark U11(X1, X2) -> a__U11(mark X1, X2),
    mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3),
        mark and(X1, X2) -> a__and(mark X1, X2),
          a__U11(X1, X2) -> U11(X1, X2),
         a__U11(tt(), N) -> mark N,
         a__plus(N, s M) -> a__U21(a__and(a__isNat M, isNat N), M, N),
         a__plus(N, 0()) -> a__U11(a__isNat N, N),
         a__plus(X1, X2) -> plus(X1, X2),
      a__U21(X1, X2, X3) -> U21(X1, X2, X3),
      a__U21(tt(), M, N) -> s a__plus(mark N, mark M),
          a__and(X1, X2) -> and(X1, X2),
         a__and(tt(), X) -> mark X,
              a__isNat X -> isNat X,
           a__isNat s V1 -> a__isNat V1,
            a__isNat 0() -> tt(),
   a__isNat plus(V1, V2) -> a__and(a__isNat V1, isNat V2)}
  UR:
   {            mark tt() -> tt(),
                 mark s X -> s mark X,
                 mark 0() -> 0(),
             mark isNat X -> a__isNat X,
        mark plus(X1, X2) -> a__plus(mark X1, mark X2),
         mark U11(X1, X2) -> a__U11(mark X1, X2),
     mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3),
         mark and(X1, X2) -> a__and(mark X1, X2),
           a__U11(X1, X2) -> U11(X1, X2),
          a__U11(tt(), N) -> mark N,
          a__plus(N, s M) -> a__U21(a__and(a__isNat M, isNat N), M, N),
          a__plus(N, 0()) -> a__U11(a__isNat N, N),
          a__plus(X1, X2) -> plus(X1, X2),
       a__U21(X1, X2, X3) -> U21(X1, X2, X3),
       a__U21(tt(), M, N) -> s a__plus(mark N, mark M),
           a__and(X1, X2) -> and(X1, X2),
          a__and(tt(), X) -> mark X,
               a__isNat X -> isNat X,
            a__isNat s V1 -> a__isNat V1,
             a__isNat 0() -> tt(),
    a__isNat plus(V1, V2) -> a__and(a__isNat V1, isNat V2)}
   EDG:
    {
     (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNat# V1)
     (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2))
     (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNat# V1)
     (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNat# V1)
     (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2))
     (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1)
     (a__U11#(tt(), N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U11#(tt(), N) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__U11#(tt(), N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (a__U11#(tt(), N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1)
     (a__U11#(tt(), N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (a__U11#(tt(), N) -> mark# N, mark# U11(X1, X2) -> mark# X1)
     (a__U11#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__U11#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2)
     (a__U11#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1)
     (a__U11#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X)
     (a__U11#(tt(), N) -> mark# N, mark# s X -> mark# X)
     (a__U21#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U21#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (a__U21#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (a__U21#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__U21#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2)
     (a__U21#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X)
     (a__U21#(tt(), M, N) -> mark# N, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X)
     (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (a__plus#(N, s M) -> a__and#(a__isNat M, isNat N), a__and#(tt(), X) -> mark# X)
     (a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2), a__and#(tt(), X) -> mark# X)
     (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X)
     (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> a__plus#(mark N, mark M))
     (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> mark# M)
     (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> mark# N)
     (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), N) -> mark# N)
     (a__plus#(N, 0()) -> a__U11#(a__isNat N, N), a__U11#(tt(), N) -> mark# N)
     (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1)
     (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2))
     (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1)
     (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1)
     (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2))
     (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1)
     (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X)
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U21#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N))
     (a__U21#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__isNat M, isNat N))
     (a__U21#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M)
     (a__U21#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U11#(a__isNat N, N))
     (a__U21#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N)
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N))
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__and#(a__isNat M, isNat N))
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M)
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U11#(a__isNat N, N))
     (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__isNat# N)
     (a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N), a__U21#(tt(), M, N) -> mark# N)
     (a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N), a__U21#(tt(), M, N) -> mark# M)
     (a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N), a__U21#(tt(), M, N) -> a__plus#(mark N, mark M))
     (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1)
     (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2))
     (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1)
     (a__U21#(tt(), M, N) -> mark# M, mark# s X -> mark# X)
     (a__U21#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X)
     (a__U21#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2)
     (a__U21#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__U21#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (a__U21#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (a__U21#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> mark# X1)
     (a__U21#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X)
     (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2, X3) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# isNat X -> a__isNat# X)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
    }
    STATUS:
     arrows: 0.746528
     SCCS (1):
      Scc:
       {             mark# s X -> mark# X,
                 mark# isNat X -> a__isNat# X,
            mark# plus(X1, X2) -> mark# X1,
            mark# plus(X1, X2) -> mark# X2,
            mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
             mark# U11(X1, X2) -> mark# X1,
             mark# U11(X1, X2) -> a__U11#(mark X1, X2),
         mark# U21(X1, X2, X3) -> mark# X1,
         mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3),
             mark# and(X1, X2) -> mark# X1,
             mark# and(X1, X2) -> a__and#(mark X1, X2),
              a__U11#(tt(), N) -> mark# N,
              a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N),
              a__plus#(N, s M) -> a__and#(a__isNat M, isNat N),
              a__plus#(N, s M) -> a__isNat# M,
              a__plus#(N, 0()) -> a__U11#(a__isNat N, N),
              a__plus#(N, 0()) -> a__isNat# N,
           a__U21#(tt(), M, N) -> mark# N,
           a__U21#(tt(), M, N) -> mark# M,
           a__U21#(tt(), M, N) -> a__plus#(mark N, mark M),
              a__and#(tt(), X) -> mark# X,
                a__isNat# s V1 -> a__isNat# V1,
        a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2),
        a__isNat# plus(V1, V2) -> a__isNat# V1}
      
      SCC (24):
       Strict:
        {             mark# s X -> mark# X,
                  mark# isNat X -> a__isNat# X,
             mark# plus(X1, X2) -> mark# X1,
             mark# plus(X1, X2) -> mark# X2,
             mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
              mark# U11(X1, X2) -> mark# X1,
              mark# U11(X1, X2) -> a__U11#(mark X1, X2),
          mark# U21(X1, X2, X3) -> mark# X1,
          mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3),
              mark# and(X1, X2) -> mark# X1,
              mark# and(X1, X2) -> a__and#(mark X1, X2),
               a__U11#(tt(), N) -> mark# N,
               a__plus#(N, s M) -> a__U21#(a__and(a__isNat M, isNat N), M, N),
               a__plus#(N, s M) -> a__and#(a__isNat M, isNat N),
               a__plus#(N, s M) -> a__isNat# M,
               a__plus#(N, 0()) -> a__U11#(a__isNat N, N),
               a__plus#(N, 0()) -> a__isNat# N,
            a__U21#(tt(), M, N) -> mark# N,
            a__U21#(tt(), M, N) -> mark# M,
            a__U21#(tt(), M, N) -> a__plus#(mark N, mark M),
               a__and#(tt(), X) -> mark# X,
                 a__isNat# s V1 -> a__isNat# V1,
         a__isNat# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2),
         a__isNat# plus(V1, V2) -> a__isNat# V1}
       Weak:
       {            mark tt() -> tt(),
                     mark s X -> s mark X,
                     mark 0() -> 0(),
                 mark isNat X -> a__isNat X,
            mark plus(X1, X2) -> a__plus(mark X1, mark X2),
             mark U11(X1, X2) -> a__U11(mark X1, X2),
         mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3),
             mark and(X1, X2) -> a__and(mark X1, X2),
               a__U11(X1, X2) -> U11(X1, X2),
              a__U11(tt(), N) -> mark N,
              a__plus(N, s M) -> a__U21(a__and(a__isNat M, isNat N), M, N),
              a__plus(N, 0()) -> a__U11(a__isNat N, N),
              a__plus(X1, X2) -> plus(X1, X2),
           a__U21(X1, X2, X3) -> U21(X1, X2, X3),
           a__U21(tt(), M, N) -> s a__plus(mark N, mark M),
               a__and(X1, X2) -> and(X1, X2),
              a__and(tt(), X) -> mark X,
                   a__isNat X -> isNat X,
                a__isNat s V1 -> a__isNat V1,
                 a__isNat 0() -> tt(),
        a__isNat plus(V1, V2) -> a__and(a__isNat V1, isNat V2)}
       Open