WORST_CASE(?,O(n^2))
* Step 1: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add(0(),x) -> x
            add(s(x),y) -> s(add(x,y))
            p(0(),s(x),y,z) -> q(x,add(x,z))
            p(s(x),y,z,u) -> p(x,s(y),s(s(z)),u)
            q(s(x),y) -> p(s(x),0(),s(0()),y)
        - Signature:
            {add/2,p/4,q/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,p,q} and constructors {0,s}
    + Applied Processor:
        Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          F (TrsFun "0") :: [] -(0)-> "A"(0)
          F (TrsFun "0") :: [] -(0)-> "A"(3)
          F (TrsFun "add") :: ["A"(0) x "A"(0)] -(1)-> "A"(0)
          F (TrsFun "p") :: ["A"(3) x "A"(3) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "q") :: ["A"(3) x "A"(0)] -(1)-> "A"(0)
          F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "s") :: ["A"(3)] -(3)-> "A"(3)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
        
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          add(0(),x) -> x
          p(0(),s(x),y,z) -> q(x,add(x,z))
          q(s(x),y) -> p(s(x),0(),s(0()),y)
        2. Weak:
          add(s(x),y) -> s(add(x,y))
          p(s(x),y,z,u) -> p(x,s(y),s(s(z)),u)
* Step 2: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add(s(x),y) -> s(add(x,y))
            p(s(x),y,z,u) -> p(x,s(y),s(s(z)),u)
        - Weak TRS:
            add(0(),x) -> x
            p(0(),s(x),y,z) -> q(x,add(x,z))
            q(s(x),y) -> p(s(x),0(),s(0()),y)
        - Signature:
            {add/2,p/4,q/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,p,q} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(q) = {2},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {add,p,q}
        TcT has computed the following interpretation:
            p(0) = 0                         
          p(add) = 2*x1 + x2                 
            p(p) = 2*x1*x2 + x1^2 + x2^2 + x4
            p(q) = x1^2 + x2                 
            p(s) = 1 + x1                    
        
        Following rules are strictly oriented:
        add(s(x),y) = 2 + 2*x + y
                    > 1 + 2*x + y
                    = s(add(x,y))
        
        
        Following rules are (at-least) weakly oriented:
             add(0(),x) =  x                                    
                        >= x                                    
                        =  x                                    
        
        p(0(),s(x),y,z) =  1 + 2*x + x^2 + z                    
                        >= 2*x + x^2 + z                        
                        =  q(x,add(x,z))                        
        
          p(s(x),y,z,u) =  1 + u + 2*x + 2*x*y + x^2 + 2*y + y^2
                        >= 1 + u + 2*x + 2*x*y + x^2 + 2*y + y^2
                        =  p(x,s(y),s(s(z)),u)                  
        
              q(s(x),y) =  1 + 2*x + x^2 + y                    
                        >= 1 + 2*x + x^2 + y                    
                        =  p(s(x),0(),s(0()),y)                 
        
* Step 3: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            p(s(x),y,z,u) -> p(x,s(y),s(s(z)),u)
        - Weak TRS:
            add(0(),x) -> x
            add(s(x),y) -> s(add(x,y))
            p(0(),s(x),y,z) -> q(x,add(x,z))
            q(s(x),y) -> p(s(x),0(),s(0()),y)
        - Signature:
            {add/2,p/4,q/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,p,q} and constructors {0,s}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(q) = {2},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {add,p,q}
        TcT has computed the following interpretation:
            p(0) = 0                                      
          p(add) = x1 + x2                                
            p(p) = 2*x1 + 4*x1*x2 + 2*x1^2 + 2*x2^2 + 2*x4
            p(q) = 2*x1 + 2*x1^2 + 2*x2                   
            p(s) = 1 + x1                                 
        
        Following rules are strictly oriented:
        p(s(x),y,z,u) = 4 + 2*u + 6*x + 4*x*y + 2*x^2 + 4*y + 2*y^2
                      > 2 + 2*u + 6*x + 4*x*y + 2*x^2 + 4*y + 2*y^2
                      = p(x,s(y),s(s(z)),u)                        
        
        
        Following rules are (at-least) weakly oriented:
             add(0(),x) =  x                    
                        >= x                    
                        =  x                    
        
            add(s(x),y) =  1 + x + y            
                        >= 1 + x + y            
                        =  s(add(x,y))          
        
        p(0(),s(x),y,z) =  2 + 4*x + 2*x^2 + 2*z
                        >= 4*x + 2*x^2 + 2*z    
                        =  q(x,add(x,z))        
        
              q(s(x),y) =  4 + 6*x + 2*x^2 + 2*y
                        >= 4 + 6*x + 2*x^2 + 2*y
                        =  p(s(x),0(),s(0()),y) 
        
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            add(0(),x) -> x
            add(s(x),y) -> s(add(x,y))
            p(0(),s(x),y,z) -> q(x,add(x,z))
            p(s(x),y,z,u) -> p(x,s(y),s(s(z)),u)
            q(s(x),y) -> p(s(x),0(),s(0()),y)
        - Signature:
            {add/2,p/4,q/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add,p,q} and constructors {0,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))