YES
Time: 0.104572
TRS:
 {        mark tt() -> tt(),
           mark 0() -> 0(),
           mark s X -> s mark X,
   mark and(X1, X2) -> a__and(mark X1, X2),
  mark plus(X1, X2) -> a__plus(mark X1, mark X2),
     a__and(X1, X2) -> and(X1, X2),
    a__and(tt(), X) -> mark X,
    a__plus(N, 0()) -> mark N,
    a__plus(N, s M) -> s a__plus(mark N, mark M),
    a__plus(X1, X2) -> plus(X1, X2)}
 DP:
  DP:
   {         mark# s X -> mark# X,
     mark# and(X1, X2) -> mark# X1,
     mark# and(X1, X2) -> a__and#(mark X1, X2),
    mark# plus(X1, X2) -> mark# X1,
    mark# plus(X1, X2) -> mark# X2,
    mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
      a__and#(tt(), X) -> mark# X,
      a__plus#(N, 0()) -> mark# N,
      a__plus#(N, s M) -> mark# N,
      a__plus#(N, s M) -> mark# M,
      a__plus#(N, s M) -> a__plus#(mark N, mark M)}
  TRS:
  {        mark tt() -> tt(),
            mark 0() -> 0(),
            mark s X -> s mark X,
    mark and(X1, X2) -> a__and(mark X1, X2),
   mark plus(X1, X2) -> a__plus(mark X1, mark X2),
      a__and(X1, X2) -> and(X1, X2),
     a__and(tt(), X) -> mark X,
     a__plus(N, 0()) -> mark N,
     a__plus(N, s M) -> s a__plus(mark N, mark M),
     a__plus(X1, X2) -> plus(X1, X2)}
  EDG:
   {(mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2)
    (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2)
    (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1)
    (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
    (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2)
    (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1)
    (a__plus#(N, 0()) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__plus#(N, 0()) -> mark# N, mark# and(X1, X2) -> mark# X1)
    (a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X)
    (a__plus#(N, s M) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__plus#(N, s M) -> mark# M, mark# plus(X1, X2) -> mark# X2)
    (a__plus#(N, s M) -> mark# M, mark# plus(X1, X2) -> mark# X1)
    (a__plus#(N, s M) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__plus#(N, s M) -> mark# M, mark# and(X1, X2) -> mark# X1)
    (a__plus#(N, s M) -> mark# M, mark# s X -> mark# X)
    (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
    (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (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) -> mark# X2, mark# and(X1, X2) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2)
    (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (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# 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))
    (a__plus#(N, s M) -> mark# N, mark# s X -> mark# X)
    (a__plus#(N, s M) -> mark# N, mark# and(X1, X2) -> mark# X1)
    (a__plus#(N, s M) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
    (a__plus#(N, s M) -> mark# N, mark# plus(X1, X2) -> mark# X1)
    (a__plus#(N, s M) -> mark# N, mark# plus(X1, X2) -> mark# X2)
    (a__plus#(N, s M) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> mark# N)
    (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> mark# N)
    (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> mark# M)
    (a__plus#(N, s M) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__plus#(mark N, mark M))
    (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> mark# N)
    (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> mark# N)
    (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> mark# M)
    (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__plus#(mark N, mark M))}
   STATUS:
    arrows: 0.537190
    SCCS (1):
     Scc:
      {         mark# s X -> mark# X,
        mark# and(X1, X2) -> mark# X1,
       mark# plus(X1, X2) -> mark# X1,
       mark# plus(X1, X2) -> mark# X2,
       mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
         a__plus#(N, 0()) -> mark# N,
         a__plus#(N, s M) -> mark# N,
         a__plus#(N, s M) -> mark# M,
         a__plus#(N, s M) -> a__plus#(mark N, mark M)}
     
     
     SCC (9):
      Strict:
       {         mark# s X -> mark# X,
         mark# and(X1, X2) -> mark# X1,
        mark# plus(X1, X2) -> mark# X1,
        mark# plus(X1, X2) -> mark# X2,
        mark# plus(X1, X2) -> a__plus#(mark X1, mark X2),
          a__plus#(N, 0()) -> mark# N,
          a__plus#(N, s M) -> mark# N,
          a__plus#(N, s M) -> mark# M,
          a__plus#(N, s M) -> a__plus#(mark N, mark M)}
      Weak:
      {        mark tt() -> tt(),
                mark 0() -> 0(),
                mark s X -> s mark X,
        mark and(X1, X2) -> a__and(mark X1, X2),
       mark plus(X1, X2) -> a__plus(mark X1, mark X2),
          a__and(X1, X2) -> and(X1, X2),
         a__and(tt(), X) -> mark X,
         a__plus(N, 0()) -> mark N,
         a__plus(N, s M) -> s a__plus(mark N, mark M),
         a__plus(X1, X2) -> plus(X1, X2)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [a__and](x0, x1) = x0 + x1 + 1,
        
        [a__plus](x0, x1) = x0 + x1,
        
        [and](x0, x1) = x0 + x1 + 1,
        
        [plus](x0, x1) = x0 + x1,
        
        [mark](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [tt] = 0,
        
        [0] = 1,
        
        [a__plus#](x0, x1) = x0 + x1,
        
        [mark#](x0) = x0 + 1
       Strict:
        a__plus#(N, s M) -> a__plus#(mark N, mark M)
        1 + 1N + 1M >= 0 + 1N + 1M
        a__plus#(N, s M) -> mark# M
        1 + 1N + 1M >= 1 + 1M
        a__plus#(N, s M) -> mark# N
        1 + 1N + 1M >= 1 + 1N
        a__plus#(N, 0()) -> mark# N
        1 + 1N >= 1 + 1N
        mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)
        1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
        mark# plus(X1, X2) -> mark# X2
        1 + 1X1 + 1X2 >= 1 + 1X2
        mark# plus(X1, X2) -> mark# X1
        1 + 1X1 + 1X2 >= 1 + 1X1
        mark# and(X1, X2) -> mark# X1
        2 + 1X1 + 1X2 >= 1 + 1X1
        mark# s X -> mark# X
        2 + 1X >= 1 + 1X
       Weak:
        a__plus(X1, X2) -> plus(X1, X2)
        0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
        a__plus(N, s M) -> s a__plus(mark N, mark M)
        1 + 1N + 1M >= 1 + 1N + 1M
        a__plus(N, 0()) -> mark N
        1 + 1N >= 0 + 1N
        a__and(tt(), X) -> mark X
        1 + 1X >= 0 + 1X
        a__and(X1, X2) -> and(X1, X2)
        1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        mark plus(X1, X2) -> a__plus(mark X1, mark X2)
        0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
        mark and(X1, X2) -> a__and(mark X1, X2)
        1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        mark s X -> s mark X
        1 + 1X >= 1 + 1X
        mark 0() -> 0()
        1 >= 1
        mark tt() -> tt()
        0 >= 0
      SCCS (1):
       Scc:
        {mark# plus(X1, X2) -> mark# X1,
         mark# plus(X1, X2) -> mark# X2}
       
       
       
       
       SCC (2):
        Strict:
         {mark# plus(X1, X2) -> mark# X1,
          mark# plus(X1, X2) -> mark# X2}
        Weak:
        {        mark tt() -> tt(),
                  mark 0() -> 0(),
                  mark s X -> s mark X,
          mark and(X1, X2) -> a__and(mark X1, X2),
         mark plus(X1, X2) -> a__plus(mark X1, mark X2),
            a__and(X1, X2) -> and(X1, X2),
           a__and(tt(), X) -> mark X,
           a__plus(N, 0()) -> mark N,
           a__plus(N, s M) -> s a__plus(mark N, mark M),
           a__plus(X1, X2) -> plus(X1, X2)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [a__and](x0, x1) = x0 + 1,
          
          [a__plus](x0, x1) = 0,
          
          [and](x0, x1) = 1,
          
          [plus](x0, x1) = x0 + x1 + 1,
          
          [mark](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [tt] = 1,
          
          [0] = 1,
          
          [mark#](x0) = x0 + 1
         Strict:
          mark# plus(X1, X2) -> mark# X2
          2 + 1X1 + 1X2 >= 1 + 1X2
          mark# plus(X1, X2) -> mark# X1
          2 + 1X1 + 1X2 >= 1 + 1X1
         Weak:
          a__plus(X1, X2) -> plus(X1, X2)
          0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2
          a__plus(N, s M) -> s a__plus(mark N, mark M)
          0 + 0N + 0M >= 1 + 0N + 0M
          a__plus(N, 0()) -> mark N
          0 + 0N >= 1 + 1N
          a__and(tt(), X) -> mark X
          2 + 0X >= 1 + 1X
          a__and(X1, X2) -> and(X1, X2)
          1 + 1X1 + 0X2 >= 1 + 0X1 + 0X2
          mark plus(X1, X2) -> a__plus(mark X1, mark X2)
          2 + 1X1 + 1X2 >= 0 + 0X1 + 0X2
          mark and(X1, X2) -> a__and(mark X1, X2)
          2 + 0X1 + 0X2 >= 2 + 1X1 + 0X2
          mark s X -> s mark X
          2 + 1X >= 2 + 1X
          mark 0() -> 0()
          2 >= 1
          mark tt() -> tt()
          2 >= 1
        Qed