MAYBE

Problem:
 a(a(y,0()),0()) -> y
 c(c(y)) -> y
 c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)

Proof:
 DP Processor:
  DPs:
   c#(a(c(c(y)),x)) -> a#(x,0())
   c#(a(c(c(y)),x)) -> c#(a(x,0()))
   c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
   c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
   c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
  TRS:
   a(a(y,0()),0()) -> y
   c(c(y)) -> y
   c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
  EDG Processor:
   DPs:
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
   TRS:
    a(a(y,0()),0()) -> y
    c(c(y)) -> y
    c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
   graph:
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> c#(a(x,0())) -> c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
   SCC Processor:
    #sccs: 1
    #rules: 3
    #arcs: 15/25
    DPs:
     c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
     c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
     c#(a(c(c(y)),x)) -> c#(a(x,0()))
    TRS:
     a(a(y,0()),0()) -> y
     c(c(y)) -> y
     c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [c#](x0) = x0,
      
      [c](x0) = x0 + 1,
      
      [a](x0, x1) = x0 + x1,
      
      [0] = 0
     orientation:
      c#(a(c(c(y)),x)) = x + y + 2 >= x + 2 = c#(c(c(a(x,0()))))
      
      c#(a(c(c(y)),x)) = x + y + 2 >= x + 1 = c#(c(a(x,0())))
      
      c#(a(c(c(y)),x)) = x + y + 2 >= x = c#(a(x,0()))
      
      a(a(y,0()),0()) = y >= y = y
      
      c(c(y)) = y + 2 >= y = y
      
      c(a(c(c(y)),x)) = x + y + 3 >= x + y + 3 = a(c(c(c(a(x,0())))),y)
     problem:
      DPs:
       c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
      TRS:
       a(a(y,0()),0()) -> y
       c(c(y)) -> y
       c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
     Open