Problem:
 eq(n,xs,xs) -> T()
 eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
 nats() -> c(0(),inc(nats()))
 inc(c(x,xs)) -> c(s(x),inc(xs))

Proof:
 Church Rosser Transformation Processor (to relative problem):
  strict:
   eq(n,xs,xs) -> T()
   eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
   nats() -> c(0(),inc(nats()))
   inc(c(x,xs)) -> c(s(x),inc(xs))
  weak:
   
  original problem:
   eq(n,xs,xs) -> T()
   eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
   nats() -> c(0(),inc(nats()))
   inc(c(x,xs)) -> c(s(x),inc(xs))
  critical peaks: 
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [nats] = 0,
     
     [T] = 0,
     
     [c](x0, x1) = x0 + x1,
     
     [0] = 0,
     
     [eq](x0, x1, x2) = x0 + x1 + x2 + 4,
     
     [inc](x0) = 4x0,
     
     [s](x0) = 4x0
    orientation:
     eq(n,xs,xs) = n + 2xs + 4 >= 0 = T()
     
     eq(s(n),c(x,xs),c(x,ys)) = 4n + 2x + xs + ys + 4 >= n + xs + ys + 4 = eq(n,xs,ys)
     
     nats() = 0 >= 0 = c(0(),inc(nats()))
     
     inc(c(x,xs)) = 4x + 4xs >= 4x + 4xs = c(s(x),inc(xs))
    problem:
     strict:
      eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
      nats() -> c(0(),inc(nats()))
      inc(c(x,xs)) -> c(s(x),inc(xs))
     weak:
      
     original problem:
      eq(n,xs,xs) -> T()
      eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
      nats() -> c(0(),inc(nats()))
      inc(c(x,xs)) -> c(s(x),inc(xs))
    Matrix Interpretation Processor: dim=2
     
     interpretation:
               [0]
      [nats] = [2],
      
                    [1 0]     [1 0]  
      [c](x0, x1) = [1 1]x0 + [0 0]x1,
      
            [0]
      [0] = [1],
      
                         [2 1]     [1 0]     [2 0]     [1]
      [eq](x0, x1, x2) = [1 3]x0 + [0 0]x1 + [0 0]x2 + [0],
      
                  [2 0]     [0]
      [inc](x0) = [1 1]x0 + [1],
      
                     [0]
      [s](x0) = x0 + [1]
     orientation:
                                 [2 1]    [3 0]    [1 0]     [2 0]     [2]    [2 1]    [1 0]     [2 0]     [1]              
      eq(s(n),c(x,xs),c(x,ys)) = [1 3]n + [0 0]x + [0 0]xs + [0 0]ys + [3] >= [1 3]n + [0 0]xs + [0 0]ys + [0] = eq(n,xs,ys)
      
               [0]    [0]                     
      nats() = [2] >= [1] = c(0(),inc(nats()))
      
                     [2 0]    [2 0]     [0]    [1 0]    [2 0]     [0]                  
      inc(c(x,xs)) = [2 1]x + [1 0]xs + [1] >= [1 1]x + [0 0]xs + [1] = c(s(x),inc(xs))
     problem:
      strict:
       nats() -> c(0(),inc(nats()))
       inc(c(x,xs)) -> c(s(x),inc(xs))
      weak:
       
      original problem:
       eq(n,xs,xs) -> T()
       eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
       nats() -> c(0(),inc(nats()))
       inc(c(x,xs)) -> c(s(x),inc(xs))
     KH confluence processor
      Split input TRS into two TRSs S and T:
      
      TRS S:
       nats() -> c(0(),inc(nats()))
       inc(c(x,xs)) -> c(s(x),inc(xs))
      
      TRS T:
       eq(n,xs,xs) -> T()
       eq(s(n),c(x,xs),c(x,ys)) -> eq(n,xs,ys)
      
      As established above, T/S is terminating.
      T is strongly non-overlapping on S and S is strongly non-overlapping on T
      
       We get the following critical pairs, which are also S-critical pairs:
      
      T() = eq(n,xs,xs), eq(x233,x236,x236) = T()
      
       all these critical pairs are joinable with S union T.
      
      Please install theorem prover 'Prover9' and 'Mace4' for handling more TRSs.
      
       All S-critical pairs are joinable.
      
      We have to check confluence of S.
      
      Church Rosser Transformation Processor (no redundant rules):
       strict:
        inc(c(x,xs)) -> c(s(x),inc(xs))
        nats() -> c(0(),inc(nats()))
       weak:
        
       critical peaks: 0
       Closedness Processor (*feeble*):
        
        Qed