WORST_CASE(?,O(n^2))
* Step 1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
            attach(x,nil()) -> nil()
            pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
            pairs(nil()) -> nil()
        - Signature:
            {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair}
    + 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(append) = {1,2},
          uargs(cons) = {2}
        
        Following symbols are considered usable:
          {append,attach,pairs}
        TcT has computed the following interpretation:
          p(append) = x1 + x2
          p(attach) = 0      
            p(cons) = x2     
             p(nil) = 0      
            p(pair) = 0      
           p(pairs) = 2      
        
        Following rules are strictly oriented:
        pairs(nil()) = 2    
                     > 0    
                     = nil()
        
        
        Following rules are (at-least) weakly oriented:
        append(cons(x,xs),ys) =  xs + ys                       
                              >= xs + ys                       
                              =  cons(x,append(xs,ys))         
        
             append(nil(),ys) =  ys                            
                              >= ys                            
                              =  ys                            
        
         attach(x,cons(y,ys)) =  0                             
                              >= 0                             
                              =  cons(pair(x,y),attach(x,ys))  
        
              attach(x,nil()) =  0                             
                              >= 0                             
                              =  nil()                         
        
            pairs(cons(x,xs)) =  2                             
                              >= 2                             
                              =  append(attach(x,xs),pairs(xs))
        
* Step 2: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
            attach(x,nil()) -> nil()
            pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
        - Weak TRS:
            pairs(nil()) -> nil()
        - Signature:
            {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair}
    + 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(append) = {1,2},
          uargs(cons) = {2}
        
        Following symbols are considered usable:
          {append,attach,pairs}
        TcT has computed the following interpretation:
          p(append) = 1 + x1 + x2
          p(attach) = 2 + x2     
            p(cons) = 2 + x2     
             p(nil) = 0          
            p(pair) = x1         
           p(pairs) = x1^2       
        
        Following rules are strictly oriented:
         append(nil(),ys) = 1 + ys                        
                          > ys                            
                          = ys                            
        
          attach(x,nil()) = 2                             
                          > 0                             
                          = nil()                         
        
        pairs(cons(x,xs)) = 4 + 4*xs + xs^2               
                          > 3 + xs + xs^2                 
                          = append(attach(x,xs),pairs(xs))
        
        
        Following rules are (at-least) weakly oriented:
        append(cons(x,xs),ys) =  3 + xs + ys                 
                              >= 3 + xs + ys                 
                              =  cons(x,append(xs,ys))       
        
         attach(x,cons(y,ys)) =  4 + ys                      
                              >= 4 + ys                      
                              =  cons(pair(x,y),attach(x,ys))
        
                 pairs(nil()) =  0                           
                              >= 0                           
                              =  nil()                       
        
* Step 3: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
        - Weak TRS:
            append(nil(),ys) -> ys
            attach(x,nil()) -> nil()
            pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
            pairs(nil()) -> nil()
        - Signature:
            {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair}
    + 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(append) = {1,2},
          uargs(cons) = {2}
        
        Following symbols are considered usable:
          {append,attach,pairs}
        TcT has computed the following interpretation:
          p(append) = 2*x1 + x2
          p(attach) = x2       
            p(cons) = 1 + x2   
             p(nil) = 0        
            p(pair) = 1 + x1   
           p(pairs) = x1^2     
        
        Following rules are strictly oriented:
        append(cons(x,xs),ys) = 2 + 2*xs + ys        
                              > 1 + 2*xs + ys        
                              = cons(x,append(xs,ys))
        
        
        Following rules are (at-least) weakly oriented:
            append(nil(),ys) =  ys                            
                             >= ys                            
                             =  ys                            
        
        attach(x,cons(y,ys)) =  1 + ys                        
                             >= 1 + ys                        
                             =  cons(pair(x,y),attach(x,ys))  
        
             attach(x,nil()) =  0                             
                             >= 0                             
                             =  nil()                         
        
           pairs(cons(x,xs)) =  1 + 2*xs + xs^2               
                             >= 2*xs + xs^2                   
                             =  append(attach(x,xs),pairs(xs))
        
                pairs(nil()) =  0                             
                             >= 0                             
                             =  nil()                         
        
* Step 4: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            attach(x,nil()) -> nil()
            pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
            pairs(nil()) -> nil()
        - Signature:
            {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair}
    + 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(append) = {1,2},
          uargs(cons) = {2}
        
        Following symbols are considered usable:
          {append,attach,pairs}
        TcT has computed the following interpretation:
          p(append) = 4*x1 + x2  
          p(attach) = 2*x2       
            p(cons) = 2 + x1 + x2
             p(nil) = 2          
            p(pair) = x2         
           p(pairs) = x1 + 3*x1^2
        
        Following rules are strictly oriented:
        attach(x,cons(y,ys)) = 4 + 2*y + 2*ys              
                             > 2 + y + 2*ys                
                             = cons(pair(x,y),attach(x,ys))
        
        
        Following rules are (at-least) weakly oriented:
        append(cons(x,xs),ys) =  8 + 4*x + 4*xs + ys                        
                              >= 2 + x + 4*xs + ys                          
                              =  cons(x,append(xs,ys))                      
        
             append(nil(),ys) =  8 + ys                                     
                              >= ys                                         
                              =  ys                                         
        
              attach(x,nil()) =  4                                          
                              >= 2                                          
                              =  nil()                                      
        
            pairs(cons(x,xs)) =  14 + 13*x + 6*x*xs + 3*x^2 + 13*xs + 3*xs^2
                              >= 9*xs + 3*xs^2                              
                              =  append(attach(x,xs),pairs(xs))             
        
                 pairs(nil()) =  14                                         
                              >= 2                                          
                              =  nil()                                      
        
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
            attach(x,nil()) -> nil()
            pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
            pairs(nil()) -> nil()
        - Signature:
            {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))