*** 1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
        car(.(x,y)) -> x
        cdr(.(x,y)) -> y
        null(.(x,y)) -> false()
        null(nil()) -> true()
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        rev(nil()) -> nil()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {++/2,car/1,cdr/1,null/1,rev/1} / {./2,false/0,nil/0,true/0}
      Obligation:
        Innermost
        basic terms: {++,car,cdr,null,rev}/{.,false,nil,true}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        ++#(.(x,y),z) -> c_1(++#(y,z))
        ++#(nil(),y) -> c_2()
        car#(.(x,y)) -> c_3()
        cdr#(.(x,y)) -> c_4()
        null#(.(x,y)) -> c_5()
        null#(nil()) -> c_6()
        rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        rev#(nil()) -> c_8()
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        ++#(.(x,y),z) -> c_1(++#(y,z))
        ++#(nil(),y) -> c_2()
        car#(.(x,y)) -> c_3()
        cdr#(.(x,y)) -> c_4()
        null#(.(x,y)) -> c_5()
        null#(nil()) -> c_6()
        rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        rev#(nil()) -> c_8()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
        car(.(x,y)) -> x
        cdr(.(x,y)) -> y
        null(.(x,y)) -> false()
        null(nil()) -> true()
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        rev(nil()) -> nil()
      Signature:
        {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
      Obligation:
        Innermost
        basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        rev(nil()) -> nil()
        ++#(.(x,y),z) -> c_1(++#(y,z))
        ++#(nil(),y) -> c_2()
        car#(.(x,y)) -> c_3()
        cdr#(.(x,y)) -> c_4()
        null#(.(x,y)) -> c_5()
        null#(nil()) -> c_6()
        rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        rev#(nil()) -> c_8()
*** 1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        ++#(.(x,y),z) -> c_1(++#(y,z))
        ++#(nil(),y) -> c_2()
        car#(.(x,y)) -> c_3()
        cdr#(.(x,y)) -> c_4()
        null#(.(x,y)) -> c_5()
        null#(nil()) -> c_6()
        rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        rev#(nil()) -> c_8()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        rev(nil()) -> nil()
      Signature:
        {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
      Obligation:
        Innermost
        basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {2,3,4,5,6,8}
      by application of
        Pre({2,3,4,5,6,8}) = {1,7}.
      Here rules are labelled as follows:
        1: ++#(.(x,y),z) -> c_1(++#(y,z))     
        2: ++#(nil(),y) -> c_2()              
        3: car#(.(x,y)) -> c_3()              
        4: cdr#(.(x,y)) -> c_4()              
        5: null#(.(x,y)) -> c_5()             
        6: null#(nil()) -> c_6()              
        7: rev#(.(x,y)) -> c_7(++#(rev(y)     
                                  ,.(x,nil()))
                              ,rev#(y))       
        8: rev#(nil()) -> c_8()               
*** 1.1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        ++#(.(x,y),z) -> c_1(++#(y,z))
        rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
      Strict TRS Rules:
        
      Weak DP Rules:
        ++#(nil(),y) -> c_2()
        car#(.(x,y)) -> c_3()
        cdr#(.(x,y)) -> c_4()
        null#(.(x,y)) -> c_5()
        null#(nil()) -> c_6()
        rev#(nil()) -> c_8()
      Weak TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        rev(nil()) -> nil()
      Signature:
        {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
      Obligation:
        Innermost
        basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:++#(.(x,y),z) -> c_1(++#(y,z))
           -->_1 ++#(nil(),y) -> c_2():3
           -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):1
        
        2:S:rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
           -->_2 rev#(nil()) -> c_8():8
           -->_1 ++#(nil(),y) -> c_2():3
           -->_2 rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)):2
           -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):1
        
        3:W:++#(nil(),y) -> c_2()
           
        
        4:W:car#(.(x,y)) -> c_3()
           
        
        5:W:cdr#(.(x,y)) -> c_4()
           
        
        6:W:null#(.(x,y)) -> c_5()
           
        
        7:W:null#(nil()) -> c_6()
           
        
        8:W:rev#(nil()) -> c_8()
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        7: null#(nil()) -> c_6() 
        6: null#(.(x,y)) -> c_5()
        5: cdr#(.(x,y)) -> c_4() 
        4: car#(.(x,y)) -> c_3() 
        8: rev#(nil()) -> c_8()  
        3: ++#(nil(),y) -> c_2() 
