WORST_CASE(?,O(n^1))
* Step 1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [1]                                             
                   p(<) = [5]                                             
               p(False) = [4]                                             
                   p(S) = [0]                                             
                p(True) = [1]                                             
            p(bool2Nat) = [1] x1 + [5]                                    
                  p(e1) = [0]                                             
                  p(e2) = [1] x4 + [0]                                    
                  p(e3) = [0]                                             
                  p(e4) = [1] x4 + [6]                                    
                  p(e5) = [0]                                             
                  p(e6) = [0]                                             
                  p(e7) = [0]                                             
                  p(e8) = [1] x3 + [2]                                    
              p(equal0) = [4]                                             
                 p(gcd) = [1] x1 + [1] x2 + [1]                           
               p(help1) = [7]                                             
                  p(l1) = [1] x1 + [1] x2 + [2] x3 + [2] x5 + [0]         
                 p(l10) = [1] x1 + [1] x2 + [1] x4 + [0]                  
                 p(l11) = [1] x2 + [1] x4 + [1] x6 + [1]                  
                 p(l12) = [1] x2 + [1] x4 + [6] x6 + [0]                  
                 p(l13) = [1] x2 + [1] x5 + [6] x6 + [0]                  
                 p(l14) = [1] x2 + [2] x6 + [0]                           
                 p(l15) = [1] x2 + [1] x5 + [2] x6 + [1]                  
                 p(l16) = [1] x3 + [0]                                    
                  p(l2) = [1] x1 + [1] x2 + [2] x3 + [2] x5 + [0]         
                  p(l3) = [1] x1 + [1] x2 + [1] x3 + [2] x5 + [3] x6 + [0]
                  p(l4) = [1] x1 + [1] x2 + [1] x3 + [2] x5 + [0]         
                  p(l5) = [1] x1 + [1] x2 + [2] x5 + [2] x6 + [0]         
                  p(l6) = [0]                                             
                  p(l7) = [1] x1 + [1] x2 + [2] x5 + [1] x6 + [1]         
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [4]                  
                  p(l9) = [1] x1 + [1]                                    
                  p(m1) = [2] x3 + [1] x4 + [1]                           
                  p(m2) = [2] x3 + [4]                                    
                  p(m3) = [1] x1 + [1] x2 + [1] x3 + [1]                  
                  p(m4) = [1] x4 + [2]                                    
                  p(m5) = [1] x1 + [1] x3 + [1] x4 + [1]                  
               p(monus) = [0]                                             
          
          Following rules are strictly oriented:
                     bool2Nat(False()) = [9]                                
                                       > [1]                                
                                       = 0()                                
          
                      bool2Nat(True()) = [6]                                
                                       > [0]                                
                                       = S(0())                             
          
                    e2(a,b,res,True()) = [1]                                
                                       > [0]                                
                                       = e3(a,b,res,True())                 
          
                   e4(a,b,res,False()) = [10]                               
                                       > [4]                                
                                       = False()                            
          
                    e4(a,b,res,True()) = [7]                                
                                       > [1]                                
                                       = True()                             
          
                         e8(a,b,res,t) = [1] res + [2]                      
                                       > [1] res + [0]                      
                                       = res                                
          
                           equal0(a,b) = [4]                                
                                       > [0]                                
                                       = e1(a,b,False(),False())            
          
                            help1(0()) = [7]                                
                                       > [4]                                
                                       = False()                            
          
                         help1(S(0())) = [7]                                
                                       > [4]                                
                                       = False()                            
          
                        help1(S(S(x))) = [7]                                
                                       > [1]                                
                                       = True()                             
          
            l13(x,y,res,tmp,False(),t) = [6] t + [1] y + [4]                
                                       > [1] y + [2]                        
                                       = l16(x,y,gcd(0(),y),tmp,False(),t)  
          
            l15(x,y,res,tmp,False(),t) = [2] t + [1] y + [5]                
                                       > [1] y + [2]                        
                                       = l16(x,y,gcd(y,0()),tmp,False(),t)  
          
             l15(x,y,res,tmp,True(),t) = [2] t + [1] y + [2]                
                                       > [1] y + [1]                        
                                       = l16(x,y,gcd(y,S(0())),tmp,True(),t)
          
          l5(x,y,res,tmp,mtmp,False()) = [2] mtmp + [1] x + [1] y + [8]     
                                       > [2] mtmp + [1] x + [1] y + [5]     
                                       = l7(x,y,res,tmp,mtmp,False())       
          
           l5(x,y,res,tmp,mtmp,True()) = [2] mtmp + [1] x + [1] y + [2]     
                                       > [1]                                
                                       = 0()                                
          
          l8(res,y,res',True(),mtmp,t) = [1] res + [1] y + [5]              
                                       > [1] res + [0]                      
                                       = res                                
          
            l8(x,y,res,False(),mtmp,t) = [1] x + [1] y + [8]                
                                       > [1] x + [1] y + [4]                
                                       = l10(x,y,res,False(),mtmp,t)        
          
             l9(res,y,res',tmp,mtmp,t) = [1] res + [1]                      
                                       > [1] res + [0]                      
                                       = res                                
          
              m2(S(S(x)),b,res,True()) = [2] res + [4]                      
                                       > [1]                                
                                       = True()                             
          
                  m4(S(x'),S(x),res,t) = [1] t + [2]                        
                                       > [1] t + [1]                        
                                       = m5(S(x'),S(x),monus(x',x),t)       
          
                         m5(a,b,res,t) = [1] a + [1] res + [1] t + [1]      
                                       > [1] res + [0]                      
                                       = res                                
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [5]                                             
                                        >= [4]                                             
                                        =  False()                                         
          
                            <(0(),S(y)) =  [5]                                             
                                        >= [1]                                             
                                        =  True()                                          
          
                           <(S(x),S(y)) =  [5]                                             
                                        >= [5]                                             
                                        =  <(x,y)                                          
          
                          e1(a,b,res,t) =  [0]                                             
                                        >= [5]                                             
                                        =  e2(a,b,res,<(a,b))                              
          
                    e2(a,b,res,False()) =  [4]                                             
                                        >= [4]                                             
                                        =  False()                                         
          
                          e3(a,b,res,t) =  [0]                                             
                                        >= [11]                                            
                                        =  e4(a,b,res,<(b,a))                              
          
                          e5(a,b,res,t) =  [0]                                             
                                        >= [1]                                             
                                        =  True()                                          
          
                          e6(a,b,res,t) =  [0]                                             
                                        >= [4]                                             
                                        =  False()                                         
          
                          e7(a,b,res,t) =  [0]                                             
                                        >= [4]                                             
                                        =  False()                                         
          
                               gcd(x,y) =  [1] x + [1] y + [1]                             
                                        >= [1] x + [1] y + [10]                            
                                        =  l1(x,y,0(),False(),False(),False())             
          
                 l1(x,y,res,tmp,mtmp,t) =  [2] mtmp + [2] res + [1] x + [1] y + [0]        
                                        >= [2] mtmp + [2] res + [1] x + [1] y + [0]        
                                        =  l2(x,y,res,tmp,mtmp,False())                    
          
                l10(x,y,res,tmp,mtmp,t) =  [1] tmp + [1] x + [1] y + [0]                   
                                        >= [1] tmp + [1] y + [6]                           
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                    
          
          l11(x,y,res,tmp,mtmp,False()) =  [1] tmp + [1] y + [5]                           
                                        >= [1] y + [8]                                     
                                        =  l14(x,y,res,tmp,mtmp,False())                   
          
           l11(x,y,res,tmp,mtmp,True()) =  [1] tmp + [1] y + [2]                           
                                        >= [1] tmp + [1] y + [6]                           
                                        =  l12(x,y,res,tmp,mtmp,True())                    
          
                l12(x,y,res,tmp,mtmp,t) =  [6] t + [1] tmp + [1] y + [0]                   
                                        >= [6] t + [1] y + [0]                             
                                        =  l13(x,y,res,tmp,monus(x,y),t)                   
          
              l13(x,y,res,tmp,True(),t) =  [6] t + [1] y + [1]                             
                                        >= [1] y + [1]                                     
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)             
          
                l14(x,y,res,tmp,mtmp,t) =  [2] t + [1] y + [0]                             
                                        >= [2] t + [1] y + [1]                             
                                        =  l15(x,y,res,tmp,monus(x,y),t)                   
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
           l2(x,y,res,tmp,mtmp,False()) =  [2] mtmp + [2] res + [1] x + [1] y + [0]        
                                        >= [2] mtmp + [1] res + [1] x + [1] y + [12]       
                                        =  l3(x,y,res,tmp,mtmp,False())                    
          
            l2(x,y,res,tmp,mtmp,True()) =  [2] mtmp + [2] res + [1] x + [1] y + [0]        
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                 l3(x,y,res,tmp,mtmp,t) =  [2] mtmp + [1] res + [3] t + [1] x + [1] y + [0]
                                        >= [2] mtmp + [1] x + [1] y + [1]                  
                                        =  l4(x,y,0(),tmp,mtmp,t)                          
          
                l4(x',x,res,tmp,mtmp,t) =  [2] mtmp + [1] res + [1] x + [1] x' + [0]       
                                        >= [2] mtmp + [1] x + [1] x' + [8]                 
                                        =  l5(x',x,res,tmp,mtmp,False())                   
          
                 l6(x,y,res,tmp,mtmp,t) =  [0]                                             
                                        >= [1]                                             
                                        =  0()                                             
          
                 l7(x,y,res,tmp,mtmp,t) =  [2] mtmp + [1] t + [1] x + [1] y + [1]          
                                        >= [1] x + [1] y + [8]                             
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                  
          
                          m1(a,x,res,t) =  [2] res + [1] t + [1]                           
                                        >= [2] res + [4]                                   
                                        =  m2(a,x,res,False())                             
          
                    m2(a,b,res,False()) =  [2] res + [4]                                   
                                        >= [6]                                             
                                        =  m4(a,b,res,False())                             
          
                   m2(0(),b,res,True()) =  [2] res + [4]                                   
                                        >= [4]                                             
                                        =  False()                                         
          
                m2(S(0()),b,res,True()) =  [2] res + [4]                                   
                                        >= [4]                                             
                                        =  False()                                         
          
                        m3(0(),b,res,t) =  [1] b + [1] res + [2]                           
                                        >= [4]                                             
                                        =  False()                                         
          
                     m3(S(0()),b,res,t) =  [1] b + [1] res + [1]                           
                                        >= [4]                                             
                                        =  False()                                         
          
                    m3(S(S(x)),b,res,t) =  [1] b + [1] res + [1]                           
                                        >= [1]                                             
                                        =  True()                                          
          
                             monus(a,b) =  [0]                                             
                                        >= [13]                                            
                                        =  m1(a,b,False(),False())                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m2(S(S(x)),b,res,True()) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(e2) = {4},
          uargs(e4) = {4},
          uargs(l11) = {6},
          uargs(l13) = {5},
          uargs(l15) = {5},
          uargs(l16) = {3},
          uargs(l8) = {4},
          uargs(m5) = {3}
        
        Following symbols are considered usable:
          {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8
          ,l9,m1,m2,m3,m4,m5,monus}
        TcT has computed the following interpretation:
                 p(0) = [0]                                                      
                 p(<) = [0]                                                      
             p(False) = [0]                                                      
                 p(S) = [0]                                                      
              p(True) = [0]                                                      
          p(bool2Nat) = [0]                                                      
                p(e1) = [1] x3 + [0]                                             
                p(e2) = [1] x3 + [2] x4 + [0]                                    
                p(e3) = [0]                                                      
                p(e4) = [1] x4 + [0]                                             
                p(e5) = [1] x1 + [1] x4 + [1]                                    
                p(e6) = [1] x1 + [2] x2 + [5]                                    
                p(e7) = [1] x3 + [5]                                             
                p(e8) = [1] x1 + [1] x2 + [4] x3 + [0]                           
            p(equal0) = [0]                                                      
               p(gcd) = [4] x1 + [4] x2 + [0]                                    
             p(help1) = [7]                                                      
                p(l1) = [1] x1 + [4] x2 + [4] x3 + [2] x4 + [7] x5 + [1] x6 + [0]
               p(l10) = [1] x1 + [4] x2 + [1] x3 + [1] x4 + [4] x5 + [1] x6 + [0]
               p(l11) = [4] x2 + [1] x3 + [1] x5 + [4] x6 + [0]                  
               p(l12) = [4] x2 + [0]                                             
               p(l13) = [4] x2 + [4] x5 + [0]                                    
               p(l14) = [4] x2 + [1] x6 + [0]                                    
               p(l15) = [4] x2 + [2] x5 + [0]                                    
               p(l16) = [1] x3 + [1] x5 + [0]                                    
                p(l2) = [1] x1 + [4] x2 + [4] x3 + [2] x4 + [7] x5 + [1] x6 + [0]
                p(l3) = [1] x1 + [4] x2 + [2] x3 + [7] x5 + [0]                  
                p(l4) = [1] x1 + [4] x2 + [4] x3 + [7] x5 + [0]                  
                p(l5) = [1] x1 + [4] x2 + [4] x3 + [6] x5 + [0]                  
                p(l6) = [1] x2 + [1] x3 + [1] x6 + [1]                           
                p(l7) = [1] x1 + [4] x2 + [4] x3 + [5] x5 + [1] x6 + [0]         
                p(l8) = [1] x1 + [4] x2 + [4] x3 + [4] x4 + [4] x5 + [1] x6 + [0]
                p(l9) = [4] x1 + [2] x2 + [1] x5 + [1] x6 + [2]                  
                p(m1) = [0]                                                      
                p(m2) = [0]                                                      
                p(m3) = [1] x3 + [2] x4 + [5]                                    
                p(m4) = [0]                                                      
                p(m5) = [1] x1 + [4] x2 + [4] x3 + [0]                           
             p(monus) = [0]                                                      
        
        Following rules are strictly oriented:
                 e5(a,b,res,t) = [1] a + [1] t + [1]          
                               > [0]                          
                               = True()                       
        
                 e6(a,b,res,t) = [1] a + [2] b + [5]          
                               > [0]                          
                               = False()                      
        
                 e7(a,b,res,t) = [1] res + [5]                
                               > [0]                          
                               = False()                      
        
        l6(x,y,res,tmp,mtmp,t) = [1] res + [1] t + [1] y + [1]
                               > [0]                          
                               = 0()                          
        
               m3(0(),b,res,t) = [1] res + [2] t + [5]        
                               > [0]                          
                               = False()                      
        
            m3(S(0()),b,res,t) = [1] res + [2] t + [5]        
                               > [0]                          
                               = False()                      
        
           m3(S(S(x)),b,res,t) = [1] res + [2] t + [5]        
                               > [0]                          
                               = True()                       
        
        
        Following rules are (at-least) weakly oriented:
                             <(x,0()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  False()                                                   
        
                          <(0(),S(y)) =  [0]                                                       
                                      >= [0]                                                       
                                      =  True()                                                    
        
                         <(S(x),S(y)) =  [0]                                                       
                                      >= [0]                                                       
                                      =  <(x,y)                                                    
        
                    bool2Nat(False()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  0()                                                       
        
                     bool2Nat(True()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  S(0())                                                    
        
                        e1(a,b,res,t) =  [1] res + [0]                                             
                                      >= [1] res + [0]                                             
                                      =  e2(a,b,res,<(a,b))                                        
        
                  e2(a,b,res,False()) =  [1] res + [0]                                             
                                      >= [0]                                                       
                                      =  False()                                                   
        
                   e2(a,b,res,True()) =  [1] res + [0]                                             
                                      >= [0]                                                       
                                      =  e3(a,b,res,True())                                        
        
                        e3(a,b,res,t) =  [0]                                                       
                                      >= [0]                                                       
                                      =  e4(a,b,res,<(b,a))                                        
        
                  e4(a,b,res,False()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  False()                                                   
        
                   e4(a,b,res,True()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  True()                                                    
        
                        e8(a,b,res,t) =  [1] a + [1] b + [4] res + [0]                             
                                      >= [1] res + [0]                                             
                                      =  res                                                       
        
                          equal0(a,b) =  [0]                                                       
                                      >= [0]                                                       
                                      =  e1(a,b,False(),False())                                   
        
                             gcd(x,y) =  [4] x + [4] y + [0]                                       
                                      >= [1] x + [4] y + [0]                                       
                                      =  l1(x,y,0(),False(),False(),False())                       
        
                           help1(0()) =  [7]                                                       
                                      >= [0]                                                       
                                      =  False()                                                   
        
                        help1(S(0())) =  [7]                                                       
                                      >= [0]                                                       
                                      =  False()                                                   
        
                       help1(S(S(x))) =  [7]                                                       
                                      >= [0]                                                       
                                      =  True()                                                    
        
               l1(x,y,res,tmp,mtmp,t) =  [7] mtmp + [4] res + [1] t + [2] tmp + [1] x + [4] y + [0]
                                      >= [7] mtmp + [4] res + [2] tmp + [1] x + [4] y + [0]        
                                      =  l2(x,y,res,tmp,mtmp,False())                              
        
              l10(x,y,res,tmp,mtmp,t) =  [4] mtmp + [1] res + [1] t + [1] tmp + [1] x + [4] y + [0]
                                      >= [1] mtmp + [1] res + [4] y + [0]                          
                                      =  l11(x,y,res,tmp,mtmp,<(x,y))                              
        
        l11(x,y,res,tmp,mtmp,False()) =  [1] mtmp + [1] res + [4] y + [0]                          
                                      >= [4] y + [0]                                               
                                      =  l14(x,y,res,tmp,mtmp,False())                             
        
         l11(x,y,res,tmp,mtmp,True()) =  [1] mtmp + [1] res + [4] y + [0]                          
                                      >= [4] y + [0]                                               
                                      =  l12(x,y,res,tmp,mtmp,True())                              
        
              l12(x,y,res,tmp,mtmp,t) =  [4] y + [0]                                               
                                      >= [4] y + [0]                                               
                                      =  l13(x,y,res,tmp,monus(x,y),t)                             
        
           l13(x,y,res,tmp,False(),t) =  [4] y + [0]                                               
                                      >= [4] y + [0]                                               
                                      =  l16(x,y,gcd(0(),y),tmp,False(),t)                         
        
            l13(x,y,res,tmp,True(),t) =  [4] y + [0]                                               
                                      >= [4] y + [0]                                               
                                      =  l16(x,y,gcd(S(0()),y),tmp,True(),t)                       
        
              l14(x,y,res,tmp,mtmp,t) =  [1] t + [4] y + [0]                                       
                                      >= [4] y + [0]                                               
                                      =  l15(x,y,res,tmp,monus(x,y),t)                             
        
           l15(x,y,res,tmp,False(),t) =  [4] y + [0]                                               
                                      >= [4] y + [0]                                               
                                      =  l16(x,y,gcd(y,0()),tmp,False(),t)                         
        
            l15(x,y,res,tmp,True(),t) =  [4] y + [0]                                               
                                      >= [4] y + [0]                                               
                                      =  l16(x,y,gcd(y,S(0())),tmp,True(),t)                       
        
              l16(x,y,res,tmp,mtmp,t) =  [1] mtmp + [1] res + [0]                                  
                                      >= [1] res + [0]                                             
                                      =  res                                                       
        
         l2(x,y,res,tmp,mtmp,False()) =  [7] mtmp + [4] res + [2] tmp + [1] x + [4] y + [0]        
                                      >= [7] mtmp + [2] res + [1] x + [4] y + [0]                  
                                      =  l3(x,y,res,tmp,mtmp,False())                              
        
          l2(x,y,res,tmp,mtmp,True()) =  [7] mtmp + [4] res + [2] tmp + [1] x + [4] y + [0]        
                                      >= [1] res + [0]                                             
                                      =  res                                                       
        
               l3(x,y,res,tmp,mtmp,t) =  [7] mtmp + [2] res + [1] x + [4] y + [0]                  
                                      >= [7] mtmp + [1] x + [4] y + [0]                            
                                      =  l4(x,y,0(),tmp,mtmp,t)                                    
        
              l4(x',x,res,tmp,mtmp,t) =  [7] mtmp + [4] res + [4] x + [1] x' + [0]                 
                                      >= [6] mtmp + [4] res + [4] x + [1] x' + [0]                 
                                      =  l5(x',x,res,tmp,mtmp,False())                             
        
         l5(x,y,res,tmp,mtmp,False()) =  [6] mtmp + [4] res + [1] x + [4] y + [0]                  
                                      >= [5] mtmp + [4] res + [1] x + [4] y + [0]                  
                                      =  l7(x,y,res,tmp,mtmp,False())                              
        
          l5(x,y,res,tmp,mtmp,True()) =  [6] mtmp + [4] res + [1] x + [4] y + [0]                  
                                      >= [0]                                                       
                                      =  0()                                                       
        
               l7(x,y,res,tmp,mtmp,t) =  [5] mtmp + [4] res + [1] t + [1] x + [4] y + [0]          
                                      >= [4] mtmp + [4] res + [1] t + [1] x + [4] y + [0]          
                                      =  l8(x,y,res,equal0(x,y),mtmp,t)                            
        
         l8(res,y,res',True(),mtmp,t) =  [4] mtmp + [1] res + [4] res' + [1] t + [4] y + [0]       
                                      >= [1] res + [0]                                             
                                      =  res                                                       
        
           l8(x,y,res,False(),mtmp,t) =  [4] mtmp + [4] res + [1] t + [1] x + [4] y + [0]          
                                      >= [4] mtmp + [1] res + [1] t + [1] x + [4] y + [0]          
                                      =  l10(x,y,res,False(),mtmp,t)                               
        
            l9(res,y,res',tmp,mtmp,t) =  [1] mtmp + [4] res + [1] t + [2] y + [2]                  
                                      >= [1] res + [0]                                             
                                      =  res                                                       
        
                        m1(a,x,res,t) =  [0]                                                       
                                      >= [0]                                                       
                                      =  m2(a,x,res,False())                                       
        
                  m2(a,b,res,False()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  m4(a,b,res,False())                                       
        
                 m2(0(),b,res,True()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  False()                                                   
        
              m2(S(0()),b,res,True()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  False()                                                   
        
             m2(S(S(x)),b,res,True()) =  [0]                                                       
                                      >= [0]                                                       
                                      =  True()                                                    
        
                 m4(S(x'),S(x),res,t) =  [0]                                                       
                                      >= [0]                                                       
                                      =  m5(S(x'),S(x),monus(x',x),t)                              
        
                        m5(a,b,res,t) =  [1] a + [4] b + [4] res + [0]                             
                                      >= [1] res + [0]                                             
                                      =  res                                                       
        
                           monus(a,b) =  [0]                                                       
                                      >= [0]                                                       
                                      =  m1(a,b,False(),False())                                   
        
* Step 3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                             
                   p(<) = [0]                                             
               p(False) = [0]                                             
                   p(S) = [1]                                             
                p(True) = [0]                                             
            p(bool2Nat) = [6]                                             
                  p(e1) = [1] x3 + [0]                                    
                  p(e2) = [1] x3 + [1] x4 + [5]                           
                  p(e3) = [0]                                             
                  p(e4) = [1] x4 + [3]                                    
                  p(e5) = [0]                                             
                  p(e6) = [0]                                             
                  p(e7) = [0]                                             
                  p(e8) = [1] x3 + [0]                                    
              p(equal0) = [0]                                             
                 p(gcd) = [4] x1 + [4] x2 + [1]                           
               p(help1) = [0]                                             
                  p(l1) = [4] x1 + [4] x2 + [1] x3 + [5] x4 + [1] x6 + [1]
                 p(l10) = [2] x1 + [4] x2 + [4]                           
                 p(l11) = [1] x1 + [4] x2 + [1] x6 + [0]                  
                 p(l12) = [4] x2 + [2] x6 + [0]                           
                 p(l13) = [4] x2 + [1] x5 + [1]                           
                 p(l14) = [1] x1 + [4] x2 + [2] x6 + [0]                  
                 p(l15) = [1] x1 + [4] x2 + [1] x5 + [2] x6 + [6]         
                 p(l16) = [1] x3 + [0]                                    
                  p(l2) = [4] x1 + [4] x2 + [1] x3 + [1] x4 + [0]         
                  p(l3) = [4] x1 + [4] x2 + [1] x3 + [1] x4 + [0]         
                  p(l4) = [4] x1 + [4] x2 + [5] x3 + [0]                  
                  p(l5) = [4] x1 + [4] x2 + [4] x3 + [0]                  
                  p(l6) = [2]                                             
                  p(l7) = [2] x1 + [4] x2 + [4] x3 + [0]                  
                  p(l8) = [2] x1 + [4] x2 + [4] x3 + [1] x4 + [5]         
                  p(l9) = [1] x1 + [0]                                    
                  p(m1) = [3] x3 + [0]                                    
                  p(m2) = [3] x3 + [1] x4 + [5]                           
                  p(m3) = [4] x1 + [1]                                    
                  p(m4) = [2] x3 + [1] x4 + [1]                           
                  p(m5) = [1] x3 + [0]                                    
               p(monus) = [0]                                             
          
          Following rules are strictly oriented:
              e2(a,b,res,False()) = [1] res + [5]                                  
                                  > [0]                                            
                                  = False()                                        
          
           l1(x,y,res,tmp,mtmp,t) = [1] res + [1] t + [5] tmp + [4] x + [4] y + [1]
                                  > [1] res + [1] tmp + [4] x + [4] y + [0]        
                                  = l2(x,y,res,tmp,mtmp,False())                   
          
          l10(x,y,res,tmp,mtmp,t) = [2] x + [4] y + [4]                            
                                  > [1] x + [4] y + [0]                            
                                  = l11(x,y,res,tmp,mtmp,<(x,y))                   
          
              m2(a,b,res,False()) = [3] res + [5]                                  
                                  > [2] res + [1]                                  
                                  = m4(a,b,res,False())                            
          
             m2(0(),b,res,True()) = [3] res + [5]                                  
                                  > [0]                                            
                                  = False()                                        
          
          m2(S(0()),b,res,True()) = [3] res + [5]                                  
                                  > [0]                                            
                                  = False()                                        
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                            <(0(),S(y)) =  [0]                                    
                                        >= [0]                                    
                                        =  True()                                 
          
                           <(S(x),S(y)) =  [0]                                    
                                        >= [0]                                    
                                        =  <(x,y)                                 
          
                      bool2Nat(False()) =  [6]                                    
                                        >= [0]                                    
                                        =  0()                                    
          
                       bool2Nat(True()) =  [6]                                    
                                        >= [1]                                    
                                        =  S(0())                                 
          
                          e1(a,b,res,t) =  [1] res + [0]                          
                                        >= [1] res + [5]                          
                                        =  e2(a,b,res,<(a,b))                     
          
                     e2(a,b,res,True()) =  [1] res + [5]                          
                                        >= [0]                                    
                                        =  e3(a,b,res,True())                     
          
                          e3(a,b,res,t) =  [0]                                    
                                        >= [3]                                    
                                        =  e4(a,b,res,<(b,a))                     
          
                    e4(a,b,res,False()) =  [3]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                     e4(a,b,res,True()) =  [3]                                    
                                        >= [0]                                    
                                        =  True()                                 
          
                          e5(a,b,res,t) =  [0]                                    
                                        >= [0]                                    
                                        =  True()                                 
          
                          e6(a,b,res,t) =  [0]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                          e7(a,b,res,t) =  [0]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                          e8(a,b,res,t) =  [1] res + [0]                          
                                        >= [1] res + [0]                          
                                        =  res                                    
          
                            equal0(a,b) =  [0]                                    
                                        >= [0]                                    
                                        =  e1(a,b,False(),False())                
          
                               gcd(x,y) =  [4] x + [4] y + [1]                    
                                        >= [4] x + [4] y + [1]                    
                                        =  l1(x,y,0(),False(),False(),False())    
          
                             help1(0()) =  [0]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                          help1(S(0())) =  [0]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                         help1(S(S(x))) =  [0]                                    
                                        >= [0]                                    
                                        =  True()                                 
          
          l11(x,y,res,tmp,mtmp,False()) =  [1] x + [4] y + [0]                    
                                        >= [1] x + [4] y + [0]                    
                                        =  l14(x,y,res,tmp,mtmp,False())          
          
           l11(x,y,res,tmp,mtmp,True()) =  [1] x + [4] y + [0]                    
                                        >= [4] y + [0]                            
                                        =  l12(x,y,res,tmp,mtmp,True())           
          
                l12(x,y,res,tmp,mtmp,t) =  [2] t + [4] y + [0]                    
                                        >= [4] y + [1]                            
                                        =  l13(x,y,res,tmp,monus(x,y),t)          
          
             l13(x,y,res,tmp,False(),t) =  [4] y + [1]                            
                                        >= [4] y + [1]                            
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)      
          
              l13(x,y,res,tmp,True(),t) =  [4] y + [1]                            
                                        >= [4] y + [5]                            
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)    
          
                l14(x,y,res,tmp,mtmp,t) =  [2] t + [1] x + [4] y + [0]            
                                        >= [2] t + [1] x + [4] y + [6]            
                                        =  l15(x,y,res,tmp,monus(x,y),t)          
          
             l15(x,y,res,tmp,False(),t) =  [2] t + [1] x + [4] y + [6]            
                                        >= [4] y + [1]                            
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)      
          
              l15(x,y,res,tmp,True(),t) =  [2] t + [1] x + [4] y + [6]            
                                        >= [4] y + [5]                            
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)    
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                          
                                        >= [1] res + [0]                          
                                        =  res                                    
          
           l2(x,y,res,tmp,mtmp,False()) =  [1] res + [1] tmp + [4] x + [4] y + [0]
                                        >= [1] res + [1] tmp + [4] x + [4] y + [0]
                                        =  l3(x,y,res,tmp,mtmp,False())           
          
            l2(x,y,res,tmp,mtmp,True()) =  [1] res + [1] tmp + [4] x + [4] y + [0]
                                        >= [1] res + [0]                          
                                        =  res                                    
          
                 l3(x,y,res,tmp,mtmp,t) =  [1] res + [1] tmp + [4] x + [4] y + [0]
                                        >= [4] x + [4] y + [0]                    
                                        =  l4(x,y,0(),tmp,mtmp,t)                 
          
                l4(x',x,res,tmp,mtmp,t) =  [5] res + [4] x + [4] x' + [0]         
                                        >= [4] res + [4] x + [4] x' + [0]         
                                        =  l5(x',x,res,tmp,mtmp,False())          
          
           l5(x,y,res,tmp,mtmp,False()) =  [4] res + [4] x + [4] y + [0]          
                                        >= [4] res + [2] x + [4] y + [0]          
                                        =  l7(x,y,res,tmp,mtmp,False())           
          
            l5(x,y,res,tmp,mtmp,True()) =  [4] res + [4] x + [4] y + [0]          
                                        >= [0]                                    
                                        =  0()                                    
          
                 l6(x,y,res,tmp,mtmp,t) =  [2]                                    
                                        >= [0]                                    
                                        =  0()                                    
          
                 l7(x,y,res,tmp,mtmp,t) =  [4] res + [2] x + [4] y + [0]          
                                        >= [4] res + [2] x + [4] y + [5]          
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)         
          
           l8(res,y,res',True(),mtmp,t) =  [2] res + [4] res' + [4] y + [5]       
                                        >= [1] res + [0]                          
                                        =  res                                    
          
             l8(x,y,res,False(),mtmp,t) =  [4] res + [2] x + [4] y + [5]          
                                        >= [2] x + [4] y + [4]                    
                                        =  l10(x,y,res,False(),mtmp,t)            
          
              l9(res,y,res',tmp,mtmp,t) =  [1] res + [0]                          
                                        >= [1] res + [0]                          
                                        =  res                                    
          
                          m1(a,x,res,t) =  [3] res + [0]                          
                                        >= [3] res + [5]                          
                                        =  m2(a,x,res,False())                    
          
               m2(S(S(x)),b,res,True()) =  [3] res + [5]                          
                                        >= [0]                                    
                                        =  True()                                 
          
                        m3(0(),b,res,t) =  [1]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                     m3(S(0()),b,res,t) =  [5]                                    
                                        >= [0]                                    
                                        =  False()                                
          
                    m3(S(S(x)),b,res,t) =  [5]                                    
                                        >= [0]                                    
                                        =  True()                                 
          
                   m4(S(x'),S(x),res,t) =  [2] res + [1] t + [1]                  
                                        >= [0]                                    
                                        =  m5(S(x'),S(x),monus(x',x),t)           
          
                          m5(a,b,res,t) =  [1] res + [0]                          
                                        >= [1] res + [0]                          
                                        =  res                                    
          
                             monus(a,b) =  [0]                                    
                                        >= [0]                                    
                                        =  m1(a,b,False(),False())                
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            m1(a,x,res,t) -> m2(a,x,res,False())
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [2]                                             
                   p(<) = [0]                                             
               p(False) = [0]                                             
                   p(S) = [0]                                             
                p(True) = [0]                                             
            p(bool2Nat) = [7]                                             
                  p(e1) = [1] x3 + [5]                                    
                  p(e2) = [1] x3 + [1] x4 + [4]                           
                  p(e3) = [0]                                             
                  p(e4) = [1] x4 + [6]                                    
                  p(e5) = [4]                                             
                  p(e6) = [0]                                             
                  p(e7) = [4]                                             
                  p(e8) = [1] x3 + [0]                                    
              p(equal0) = [5]                                             
                 p(gcd) = [1] x1 + [1] x2 + [0]                           
               p(help1) = [2]                                             
                  p(l1) = [1] x1 + [1] x2 + [1] x3 + [2] x5 + [1] x6 + [5]
                 p(l10) = [1] x1 + [1] x2 + [2]                           
                 p(l11) = [1] x1 + [1] x2 + [1] x6 + [0]                  
                 p(l12) = [1] x1 + [1] x2 + [1] x6 + [0]                  
                 p(l13) = [1] x1 + [1] x2 + [1] x5 + [3]                  
                 p(l14) = [1] x2 + [2] x6 + [0]                           
                 p(l15) = [1] x2 + [1] x5 + [3]                           
                 p(l16) = [1] x3 + [0]                                    
                  p(l2) = [1] x1 + [1] x2 + [1] x3 + [2] x5 + [0]         
                  p(l3) = [1] x1 + [1] x2 + [2] x5 + [2] x6 + [0]         
                  p(l4) = [1] x1 + [1] x2 + [2] x3 + [2] x5 + [2] x6 + [1]
                  p(l5) = [1] x1 + [1] x2 + [2] x3 + [2] x5 + [3]         
                  p(l6) = [2]                                             
                  p(l7) = [1] x1 + [1] x2 + [1] x6 + [3]                  
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [5]                  
                  p(l9) = [2] x1 + [1]                                    
                  p(m1) = [4] x3 + [5]                                    
                  p(m2) = [4] x3 + [2]                                    
                  p(m3) = [4] x1 + [2]                                    
                  p(m4) = [2] x4 + [2]                                    
                  p(m5) = [2] x1 + [1] x3 + [2] x4 + [2]                  
               p(monus) = [0]                                             
          
          Following rules are strictly oriented:
                      e1(a,b,res,t) = [1] res + [5]                      
                                    > [1] res + [4]                      
                                    = e2(a,b,res,<(a,b))                 
          
          l13(x,y,res,tmp,True(),t) = [1] x + [1] y + [3]                
                                    > [1] y + [0]                        
                                    = l16(x,y,gcd(S(0()),y),tmp,True(),t)
          
                      m1(a,x,res,t) = [4] res + [5]                      
                                    > [4] res + [2]                      
                                    = m2(a,x,res,False())                
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                            <(0(),S(y)) =  [0]                                              
                                        >= [0]                                              
                                        =  True()                                           
          
                           <(S(x),S(y)) =  [0]                                              
                                        >= [0]                                              
                                        =  <(x,y)                                           
          
                      bool2Nat(False()) =  [7]                                              
                                        >= [2]                                              
                                        =  0()                                              
          
                       bool2Nat(True()) =  [7]                                              
                                        >= [0]                                              
                                        =  S(0())                                           
          
                    e2(a,b,res,False()) =  [1] res + [4]                                    
                                        >= [0]                                              
                                        =  False()                                          
          
                     e2(a,b,res,True()) =  [1] res + [4]                                    
                                        >= [0]                                              
                                        =  e3(a,b,res,True())                               
          
                          e3(a,b,res,t) =  [0]                                              
                                        >= [6]                                              
                                        =  e4(a,b,res,<(b,a))                               
          
                    e4(a,b,res,False()) =  [6]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                     e4(a,b,res,True()) =  [6]                                              
                                        >= [0]                                              
                                        =  True()                                           
          
                          e5(a,b,res,t) =  [4]                                              
                                        >= [0]                                              
                                        =  True()                                           
          
                          e6(a,b,res,t) =  [0]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                          e7(a,b,res,t) =  [4]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                          e8(a,b,res,t) =  [1] res + [0]                                    
                                        >= [1] res + [0]                                    
                                        =  res                                              
          
                            equal0(a,b) =  [5]                                              
                                        >= [5]                                              
                                        =  e1(a,b,False(),False())                          
          
                               gcd(x,y) =  [1] x + [1] y + [0]                              
                                        >= [1] x + [1] y + [7]                              
                                        =  l1(x,y,0(),False(),False(),False())              
          
                             help1(0()) =  [2]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                          help1(S(0())) =  [2]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                         help1(S(S(x))) =  [2]                                              
                                        >= [0]                                              
                                        =  True()                                           
          
                 l1(x,y,res,tmp,mtmp,t) =  [2] mtmp + [1] res + [1] t + [1] x + [1] y + [5] 
                                        >= [2] mtmp + [1] res + [1] x + [1] y + [0]         
                                        =  l2(x,y,res,tmp,mtmp,False())                     
          
                l10(x,y,res,tmp,mtmp,t) =  [1] x + [1] y + [2]                              
                                        >= [1] x + [1] y + [0]                              
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                     
          
          l11(x,y,res,tmp,mtmp,False()) =  [1] x + [1] y + [0]                              
                                        >= [1] y + [0]                                      
                                        =  l14(x,y,res,tmp,mtmp,False())                    
          
           l11(x,y,res,tmp,mtmp,True()) =  [1] x + [1] y + [0]                              
                                        >= [1] x + [1] y + [0]                              
                                        =  l12(x,y,res,tmp,mtmp,True())                     
          
                l12(x,y,res,tmp,mtmp,t) =  [1] t + [1] x + [1] y + [0]                      
                                        >= [1] x + [1] y + [3]                              
                                        =  l13(x,y,res,tmp,monus(x,y),t)                    
          
             l13(x,y,res,tmp,False(),t) =  [1] x + [1] y + [3]                              
                                        >= [1] y + [2]                                      
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)                
          
                l14(x,y,res,tmp,mtmp,t) =  [2] t + [1] y + [0]                              
                                        >= [1] y + [3]                                      
                                        =  l15(x,y,res,tmp,monus(x,y),t)                    
          
             l15(x,y,res,tmp,False(),t) =  [1] y + [3]                                      
                                        >= [1] y + [2]                                      
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)                
          
              l15(x,y,res,tmp,True(),t) =  [1] y + [3]                                      
                                        >= [1] y + [0]                                      
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)              
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                                    
                                        >= [1] res + [0]                                    
                                        =  res                                              
          
           l2(x,y,res,tmp,mtmp,False()) =  [2] mtmp + [1] res + [1] x + [1] y + [0]         
                                        >= [2] mtmp + [1] x + [1] y + [0]                   
                                        =  l3(x,y,res,tmp,mtmp,False())                     
          
            l2(x,y,res,tmp,mtmp,True()) =  [2] mtmp + [1] res + [1] x + [1] y + [0]         
                                        >= [1] res + [0]                                    
                                        =  res                                              
          
                 l3(x,y,res,tmp,mtmp,t) =  [2] mtmp + [2] t + [1] x + [1] y + [0]           
                                        >= [2] mtmp + [2] t + [1] x + [1] y + [5]           
                                        =  l4(x,y,0(),tmp,mtmp,t)                           
          
                l4(x',x,res,tmp,mtmp,t) =  [2] mtmp + [2] res + [2] t + [1] x + [1] x' + [1]
                                        >= [2] mtmp + [2] res + [1] x + [1] x' + [3]        
                                        =  l5(x',x,res,tmp,mtmp,False())                    
          
           l5(x,y,res,tmp,mtmp,False()) =  [2] mtmp + [2] res + [1] x + [1] y + [3]         
                                        >= [1] x + [1] y + [3]                              
                                        =  l7(x,y,res,tmp,mtmp,False())                     
          
            l5(x,y,res,tmp,mtmp,True()) =  [2] mtmp + [2] res + [1] x + [1] y + [3]         
                                        >= [2]                                              
                                        =  0()                                              
          
                 l6(x,y,res,tmp,mtmp,t) =  [2]                                              
                                        >= [2]                                              
                                        =  0()                                              
          
                 l7(x,y,res,tmp,mtmp,t) =  [1] t + [1] x + [1] y + [3]                      
                                        >= [1] x + [1] y + [10]                             
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                   
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [1] y + [5]                            
                                        >= [1] res + [0]                                    
                                        =  res                                              
          
             l8(x,y,res,False(),mtmp,t) =  [1] x + [1] y + [5]                              
                                        >= [1] x + [1] y + [2]                              
                                        =  l10(x,y,res,False(),mtmp,t)                      
          
              l9(res,y,res',tmp,mtmp,t) =  [2] res + [1]                                    
                                        >= [1] res + [0]                                    
                                        =  res                                              
          
                    m2(a,b,res,False()) =  [4] res + [2]                                    
                                        >= [2]                                              
                                        =  m4(a,b,res,False())                              
          
                   m2(0(),b,res,True()) =  [4] res + [2]                                    
                                        >= [0]                                              
                                        =  False()                                          
          
                m2(S(0()),b,res,True()) =  [4] res + [2]                                    
                                        >= [0]                                              
                                        =  False()                                          
          
               m2(S(S(x)),b,res,True()) =  [4] res + [2]                                    
                                        >= [0]                                              
                                        =  True()                                           
          
                        m3(0(),b,res,t) =  [10]                                             
                                        >= [0]                                              
                                        =  False()                                          
          
                     m3(S(0()),b,res,t) =  [2]                                              
                                        >= [0]                                              
                                        =  False()                                          
          
                    m3(S(S(x)),b,res,t) =  [2]                                              
                                        >= [0]                                              
                                        =  True()                                           
          
                   m4(S(x'),S(x),res,t) =  [2] t + [2]                                      
                                        >= [2] t + [2]                                      
                                        =  m5(S(x'),S(x),monus(x',x),t)                     
          
                          m5(a,b,res,t) =  [2] a + [1] res + [2] t + [2]                    
                                        >= [1] res + [0]                                    
                                        =  res                                              
          
                             monus(a,b) =  [0]                                              
                                        >= [5]                                              
                                        =  m1(a,b,False(),False())                          
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [2]                                    
                   p(<) = [4]                                    
               p(False) = [0]                                    
                   p(S) = [0]                                    
                p(True) = [2]                                    
            p(bool2Nat) = [5] x1 + [4]                           
                  p(e1) = [5]                                    
                  p(e2) = [1] x4 + [0]                           
                  p(e3) = [0]                                    
                  p(e4) = [1] x4 + [0]                           
                  p(e5) = [4]                                    
                  p(e6) = [0]                                    
                  p(e7) = [0]                                    
                  p(e8) = [1] x3 + [1]                           
              p(equal0) = [6]                                    
                 p(gcd) = [1] x1 + [1] x2 + [2]                  
               p(help1) = [4] x1 + [5]                           
                  p(l1) = [1] x1 + [1] x2 + [4] x3 + [0]         
                 p(l10) = [1] x2 + [5]                           
                 p(l11) = [1] x2 + [1] x6 + [1]                  
                 p(l12) = [1] x2 + [0]                           
                 p(l13) = [1] x2 + [1] x5 + [5]                  
                 p(l14) = [1] x2 + [0]                           
                 p(l15) = [1] x2 + [1] x5 + [6]                  
                 p(l16) = [1] x3 + [0]                           
                  p(l2) = [1] x1 + [1] x2 + [4] x3 + [0]         
                  p(l3) = [1] x1 + [1] x2 + [0]                  
                  p(l4) = [1] x1 + [1] x2 + [0]                  
                  p(l5) = [1] x1 + [1] x2 + [5]                  
                  p(l6) = [2]                                    
                  p(l7) = [1] x1 + [1] x2 + [1] x6 + [0]         
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [1] x6 + [5]
                  p(l9) = [1] x1 + [0]                           
                  p(m1) = [3]                                    
                  p(m2) = [1] x4 + [2]                           
                  p(m3) = [4]                                    
                  p(m4) = [0]                                    
                  p(m5) = [1] x3 + [0]                           
               p(monus) = [0]                                    
          
          Following rules are strictly oriented:
          l11(x,y,res,tmp,mtmp,False()) = [1] y + [1]                  
                                        > [1] y + [0]                  
                                        = l14(x,y,res,tmp,mtmp,False())
          
           l11(x,y,res,tmp,mtmp,True()) = [1] y + [3]                  
                                        > [1] y + [0]                  
                                        = l12(x,y,res,tmp,mtmp,True()) 
          
          
          Following rules are (at-least) weakly oriented:
                              <(x,0()) =  [4]                                
                                       >= [0]                                
                                       =  False()                            
          
                           <(0(),S(y)) =  [4]                                
                                       >= [2]                                
                                       =  True()                             
          
                          <(S(x),S(y)) =  [4]                                
                                       >= [4]                                
                                       =  <(x,y)                             
          
                     bool2Nat(False()) =  [4]                                
                                       >= [2]                                
                                       =  0()                                
          
                      bool2Nat(True()) =  [14]                               
                                       >= [0]                                
                                       =  S(0())                             
          
                         e1(a,b,res,t) =  [5]                                
                                       >= [4]                                
                                       =  e2(a,b,res,<(a,b))                 
          
                   e2(a,b,res,False()) =  [0]                                
                                       >= [0]                                
                                       =  False()                            
          
                    e2(a,b,res,True()) =  [2]                                
                                       >= [0]                                
                                       =  e3(a,b,res,True())                 
          
                         e3(a,b,res,t) =  [0]                                
                                       >= [4]                                
                                       =  e4(a,b,res,<(b,a))                 
          
                   e4(a,b,res,False()) =  [0]                                
                                       >= [0]                                
                                       =  False()                            
          
                    e4(a,b,res,True()) =  [2]                                
                                       >= [2]                                
                                       =  True()                             
          
                         e5(a,b,res,t) =  [4]                                
                                       >= [2]                                
                                       =  True()                             
          
                         e6(a,b,res,t) =  [0]                                
                                       >= [0]                                
                                       =  False()                            
          
                         e7(a,b,res,t) =  [0]                                
                                       >= [0]                                
                                       =  False()                            
          
                         e8(a,b,res,t) =  [1] res + [1]                      
                                       >= [1] res + [0]                      
                                       =  res                                
          
                           equal0(a,b) =  [6]                                
                                       >= [5]                                
                                       =  e1(a,b,False(),False())            
          
                              gcd(x,y) =  [1] x + [1] y + [2]                
                                       >= [1] x + [1] y + [8]                
                                       =  l1(x,y,0(),False(),False(),False())
          
                            help1(0()) =  [13]                               
                                       >= [0]                                
                                       =  False()                            
          
                         help1(S(0())) =  [5]                                
                                       >= [0]                                
                                       =  False()                            
          
                        help1(S(S(x))) =  [5]                                
                                       >= [2]                                
                                       =  True()                             
          
                l1(x,y,res,tmp,mtmp,t) =  [4] res + [1] x + [1] y + [0]      
                                       >= [4] res + [1] x + [1] y + [0]      
                                       =  l2(x,y,res,tmp,mtmp,False())       
          
               l10(x,y,res,tmp,mtmp,t) =  [1] y + [5]                        
                                       >= [1] y + [5]                        
                                       =  l11(x,y,res,tmp,mtmp,<(x,y))       
          
               l12(x,y,res,tmp,mtmp,t) =  [1] y + [0]                        
                                       >= [1] y + [5]                        
                                       =  l13(x,y,res,tmp,monus(x,y),t)      
          
            l13(x,y,res,tmp,False(),t) =  [1] y + [5]                        
                                       >= [1] y + [4]                        
                                       =  l16(x,y,gcd(0(),y),tmp,False(),t)  
          
             l13(x,y,res,tmp,True(),t) =  [1] y + [7]                        
                                       >= [1] y + [2]                        
                                       =  l16(x,y,gcd(S(0()),y),tmp,True(),t)
          
               l14(x,y,res,tmp,mtmp,t) =  [1] y + [0]                        
                                       >= [1] y + [6]                        
                                       =  l15(x,y,res,tmp,monus(x,y),t)      
          
            l15(x,y,res,tmp,False(),t) =  [1] y + [6]                        
                                       >= [1] y + [4]                        
                                       =  l16(x,y,gcd(y,0()),tmp,False(),t)  
          
             l15(x,y,res,tmp,True(),t) =  [1] y + [8]                        
                                       >= [1] y + [2]                        
                                       =  l16(x,y,gcd(y,S(0())),tmp,True(),t)
          
               l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                      
                                       >= [1] res + [0]                      
                                       =  res                                
          
          l2(x,y,res,tmp,mtmp,False()) =  [4] res + [1] x + [1] y + [0]      
                                       >= [1] x + [1] y + [0]                
                                       =  l3(x,y,res,tmp,mtmp,False())       
          
           l2(x,y,res,tmp,mtmp,True()) =  [4] res + [1] x + [1] y + [0]      
                                       >= [1] res + [0]                      
                                       =  res                                
          
                l3(x,y,res,tmp,mtmp,t) =  [1] x + [1] y + [0]                
                                       >= [1] x + [1] y + [0]                
                                       =  l4(x,y,0(),tmp,mtmp,t)             
          
               l4(x',x,res,tmp,mtmp,t) =  [1] x + [1] x' + [0]               
                                       >= [1] x + [1] x' + [5]               
                                       =  l5(x',x,res,tmp,mtmp,False())      
          
          l5(x,y,res,tmp,mtmp,False()) =  [1] x + [1] y + [5]                
                                       >= [1] x + [1] y + [0]                
                                       =  l7(x,y,res,tmp,mtmp,False())       
          
           l5(x,y,res,tmp,mtmp,True()) =  [1] x + [1] y + [5]                
                                       >= [2]                                
                                       =  0()                                
          
                l6(x,y,res,tmp,mtmp,t) =  [2]                                
                                       >= [2]                                
                                       =  0()                                
          
                l7(x,y,res,tmp,mtmp,t) =  [1] t + [1] x + [1] y + [0]        
                                       >= [1] t + [1] x + [1] y + [11]       
                                       =  l8(x,y,res,equal0(x,y),mtmp,t)     
          
          l8(res,y,res',True(),mtmp,t) =  [1] res + [1] t + [1] y + [7]      
                                       >= [1] res + [0]                      
                                       =  res                                
          
            l8(x,y,res,False(),mtmp,t) =  [1] t + [1] x + [1] y + [5]        
                                       >= [1] y + [5]                        
                                       =  l10(x,y,res,False(),mtmp,t)        
          
             l9(res,y,res',tmp,mtmp,t) =  [1] res + [0]                      
                                       >= [1] res + [0]                      
                                       =  res                                
          
                         m1(a,x,res,t) =  [3]                                
                                       >= [2]                                
                                       =  m2(a,x,res,False())                
          
                   m2(a,b,res,False()) =  [2]                                
                                       >= [0]                                
                                       =  m4(a,b,res,False())                
          
                  m2(0(),b,res,True()) =  [4]                                
                                       >= [0]                                
                                       =  False()                            
          
               m2(S(0()),b,res,True()) =  [4]                                
                                       >= [0]                                
                                       =  False()                            
          
              m2(S(S(x)),b,res,True()) =  [4]                                
                                       >= [2]                                
                                       =  True()                             
          
                       m3(0(),b,res,t) =  [4]                                
                                       >= [0]                                
                                       =  False()                            
          
                    m3(S(0()),b,res,t) =  [4]                                
                                       >= [0]                                
                                       =  False()                            
          
                   m3(S(S(x)),b,res,t) =  [4]                                
                                       >= [2]                                
                                       =  True()                             
          
                  m4(S(x'),S(x),res,t) =  [0]                                
                                       >= [0]                                
                                       =  m5(S(x'),S(x),monus(x',x),t)       
          
                         m5(a,b,res,t) =  [1] res + [0]                      
                                       >= [1] res + [0]                      
                                       =  res                                
          
                            monus(a,b) =  [0]                                
                                       >= [3]                                
                                       =  m1(a,b,False(),False())            
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                             
                   p(<) = [1]                                             
               p(False) = [1]                                             
                   p(S) = [0]                                             
                p(True) = [0]                                             
            p(bool2Nat) = [4] x1 + [5]                                    
                  p(e1) = [2] x3 + [2]                                    
                  p(e2) = [1] x4 + [0]                                    
                  p(e3) = [0]                                             
                  p(e4) = [1] x4 + [0]                                    
                  p(e5) = [1]                                             
                  p(e6) = [1]                                             
                  p(e7) = [1]                                             
                  p(e8) = [1] x3 + [0]                                    
              p(equal0) = [4]                                             
                 p(gcd) = [1] x1 + [4] x2 + [0]                           
               p(help1) = [7]                                             
                  p(l1) = [1] x1 + [4] x2 + [4] x3 + [4] x5 + [0]         
                 p(l10) = [1] x1 + [4] x2 + [1] x4 + [4] x6 + [7]         
                 p(l11) = [4] x2 + [1] x6 + [6]                           
                 p(l12) = [4] x2 + [1] x6 + [6]                           
                 p(l13) = [4] x2 + [1] x5 + [0]                           
                 p(l14) = [2] x2 + [0]                                    
                 p(l15) = [1] x2 + [1] x5 + [1]                           
                 p(l16) = [1] x3 + [0]                                    
                  p(l2) = [1] x1 + [4] x2 + [4] x3 + [4] x5 + [0]         
                  p(l3) = [1] x1 + [4] x2 + [4] x3 + [4] x5 + [7] x6 + [0]
                  p(l4) = [1] x1 + [4] x2 + [1] x3 + [4] x6 + [0]         
                  p(l5) = [1] x1 + [4] x2 + [1] x3 + [5] x6 + [3]         
                  p(l6) = [0]                                             
                  p(l7) = [1] x1 + [4] x2 + [1] x3 + [4] x6 + [0]         
                  p(l8) = [1] x1 + [4] x2 + [1] x3 + [1] x4 + [4] x6 + [7]
                  p(l9) = [1] x1 + [2] x3 + [1] x6 + [0]                  
                  p(m1) = [5] x3 + [2] x4 + [4]                           
                  p(m2) = [3] x4 + [1]                                    
                  p(m3) = [2] x1 + [1] x3 + [5]                           
                  p(m4) = [3]                                             
                  p(m5) = [1] x1 + [1] x2 + [1] x3 + [2]                  
               p(monus) = [1]                                             
          
          Following rules are strictly oriented:
          l12(x,y,res,tmp,mtmp,t) = [1] t + [4] y + [6]          
                                  > [4] y + [1]                  
                                  = l13(x,y,res,tmp,monus(x,y),t)
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                            <(0(),S(y)) =  [1]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                           <(S(x),S(y)) =  [1]                                             
                                        >= [1]                                             
                                        =  <(x,y)                                          
          
                      bool2Nat(False()) =  [9]                                             
                                        >= [0]                                             
                                        =  0()                                             
          
                       bool2Nat(True()) =  [5]                                             
                                        >= [0]                                             
                                        =  S(0())                                          
          
                          e1(a,b,res,t) =  [2] res + [2]                                   
                                        >= [1]                                             
                                        =  e2(a,b,res,<(a,b))                              
          
                    e2(a,b,res,False()) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                     e2(a,b,res,True()) =  [0]                                             
                                        >= [0]                                             
                                        =  e3(a,b,res,True())                              
          
                          e3(a,b,res,t) =  [0]                                             
                                        >= [1]                                             
                                        =  e4(a,b,res,<(b,a))                              
          
                    e4(a,b,res,False()) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                     e4(a,b,res,True()) =  [0]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                          e5(a,b,res,t) =  [1]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                          e6(a,b,res,t) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                          e7(a,b,res,t) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                          e8(a,b,res,t) =  [1] res + [0]                                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                            equal0(a,b) =  [4]                                             
                                        >= [4]                                             
                                        =  e1(a,b,False(),False())                         
          
                               gcd(x,y) =  [1] x + [4] y + [0]                             
                                        >= [1] x + [4] y + [4]                             
                                        =  l1(x,y,0(),False(),False(),False())             
          
                             help1(0()) =  [7]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                          help1(S(0())) =  [7]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                         help1(S(S(x))) =  [7]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                 l1(x,y,res,tmp,mtmp,t) =  [4] mtmp + [4] res + [1] x + [4] y + [0]        
                                        >= [4] mtmp + [4] res + [1] x + [4] y + [0]        
                                        =  l2(x,y,res,tmp,mtmp,False())                    
          
                l10(x,y,res,tmp,mtmp,t) =  [4] t + [1] tmp + [1] x + [4] y + [7]           
                                        >= [4] y + [7]                                     
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                    
          
          l11(x,y,res,tmp,mtmp,False()) =  [4] y + [7]                                     
                                        >= [2] y + [0]                                     
                                        =  l14(x,y,res,tmp,mtmp,False())                   
          
           l11(x,y,res,tmp,mtmp,True()) =  [4] y + [6]                                     
                                        >= [4] y + [6]                                     
                                        =  l12(x,y,res,tmp,mtmp,True())                    
          
             l13(x,y,res,tmp,False(),t) =  [4] y + [1]                                     
                                        >= [4] y + [0]                                     
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)               
          
              l13(x,y,res,tmp,True(),t) =  [4] y + [0]                                     
                                        >= [4] y + [0]                                     
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)             
          
                l14(x,y,res,tmp,mtmp,t) =  [2] y + [0]                                     
                                        >= [1] y + [2]                                     
                                        =  l15(x,y,res,tmp,monus(x,y),t)                   
          
             l15(x,y,res,tmp,False(),t) =  [1] y + [2]                                     
                                        >= [1] y + [0]                                     
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)               
          
              l15(x,y,res,tmp,True(),t) =  [1] y + [1]                                     
                                        >= [1] y + [0]                                     
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)             
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
           l2(x,y,res,tmp,mtmp,False()) =  [4] mtmp + [4] res + [1] x + [4] y + [0]        
                                        >= [4] mtmp + [4] res + [1] x + [4] y + [7]        
                                        =  l3(x,y,res,tmp,mtmp,False())                    
          
            l2(x,y,res,tmp,mtmp,True()) =  [4] mtmp + [4] res + [1] x + [4] y + [0]        
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                 l3(x,y,res,tmp,mtmp,t) =  [4] mtmp + [4] res + [7] t + [1] x + [4] y + [0]
                                        >= [4] t + [1] x + [4] y + [0]                     
                                        =  l4(x,y,0(),tmp,mtmp,t)                          
          
                l4(x',x,res,tmp,mtmp,t) =  [1] res + [4] t + [4] x + [1] x' + [0]          
                                        >= [1] res + [4] x + [1] x' + [8]                  
                                        =  l5(x',x,res,tmp,mtmp,False())                   
          
           l5(x,y,res,tmp,mtmp,False()) =  [1] res + [1] x + [4] y + [8]                   
                                        >= [1] res + [1] x + [4] y + [4]                   
                                        =  l7(x,y,res,tmp,mtmp,False())                    
          
            l5(x,y,res,tmp,mtmp,True()) =  [1] res + [1] x + [4] y + [3]                   
                                        >= [0]                                             
                                        =  0()                                             
          
                 l6(x,y,res,tmp,mtmp,t) =  [0]                                             
                                        >= [0]                                             
                                        =  0()                                             
          
                 l7(x,y,res,tmp,mtmp,t) =  [1] res + [4] t + [1] x + [4] y + [0]           
                                        >= [1] res + [4] t + [1] x + [4] y + [11]          
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                  
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [1] res' + [4] t + [4] y + [7]        
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
             l8(x,y,res,False(),mtmp,t) =  [1] res + [4] t + [1] x + [4] y + [8]           
                                        >= [4] t + [1] x + [4] y + [8]                     
                                        =  l10(x,y,res,False(),mtmp,t)                     
          
              l9(res,y,res',tmp,mtmp,t) =  [1] res + [2] res' + [1] t + [0]                
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                          m1(a,x,res,t) =  [5] res + [2] t + [4]                           
                                        >= [4]                                             
                                        =  m2(a,x,res,False())                             
          
                    m2(a,b,res,False()) =  [4]                                             
                                        >= [3]                                             
                                        =  m4(a,b,res,False())                             
          
                   m2(0(),b,res,True()) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
                m2(S(0()),b,res,True()) =  [1]                                             
                                        >= [1]                                             
                                        =  False()                                         
          
               m2(S(S(x)),b,res,True()) =  [1]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                        m3(0(),b,res,t) =  [1] res + [5]                                   
                                        >= [1]                                             
                                        =  False()                                         
          
                     m3(S(0()),b,res,t) =  [1] res + [5]                                   
                                        >= [1]                                             
                                        =  False()                                         
          
                    m3(S(S(x)),b,res,t) =  [1] res + [5]                                   
                                        >= [0]                                             
                                        =  True()                                          
          
                   m4(S(x'),S(x),res,t) =  [3]                                             
                                        >= [3]                                             
                                        =  m5(S(x'),S(x),monus(x',x),t)                    
          
                          m5(a,b,res,t) =  [1] a + [1] b + [1] res + [2]                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                             monus(a,b) =  [1]                                             
                                        >= [11]                                            
                                        =  m1(a,b,False(),False())                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                             
                   p(<) = [1]                                             
               p(False) = [0]                                             
                   p(S) = [0]                                             
                p(True) = [0]                                             
            p(bool2Nat) = [0]                                             
                  p(e1) = [3] x1 + [5] x3 + [5]                           
                  p(e2) = [2] x1 + [1] x4 + [3]                           
                  p(e3) = [2] x1 + [3]                                    
                  p(e4) = [1] x4 + [0]                                    
                  p(e5) = [1]                                             
                  p(e6) = [0]                                             
                  p(e7) = [0]                                             
                  p(e8) = [1] x3 + [4]                                    
              p(equal0) = [3] x1 + [6]                                    
                 p(gcd) = [4] x1 + [4] x2 + [0]                           
               p(help1) = [2] x1 + [0]                                    
                  p(l1) = [4] x1 + [4] x2 + [2] x3 + [2] x4 + [3] x5 + [7]
                 p(l10) = [1] x1 + [4] x2 + [2] x4 + [1]                  
                 p(l11) = [1] x1 + [4] x2 + [2] x4 + [1] x6 + [0]         
                 p(l12) = [1] x1 + [4] x2 + [1] x4 + [4] x6 + [0]         
                 p(l13) = [4] x2 + [1] x4 + [1] x5 + [4] x6 + [0]         
                 p(l14) = [4] x2 + [2] x4 + [4] x6 + [0]                  
                 p(l15) = [4] x2 + [2] x4 + [1] x5 + [1]                  
                 p(l16) = [1] x3 + [1] x4 + [0]                           
                  p(l2) = [4] x1 + [4] x2 + [1] x3 + [2] x4 + [3] x5 + [2]
                  p(l3) = [4] x1 + [4] x2 + [2] x4 + [2] x5 + [2]         
                  p(l4) = [4] x1 + [4] x2 + [2] x4 + [1] x5 + [7]         
                  p(l5) = [4] x1 + [4] x2 + [1] x5 + [5]                  
                  p(l6) = [4] x6 + [1]                                    
                  p(l7) = [4] x1 + [4] x2 + [1] x5 + [1] x6 + [1]         
                  p(l8) = [1] x1 + [4] x2 + [1] x4 + [1]                  
                  p(l9) = [1] x1 + [1] x2 + [2] x3 + [1] x4 + [1] x6 + [1]
                  p(m1) = [1] x3 + [6]                                    
                  p(m2) = [1] x3 + [4] x4 + [4]                           
                  p(m3) = [2] x1 + [1] x2 + [4] x3 + [1] x4 + [5]         
                  p(m4) = [1] x3 + [2] x4 + [4]                           
                  p(m5) = [4] x2 + [1] x3 + [4]                           
               p(monus) = [0]                                             
          
          Following rules are strictly oriented:
                        e3(a,b,res,t) = [2] a + [3]                                       
                                      > [1]                                               
                                      = e4(a,b,res,<(b,a))                                
          
          l2(x,y,res,tmp,mtmp,True()) = [3] mtmp + [1] res + [2] tmp + [4] x + [4] y + [2]
                                      > [1] res + [0]                                     
                                      = res                                               
          
              l4(x',x,res,tmp,mtmp,t) = [1] mtmp + [2] tmp + [4] x + [4] x' + [7]         
                                      > [1] mtmp + [4] x + [4] x' + [5]                   
                                      = l5(x',x,res,tmp,mtmp,False())                     
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [1]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                            <(0(),S(y)) =  [1]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                           <(S(x),S(y)) =  [1]                                               
                                        >= [1]                                               
                                        =  <(x,y)                                            
          
                      bool2Nat(False()) =  [0]                                               
                                        >= [0]                                               
                                        =  0()                                               
          
                       bool2Nat(True()) =  [0]                                               
                                        >= [0]                                               
                                        =  S(0())                                            
          
                          e1(a,b,res,t) =  [3] a + [5] res + [5]                             
                                        >= [2] a + [4]                                       
                                        =  e2(a,b,res,<(a,b))                                
          
                    e2(a,b,res,False()) =  [2] a + [3]                                       
                                        >= [0]                                               
                                        =  False()                                           
          
                     e2(a,b,res,True()) =  [2] a + [3]                                       
                                        >= [2] a + [3]                                       
                                        =  e3(a,b,res,True())                                
          
                    e4(a,b,res,False()) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                     e4(a,b,res,True()) =  [0]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                          e5(a,b,res,t) =  [1]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                          e6(a,b,res,t) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                          e7(a,b,res,t) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                          e8(a,b,res,t) =  [1] res + [4]                                     
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                            equal0(a,b) =  [3] a + [6]                                       
                                        >= [3] a + [5]                                       
                                        =  e1(a,b,False(),False())                           
          
                               gcd(x,y) =  [4] x + [4] y + [0]                               
                                        >= [4] x + [4] y + [7]                               
                                        =  l1(x,y,0(),False(),False(),False())               
          
                             help1(0()) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                          help1(S(0())) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                         help1(S(S(x))) =  [0]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                 l1(x,y,res,tmp,mtmp,t) =  [3] mtmp + [2] res + [2] tmp + [4] x + [4] y + [7]
                                        >= [3] mtmp + [1] res + [2] tmp + [4] x + [4] y + [2]
                                        =  l2(x,y,res,tmp,mtmp,False())                      
          
                l10(x,y,res,tmp,mtmp,t) =  [2] tmp + [1] x + [4] y + [1]                     
                                        >= [2] tmp + [1] x + [4] y + [1]                     
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                      
          
          l11(x,y,res,tmp,mtmp,False()) =  [2] tmp + [1] x + [4] y + [0]                     
                                        >= [2] tmp + [4] y + [0]                             
                                        =  l14(x,y,res,tmp,mtmp,False())                     
          
           l11(x,y,res,tmp,mtmp,True()) =  [2] tmp + [1] x + [4] y + [0]                     
                                        >= [1] tmp + [1] x + [4] y + [0]                     
                                        =  l12(x,y,res,tmp,mtmp,True())                      
          
                l12(x,y,res,tmp,mtmp,t) =  [4] t + [1] tmp + [1] x + [4] y + [0]             
                                        >= [4] t + [1] tmp + [4] y + [0]                     
                                        =  l13(x,y,res,tmp,monus(x,y),t)                     
          
             l13(x,y,res,tmp,False(),t) =  [4] t + [1] tmp + [4] y + [0]                     
                                        >= [1] tmp + [4] y + [0]                             
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)                 
          
              l13(x,y,res,tmp,True(),t) =  [4] t + [1] tmp + [4] y + [0]                     
                                        >= [1] tmp + [4] y + [0]                             
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)               
          
                l14(x,y,res,tmp,mtmp,t) =  [4] t + [2] tmp + [4] y + [0]                     
                                        >= [2] tmp + [4] y + [1]                             
                                        =  l15(x,y,res,tmp,monus(x,y),t)                     
          
             l15(x,y,res,tmp,False(),t) =  [2] tmp + [4] y + [1]                             
                                        >= [1] tmp + [4] y + [0]                             
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)                 
          
              l15(x,y,res,tmp,True(),t) =  [2] tmp + [4] y + [1]                             
                                        >= [1] tmp + [4] y + [0]                             
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)               
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [1] tmp + [0]                           
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
           l2(x,y,res,tmp,mtmp,False()) =  [3] mtmp + [1] res + [2] tmp + [4] x + [4] y + [2]
                                        >= [2] mtmp + [2] tmp + [4] x + [4] y + [2]          
                                        =  l3(x,y,res,tmp,mtmp,False())                      
          
                 l3(x,y,res,tmp,mtmp,t) =  [2] mtmp + [2] tmp + [4] x + [4] y + [2]          
                                        >= [1] mtmp + [2] tmp + [4] x + [4] y + [7]          
                                        =  l4(x,y,0(),tmp,mtmp,t)                            
          
           l5(x,y,res,tmp,mtmp,False()) =  [1] mtmp + [4] x + [4] y + [5]                    
                                        >= [1] mtmp + [4] x + [4] y + [1]                    
                                        =  l7(x,y,res,tmp,mtmp,False())                      
          
            l5(x,y,res,tmp,mtmp,True()) =  [1] mtmp + [4] x + [4] y + [5]                    
                                        >= [0]                                               
                                        =  0()                                               
          
                 l6(x,y,res,tmp,mtmp,t) =  [4] t + [1]                                       
                                        >= [0]                                               
                                        =  0()                                               
          
                 l7(x,y,res,tmp,mtmp,t) =  [1] mtmp + [1] t + [4] x + [4] y + [1]            
                                        >= [4] x + [4] y + [7]                               
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                    
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [4] y + [1]                             
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
             l8(x,y,res,False(),mtmp,t) =  [1] x + [4] y + [1]                               
                                        >= [1] x + [4] y + [1]                               
                                        =  l10(x,y,res,False(),mtmp,t)                       
          
              l9(res,y,res',tmp,mtmp,t) =  [1] res + [2] res' + [1] t + [1] tmp + [1] y + [1]
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                          m1(a,x,res,t) =  [1] res + [6]                                     
                                        >= [1] res + [4]                                     
                                        =  m2(a,x,res,False())                               
          
                    m2(a,b,res,False()) =  [1] res + [4]                                     
                                        >= [1] res + [4]                                     
                                        =  m4(a,b,res,False())                               
          
                   m2(0(),b,res,True()) =  [1] res + [4]                                     
                                        >= [0]                                               
                                        =  False()                                           
          
                m2(S(0()),b,res,True()) =  [1] res + [4]                                     
                                        >= [0]                                               
                                        =  False()                                           
          
               m2(S(S(x)),b,res,True()) =  [1] res + [4]                                     
                                        >= [0]                                               
                                        =  True()                                            
          
                        m3(0(),b,res,t) =  [1] b + [4] res + [1] t + [5]                     
                                        >= [0]                                               
                                        =  False()                                           
          
                     m3(S(0()),b,res,t) =  [1] b + [4] res + [1] t + [5]                     
                                        >= [0]                                               
                                        =  False()                                           
          
                    m3(S(S(x)),b,res,t) =  [1] b + [4] res + [1] t + [5]                     
                                        >= [0]                                               
                                        =  True()                                            
          
                   m4(S(x'),S(x),res,t) =  [1] res + [2] t + [4]                             
                                        >= [4]                                               
                                        =  m5(S(x'),S(x),monus(x',x),t)                      
          
                          m5(a,b,res,t) =  [4] b + [1] res + [4]                             
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                             monus(a,b) =  [0]                                               
                                        >= [6]                                               
                                        =  m1(a,b,False(),False())                           
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l2(x,y,res,tmp,mtmp,True()) -> res
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                           
                   p(<) = [0]                           
               p(False) = [0]                           
                   p(S) = [0]                           
                p(True) = [0]                           
            p(bool2Nat) = [1]                           
                  p(e1) = [4]                           
                  p(e2) = [1] x4 + [4]                  
                  p(e3) = [3]                           
                  p(e4) = [1] x4 + [2]                  
                  p(e5) = [0]                           
                  p(e6) = [0]                           
                  p(e7) = [1]                           
                  p(e8) = [1] x3 + [1]                  
              p(equal0) = [4]                           
                 p(gcd) = [1] x1 + [1] x2 + [1]         
               p(help1) = [7]                           
                  p(l1) = [1] x1 + [1] x2 + [4] x3 + [2]
                 p(l10) = [1] x2 + [1]                  
                 p(l11) = [1] x2 + [1] x6 + [1]         
                 p(l12) = [1] x2 + [1]                  
                 p(l13) = [1] x2 + [1] x5 + [1]         
                 p(l14) = [1] x2 + [0]                  
                 p(l15) = [1] x2 + [1] x5 + [1]         
                 p(l16) = [1] x3 + [2] x5 + [0]         
                  p(l2) = [1] x1 + [1] x2 + [2] x3 + [1]
                  p(l3) = [1] x1 + [1] x2 + [0]         
                  p(l4) = [1] x1 + [1] x2 + [4]         
                  p(l5) = [1] x1 + [1] x2 + [4]         
                  p(l6) = [0]                           
                  p(l7) = [1] x1 + [1] x2 + [0]         
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [5]
                  p(l9) = [1] x1 + [2]                  
                  p(m1) = [3]                           
                  p(m2) = [3]                           
                  p(m3) = [2] x4 + [0]                  
                  p(m4) = [2] x4 + [3]                  
                  p(m5) = [1] x1 + [1] x3 + [3]         
               p(monus) = [0]                           
          
          Following rules are strictly oriented:
          l2(x,y,res,tmp,mtmp,False()) = [2] res + [1] x + [1] y + [1]
                                       > [1] x + [1] y + [0]          
                                       = l3(x,y,res,tmp,mtmp,False()) 
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                                
                                        >= [0]                                
                                        =  False()                            
          
                            <(0(),S(y)) =  [0]                                
                                        >= [0]                                
                                        =  True()                             
          
                           <(S(x),S(y)) =  [0]                                
                                        >= [0]                                
                                        =  <(x,y)                             
          
                      bool2Nat(False()) =  [1]                                
                                        >= [0]                                
                                        =  0()                                
          
                       bool2Nat(True()) =  [1]                                
                                        >= [0]                                
                                        =  S(0())                             
          
                          e1(a,b,res,t) =  [4]                                
                                        >= [4]                                
                                        =  e2(a,b,res,<(a,b))                 
          
                    e2(a,b,res,False()) =  [4]                                
                                        >= [0]                                
                                        =  False()                            
          
                     e2(a,b,res,True()) =  [4]                                
                                        >= [3]                                
                                        =  e3(a,b,res,True())                 
          
                          e3(a,b,res,t) =  [3]                                
                                        >= [2]                                
                                        =  e4(a,b,res,<(b,a))                 
          
                    e4(a,b,res,False()) =  [2]                                
                                        >= [0]                                
                                        =  False()                            
          
                     e4(a,b,res,True()) =  [2]                                
                                        >= [0]                                
                                        =  True()                             
          
                          e5(a,b,res,t) =  [0]                                
                                        >= [0]                                
                                        =  True()                             
          
                          e6(a,b,res,t) =  [0]                                
                                        >= [0]                                
                                        =  False()                            
          
                          e7(a,b,res,t) =  [1]                                
                                        >= [0]                                
                                        =  False()                            
          
                          e8(a,b,res,t) =  [1] res + [1]                      
                                        >= [1] res + [0]                      
                                        =  res                                
          
                            equal0(a,b) =  [4]                                
                                        >= [4]                                
                                        =  e1(a,b,False(),False())            
          
                               gcd(x,y) =  [1] x + [1] y + [1]                
                                        >= [1] x + [1] y + [2]                
                                        =  l1(x,y,0(),False(),False(),False())
          
                             help1(0()) =  [7]                                
                                        >= [0]                                
                                        =  False()                            
          
                          help1(S(0())) =  [7]                                
                                        >= [0]                                
                                        =  False()                            
          
                         help1(S(S(x))) =  [7]                                
                                        >= [0]                                
                                        =  True()                             
          
                 l1(x,y,res,tmp,mtmp,t) =  [4] res + [1] x + [1] y + [2]      
                                        >= [2] res + [1] x + [1] y + [1]      
                                        =  l2(x,y,res,tmp,mtmp,False())       
          
                l10(x,y,res,tmp,mtmp,t) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))       
          
          l11(x,y,res,tmp,mtmp,False()) =  [1] y + [1]                        
                                        >= [1] y + [0]                        
                                        =  l14(x,y,res,tmp,mtmp,False())      
          
           l11(x,y,res,tmp,mtmp,True()) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l12(x,y,res,tmp,mtmp,True())       
          
                l12(x,y,res,tmp,mtmp,t) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l13(x,y,res,tmp,monus(x,y),t)      
          
             l13(x,y,res,tmp,False(),t) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)  
          
              l13(x,y,res,tmp,True(),t) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)
          
                l14(x,y,res,tmp,mtmp,t) =  [1] y + [0]                        
                                        >= [1] y + [1]                        
                                        =  l15(x,y,res,tmp,monus(x,y),t)      
          
             l15(x,y,res,tmp,False(),t) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)  
          
              l15(x,y,res,tmp,True(),t) =  [1] y + [1]                        
                                        >= [1] y + [1]                        
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)
          
                l16(x,y,res,tmp,mtmp,t) =  [2] mtmp + [1] res + [0]           
                                        >= [1] res + [0]                      
                                        =  res                                
          
            l2(x,y,res,tmp,mtmp,True()) =  [2] res + [1] x + [1] y + [1]      
                                        >= [1] res + [0]                      
                                        =  res                                
          
                 l3(x,y,res,tmp,mtmp,t) =  [1] x + [1] y + [0]                
                                        >= [1] x + [1] y + [4]                
                                        =  l4(x,y,0(),tmp,mtmp,t)             
          
                l4(x',x,res,tmp,mtmp,t) =  [1] x + [1] x' + [4]               
                                        >= [1] x + [1] x' + [4]               
                                        =  l5(x',x,res,tmp,mtmp,False())      
          
           l5(x,y,res,tmp,mtmp,False()) =  [1] x + [1] y + [4]                
                                        >= [1] x + [1] y + [0]                
                                        =  l7(x,y,res,tmp,mtmp,False())       
          
            l5(x,y,res,tmp,mtmp,True()) =  [1] x + [1] y + [4]                
                                        >= [0]                                
                                        =  0()                                
          
                 l6(x,y,res,tmp,mtmp,t) =  [0]                                
                                        >= [0]                                
                                        =  0()                                
          
                 l7(x,y,res,tmp,mtmp,t) =  [1] x + [1] y + [0]                
                                        >= [1] x + [1] y + [9]                
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)     
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [1] y + [5]              
                                        >= [1] res + [0]                      
                                        =  res                                
          
             l8(x,y,res,False(),mtmp,t) =  [1] x + [1] y + [5]                
                                        >= [1] y + [1]                        
                                        =  l10(x,y,res,False(),mtmp,t)        
          
              l9(res,y,res',tmp,mtmp,t) =  [1] res + [2]                      
                                        >= [1] res + [0]                      
                                        =  res                                
          
                          m1(a,x,res,t) =  [3]                                
                                        >= [3]                                
                                        =  m2(a,x,res,False())                
          
                    m2(a,b,res,False()) =  [3]                                
                                        >= [3]                                
                                        =  m4(a,b,res,False())                
          
                   m2(0(),b,res,True()) =  [3]                                
                                        >= [0]                                
                                        =  False()                            
          
                m2(S(0()),b,res,True()) =  [3]                                
                                        >= [0]                                
                                        =  False()                            
          
               m2(S(S(x)),b,res,True()) =  [3]                                
                                        >= [0]                                
                                        =  True()                             
          
                        m3(0(),b,res,t) =  [2] t + [0]                        
                                        >= [0]                                
                                        =  False()                            
          
                     m3(S(0()),b,res,t) =  [2] t + [0]                        
                                        >= [0]                                
                                        =  False()                            
          
                    m3(S(S(x)),b,res,t) =  [2] t + [0]                        
                                        >= [0]                                
                                        =  True()                             
          
                   m4(S(x'),S(x),res,t) =  [2] t + [3]                        
                                        >= [3]                                
                                        =  m5(S(x'),S(x),monus(x',x),t)       
          
                          m5(a,b,res,t) =  [1] a + [1] res + [3]              
                                        >= [1] res + [0]                      
                                        =  res                                
          
                             monus(a,b) =  [0]                                
                                        >= [3]                                
                                        =  m1(a,b,False(),False())            
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                             
                   p(<) = [0]                                             
               p(False) = [0]                                             
                   p(S) = [0]                                             
                p(True) = [0]                                             
            p(bool2Nat) = [3]                                             
                  p(e1) = [2]                                             
                  p(e2) = [1] x4 + [2]                                    
                  p(e3) = [1]                                             
                  p(e4) = [1] x4 + [1]                                    
                  p(e5) = [0]                                             
                  p(e6) = [0]                                             
                  p(e7) = [0]                                             
                  p(e8) = [1] x3 + [1]                                    
              p(equal0) = [2]                                             
                 p(gcd) = [4] x1 + [4] x2 + [0]                           
               p(help1) = [7]                                             
                  p(l1) = [4] x1 + [4] x2 + [5] x3 + [4] x5 + [1] x6 + [5]
                 p(l10) = [1] x1 + [4] x2 + [4] x4 + [4]                  
                 p(l11) = [1] x1 + [4] x2 + [1] x4 + [1] x6 + [3]         
                 p(l12) = [1] x1 + [4] x2 + [1] x4 + [4] x6 + [3]         
                 p(l13) = [1] x1 + [4] x2 + [1] x5 + [0]                  
                 p(l14) = [4] x2 + [3] x6 + [2]                           
                 p(l15) = [4] x2 + [1] x5 + [1] x6 + [0]                  
                 p(l16) = [1] x3 + [0]                                    
                  p(l2) = [4] x1 + [4] x2 + [4] x3 + [1] x5 + [2] x6 + [5]
                  p(l3) = [2] x1 + [4] x2 + [5]                           
                  p(l4) = [2] x1 + [4] x2 + [4]                           
                  p(l5) = [1] x1 + [4] x2 + [3]                           
                  p(l6) = [0]                                             
                  p(l7) = [1] x1 + [4] x2 + [0]                           
                  p(l8) = [1] x1 + [4] x2 + [1] x4 + [4]                  
                  p(l9) = [1] x1 + [0]                                    
                  p(m1) = [3]                                             
                  p(m2) = [3]                                             
                  p(m3) = [0]                                             
                  p(m4) = [4] x4 + [3]                                    
                  p(m5) = [1] x3 + [4] x4 + [0]                           
               p(monus) = [2]                                             
          
          Following rules are strictly oriented:
          l3(x,y,res,tmp,mtmp,t) = [2] x + [4] y + [5]   
                                 > [2] x + [4] y + [4]   
                                 = l4(x,y,0(),tmp,mtmp,t)
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                            <(0(),S(y)) =  [0]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                           <(S(x),S(y)) =  [0]                                             
                                        >= [0]                                             
                                        =  <(x,y)                                          
          
                      bool2Nat(False()) =  [3]                                             
                                        >= [0]                                             
                                        =  0()                                             
          
                       bool2Nat(True()) =  [3]                                             
                                        >= [0]                                             
                                        =  S(0())                                          
          
                          e1(a,b,res,t) =  [2]                                             
                                        >= [2]                                             
                                        =  e2(a,b,res,<(a,b))                              
          
                    e2(a,b,res,False()) =  [2]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                     e2(a,b,res,True()) =  [2]                                             
                                        >= [1]                                             
                                        =  e3(a,b,res,True())                              
          
                          e3(a,b,res,t) =  [1]                                             
                                        >= [1]                                             
                                        =  e4(a,b,res,<(b,a))                              
          
                    e4(a,b,res,False()) =  [1]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                     e4(a,b,res,True()) =  [1]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                          e5(a,b,res,t) =  [0]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                          e6(a,b,res,t) =  [0]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                          e7(a,b,res,t) =  [0]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                          e8(a,b,res,t) =  [1] res + [1]                                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                            equal0(a,b) =  [2]                                             
                                        >= [2]                                             
                                        =  e1(a,b,False(),False())                         
          
                               gcd(x,y) =  [4] x + [4] y + [0]                             
                                        >= [4] x + [4] y + [5]                             
                                        =  l1(x,y,0(),False(),False(),False())             
          
                             help1(0()) =  [7]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                          help1(S(0())) =  [7]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                         help1(S(S(x))) =  [7]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                 l1(x,y,res,tmp,mtmp,t) =  [4] mtmp + [5] res + [1] t + [4] x + [4] y + [5]
                                        >= [1] mtmp + [4] res + [4] x + [4] y + [5]        
                                        =  l2(x,y,res,tmp,mtmp,False())                    
          
                l10(x,y,res,tmp,mtmp,t) =  [4] tmp + [1] x + [4] y + [4]                   
                                        >= [1] tmp + [1] x + [4] y + [3]                   
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                    
          
          l11(x,y,res,tmp,mtmp,False()) =  [1] tmp + [1] x + [4] y + [3]                   
                                        >= [4] y + [2]                                     
                                        =  l14(x,y,res,tmp,mtmp,False())                   
          
           l11(x,y,res,tmp,mtmp,True()) =  [1] tmp + [1] x + [4] y + [3]                   
                                        >= [1] tmp + [1] x + [4] y + [3]                   
                                        =  l12(x,y,res,tmp,mtmp,True())                    
          
                l12(x,y,res,tmp,mtmp,t) =  [4] t + [1] tmp + [1] x + [4] y + [3]           
                                        >= [1] x + [4] y + [2]                             
                                        =  l13(x,y,res,tmp,monus(x,y),t)                   
          
             l13(x,y,res,tmp,False(),t) =  [1] x + [4] y + [0]                             
                                        >= [4] y + [0]                                     
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)               
          
              l13(x,y,res,tmp,True(),t) =  [1] x + [4] y + [0]                             
                                        >= [4] y + [0]                                     
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)             
          
                l14(x,y,res,tmp,mtmp,t) =  [3] t + [4] y + [2]                             
                                        >= [1] t + [4] y + [2]                             
                                        =  l15(x,y,res,tmp,monus(x,y),t)                   
          
             l15(x,y,res,tmp,False(),t) =  [1] t + [4] y + [0]                             
                                        >= [4] y + [0]                                     
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)               
          
              l15(x,y,res,tmp,True(),t) =  [1] t + [4] y + [0]                             
                                        >= [4] y + [0]                                     
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)             
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
           l2(x,y,res,tmp,mtmp,False()) =  [1] mtmp + [4] res + [4] x + [4] y + [5]        
                                        >= [2] x + [4] y + [5]                             
                                        =  l3(x,y,res,tmp,mtmp,False())                    
          
            l2(x,y,res,tmp,mtmp,True()) =  [1] mtmp + [4] res + [4] x + [4] y + [5]        
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                l4(x',x,res,tmp,mtmp,t) =  [4] x + [2] x' + [4]                            
                                        >= [4] x + [1] x' + [3]                            
                                        =  l5(x',x,res,tmp,mtmp,False())                   
          
           l5(x,y,res,tmp,mtmp,False()) =  [1] x + [4] y + [3]                             
                                        >= [1] x + [4] y + [0]                             
                                        =  l7(x,y,res,tmp,mtmp,False())                    
          
            l5(x,y,res,tmp,mtmp,True()) =  [1] x + [4] y + [3]                             
                                        >= [0]                                             
                                        =  0()                                             
          
                 l6(x,y,res,tmp,mtmp,t) =  [0]                                             
                                        >= [0]                                             
                                        =  0()                                             
          
                 l7(x,y,res,tmp,mtmp,t) =  [1] x + [4] y + [0]                             
                                        >= [1] x + [4] y + [6]                             
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                  
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [4] y + [4]                           
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
             l8(x,y,res,False(),mtmp,t) =  [1] x + [4] y + [4]                             
                                        >= [1] x + [4] y + [4]                             
                                        =  l10(x,y,res,False(),mtmp,t)                     
          
              l9(res,y,res',tmp,mtmp,t) =  [1] res + [0]                                   
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                          m1(a,x,res,t) =  [3]                                             
                                        >= [3]                                             
                                        =  m2(a,x,res,False())                             
          
                    m2(a,b,res,False()) =  [3]                                             
                                        >= [3]                                             
                                        =  m4(a,b,res,False())                             
          
                   m2(0(),b,res,True()) =  [3]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                m2(S(0()),b,res,True()) =  [3]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
               m2(S(S(x)),b,res,True()) =  [3]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                        m3(0(),b,res,t) =  [0]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                     m3(S(0()),b,res,t) =  [0]                                             
                                        >= [0]                                             
                                        =  False()                                         
          
                    m3(S(S(x)),b,res,t) =  [0]                                             
                                        >= [0]                                             
                                        =  True()                                          
          
                   m4(S(x'),S(x),res,t) =  [4] t + [3]                                     
                                        >= [4] t + [2]                                     
                                        =  m5(S(x'),S(x),monus(x',x),t)                    
          
                          m5(a,b,res,t) =  [1] res + [4] t + [0]                           
                                        >= [1] res + [0]                                   
                                        =  res                                             
          
                             monus(a,b) =  [2]                                             
                                        >= [3]                                             
                                        =  m1(a,b,False(),False())                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 10: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                                      
                   p(<) = [1]                                                      
               p(False) = [0]                                                      
                   p(S) = [1] x1 + [0]                                             
                p(True) = [0]                                                      
            p(bool2Nat) = [1] x1 + [1]                                             
                  p(e1) = [2] x3 + [3]                                             
                  p(e2) = [2] x3 + [1] x4 + [2]                                    
                  p(e3) = [2] x3 + [2]                                             
                  p(e4) = [1] x4 + [1]                                             
                  p(e5) = [2] x1 + [0]                                             
                  p(e6) = [1]                                                      
                  p(e7) = [1]                                                      
                  p(e8) = [1] x1 + [1] x2 + [4] x3 + [2] x4 + [0]                  
              p(equal0) = [3]                                                      
                 p(gcd) = [1] x1 + [1] x2 + [0]                                    
               p(help1) = [0]                                                      
                  p(l1) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [1] x6 + [1]
                 p(l10) = [1] x2 + [6] x4 + [1] x6 + [4]                           
                 p(l11) = [1] x2 + [5] x4 + [1] x6 + [1]                           
                 p(l12) = [1] x2 + [4] x4 + [1]                                    
                 p(l13) = [1] x2 + [4] x4 + [1] x5 + [1]                           
                 p(l14) = [1] x2 + [2] x4 + [4] x6 + [1]                           
                 p(l15) = [1] x2 + [2] x4 + [1] x5 + [4] x6 + [0]                  
                 p(l16) = [1] x3 + [2] x4 + [0]                                    
                  p(l2) = [1] x1 + [1] x2 + [1] x3 + [1] x5 + [1]                  
                  p(l3) = [1] x1 + [1] x2 + [1] x3 + [1]                           
                  p(l4) = [1] x1 + [1] x2 + [0]                                    
                  p(l5) = [1] x1 + [1] x2 + [0]                                    
                  p(l6) = [1] x2 + [1] x3 + [1]                                    
                  p(l7) = [1] x1 + [1] x2 + [5] x6 + [0]                           
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [1] x6 + [5]                  
                  p(l9) = [2] x1 + [1] x2 + [1] x4 + [4]                           
                  p(m1) = [1] x3 + [1] x4 + [5]                                    
                  p(m2) = [1] x3 + [1] x4 + [5]                                    
                  p(m3) = [4] x1 + [1] x3 + [4] x4 + [0]                           
                  p(m4) = [1] x3 + [2] x4 + [2]                                    
                  p(m5) = [1] x3 + [1] x4 + [1]                                    
               p(monus) = [0]                                                      
          
          Following rules are strictly oriented:
          l14(x,y,res,tmp,mtmp,t) = [4] t + [2] tmp + [1] y + [1]
                                  > [4] t + [2] tmp + [1] y + [0]
                                  = l15(x,y,res,tmp,monus(x,y),t)
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [1]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                            <(0(),S(y)) =  [1]                                                       
                                        >= [0]                                                       
                                        =  True()                                                    
          
                           <(S(x),S(y)) =  [1]                                                       
                                        >= [1]                                                       
                                        =  <(x,y)                                                    
          
                      bool2Nat(False()) =  [1]                                                       
                                        >= [0]                                                       
                                        =  0()                                                       
          
                       bool2Nat(True()) =  [1]                                                       
                                        >= [0]                                                       
                                        =  S(0())                                                    
          
                          e1(a,b,res,t) =  [2] res + [3]                                             
                                        >= [2] res + [3]                                             
                                        =  e2(a,b,res,<(a,b))                                        
          
                    e2(a,b,res,False()) =  [2] res + [2]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     e2(a,b,res,True()) =  [2] res + [2]                                             
                                        >= [2] res + [2]                                             
                                        =  e3(a,b,res,True())                                        
          
                          e3(a,b,res,t) =  [2] res + [2]                                             
                                        >= [2]                                                       
                                        =  e4(a,b,res,<(b,a))                                        
          
                    e4(a,b,res,False()) =  [1]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     e4(a,b,res,True()) =  [1]                                                       
                                        >= [0]                                                       
                                        =  True()                                                    
          
                          e5(a,b,res,t) =  [2] a + [0]                                               
                                        >= [0]                                                       
                                        =  True()                                                    
          
                          e6(a,b,res,t) =  [1]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          e7(a,b,res,t) =  [1]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          e8(a,b,res,t) =  [1] a + [1] b + [4] res + [2] t + [0]                     
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                            equal0(a,b) =  [3]                                                       
                                        >= [3]                                                       
                                        =  e1(a,b,False(),False())                                   
          
                               gcd(x,y) =  [1] x + [1] y + [0]                                       
                                        >= [1] x + [1] y + [1]                                       
                                        =  l1(x,y,0(),False(),False(),False())                       
          
                             help1(0()) =  [0]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          help1(S(0())) =  [0]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                         help1(S(S(x))) =  [0]                                                       
                                        >= [0]                                                       
                                        =  True()                                                    
          
                 l1(x,y,res,tmp,mtmp,t) =  [1] mtmp + [1] res + [1] t + [1] tmp + [1] x + [1] y + [1]
                                        >= [1] mtmp + [1] res + [1] x + [1] y + [1]                  
                                        =  l2(x,y,res,tmp,mtmp,False())                              
          
                l10(x,y,res,tmp,mtmp,t) =  [1] t + [6] tmp + [1] y + [4]                             
                                        >= [5] tmp + [1] y + [2]                                     
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                              
          
          l11(x,y,res,tmp,mtmp,False()) =  [5] tmp + [1] y + [1]                                     
                                        >= [2] tmp + [1] y + [1]                                     
                                        =  l14(x,y,res,tmp,mtmp,False())                             
          
           l11(x,y,res,tmp,mtmp,True()) =  [5] tmp + [1] y + [1]                                     
                                        >= [4] tmp + [1] y + [1]                                     
                                        =  l12(x,y,res,tmp,mtmp,True())                              
          
                l12(x,y,res,tmp,mtmp,t) =  [4] tmp + [1] y + [1]                                     
                                        >= [4] tmp + [1] y + [1]                                     
                                        =  l13(x,y,res,tmp,monus(x,y),t)                             
          
             l13(x,y,res,tmp,False(),t) =  [4] tmp + [1] y + [1]                                     
                                        >= [2] tmp + [1] y + [0]                                     
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)                         
          
              l13(x,y,res,tmp,True(),t) =  [4] tmp + [1] y + [1]                                     
                                        >= [2] tmp + [1] y + [0]                                     
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)                       
          
             l15(x,y,res,tmp,False(),t) =  [4] t + [2] tmp + [1] y + [0]                             
                                        >= [2] tmp + [1] y + [0]                                     
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)                         
          
              l15(x,y,res,tmp,True(),t) =  [4] t + [2] tmp + [1] y + [0]                             
                                        >= [2] tmp + [1] y + [0]                                     
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)                       
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [2] tmp + [0]                                   
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
           l2(x,y,res,tmp,mtmp,False()) =  [1] mtmp + [1] res + [1] x + [1] y + [1]                  
                                        >= [1] res + [1] x + [1] y + [1]                             
                                        =  l3(x,y,res,tmp,mtmp,False())                              
          
            l2(x,y,res,tmp,mtmp,True()) =  [1] mtmp + [1] res + [1] x + [1] y + [1]                  
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                 l3(x,y,res,tmp,mtmp,t) =  [1] res + [1] x + [1] y + [1]                             
                                        >= [1] x + [1] y + [0]                                       
                                        =  l4(x,y,0(),tmp,mtmp,t)                                    
          
                l4(x',x,res,tmp,mtmp,t) =  [1] x + [1] x' + [0]                                      
                                        >= [1] x + [1] x' + [0]                                      
                                        =  l5(x',x,res,tmp,mtmp,False())                             
          
           l5(x,y,res,tmp,mtmp,False()) =  [1] x + [1] y + [0]                                       
                                        >= [1] x + [1] y + [0]                                       
                                        =  l7(x,y,res,tmp,mtmp,False())                              
          
            l5(x,y,res,tmp,mtmp,True()) =  [1] x + [1] y + [0]                                       
                                        >= [0]                                                       
                                        =  0()                                                       
          
                 l6(x,y,res,tmp,mtmp,t) =  [1] res + [1] y + [1]                                     
                                        >= [0]                                                       
                                        =  0()                                                       
          
                 l7(x,y,res,tmp,mtmp,t) =  [5] t + [1] x + [1] y + [0]                               
                                        >= [1] t + [1] x + [1] y + [8]                               
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                            
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [1] t + [1] y + [5]                             
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
             l8(x,y,res,False(),mtmp,t) =  [1] t + [1] x + [1] y + [5]                               
                                        >= [1] t + [1] y + [4]                                       
                                        =  l10(x,y,res,False(),mtmp,t)                               
          
              l9(res,y,res',tmp,mtmp,t) =  [2] res + [1] tmp + [1] y + [4]                           
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                          m1(a,x,res,t) =  [1] res + [1] t + [5]                                     
                                        >= [1] res + [5]                                             
                                        =  m2(a,x,res,False())                                       
          
                    m2(a,b,res,False()) =  [1] res + [5]                                             
                                        >= [1] res + [2]                                             
                                        =  m4(a,b,res,False())                                       
          
                   m2(0(),b,res,True()) =  [1] res + [5]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                m2(S(0()),b,res,True()) =  [1] res + [5]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
               m2(S(S(x)),b,res,True()) =  [1] res + [5]                                             
                                        >= [0]                                                       
                                        =  True()                                                    
          
                        m3(0(),b,res,t) =  [1] res + [4] t + [0]                                     
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     m3(S(0()),b,res,t) =  [1] res + [4] t + [0]                                     
                                        >= [0]                                                       
                                        =  False()                                                   
          
                    m3(S(S(x)),b,res,t) =  [1] res + [4] t + [4] x + [0]                             
                                        >= [0]                                                       
                                        =  True()                                                    
          
                   m4(S(x'),S(x),res,t) =  [1] res + [2] t + [2]                                     
                                        >= [1] t + [1]                                               
                                        =  m5(S(x'),S(x),monus(x',x),t)                              
          
                          m5(a,b,res,t) =  [1] res + [1] t + [1]                                     
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                             monus(a,b) =  [0]                                                       
                                        >= [5]                                                       
                                        =  m1(a,b,False(),False())                                   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 11: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l16(x,y,res,tmp,mtmp,t) -> res
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                                      
                   p(<) = [2]                                                      
               p(False) = [0]                                                      
                   p(S) = [1] x1 + [1]                                             
                p(True) = [2]                                                      
            p(bool2Nat) = [1] x1 + [3]                                             
                  p(e1) = [5] x3 + [4]                                             
                  p(e2) = [4] x3 + [1] x4 + [2]                                    
                  p(e3) = [1] x3 + [1] x4 + [2]                                    
                  p(e4) = [1] x4 + [0]                                             
                  p(e5) = [1] x2 + [2] x3 + [1] x4 + [3]                           
                  p(e6) = [2] x1 + [1] x2 + [1] x4 + [0]                           
                  p(e7) = [4] x2 + [1] x3 + [3]                                    
                  p(e8) = [1] x1 + [4] x3 + [2]                                    
              p(equal0) = [4]                                                      
                 p(gcd) = [1] x1 + [1] x2 + [0]                                    
               p(help1) = [4] x1 + [4]                                             
                  p(l1) = [1] x1 + [1] x2 + [1] x3 + [4] x4 + [1] x6 + [7]         
                 p(l10) = [1] x1 + [1] x2 + [3] x4 + [2]                           
                 p(l11) = [1] x1 + [1] x2 + [2] x4 + [1] x6 + [0]                  
                 p(l12) = [1] x1 + [1] x2 + [0]                                    
                 p(l13) = [1] x1 + [1] x2 + [1] x5 + [0]                           
                 p(l14) = [1] x1 + [1] x2 + [1] x4 + [5] x6 + [0]                  
                 p(l15) = [1] x1 + [1] x2 + [1] x4 + [1] x5 + [1] x6 + [0]         
                 p(l16) = [1] x3 + [0]                                             
                  p(l2) = [1] x1 + [1] x2 + [1] x3 + [4] x4 + [7]                  
                  p(l3) = [1] x1 + [1] x2 + [1] x3 + [4] x4 + [4] x6 + [7]         
                  p(l4) = [1] x1 + [1] x2 + [4] x4 + [7]                           
                  p(l5) = [1] x1 + [1] x2 + [1] x4 + [4] x6 + [7]                  
                  p(l6) = [1] x1 + [4] x2 + [1] x3 + [1] x4 + [4] x5 + [1] x6 + [0]
                  p(l7) = [1] x1 + [1] x2 + [5] x6 + [7]                           
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [1] x6 + [2]                  
                  p(l9) = [1] x1 + [1] x2 + [1]                                    
                  p(m1) = [3]                                                      
                  p(m2) = [4] x4 + [1]                                             
                  p(m3) = [6] x1 + [2] x2 + [1] x3 + [1] x4 + [2]                  
                  p(m4) = [1]                                                      
                  p(m5) = [1] x3 + [0]                                             
               p(monus) = [0]                                                      
          
          Following rules are strictly oriented:
          l7(x,y,res,tmp,mtmp,t) = [5] t + [1] x + [1] y + [7]   
                                 > [1] t + [1] x + [1] y + [6]   
                                 = l8(x,y,res,equal0(x,y),mtmp,t)
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [2]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                            <(0(),S(y)) =  [2]                                                       
                                        >= [2]                                                       
                                        =  True()                                                    
          
                           <(S(x),S(y)) =  [2]                                                       
                                        >= [2]                                                       
                                        =  <(x,y)                                                    
          
                      bool2Nat(False()) =  [3]                                                       
                                        >= [0]                                                       
                                        =  0()                                                       
          
                       bool2Nat(True()) =  [5]                                                       
                                        >= [1]                                                       
                                        =  S(0())                                                    
          
                          e1(a,b,res,t) =  [5] res + [4]                                             
                                        >= [4] res + [4]                                             
                                        =  e2(a,b,res,<(a,b))                                        
          
                    e2(a,b,res,False()) =  [4] res + [2]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     e2(a,b,res,True()) =  [4] res + [4]                                             
                                        >= [1] res + [4]                                             
                                        =  e3(a,b,res,True())                                        
          
                          e3(a,b,res,t) =  [1] res + [1] t + [2]                                     
                                        >= [2]                                                       
                                        =  e4(a,b,res,<(b,a))                                        
          
                    e4(a,b,res,False()) =  [0]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     e4(a,b,res,True()) =  [2]                                                       
                                        >= [2]                                                       
                                        =  True()                                                    
          
                          e5(a,b,res,t) =  [1] b + [2] res + [1] t + [3]                             
                                        >= [2]                                                       
                                        =  True()                                                    
          
                          e6(a,b,res,t) =  [2] a + [1] b + [1] t + [0]                               
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          e7(a,b,res,t) =  [4] b + [1] res + [3]                                     
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          e8(a,b,res,t) =  [1] a + [4] res + [2]                                     
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                            equal0(a,b) =  [4]                                                       
                                        >= [4]                                                       
                                        =  e1(a,b,False(),False())                                   
          
                               gcd(x,y) =  [1] x + [1] y + [0]                                       
                                        >= [1] x + [1] y + [7]                                       
                                        =  l1(x,y,0(),False(),False(),False())                       
          
                             help1(0()) =  [4]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          help1(S(0())) =  [8]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                         help1(S(S(x))) =  [4] x + [12]                                              
                                        >= [2]                                                       
                                        =  True()                                                    
          
                 l1(x,y,res,tmp,mtmp,t) =  [1] res + [1] t + [4] tmp + [1] x + [1] y + [7]           
                                        >= [1] res + [4] tmp + [1] x + [1] y + [7]                   
                                        =  l2(x,y,res,tmp,mtmp,False())                              
          
                l10(x,y,res,tmp,mtmp,t) =  [3] tmp + [1] x + [1] y + [2]                             
                                        >= [2] tmp + [1] x + [1] y + [2]                             
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                              
          
          l11(x,y,res,tmp,mtmp,False()) =  [2] tmp + [1] x + [1] y + [0]                             
                                        >= [1] tmp + [1] x + [1] y + [0]                             
                                        =  l14(x,y,res,tmp,mtmp,False())                             
          
           l11(x,y,res,tmp,mtmp,True()) =  [2] tmp + [1] x + [1] y + [2]                             
                                        >= [1] x + [1] y + [0]                                       
                                        =  l12(x,y,res,tmp,mtmp,True())                              
          
                l12(x,y,res,tmp,mtmp,t) =  [1] x + [1] y + [0]                                       
                                        >= [1] x + [1] y + [0]                                       
                                        =  l13(x,y,res,tmp,monus(x,y),t)                             
          
             l13(x,y,res,tmp,False(),t) =  [1] x + [1] y + [0]                                       
                                        >= [1] y + [0]                                               
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)                         
          
              l13(x,y,res,tmp,True(),t) =  [1] x + [1] y + [2]                                       
                                        >= [1] y + [1]                                               
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)                       
          
                l14(x,y,res,tmp,mtmp,t) =  [5] t + [1] tmp + [1] x + [1] y + [0]                     
                                        >= [1] t + [1] tmp + [1] x + [1] y + [0]                     
                                        =  l15(x,y,res,tmp,monus(x,y),t)                             
          
             l15(x,y,res,tmp,False(),t) =  [1] t + [1] tmp + [1] x + [1] y + [0]                     
                                        >= [1] y + [0]                                               
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)                         
          
              l15(x,y,res,tmp,True(),t) =  [1] t + [1] tmp + [1] x + [1] y + [2]                     
                                        >= [1] y + [1]                                               
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)                       
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [0]                                             
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
           l2(x,y,res,tmp,mtmp,False()) =  [1] res + [4] tmp + [1] x + [1] y + [7]                   
                                        >= [1] res + [4] tmp + [1] x + [1] y + [7]                   
                                        =  l3(x,y,res,tmp,mtmp,False())                              
          
            l2(x,y,res,tmp,mtmp,True()) =  [1] res + [4] tmp + [1] x + [1] y + [7]                   
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                 l3(x,y,res,tmp,mtmp,t) =  [1] res + [4] t + [4] tmp + [1] x + [1] y + [7]           
                                        >= [4] tmp + [1] x + [1] y + [7]                             
                                        =  l4(x,y,0(),tmp,mtmp,t)                                    
          
                l4(x',x,res,tmp,mtmp,t) =  [4] tmp + [1] x + [1] x' + [7]                            
                                        >= [1] tmp + [1] x + [1] x' + [7]                            
                                        =  l5(x',x,res,tmp,mtmp,False())                             
          
           l5(x,y,res,tmp,mtmp,False()) =  [1] tmp + [1] x + [1] y + [7]                             
                                        >= [1] x + [1] y + [7]                                       
                                        =  l7(x,y,res,tmp,mtmp,False())                              
          
            l5(x,y,res,tmp,mtmp,True()) =  [1] tmp + [1] x + [1] y + [15]                            
                                        >= [0]                                                       
                                        =  0()                                                       
          
                 l6(x,y,res,tmp,mtmp,t) =  [4] mtmp + [1] res + [1] t + [1] tmp + [1] x + [4] y + [0]
                                        >= [0]                                                       
                                        =  0()                                                       
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [1] t + [1] y + [4]                             
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
             l8(x,y,res,False(),mtmp,t) =  [1] t + [1] x + [1] y + [2]                               
                                        >= [1] x + [1] y + [2]                                       
                                        =  l10(x,y,res,False(),mtmp,t)                               
          
              l9(res,y,res',tmp,mtmp,t) =  [1] res + [1] y + [1]                                     
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                          m1(a,x,res,t) =  [3]                                                       
                                        >= [1]                                                       
                                        =  m2(a,x,res,False())                                       
          
                    m2(a,b,res,False()) =  [1]                                                       
                                        >= [1]                                                       
                                        =  m4(a,b,res,False())                                       
          
                   m2(0(),b,res,True()) =  [9]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                m2(S(0()),b,res,True()) =  [9]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
               m2(S(S(x)),b,res,True()) =  [9]                                                       
                                        >= [2]                                                       
                                        =  True()                                                    
          
                        m3(0(),b,res,t) =  [2] b + [1] res + [1] t + [2]                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     m3(S(0()),b,res,t) =  [2] b + [1] res + [1] t + [8]                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                    m3(S(S(x)),b,res,t) =  [2] b + [1] res + [1] t + [6] x + [14]                    
                                        >= [2]                                                       
                                        =  True()                                                    
          
                   m4(S(x'),S(x),res,t) =  [1]                                                       
                                        >= [0]                                                       
                                        =  m5(S(x'),S(x),monus(x',x),t)                              
          
                          m5(a,b,res,t) =  [1] res + [0]                                             
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                             monus(a,b) =  [0]                                                       
                                        >= [3]                                                       
                                        =  m1(a,b,False(),False())                                   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 12: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            l16(x,y,res,tmp,mtmp,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                                      
                   p(<) = [0]                                                      
               p(False) = [0]                                                      
                   p(S) = [0]                                                      
                p(True) = [0]                                                      
            p(bool2Nat) = [2] x1 + [3]                                             
                  p(e1) = [4] x3 + [1] x4 + [0]                                    
                  p(e2) = [1] x4 + [0]                                             
                  p(e3) = [2] x4 + [0]                                             
                  p(e4) = [1] x4 + [0]                                             
                  p(e5) = [4]                                                      
                  p(e6) = [4] x3 + [4] x4 + [0]                                    
                  p(e7) = [1] x2 + [1] x3 + [4]                                    
                  p(e8) = [1] x1 + [4] x3 + [1] x4 + [0]                           
              p(equal0) = [0]                                                      
                 p(gcd) = [2] x1 + [2] x2 + [0]                                    
               p(help1) = [2]                                                      
                  p(l1) = [1] x1 + [2] x2 + [4] x3 + [3] x4 + [1] x5 + [3]         
                 p(l10) = [2] x2 + [4] x4 + [1]                                    
                 p(l11) = [2] x2 + [1] x6 + [1]                                    
                 p(l12) = [2] x2 + [1]                                             
                 p(l13) = [2] x2 + [1] x5 + [1]                                    
                 p(l14) = [2] x2 + [1]                                             
                 p(l15) = [2] x2 + [1] x5 + [1]                                    
                 p(l16) = [1] x3 + [1]                                             
                  p(l2) = [1] x1 + [2] x2 + [4] x3 + [3] x4 + [1] x5 + [1] x6 + [1]
                  p(l3) = [1] x1 + [2] x2 + [3] x4 + [1]                           
                  p(l4) = [1] x1 + [2] x2 + [2] x4 + [1]                           
                  p(l5) = [1] x1 + [2] x2 + [2] x4 + [4] x6 + [1]                  
                  p(l6) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2] x5 + [2]         
                  p(l7) = [1] x1 + [2] x2 + [1] x4 + [1] x6 + [1]                  
                  p(l8) = [1] x1 + [2] x2 + [1] x4 + [1]                           
                  p(l9) = [2] x1 + [1] x2 + [1] x4 + [2] x5 + [1] x6 + [1]         
                  p(m1) = [1] x4 + [7]                                             
                  p(m2) = [2] x4 + [2]                                             
                  p(m3) = [1] x1 + [1] x3 + [1] x4 + [5]                           
                  p(m4) = [6] x4 + [1]                                             
                  p(m5) = [4] x1 + [1] x2 + [1] x3 + [4] x4 + [0]                  
               p(monus) = [0]                                                      
          
          Following rules are strictly oriented:
          l16(x,y,res,tmp,mtmp,t) = [1] res + [1]
                                  > [1] res + [0]
                                  = res          
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                            <(0(),S(y)) =  [0]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                           <(S(x),S(y)) =  [0]                                               
                                        >= [0]                                               
                                        =  <(x,y)                                            
          
                      bool2Nat(False()) =  [3]                                               
                                        >= [0]                                               
                                        =  0()                                               
          
                       bool2Nat(True()) =  [3]                                               
                                        >= [0]                                               
                                        =  S(0())                                            
          
                          e1(a,b,res,t) =  [4] res + [1] t + [0]                             
                                        >= [0]                                               
                                        =  e2(a,b,res,<(a,b))                                
          
                    e2(a,b,res,False()) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                     e2(a,b,res,True()) =  [0]                                               
                                        >= [0]                                               
                                        =  e3(a,b,res,True())                                
          
                          e3(a,b,res,t) =  [2] t + [0]                                       
                                        >= [0]                                               
                                        =  e4(a,b,res,<(b,a))                                
          
                    e4(a,b,res,False()) =  [0]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                     e4(a,b,res,True()) =  [0]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                          e5(a,b,res,t) =  [4]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                          e6(a,b,res,t) =  [4] res + [4] t + [0]                             
                                        >= [0]                                               
                                        =  False()                                           
          
                          e7(a,b,res,t) =  [1] b + [1] res + [4]                             
                                        >= [0]                                               
                                        =  False()                                           
          
                          e8(a,b,res,t) =  [1] a + [4] res + [1] t + [0]                     
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                            equal0(a,b) =  [0]                                               
                                        >= [0]                                               
                                        =  e1(a,b,False(),False())                           
          
                               gcd(x,y) =  [2] x + [2] y + [0]                               
                                        >= [1] x + [2] y + [3]                               
                                        =  l1(x,y,0(),False(),False(),False())               
          
                             help1(0()) =  [2]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                          help1(S(0())) =  [2]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                         help1(S(S(x))) =  [2]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                 l1(x,y,res,tmp,mtmp,t) =  [1] mtmp + [4] res + [3] tmp + [1] x + [2] y + [3]
                                        >= [1] mtmp + [4] res + [3] tmp + [1] x + [2] y + [1]
                                        =  l2(x,y,res,tmp,mtmp,False())                      
          
                l10(x,y,res,tmp,mtmp,t) =  [4] tmp + [2] y + [1]                             
                                        >= [2] y + [1]                                       
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                      
          
          l11(x,y,res,tmp,mtmp,False()) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l14(x,y,res,tmp,mtmp,False())                     
          
           l11(x,y,res,tmp,mtmp,True()) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l12(x,y,res,tmp,mtmp,True())                      
          
                l12(x,y,res,tmp,mtmp,t) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l13(x,y,res,tmp,monus(x,y),t)                     
          
             l13(x,y,res,tmp,False(),t) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)                 
          
              l13(x,y,res,tmp,True(),t) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)               
          
                l14(x,y,res,tmp,mtmp,t) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l15(x,y,res,tmp,monus(x,y),t)                     
          
             l15(x,y,res,tmp,False(),t) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)                 
          
              l15(x,y,res,tmp,True(),t) =  [2] y + [1]                                       
                                        >= [2] y + [1]                                       
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)               
          
           l2(x,y,res,tmp,mtmp,False()) =  [1] mtmp + [4] res + [3] tmp + [1] x + [2] y + [1]
                                        >= [3] tmp + [1] x + [2] y + [1]                     
                                        =  l3(x,y,res,tmp,mtmp,False())                      
          
            l2(x,y,res,tmp,mtmp,True()) =  [1] mtmp + [4] res + [3] tmp + [1] x + [2] y + [1]
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                 l3(x,y,res,tmp,mtmp,t) =  [3] tmp + [1] x + [2] y + [1]                     
                                        >= [2] tmp + [1] x + [2] y + [1]                     
                                        =  l4(x,y,0(),tmp,mtmp,t)                            
          
                l4(x',x,res,tmp,mtmp,t) =  [2] tmp + [2] x + [1] x' + [1]                    
                                        >= [2] tmp + [2] x + [1] x' + [1]                    
                                        =  l5(x',x,res,tmp,mtmp,False())                     
          
           l5(x,y,res,tmp,mtmp,False()) =  [2] tmp + [1] x + [2] y + [1]                     
                                        >= [1] tmp + [1] x + [2] y + [1]                     
                                        =  l7(x,y,res,tmp,mtmp,False())                      
          
            l5(x,y,res,tmp,mtmp,True()) =  [2] tmp + [1] x + [2] y + [1]                     
                                        >= [0]                                               
                                        =  0()                                               
          
                 l6(x,y,res,tmp,mtmp,t) =  [2] mtmp + [1] res + [1] tmp + [1] x + [1] y + [2]
                                        >= [0]                                               
                                        =  0()                                               
          
                 l7(x,y,res,tmp,mtmp,t) =  [1] t + [1] tmp + [1] x + [2] y + [1]             
                                        >= [1] x + [2] y + [1]                               
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                    
          
           l8(res,y,res',True(),mtmp,t) =  [1] res + [2] y + [1]                             
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
             l8(x,y,res,False(),mtmp,t) =  [1] x + [2] y + [1]                               
                                        >= [2] y + [1]                                       
                                        =  l10(x,y,res,False(),mtmp,t)                       
          
              l9(res,y,res',tmp,mtmp,t) =  [2] mtmp + [2] res + [1] t + [1] tmp + [1] y + [1]
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                          m1(a,x,res,t) =  [1] t + [7]                                       
                                        >= [2]                                               
                                        =  m2(a,x,res,False())                               
          
                    m2(a,b,res,False()) =  [2]                                               
                                        >= [1]                                               
                                        =  m4(a,b,res,False())                               
          
                   m2(0(),b,res,True()) =  [2]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
                m2(S(0()),b,res,True()) =  [2]                                               
                                        >= [0]                                               
                                        =  False()                                           
          
               m2(S(S(x)),b,res,True()) =  [2]                                               
                                        >= [0]                                               
                                        =  True()                                            
          
                        m3(0(),b,res,t) =  [1] res + [1] t + [5]                             
                                        >= [0]                                               
                                        =  False()                                           
          
                     m3(S(0()),b,res,t) =  [1] res + [1] t + [5]                             
                                        >= [0]                                               
                                        =  False()                                           
          
                    m3(S(S(x)),b,res,t) =  [1] res + [1] t + [5]                             
                                        >= [0]                                               
                                        =  True()                                            
          
                   m4(S(x'),S(x),res,t) =  [6] t + [1]                                       
                                        >= [4] t + [0]                                       
                                        =  m5(S(x'),S(x),monus(x',x),t)                      
          
                          m5(a,b,res,t) =  [4] a + [1] b + [1] res + [4] t + [0]             
                                        >= [1] res + [0]                                     
                                        =  res                                               
          
                             monus(a,b) =  [0]                                               
                                        >= [7]                                               
                                        =  m1(a,b,False(),False())                           
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 13: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            monus(a,b) -> m1(a,b,False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(e2) = {4},
            uargs(e4) = {4},
            uargs(l11) = {6},
            uargs(l13) = {5},
            uargs(l15) = {5},
            uargs(l16) = {3},
            uargs(l8) = {4},
            uargs(m5) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                                                      
                   p(<) = [0]                                                      
               p(False) = [0]                                                      
                   p(S) = [1] x1 + [1]                                             
                p(True) = [0]                                                      
            p(bool2Nat) = [1] x1 + [1]                                             
                  p(e1) = [4] x3 + [2] x4 + [0]                                    
                  p(e2) = [2] x3 + [1] x4 + [0]                                    
                  p(e3) = [1] x3 + [0]                                             
                  p(e4) = [1] x4 + [0]                                             
                  p(e5) = [2] x2 + [1] x3 + [2] x4 + [0]                           
                  p(e6) = [1] x1 + [2] x4 + [0]                                    
                  p(e7) = [2] x1 + [1] x2 + [1] x3 + [4]                           
                  p(e8) = [4] x2 + [1] x3 + [2]                                    
              p(equal0) = [0]                                                      
                 p(gcd) = [1] x1 + [1] x2 + [2]                                    
               p(help1) = [2] x1 + [5]                                             
                  p(l1) = [1] x1 + [1] x2 + [1] x3 + [5] x4 + [7] x5 + [1] x6 + [5]
                 p(l10) = [1] x1 + [1] x2 + [7] x4 + [1] x5 + [5]                  
                 p(l11) = [1] x1 + [1] x2 + [4] x4 + [1] x5 + [1] x6 + [5]         
                 p(l12) = [1] x1 + [1] x2 + [1] x4 + [1] x5 + [4] x6 + [5]         
                 p(l13) = [1] x2 + [1] x4 + [1] x5 + [4] x6 + [4]                  
                 p(l14) = [1] x1 + [1] x2 + [4] x4 + [5]                           
                 p(l15) = [1] x2 + [1] x4 + [1] x5 + [4]                           
                 p(l16) = [1] x3 + [1]                                             
                  p(l2) = [1] x1 + [1] x2 + [1] x3 + [4] x4 + [4] x5 + [5]         
                  p(l3) = [1] x1 + [1] x2 + [1] x4 + [3] x5 + [5]                  
                  p(l4) = [1] x1 + [1] x2 + [2] x3 + [1] x4 + [3] x5 + [5]         
                  p(l5) = [1] x1 + [1] x2 + [2] x3 + [1] x4 + [3] x5 + [5]         
                  p(l6) = [1] x2 + [4] x4 + [1] x5 + [4] x6 + [5]                  
                  p(l7) = [1] x1 + [1] x2 + [2] x3 + [2] x5 + [1] x6 + [5]         
                  p(l8) = [1] x1 + [1] x2 + [1] x4 + [2] x5 + [5]                  
                  p(l9) = [2] x1 + [2] x6 + [1]                                    
                  p(m1) = [1] x1 + [5] x3 + [0]                                    
                  p(m2) = [1] x1 + [2] x3 + [1] x4 + [0]                           
                  p(m3) = [1] x2 + [4] x3 + [7]                                    
                  p(m4) = [1] x1 + [1] x4 + [0]                                    
                  p(m5) = [1] x3 + [0]                                             
               p(monus) = [1] x1 + [1]                                             
          
          Following rules are strictly oriented:
          monus(a,b) = [1] a + [1]            
                     > [1] a + [0]            
                     = m1(a,b,False(),False())
          
          
          Following rules are (at-least) weakly oriented:
                               <(x,0()) =  [0]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                            <(0(),S(y)) =  [0]                                                       
                                        >= [0]                                                       
                                        =  True()                                                    
          
                           <(S(x),S(y)) =  [0]                                                       
                                        >= [0]                                                       
                                        =  <(x,y)                                                    
          
                      bool2Nat(False()) =  [1]                                                       
                                        >= [0]                                                       
                                        =  0()                                                       
          
                       bool2Nat(True()) =  [1]                                                       
                                        >= [1]                                                       
                                        =  S(0())                                                    
          
                          e1(a,b,res,t) =  [4] res + [2] t + [0]                                     
                                        >= [2] res + [0]                                             
                                        =  e2(a,b,res,<(a,b))                                        
          
                    e2(a,b,res,False()) =  [2] res + [0]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     e2(a,b,res,True()) =  [2] res + [0]                                             
                                        >= [1] res + [0]                                             
                                        =  e3(a,b,res,True())                                        
          
                          e3(a,b,res,t) =  [1] res + [0]                                             
                                        >= [0]                                                       
                                        =  e4(a,b,res,<(b,a))                                        
          
                    e4(a,b,res,False()) =  [0]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     e4(a,b,res,True()) =  [0]                                                       
                                        >= [0]                                                       
                                        =  True()                                                    
          
                          e5(a,b,res,t) =  [2] b + [1] res + [2] t + [0]                             
                                        >= [0]                                                       
                                        =  True()                                                    
          
                          e6(a,b,res,t) =  [1] a + [2] t + [0]                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          e7(a,b,res,t) =  [2] a + [1] b + [1] res + [4]                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          e8(a,b,res,t) =  [4] b + [1] res + [2]                                     
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                            equal0(a,b) =  [0]                                                       
                                        >= [0]                                                       
                                        =  e1(a,b,False(),False())                                   
          
                               gcd(x,y) =  [1] x + [1] y + [2]                                       
                                        >= [1] x + [1] y + [5]                                       
                                        =  l1(x,y,0(),False(),False(),False())                       
          
                             help1(0()) =  [5]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                          help1(S(0())) =  [7]                                                       
                                        >= [0]                                                       
                                        =  False()                                                   
          
                         help1(S(S(x))) =  [2] x + [9]                                               
                                        >= [0]                                                       
                                        =  True()                                                    
          
                 l1(x,y,res,tmp,mtmp,t) =  [7] mtmp + [1] res + [1] t + [5] tmp + [1] x + [1] y + [5]
                                        >= [4] mtmp + [1] res + [4] tmp + [1] x + [1] y + [5]        
                                        =  l2(x,y,res,tmp,mtmp,False())                              
          
                l10(x,y,res,tmp,mtmp,t) =  [1] mtmp + [7] tmp + [1] x + [1] y + [5]                  
                                        >= [1] mtmp + [4] tmp + [1] x + [1] y + [5]                  
                                        =  l11(x,y,res,tmp,mtmp,<(x,y))                              
          
          l11(x,y,res,tmp,mtmp,False()) =  [1] mtmp + [4] tmp + [1] x + [1] y + [5]                  
                                        >= [4] tmp + [1] x + [1] y + [5]                             
                                        =  l14(x,y,res,tmp,mtmp,False())                             
          
           l11(x,y,res,tmp,mtmp,True()) =  [1] mtmp + [4] tmp + [1] x + [1] y + [5]                  
                                        >= [1] mtmp + [1] tmp + [1] x + [1] y + [5]                  
                                        =  l12(x,y,res,tmp,mtmp,True())                              
          
                l12(x,y,res,tmp,mtmp,t) =  [1] mtmp + [4] t + [1] tmp + [1] x + [1] y + [5]          
                                        >= [4] t + [1] tmp + [1] x + [1] y + [5]                     
                                        =  l13(x,y,res,tmp,monus(x,y),t)                             
          
             l13(x,y,res,tmp,False(),t) =  [4] t + [1] tmp + [1] y + [4]                             
                                        >= [1] y + [3]                                               
                                        =  l16(x,y,gcd(0(),y),tmp,False(),t)                         
          
              l13(x,y,res,tmp,True(),t) =  [4] t + [1] tmp + [1] y + [4]                             
                                        >= [1] y + [4]                                               
                                        =  l16(x,y,gcd(S(0()),y),tmp,True(),t)                       
          
                l14(x,y,res,tmp,mtmp,t) =  [4] tmp + [1] x + [1] y + [5]                             
                                        >= [1] tmp + [1] x + [1] y + [5]                             
                                        =  l15(x,y,res,tmp,monus(x,y),t)                             
          
             l15(x,y,res,tmp,False(),t) =  [1] tmp + [1] y + [4]                                     
                                        >= [1] y + [3]                                               
                                        =  l16(x,y,gcd(y,0()),tmp,False(),t)                         
          
              l15(x,y,res,tmp,True(),t) =  [1] tmp + [1] y + [4]                                     
                                        >= [1] y + [4]                                               
                                        =  l16(x,y,gcd(y,S(0())),tmp,True(),t)                       
          
                l16(x,y,res,tmp,mtmp,t) =  [1] res + [1]                                             
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
           l2(x,y,res,tmp,mtmp,False()) =  [4] mtmp + [1] res + [4] tmp + [1] x + [1] y + [5]        
                                        >= [3] mtmp + [1] tmp + [1] x + [1] y + [5]                  
                                        =  l3(x,y,res,tmp,mtmp,False())                              
          
            l2(x,y,res,tmp,mtmp,True()) =  [4] mtmp + [1] res + [4] tmp + [1] x + [1] y + [5]        
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                 l3(x,y,res,tmp,mtmp,t) =  [3] mtmp + [1] tmp + [1] x + [1] y + [5]                  
                                        >= [3] mtmp + [1] tmp + [1] x + [1] y + [5]                  
                                        =  l4(x,y,0(),tmp,mtmp,t)                                    
          
                l4(x',x,res,tmp,mtmp,t) =  [3] mtmp + [2] res + [1] tmp + [1] x + [1] x' + [5]       
                                        >= [3] mtmp + [2] res + [1] tmp + [1] x + [1] x' + [5]       
                                        =  l5(x',x,res,tmp,mtmp,False())                             
          
           l5(x,y,res,tmp,mtmp,False()) =  [3] mtmp + [2] res + [1] tmp + [1] x + [1] y + [5]        
                                        >= [2] mtmp + [2] res + [1] x + [1] y + [5]                  
                                        =  l7(x,y,res,tmp,mtmp,False())                              
          
            l5(x,y,res,tmp,mtmp,True()) =  [3] mtmp + [2] res + [1] tmp + [1] x + [1] y + [5]        
                                        >= [0]                                                       
                                        =  0()                                                       
          
                 l6(x,y,res,tmp,mtmp,t) =  [1] mtmp + [4] t + [4] tmp + [1] y + [5]                  
                                        >= [0]                                                       
                                        =  0()                                                       
          
                 l7(x,y,res,tmp,mtmp,t) =  [2] mtmp + [2] res + [1] t + [1] x + [1] y + [5]          
                                        >= [2] mtmp + [1] x + [1] y + [5]                            
                                        =  l8(x,y,res,equal0(x,y),mtmp,t)                            
          
           l8(res,y,res',True(),mtmp,t) =  [2] mtmp + [1] res + [1] y + [5]                          
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
             l8(x,y,res,False(),mtmp,t) =  [2] mtmp + [1] x + [1] y + [5]                            
                                        >= [1] mtmp + [1] x + [1] y + [5]                            
                                        =  l10(x,y,res,False(),mtmp,t)                               
          
              l9(res,y,res',tmp,mtmp,t) =  [2] res + [2] t + [1]                                     
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
                          m1(a,x,res,t) =  [1] a + [5] res + [0]                                     
                                        >= [1] a + [2] res + [0]                                     
                                        =  m2(a,x,res,False())                                       
          
                    m2(a,b,res,False()) =  [1] a + [2] res + [0]                                     
                                        >= [1] a + [0]                                               
                                        =  m4(a,b,res,False())                                       
          
                   m2(0(),b,res,True()) =  [2] res + [0]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
                m2(S(0()),b,res,True()) =  [2] res + [1]                                             
                                        >= [0]                                                       
                                        =  False()                                                   
          
               m2(S(S(x)),b,res,True()) =  [2] res + [1] x + [2]                                     
                                        >= [0]                                                       
                                        =  True()                                                    
          
                        m3(0(),b,res,t) =  [1] b + [4] res + [7]                                     
                                        >= [0]                                                       
                                        =  False()                                                   
          
                     m3(S(0()),b,res,t) =  [1] b + [4] res + [7]                                     
                                        >= [0]                                                       
                                        =  False()                                                   
          
                    m3(S(S(x)),b,res,t) =  [1] b + [4] res + [7]                                     
                                        >= [0]                                                       
                                        =  True()                                                    
          
                   m4(S(x'),S(x),res,t) =  [1] t + [1] x' + [1]                                      
                                        >= [1] x' + [1]                                              
                                        =  m5(S(x'),S(x),monus(x',x),t)                              
          
                          m5(a,b,res,t) =  [1] res + [0]                                             
                                        >= [1] res + [0]                                             
                                        =  res                                                       
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 14: NaturalMI WORST_CASE(?,O(1))
    + Considered Problem:
        - Strict TRS:
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(e2) = {4},
          uargs(e4) = {4},
          uargs(l11) = {6},
          uargs(l13) = {5},
          uargs(l15) = {5},
          uargs(l16) = {3},
          uargs(l8) = {4},
          uargs(m5) = {3}
        
        Following symbols are considered usable:
          {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8
          ,l9,m1,m2,m3,m4,m5,monus}
        TcT has computed the following interpretation:
                 p(0) = [0]                                                                  
                        [0]                                                                  
                 p(<) = [1]                                                                  
                        [2]                                                                  
             p(False) = [0]                                                                  
                        [1]                                                                  
                 p(S) = [0]                                                                  
                        [0]                                                                  
              p(True) = [1]                                                                  
                        [0]                                                                  
          p(bool2Nat) = [0 1] x1 + [0]                                                       
                        [0 0]      [2]                                                       
                p(e1) = [0 0] x2 + [2 0] x3 + [1]                                            
                        [0 3]      [3 0]      [2]                                            
                p(e2) = [0 0] x2 + [0 0] x3 + [1 0] x4 + [0]                                 
                        [0 3]      [2 0]      [0 0]      [2]                                 
                p(e3) = [0 0] x2 + [0 0] x4 + [1]                                            
                        [0 1]      [0 1]      [2]                                            
                p(e4) = [1 0] x4 + [0]                                                       
                        [0 0]      [2]                                                       
                p(e5) = [2 1] x2 + [2 2] x3 + [2]                                            
                        [0 0]      [2 0]      [0]                                            
                p(e6) = [0 0] x1 + [0 0] x3 + [2]                                            
                        [0 2]      [2 1]      [2]                                            
                p(e7) = [0 2] x3 + [0]                                                       
                        [1 0]      [2]                                                       
                p(e8) = [1 0] x3 + [1]                                                       
                        [2 1]      [0]                                                       
            p(equal0) = [0 0] x1 + [0 0] x2 + [1]                                            
                        [1 2]      [0 3]      [2]                                            
               p(gcd) = [2 0] x1 + [2 0] x2 + [3]                                            
                        [0 1]      [0 1]      [2]                                            
             p(help1) = [2 2] x1 + [3]                                                       
                        [0 0]      [2]                                                       
                p(l1) = [1 0] x1 + [2 0] x2 + [1 2] x3 + [3 0] x4 + [0 0] x5 + [2 0] x6 + [2]
                        [0 1]      [0 1]      [1 2]      [2 0]      [3 0]      [1 0]      [2]
               p(l10) = [1 0] x1 + [2 0] x2 + [1]                                            
                        [0 0]      [0 1]      [0]                                            
               p(l11) = [1 0] x1 + [2 0] x2 + [1 0] x6 + [0]                                 
                        [0 0]      [0 1]      [0 0]      [0]                                 
               p(l12) = [1 0] x1 + [2 0] x2 + [0 2] x6 + [1]                                 
                        [0 0]      [0 1]      [0 0]      [0]                                 
               p(l13) = [2 0] x2 + [2 2] x5 + [1]                                            
                        [0 1]      [2 2]      [0]                                            
               p(l14) = [1 0] x1 + [2 0] x2 + [2 0] x6 + [0]                                 
                        [0 0]      [0 1]      [2 0]      [0]                                 
               p(l15) = [2 0] x2 + [3 3] x5 + [1 0] x6 + [0]                                 
                        [0 1]      [2 2]      [2 0]      [0]                                 
               p(l16) = [1 0] x3 + [0]                                                       
                        [0 1]      [0]                                                       
                p(l2) = [1 0] x1 + [2 0] x2 + [1 1] x3 + [2 0] x4 + [0 0] x5 + [0 2] x6 + [0]
                        [0 1]      [0 1]      [0 1]      [0 0]      [3 0]      [0 0]      [2]
                p(l3) = [1 0] x1 + [2 0] x2 + [1 0] x3 + [1 0] x4 + [0 0] x5 + [0 0] x6 + [2]
                        [0 1]      [0 1]      [0 0]      [0 0]      [3 0]      [2 0]      [2]
                p(l4) = [1 0] x1 + [2 0] x2 + [0 0] x3 + [0 0] x5 + [2]                      
                        [0 1]      [0 1]      [0 2]      [3 0]      [2]                      
                p(l5) = [1 0] x1 + [2 0] x2 + [0 0] x3 + [0 0] x5 + [0 1] x6 + [1]           
                        [0 1]      [0 1]      [0 2]      [3 0]      [0 2]      [0]           
                p(l6) = [0 0] x3 + [0 2] x4 + [1 0] x5 + [0 0] x6 + [1]                      
                        [1 0]      [0 1]      [0 0]      [0 1]      [0]                      
                p(l7) = [1 0] x1 + [2 0] x2 + [0 0] x5 + [3 0] x6 + [2]                      
                        [0 1]      [0 1]      [2 0]      [2 0]      [2]                      
                p(l8) = [1 0] x1 + [2 0] x2 + [1 0] x4 + [2 0] x6 + [1]                      
                        [0 1]      [0 1]      [2 0]      [1 0]      [0]                      
                p(l9) = [2 0] x1 + [0 2] x4 + [0 0] x5 + [0 0] x6 + [0]                      
                        [0 2]      [0 2]      [0 1]      [2 2]      [0]                      
                p(m1) = [0]                                                                  
                        [0]                                                                  
                p(m2) = [1 0] x4 + [0]                                                       
                        [1 0]      [0]                                                       
                p(m3) = [2 1] x1 + [1 0] x2 + [2 0] x3 + [1]                                 
                        [0 0]      [1 2]      [0 0]      [1]                                 
                p(m4) = [1 0] x4 + [0]                                                       
                        [2 0]      [0]                                                       
                p(m5) = [0 2] x1 + [0 0] x2 + [2 0] x3 + [0]                                 
                        [0 1]      [0 2]      [0 2]      [0]                                 
             p(monus) = [0]                                                                  
                        [0]                                                                  
        
        Following rules are strictly oriented:
        gcd(x,y) = [2 0] x + [2 0] y + [3]            
                   [0 1]     [0 1]     [2]            
                 > [1 0] x + [2 0] y + [2]            
                   [0 1]     [0 1]     [2]            
                 = l1(x,y,0(),False(),False(),False())
        
        
        Following rules are (at-least) weakly oriented:
                             <(x,0()) =  [1]                                                                   
                                         [2]                                                                   
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                          <(0(),S(y)) =  [1]                                                                   
                                         [2]                                                                   
                                      >= [1]                                                                   
                                         [0]                                                                   
                                      =  True()                                                                
        
                         <(S(x),S(y)) =  [1]                                                                   
                                         [2]                                                                   
                                      >= [1]                                                                   
                                         [2]                                                                   
                                      =  <(x,y)                                                                
        
                    bool2Nat(False()) =  [1]                                                                   
                                         [2]                                                                   
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  0()                                                                   
        
                     bool2Nat(True()) =  [0]                                                                   
                                         [2]                                                                   
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  S(0())                                                                
        
                        e1(a,b,res,t) =  [0 0] b + [2 0] res + [1]                                             
                                         [0 3]     [3 0]       [2]                                             
                                      >= [0 0] b + [0 0] res + [1]                                             
                                         [0 3]     [2 0]       [2]                                             
                                      =  e2(a,b,res,<(a,b))                                                    
        
                  e2(a,b,res,False()) =  [0 0] b + [0 0] res + [0]                                             
                                         [0 3]     [2 0]       [2]                                             
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                   e2(a,b,res,True()) =  [0 0] b + [0 0] res + [1]                                             
                                         [0 3]     [2 0]       [2]                                             
                                      >= [0 0] b + [1]                                                         
                                         [0 1]     [2]                                                         
                                      =  e3(a,b,res,True())                                                    
        
                        e3(a,b,res,t) =  [0 0] b + [0 0] t + [1]                                               
                                         [0 1]     [0 1]     [2]                                               
                                      >= [1]                                                                   
                                         [2]                                                                   
                                      =  e4(a,b,res,<(b,a))                                                    
        
                  e4(a,b,res,False()) =  [0]                                                                   
                                         [2]                                                                   
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                   e4(a,b,res,True()) =  [1]                                                                   
                                         [2]                                                                   
                                      >= [1]                                                                   
                                         [0]                                                                   
                                      =  True()                                                                
        
                        e5(a,b,res,t) =  [2 1] b + [2 2] res + [2]                                             
                                         [0 0]     [2 0]       [0]                                             
                                      >= [1]                                                                   
                                         [0]                                                                   
                                      =  True()                                                                
        
                        e6(a,b,res,t) =  [0 0] a + [0 0] res + [2]                                             
                                         [0 2]     [2 1]       [2]                                             
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                        e7(a,b,res,t) =  [0 2] res + [0]                                                       
                                         [1 0]       [2]                                                       
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                        e8(a,b,res,t) =  [1 0] res + [1]                                                       
                                         [2 1]       [0]                                                       
                                      >= [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      =  res                                                                   
        
                          equal0(a,b) =  [0 0] a + [0 0] b + [1]                                               
                                         [1 2]     [0 3]     [2]                                               
                                      >= [0 0] b + [1]                                                         
                                         [0 3]     [2]                                                         
                                      =  e1(a,b,False(),False())                                               
        
                           help1(0()) =  [3]                                                                   
                                         [2]                                                                   
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                        help1(S(0())) =  [3]                                                                   
                                         [2]                                                                   
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                       help1(S(S(x))) =  [3]                                                                   
                                         [2]                                                                   
                                      >= [1]                                                                   
                                         [0]                                                                   
                                      =  True()                                                                
        
               l1(x,y,res,tmp,mtmp,t) =  [0 0] mtmp + [1 2] res + [2 0] t + [3 0] tmp + [1 0] x + [2 0] y + [2]
                                         [3 0]        [1 2]       [1 0]     [2 0]       [0 1]     [0 1]     [2]
                                      >= [0 0] mtmp + [1 1] res + [2 0] tmp + [1 0] x + [2 0] y + [2]          
                                         [3 0]        [0 1]       [0 0]       [0 1]     [0 1]     [2]          
                                      =  l2(x,y,res,tmp,mtmp,False())                                          
        
              l10(x,y,res,tmp,mtmp,t) =  [1 0] x + [2 0] y + [1]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      >= [1 0] x + [2 0] y + [1]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      =  l11(x,y,res,tmp,mtmp,<(x,y))                                          
        
        l11(x,y,res,tmp,mtmp,False()) =  [1 0] x + [2 0] y + [0]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      >= [1 0] x + [2 0] y + [0]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      =  l14(x,y,res,tmp,mtmp,False())                                         
        
         l11(x,y,res,tmp,mtmp,True()) =  [1 0] x + [2 0] y + [1]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      >= [1 0] x + [2 0] y + [1]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      =  l12(x,y,res,tmp,mtmp,True())                                          
        
              l12(x,y,res,tmp,mtmp,t) =  [0 2] t + [1 0] x + [2 0] y + [1]                                     
                                         [0 0]     [0 0]     [0 1]     [0]                                     
                                      >= [2 0] y + [1]                                                         
                                         [0 1]     [0]                                                         
                                      =  l13(x,y,res,tmp,monus(x,y),t)                                         
        
           l13(x,y,res,tmp,False(),t) =  [2 0] y + [3]                                                         
                                         [0 1]     [2]                                                         
                                      >= [2 0] y + [3]                                                         
                                         [0 1]     [2]                                                         
                                      =  l16(x,y,gcd(0(),y),tmp,False(),t)                                     
        
            l13(x,y,res,tmp,True(),t) =  [2 0] y + [3]                                                         
                                         [0 1]     [2]                                                         
                                      >= [2 0] y + [3]                                                         
                                         [0 1]     [2]                                                         
                                      =  l16(x,y,gcd(S(0()),y),tmp,True(),t)                                   
        
              l14(x,y,res,tmp,mtmp,t) =  [2 0] t + [1 0] x + [2 0] y + [0]                                     
                                         [2 0]     [0 0]     [0 1]     [0]                                     
                                      >= [1 0] t + [2 0] y + [0]                                               
                                         [2 0]     [0 1]     [0]                                               
                                      =  l15(x,y,res,tmp,monus(x,y),t)                                         
        
           l15(x,y,res,tmp,False(),t) =  [1 0] t + [2 0] y + [3]                                               
                                         [2 0]     [0 1]     [2]                                               
                                      >= [2 0] y + [3]                                                         
                                         [0 1]     [2]                                                         
                                      =  l16(x,y,gcd(y,0()),tmp,False(),t)                                     
        
            l15(x,y,res,tmp,True(),t) =  [1 0] t + [2 0] y + [3]                                               
                                         [2 0]     [0 1]     [2]                                               
                                      >= [2 0] y + [3]                                                         
                                         [0 1]     [2]                                                         
                                      =  l16(x,y,gcd(y,S(0())),tmp,True(),t)                                   
        
              l16(x,y,res,tmp,mtmp,t) =  [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      >= [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      =  res                                                                   
        
         l2(x,y,res,tmp,mtmp,False()) =  [0 0] mtmp + [1 1] res + [2 0] tmp + [1 0] x + [2 0] y + [2]          
                                         [3 0]        [0 1]       [0 0]       [0 1]     [0 1]     [2]          
                                      >= [0 0] mtmp + [1 0] res + [1 0] tmp + [1 0] x + [2 0] y + [2]          
                                         [3 0]        [0 0]       [0 0]       [0 1]     [0 1]     [2]          
                                      =  l3(x,y,res,tmp,mtmp,False())                                          
        
          l2(x,y,res,tmp,mtmp,True()) =  [0 0] mtmp + [1 1] res + [2 0] tmp + [1 0] x + [2 0] y + [0]          
                                         [3 0]        [0 1]       [0 0]       [0 1]     [0 1]     [2]          
                                      >= [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      =  res                                                                   
        
               l3(x,y,res,tmp,mtmp,t) =  [0 0] mtmp + [1 0] res + [0 0] t + [1 0] tmp + [1 0] x + [2 0] y + [2]
                                         [3 0]        [0 0]       [2 0]     [0 0]       [0 1]     [0 1]     [2]
                                      >= [0 0] mtmp + [1 0] x + [2 0] y + [2]                                  
                                         [3 0]        [0 1]     [0 1]     [2]                                  
                                      =  l4(x,y,0(),tmp,mtmp,t)                                                
        
              l4(x',x,res,tmp,mtmp,t) =  [0 0] mtmp + [0 0] res + [2 0] x + [1 0] x' + [2]                     
                                         [3 0]        [0 2]       [0 1]     [0 1]      [2]                     
                                      >= [0 0] mtmp + [0 0] res + [2 0] x + [1 0] x' + [2]                     
                                         [3 0]        [0 2]       [0 1]     [0 1]      [2]                     
                                      =  l5(x',x,res,tmp,mtmp,False())                                         
        
         l5(x,y,res,tmp,mtmp,False()) =  [0 0] mtmp + [0 0] res + [1 0] x + [2 0] y + [2]                      
                                         [3 0]        [0 2]       [0 1]     [0 1]     [2]                      
                                      >= [0 0] mtmp + [1 0] x + [2 0] y + [2]                                  
                                         [2 0]        [0 1]     [0 1]     [2]                                  
                                      =  l7(x,y,res,tmp,mtmp,False())                                          
        
          l5(x,y,res,tmp,mtmp,True()) =  [0 0] mtmp + [0 0] res + [1 0] x + [2 0] y + [1]                      
                                         [3 0]        [0 2]       [0 1]     [0 1]     [0]                      
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  0()                                                                   
        
               l6(x,y,res,tmp,mtmp,t) =  [1 0] mtmp + [0 0] res + [0 0] t + [0 2] tmp + [1]                    
                                         [0 0]        [1 0]       [0 1]     [0 1]       [0]                    
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  0()                                                                   
        
               l7(x,y,res,tmp,mtmp,t) =  [0 0] mtmp + [3 0] t + [1 0] x + [2 0] y + [2]                        
                                         [2 0]        [2 0]     [0 1]     [0 1]     [2]                        
                                      >= [2 0] t + [1 0] x + [2 0] y + [2]                                     
                                         [1 0]     [0 1]     [0 1]     [2]                                     
                                      =  l8(x,y,res,equal0(x,y),mtmp,t)                                        
        
         l8(res,y,res',True(),mtmp,t) =  [1 0] res + [2 0] t + [2 0] y + [2]                                   
                                         [0 1]       [1 0]     [0 1]     [2]                                   
                                      >= [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      =  res                                                                   
        
           l8(x,y,res,False(),mtmp,t) =  [2 0] t + [1 0] x + [2 0] y + [1]                                     
                                         [1 0]     [0 1]     [0 1]     [0]                                     
                                      >= [1 0] x + [2 0] y + [1]                                               
                                         [0 0]     [0 1]     [0]                                               
                                      =  l10(x,y,res,False(),mtmp,t)                                           
        
            l9(res,y,res',tmp,mtmp,t) =  [0 0] mtmp + [2 0] res + [0 0] t + [0 2] tmp + [0]                    
                                         [0 1]        [0 2]       [2 2]     [0 2]       [0]                    
                                      >= [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      =  res                                                                   
        
                        m1(a,x,res,t) =  [0]                                                                   
                                         [0]                                                                   
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  m2(a,x,res,False())                                                   
        
                  m2(a,b,res,False()) =  [0]                                                                   
                                         [0]                                                                   
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  m4(a,b,res,False())                                                   
        
                 m2(0(),b,res,True()) =  [1]                                                                   
                                         [1]                                                                   
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
              m2(S(0()),b,res,True()) =  [1]                                                                   
                                         [1]                                                                   
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
             m2(S(S(x)),b,res,True()) =  [1]                                                                   
                                         [1]                                                                   
                                      >= [1]                                                                   
                                         [0]                                                                   
                                      =  True()                                                                
        
                      m3(0(),b,res,t) =  [1 0] b + [2 0] res + [1]                                             
                                         [1 2]     [0 0]       [1]                                             
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                   m3(S(0()),b,res,t) =  [1 0] b + [2 0] res + [1]                                             
                                         [1 2]     [0 0]       [1]                                             
                                      >= [0]                                                                   
                                         [1]                                                                   
                                      =  False()                                                               
        
                  m3(S(S(x)),b,res,t) =  [1 0] b + [2 0] res + [1]                                             
                                         [1 2]     [0 0]       [1]                                             
                                      >= [1]                                                                   
                                         [0]                                                                   
                                      =  True()                                                                
        
                 m4(S(x'),S(x),res,t) =  [1 0] t + [0]                                                         
                                         [2 0]     [0]                                                         
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  m5(S(x'),S(x),monus(x',x),t)                                          
        
                        m5(a,b,res,t) =  [0 2] a + [0 0] b + [2 0] res + [0]                                   
                                         [0 1]     [0 2]     [0 2]       [0]                                   
                                      >= [1 0] res + [0]                                                       
                                         [0 1]       [0]                                                       
                                      =  res                                                                   
        
                           monus(a,b) =  [0]                                                                   
                                         [0]                                                                   
                                      >= [0]                                                                   
                                         [0]                                                                   
                                      =  m1(a,b,False(),False())                                               
        
* Step 15: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            <(x,0()) -> False()
            <(0(),S(y)) -> True()
            <(S(x),S(y)) -> <(x,y)
            bool2Nat(False()) -> 0()
            bool2Nat(True()) -> S(0())
            e1(a,b,res,t) -> e2(a,b,res,<(a,b))
            e2(a,b,res,False()) -> False()
            e2(a,b,res,True()) -> e3(a,b,res,True())
            e3(a,b,res,t) -> e4(a,b,res,<(b,a))
            e4(a,b,res,False()) -> False()
            e4(a,b,res,True()) -> True()
            e5(a,b,res,t) -> True()
            e6(a,b,res,t) -> False()
            e7(a,b,res,t) -> False()
            e8(a,b,res,t) -> res
            equal0(a,b) -> e1(a,b,False(),False())
            gcd(x,y) -> l1(x,y,0(),False(),False(),False())
            help1(0()) -> False()
            help1(S(0())) -> False()
            help1(S(S(x))) -> True()
            l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
            l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
            l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
            l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
            l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
            l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
            l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
            l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
            l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
            l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
            l16(x,y,res,tmp,mtmp,t) -> res
            l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
            l2(x,y,res,tmp,mtmp,True()) -> res
            l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
            l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
            l5(x,y,res,tmp,mtmp,True()) -> 0()
            l6(x,y,res,tmp,mtmp,t) -> 0()
            l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
            l8(res,y,res',True(),mtmp,t) -> res
            l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
            l9(res,y,res',tmp,mtmp,t) -> res
            m1(a,x,res,t) -> m2(a,x,res,False())
            m2(a,b,res,False()) -> m4(a,b,res,False())
            m2(0(),b,res,True()) -> False()
            m2(S(0()),b,res,True()) -> False()
            m2(S(S(x)),b,res,True()) -> True()
            m3(0(),b,res,t) -> False()
            m3(S(0()),b,res,t) -> False()
            m3(S(S(x)),b,res,t) -> True()
            m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
            m5(a,b,res,t) -> res
            monus(a,b) -> m1(a,b,False(),False())
        - Signature:
            {</2,bool2Nat/1,e1/4,e2/4,e3/4,e4/4,e5/4,e6/4,e7/4,e8/4,equal0/2,gcd/2,help1/1,l1/6,l10/6,l11/6,l12/6,l13/6
            ,l14/6,l15/6,l16/6,l2/6,l3/6,l4/6,l5/6,l6/6,l7/6,l8/6,l9/6,m1/4,m2/4,m3/4,m4/4,m5/4,monus/2} / {0/0,False/0
            ,S/1,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {<,bool2Nat,e1,e2,e3,e4,e5,e6,e7,e8,equal0,gcd,help1,l1
            ,l10,l11,l12,l13,l14,l15,l16,l2,l3,l4,l5,l6,l7,l8,l9,m1,m2,m3,m4,m5,monus} and constructors {0,False,S,True}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))