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:
     [inc](x0) = x0,
     
     [0] = 0,
     
     [nats] = 0,
     
     [c](x0, x1) = x0 + x1,
     
     [s](x0) = x0,
     
     [T] = 0,
     
     [eq](x0, x1, x2) = 2x0 + 2x1 + 2x2 + 2
    orientation:
     eq(n,xs,xs) = 2n + 4xs + 2 >= 0 = T()
     
     eq(s(n),c(x,xs),c(x,ys)) = 2n + 4x + 2xs + 2ys + 2 >= 2n + 2xs + 2ys + 2 = eq(n,xs,ys)
     
     nats() = 0 >= 0 = c(0(),inc(nats()))
     
     inc(c(x,xs)) = x + xs >= x + xs = 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:
                  [1 1]  
      [inc](x0) = [0 2]x0,
      
            [0]
      [0] = [0],
      
               [0]
      [nats] = [0],
      
                    [1 0]       
      [c](x0, x1) = [1 0]x0 + x1,
      
                [2 0]     [0]
      [s](x0) = [1 1]x0 + [2],
      
                         [1 1]     [2 0]          [0]
      [eq](x0, x1, x2) = [0 0]x0 + [0 1]x1 + x2 + [1]
     orientation:
                                 [3 1]    [3 0]    [2 0]          [2]    [1 1]    [2 0]          [0]              
      eq(s(n),c(x,xs),c(x,ys)) = [0 0]n + [2 0]x + [0 1]xs + ys + [1] >= [0 0]n + [0 1]xs + ys + [1] = eq(n,xs,ys)
      
               [0]    [0]                     
      nats() = [0] >= [0] = c(0(),inc(nats()))
      
                     [2 0]    [1 1]      [2 0]    [1 1]                    
      inc(c(x,xs)) = [2 0]x + [0 2]xs >= [2 0]x + [0 2]xs = 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