*** 1.1.1.1.1 Progress [(?,O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        ++#(.(x,y),z) -> c_1(++#(y,z))
        rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        ++(.(x,y),z) -> .(x,++(y,z))
        ++(nil(),y) -> y
        rev(.(x,y)) -> ++(rev(y),.(x,nil()))
        rev(nil()) -> nil()
      Signature:
        {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
      Obligation:
        Innermost
        basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
    Applied Processor:
      Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    Proof:
      We analyse the complexity of following sub-problems (R) and (S).
      Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
      
      Problem (R)
        Strict DP Rules:
          ++#(.(x,y),z) -> c_1(++#(y,z))
        Strict TRS Rules:
          
        Weak DP Rules:
          rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        Weak TRS Rules:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(nil(),y) -> y
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          rev(nil()) -> nil()
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
      
      Problem (S)
        Strict DP Rules:
          rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          ++#(.(x,y),z) -> c_1(++#(y,z))
        Weak TRS Rules:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(nil(),y) -> y
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          rev(nil()) -> nil()
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
  *** 1.1.1.1.1.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          ++#(.(x,y),z) -> c_1(++#(y,z))
        Strict TRS Rules:
          
        Weak DP Rules:
          rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        Weak TRS Rules:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(nil(),y) -> y
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          rev(nil()) -> nil()
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
      Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
      Proof:
        We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
          1: ++#(.(x,y),z) -> c_1(++#(y,z))
          
        The strictly oriented rules are moved into the weak component.
    *** 1.1.1.1.1.1.1 Progress [(?,O(n^2))]  ***
        Considered Problem:
          Strict DP Rules:
            ++#(.(x,y),z) -> c_1(++#(y,z))
          Strict TRS Rules:
            
          Weak DP Rules:
            rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
          Weak TRS Rules:
            ++(.(x,y),z) -> .(x,++(y,z))
            ++(nil(),y) -> y
            rev(.(x,y)) -> ++(rev(y),.(x,nil()))
            rev(nil()) -> nil()
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
        Proof:
          We apply a polynomial interpretation of kind constructor-based(mixed(2)):
          The following argument positions are considered usable:
            uargs(c_1) = {1},
            uargs(c_7) = {1,2}
          
          Following symbols are considered usable:
            {++,rev,++#,car#,cdr#,null#,rev#}
          TcT has computed the following interpretation:
               p(++) = x1 + 2*x2          
                p(.) = 1 + x1 + x2        
              p(car) = 1                  
              p(cdr) = 2                  
            p(false) = 1                  
              p(nil) = 0                  
             p(null) = 4 + 2*x1 + x1^2    
              p(rev) = 2*x1               
             p(true) = 1                  
              p(++#) = 2*x1 + 2*x1*x2 + x2
             p(car#) = 0                  
             p(cdr#) = 2 + x1 + 2*x1^2    
            p(null#) = 2*x1 + x1^2        
             p(rev#) = 1 + 2*x1 + 6*x1^2  
              p(c_1) = x1                 
              p(c_2) = 1                  
              p(c_3) = 0                  
              p(c_4) = 1                  
              p(c_5) = 1                  
              p(c_6) = 0                  
              p(c_7) = x1 + x2            
              p(c_8) = 1                  
          
          Following rules are strictly oriented:
          ++#(.(x,y),z) = 2 + 2*x + 2*x*z + 2*y + 2*y*z + 3*z
                        > 2*y + 2*y*z + z                    
                        = c_1(++#(y,z))                      
          
          
          Following rules are (at-least) weakly oriented:
          rev#(.(x,y)) =  9 + 14*x + 12*x*y + 6*x^2 + 14*y + 6*y^2
                       >= 2 + x + 4*x*y + 10*y + 6*y^2            
                       =  c_7(++#(rev(y),.(x,nil()))              
                             ,rev#(y))                            
          
          ++(.(x,y),z) =  1 + x + y + 2*z                         
                       >= 1 + x + y + 2*z                         
                       =  .(x,++(y,z))                            
          
           ++(nil(),y) =  2*y                                     
                       >= y                                       
                       =  y                                       
          
           rev(.(x,y)) =  2 + 2*x + 2*y                           
                       >= 2 + 2*x + 2*y                           
                       =  ++(rev(y),.(x,nil()))                   
          
            rev(nil()) =  0                                       
                       >= 0                                       
                       =  nil()                                   
          
    *** 1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            ++#(.(x,y),z) -> c_1(++#(y,z))
            rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
          Weak TRS Rules:
            ++(.(x,y),z) -> .(x,++(y,z))
            ++(nil(),y) -> y
            rev(.(x,y)) -> ++(rev(y),.(x,nil()))
            rev(nil()) -> nil()
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          Assumption
        Proof:
          ()
    
    *** 1.1.1.1.1.1.2 Progress [(O(1),O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            ++#(.(x,y),z) -> c_1(++#(y,z))
            rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
          Weak TRS Rules:
            ++(.(x,y),z) -> .(x,++(y,z))
            ++(nil(),y) -> y
            rev(.(x,y)) -> ++(rev(y),.(x,nil()))
            rev(nil()) -> nil()
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          RemoveWeakSuffixes
        Proof:
          Consider the dependency graph
            1:W:++#(.(x,y),z) -> c_1(++#(y,z))
               -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):1
            
            2:W:rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
               -->_2 rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)):2
               -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):1
            
          The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
            2: rev#(.(x,y)) -> c_7(++#(rev(y)     
                                      ,.(x,nil()))
                                  ,rev#(y))       
            1: ++#(.(x,y),z) -> c_1(++#(y,z))     
    *** 1.1.1.1.1.1.2.1 Progress [(O(1),O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS Rules:
            ++(.(x,y),z) -> .(x,++(y,z))
            ++(nil(),y) -> y
            rev(.(x,y)) -> ++(rev(y),.(x,nil()))
            rev(nil()) -> nil()
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          EmptyProcessor
        Proof:
          The problem is already closed. The intended complexity is O(1).
    
  *** 1.1.1.1.1.2 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          ++#(.(x,y),z) -> c_1(++#(y,z))
        Weak TRS Rules:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(nil(),y) -> y
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          rev(nil()) -> nil()
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
      Applied Processor:
        RemoveWeakSuffixes
      Proof:
        Consider the dependency graph
          1:S:rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
             -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):2
             -->_2 rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)):1
          
          2:W:++#(.(x,y),z) -> c_1(++#(y,z))
             -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):2
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          2: ++#(.(x,y),z) -> c_1(++#(y,z))
  *** 1.1.1.1.1.2.1 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(nil(),y) -> y
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          rev(nil()) -> nil()
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
      Applied Processor:
        SimplifyRHS
      Proof:
        Consider the dependency graph
          1:S:rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y))
             -->_2 rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          rev#(.(x,y)) -> c_7(rev#(y))
  *** 1.1.1.1.1.2.1.1 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          rev#(.(x,y)) -> c_7(rev#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          ++(.(x,y),z) -> .(x,++(y,z))
          ++(nil(),y) -> y
          rev(.(x,y)) -> ++(rev(y),.(x,nil()))
          rev(nil()) -> nil()
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
      Applied Processor:
        UsableRules
      Proof:
        We replace rewrite rules by usable rules:
          rev#(.(x,y)) -> c_7(rev#(y))
  *** 1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          rev#(.(x,y)) -> c_7(rev#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          
        Signature:
          {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0}
        Obligation:
          Innermost
          basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
      Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
      Proof:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
          1: rev#(.(x,y)) -> c_7(rev#(y))
          
        The strictly oriented rules are moved into the weak component.
    *** 1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            rev#(.(x,y)) -> c_7(rev#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS Rules:
            
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
        Proof:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_7) = {1}
          
          Following symbols are considered usable:
            {++#,car#,cdr#,null#,rev#}
          TcT has computed the following interpretation:
               p(++) = [0]                  
                p(.) = [1] x1 + [1] x2 + [4]
              p(car) = [0]                  
              p(cdr) = [0]                  
            p(false) = [0]                  
              p(nil) = [0]                  
             p(null) = [1] x1 + [0]         
              p(rev) = [1]                  
             p(true) = [1]                  
              p(++#) = [1] x1 + [1]         
             p(car#) = [1] x1 + [8]         
             p(cdr#) = [1] x1 + [4]         
            p(null#) = [8] x1 + [2]         
             p(rev#) = [4] x1 + [1]         
              p(c_1) = [4]                  
              p(c_2) = [0]                  
              p(c_3) = [1]                  
              p(c_4) = [1]                  
              p(c_5) = [0]                  
              p(c_6) = [1]                  
              p(c_7) = [1] x1 + [12]        
              p(c_8) = [2]                  
          
          Following rules are strictly oriented:
          rev#(.(x,y)) = [4] x + [4] y + [17]
                       > [4] y + [13]        
                       = c_7(rev#(y))        
          
          
          Following rules are (at-least) weakly oriented:
          
    *** 1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            rev#(.(x,y)) -> c_7(rev#(y))
          Weak TRS Rules:
            
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          Assumption
        Proof:
          ()
    
    *** 1.1.1.1.1.2.1.1.1.2 Progress [(O(1),O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            rev#(.(x,y)) -> c_7(rev#(y))
          Weak TRS Rules:
            
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          RemoveWeakSuffixes
        Proof:
          Consider the dependency graph
            1:W:rev#(.(x,y)) -> c_7(rev#(y))
               -->_1 rev#(.(x,y)) -> c_7(rev#(y)):1
            
          The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
            1: rev#(.(x,y)) -> c_7(rev#(y))
    *** 1.1.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS Rules:
            
          Signature:
            {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0}
          Obligation:
            Innermost
            basic terms: {++#,car#,cdr#,null#,rev#}/{.,false,nil,true}
        Applied Processor:
          EmptyProcessor
        Proof:
          The problem is already closed. The intended complexity is O(1).