*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        goal(xs,ys) -> revapp(xs,ys)
        revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
        revapp(Nil(),rest) -> rest
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {goal/2,revapp/2} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {goal,revapp}/{Cons,Nil}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 1, 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:
      The following argument positions are considered usable:
        none
      
      Following symbols are considered usable:
        {goal,revapp}
      TcT has computed the following interpretation:
          p(Cons) = [1] x1 + [1] x2 + [2] 
           p(Nil) = [0]                   
          p(goal) = [10] x1 + [8] x2 + [9]
        p(revapp) = [9] x1 + [8] x2 + [7] 
      
      Following rules are strictly oriented:
                  goal(xs,ys) = [10] xs + [8] ys + [9]          
                              > [9] xs + [8] ys + [7]           
                              = revapp(xs,ys)                   
      
      revapp(Cons(x,xs),rest) = [8] rest + [9] x + [9] xs + [25]
                              > [8] rest + [8] x + [9] xs + [23]
                              = revapp(xs,Cons(x,rest))         
      
           revapp(Nil(),rest) = [8] rest + [7]                  
                              > [1] rest + [0]                  
                              = rest                            
      
      
      Following rules are (at-least) weakly oriented:
      
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        goal(xs,ys) -> revapp(xs,ys)
        revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
        revapp(Nil(),rest) -> rest
      Signature:
        {goal/2,revapp/2} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {goal,revapp}/{Cons,Nil}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).