*** 1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
        c(c(c(y))) -> c(c(a(y,0())))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {c/1} / {0/0,a/2}
      Obligation:
        Innermost
        basic terms: {c}/{0,a}
    Applied Processor:
      InnermostRuleRemoval
    Proof:
      Arguments of following rules are not normal-forms.
        c(c(c(y))) -> c(c(a(y,0())))
      All above mentioned rules can be savely removed.
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {c/1} / {0/0,a/2}
      Obligation:
        Innermost
        basic terms: {c}/{0,a}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        c#(y) -> c_1()
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0()))
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        c#(y) -> c_1()
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0()))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      Signature:
        {c/1,c#/1} / {0/0,a/2,c_1/0,c_2/3}
      Obligation:
        Innermost
        basic terms: {c#}/{0,a}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {1}
      by application of
        Pre({1}) = {2}.
      Here rules are labelled as follows:
        1: c#(y) -> c_1()      
        2: c#(a(a(0(),x),y)) ->
             c_2(c#(c(c(0()))) 
                ,c#(c(0()))    
                ,c#(0()))      
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0()))
      Strict TRS Rules:
        
      Weak DP Rules:
        c#(y) -> c_1()
      Weak TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      Signature:
        {c/1,c#/1} / {0/0,a/2,c_1/0,c_2/3}
      Obligation:
        Innermost
        basic terms: {c#}/{0,a}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0()))
           -->_3 c#(y) -> c_1():2
           -->_2 c#(y) -> c_1():2
           -->_1 c#(y) -> c_1():2
           -->_2 c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0())):1
           -->_1 c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0())):1
        
        2:W:c#(y) -> c_1()
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        2: c#(y) -> c_1()
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0()))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      Signature:
        {c/1,c#/1} / {0/0,a/2,c_1/0,c_2/3}
      Obligation:
        Innermost
        basic terms: {c#}/{0,a}
    Applied Processor:
      SimplifyRHS
    Proof:
      Consider the dependency graph
        1:S:c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0()))
           -->_2 c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0())):1
           -->_1 c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())),c#(0())):1
        
      Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())))
*** 1.1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      Signature:
        {c/1,c#/1} / {0/0,a/2,c_1/0,c_2/2}
      Obligation:
        Innermost
        basic terms: {c#}/{0,a}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
      The following argument positions are considered usable:
        uargs(c_2) = {1,2}
      
      Following symbols are considered usable:
        {c,c#}
      TcT has computed the following interpretation:
          p(0) = [0]                  
          p(a) = [12]                 
          p(c) = [2] x1 + [1]         
         p(c#) = [2] x1 + [6]         
        p(c_1) = [0]                  
        p(c_2) = [1] x1 + [1] x2 + [4]
      
      Following rules are strictly oriented:
      c#(a(a(0(),x),y)) = [30]                         
                        > [24]                         
                        = c_2(c#(c(c(0()))),c#(c(0())))
      
      
      Following rules are (at-least) weakly oriented:
                  c(y) =  [2] y + [1]      
                       >= [1] y + [0]      
                       =  y                
      
      c(a(a(0(),x),y)) =  [25]             
                       >= [12]             
                       =  a(c(c(c(0()))),y)
      
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        c#(a(a(0(),x),y)) -> c_2(c#(c(c(0()))),c#(c(0())))
      Weak TRS Rules:
        c(y) -> y
        c(a(a(0(),x),y)) -> a(c(c(c(0()))),y)
      Signature:
        {c/1,c#/1} / {0/0,a/2,c_1/0,c_2/2}
      Obligation:
        Innermost
        basic terms: {c#}/{0,a}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).