YES(O(1),O(n^2))
11.79/3.27	YES(O(1),O(n^2))
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^2)).
11.79/3.27	
11.79/3.27	Strict Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y)
11.79/3.27	  , gcd(0(), y) -> y
11.79/3.27	  , gcd(s(x), 0()) -> s(x)
11.79/3.27	  , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
11.79/3.27	  , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
11.79/3.27	  , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^2))
11.79/3.27	
11.79/3.27	We add the following weak dependency pairs:
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { le^#(0(), y) -> c_1()
11.79/3.27	  , le^#(s(x), 0()) -> c_2()
11.79/3.27	  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(x, 0()) -> c_4()
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	  , gcd^#(0(), y) -> c_6()
11.79/3.27	  , gcd^#(s(x), 0()) -> c_7()
11.79/3.27	  , gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	
11.79/3.27	and mark the set of starting terms.
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^2)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { le^#(0(), y) -> c_1()
11.79/3.27	  , le^#(s(x), 0()) -> c_2()
11.79/3.27	  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(x, 0()) -> c_4()
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	  , gcd^#(0(), y) -> c_6()
11.79/3.27	  , gcd^#(s(x), 0()) -> c_7()
11.79/3.27	  , gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Strict Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y)
11.79/3.27	  , gcd(0(), y) -> y
11.79/3.27	  , gcd(s(x), 0()) -> s(x)
11.79/3.27	  , gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
11.79/3.27	  , if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
11.79/3.27	  , if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^2))
11.79/3.27	
11.79/3.27	We replace rewrite rules by usable rules:
11.79/3.27	
11.79/3.27	  Strict Usable Rules:
11.79/3.27	    { le(0(), y) -> true()
11.79/3.27	    , le(s(x), 0()) -> false()
11.79/3.27	    , le(s(x), s(y)) -> le(x, y)
11.79/3.27	    , minus(x, 0()) -> x
11.79/3.27	    , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^2)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { le^#(0(), y) -> c_1()
11.79/3.27	  , le^#(s(x), 0()) -> c_2()
11.79/3.27	  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(x, 0()) -> c_4()
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	  , gcd^#(0(), y) -> c_6()
11.79/3.27	  , gcd^#(s(x), 0()) -> c_7()
11.79/3.27	  , gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Strict Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^2))
11.79/3.27	
11.79/3.27	The weightgap principle applies (using the following constant
11.79/3.27	growth matrix-interpretation)
11.79/3.27	
11.79/3.27	The following argument positions are usable:
11.79/3.27	  Uargs(c_3) = {1}, Uargs(c_5) = {1}, Uargs(gcd^#) = {1},
11.79/3.27	  Uargs(c_8) = {1}, Uargs(if_gcd^#) = {1}, Uargs(c_9) = {1},
11.79/3.27	  Uargs(c_10) = {1}
11.79/3.27	
11.79/3.27	TcT has computed the following constructor-restricted matrix
11.79/3.27	interpretation.
11.79/3.27	
11.79/3.27	            [le](x1, x2) = [0 1] x2 + [2]                      
11.79/3.27	                           [0 0]      [2]                      
11.79/3.27	                                                               
11.79/3.27	                     [0] = [2]                                 
11.79/3.27	                           [2]                                 
11.79/3.27	                                                               
11.79/3.27	                  [true] = [0]                                 
11.79/3.27	                           [2]                                 
11.79/3.27	                                                               
11.79/3.27	                 [s](x1) = [1 1] x1 + [1]                      
11.79/3.27	                           [0 1]      [1]                      
11.79/3.27	                                                               
11.79/3.27	                 [false] = [0]                                 
11.79/3.27	                           [0]                                 
11.79/3.27	                                                               
11.79/3.27	         [minus](x1, x2) = [1 0] x1 + [1]                      
11.79/3.27	                           [0 1]      [0]                      
11.79/3.27	                                                               
11.79/3.27	          [le^#](x1, x2) = [0]                                 
11.79/3.27	                           [0]                                 
11.79/3.27	                                                               
11.79/3.27	                   [c_1] = [1]                                 
11.79/3.27	                           [1]                                 
11.79/3.27	                                                               
11.79/3.27	                   [c_2] = [2]                                 
11.79/3.27	                           [1]                                 
11.79/3.27	                                                               
11.79/3.27	               [c_3](x1) = [1 0] x1 + [2]                      
11.79/3.27	                           [0 1]      [2]                      
11.79/3.27	                                                               
11.79/3.27	       [minus^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]           
11.79/3.27	                           [2 1]      [1 2]      [1]           
11.79/3.27	                                                               
11.79/3.27	                   [c_4] = [1]                                 
11.79/3.27	                           [1]                                 
11.79/3.27	                                                               
11.79/3.27	               [c_5](x1) = [1 0] x1 + [1]                      
11.79/3.27	                           [0 1]      [1]                      
11.79/3.27	                                                               
11.79/3.27	         [gcd^#](x1, x2) = [1 1] x1 + [1 0] x2 + [0]           
11.79/3.27	                           [0 0]      [0 0]      [0]           
11.79/3.27	                                                               
11.79/3.27	                   [c_6] = [1]                                 
11.79/3.27	                           [1]                                 
11.79/3.27	                                                               
11.79/3.27	                   [c_7] = [1]                                 
11.79/3.27	                           [1]                                 
11.79/3.27	                                                               
11.79/3.27	               [c_8](x1) = [1 0] x1 + [1]                      
11.79/3.27	                           [0 1]      [2]                      
11.79/3.27	                                                               
11.79/3.27	  [if_gcd^#](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [1 0] x3 + [0]
11.79/3.27	                           [0 0]      [0 0]      [0 0]      [0]
11.79/3.27	                                                               
11.79/3.27	               [c_9](x1) = [1 0] x1 + [2]                      
11.79/3.27	                           [0 1]      [2]                      
11.79/3.27	                                                               
11.79/3.27	              [c_10](x1) = [1 0] x1 + [2]                      
11.79/3.27	                           [0 1]      [2]                      
11.79/3.27	
11.79/3.27	The order satisfies the following ordering constraints:
11.79/3.27	
11.79/3.27	                     [le(0(), y)] = [0 1] y + [2]                        
11.79/3.27	                                    [0 0]     [2]                        
11.79/3.27	                                  > [0]                                  
11.79/3.27	                                    [2]                                  
11.79/3.27	                                  = [true()]                             
11.79/3.27	                                                                         
11.79/3.27	                  [le(s(x), 0())] = [4]                                  
11.79/3.27	                                    [2]                                  
11.79/3.27	                                  > [0]                                  
11.79/3.27	                                    [0]                                  
11.79/3.27	                                  = [false()]                            
11.79/3.27	                                                                         
11.79/3.27	                 [le(s(x), s(y))] = [0 1] y + [3]                        
11.79/3.27	                                    [0 0]     [2]                        
11.79/3.27	                                  > [0 1] y + [2]                        
11.79/3.27	                                    [0 0]     [2]                        
11.79/3.27	                                  = [le(x, y)]                           
11.79/3.27	                                                                         
11.79/3.27	                  [minus(x, 0())] = [1 0] x + [1]                        
11.79/3.27	                                    [0 1]     [0]                        
11.79/3.27	                                  > [1 0] x + [0]                        
11.79/3.27	                                    [0 1]     [0]                        
11.79/3.27	                                  = [x]                                  
11.79/3.27	                                                                         
11.79/3.27	              [minus(s(x), s(y))] = [1 1] x + [2]                        
11.79/3.27	                                    [0 1]     [1]                        
11.79/3.27	                                  > [1 0] x + [1]                        
11.79/3.27	                                    [0 1]     [0]                        
11.79/3.27	                                  = [minus(x, y)]                        
11.79/3.27	                                                                         
11.79/3.27	                   [le^#(0(), y)] = [0]                                  
11.79/3.27	                                    [0]                                  
11.79/3.27	                                  ? [1]                                  
11.79/3.27	                                    [1]                                  
11.79/3.27	                                  = [c_1()]                              
11.79/3.27	                                                                         
11.79/3.27	                [le^#(s(x), 0())] = [0]                                  
11.79/3.27	                                    [0]                                  
11.79/3.27	                                  ? [2]                                  
11.79/3.27	                                    [1]                                  
11.79/3.27	                                  = [c_2()]                              
11.79/3.27	                                                                         
11.79/3.27	               [le^#(s(x), s(y))] = [0]                                  
11.79/3.27	                                    [0]                                  
11.79/3.27	                                  ? [2]                                  
11.79/3.27	                                    [2]                                  
11.79/3.27	                                  = [c_3(le^#(x, y))]                    
11.79/3.27	                                                                         
11.79/3.27	                [minus^#(x, 0())] = [0 0] x + [2]                        
11.79/3.27	                                    [2 1]     [7]                        
11.79/3.27	                                  > [1]                                  
11.79/3.27	                                    [1]                                  
11.79/3.27	                                  = [c_4()]                              
11.79/3.27	                                                                         
11.79/3.27	            [minus^#(s(x), s(y))] = [0 0] y + [0 0] x + [2]              
11.79/3.27	                                    [1 3]     [2 3]     [7]              
11.79/3.27	                                  ? [0 0] y + [0 0] x + [3]              
11.79/3.27	                                    [1 2]     [2 1]     [2]              
11.79/3.27	                                  = [c_5(minus^#(x, y))]                 
11.79/3.27	                                                                         
11.79/3.27	                  [gcd^#(0(), y)] = [1 0] y + [4]                        
11.79/3.27	                                    [0 0]     [0]                        
11.79/3.27	                                  ? [1]                                  
11.79/3.27	                                    [1]                                  
11.79/3.27	                                  = [c_6()]                              
11.79/3.27	                                                                         
11.79/3.27	               [gcd^#(s(x), 0())] = [1 2] x + [4]                        
11.79/3.27	                                    [0 0]     [0]                        
11.79/3.27	                                  ? [1]                                  
11.79/3.27	                                    [1]                                  
11.79/3.27	                                  = [c_7()]                              
11.79/3.27	                                                                         
11.79/3.27	              [gcd^#(s(x), s(y))] = [1 1] y + [1 2] x + [3]              
11.79/3.27	                                    [0 0]     [0 0]     [0]              
11.79/3.27	                                  ? [1 1] y + [1 2] x + [7]              
11.79/3.27	                                    [0 0]     [0 0]     [2]              
11.79/3.27	                                  = [c_8(if_gcd^#(le(y, x), s(x), s(y)))]
11.79/3.27	                                                                         
11.79/3.27	   [if_gcd^#(true(), s(x), s(y))] = [1 1] y + [1 1] x + [4]              
11.79/3.27	                                    [0 0]     [0 0]     [0]              
11.79/3.27	                                  ? [1 1] y + [1 1] x + [4]              
11.79/3.27	                                    [0 0]     [0 0]     [2]              
11.79/3.27	                                  = [c_9(gcd^#(minus(x, y), s(y)))]      
11.79/3.27	                                                                         
11.79/3.27	  [if_gcd^#(false(), s(x), s(y))] = [1 1] y + [1 1] x + [2]              
11.79/3.27	                                    [0 0]     [0 0]     [0]              
11.79/3.27	                                  ? [1 1] y + [1 1] x + [4]              
11.79/3.27	                                    [0 0]     [0 0]     [2]              
11.79/3.27	                                  = [c_10(gcd^#(minus(y, x), s(x)))]     
11.79/3.27	                                                                         
11.79/3.27	
11.79/3.27	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^1)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { le^#(0(), y) -> c_1()
11.79/3.27	  , le^#(s(x), 0()) -> c_2()
11.79/3.27	  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	  , gcd^#(0(), y) -> c_6()
11.79/3.27	  , gcd^#(s(x), 0()) -> c_7()
11.79/3.27	  , gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Weak DPs: { minus^#(x, 0()) -> c_4() }
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^1))
11.79/3.27	
11.79/3.27	We estimate the number of application of {1,2,5,6} by applications
11.79/3.27	of Pre({1,2,5,6}) = {3,8,9}. Here rules are labeled as follows:
11.79/3.27	
11.79/3.27	  DPs:
11.79/3.27	    { 1: le^#(0(), y) -> c_1()
11.79/3.27	    , 2: le^#(s(x), 0()) -> c_2()
11.79/3.27	    , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	    , 4: minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	    , 5: gcd^#(0(), y) -> c_6()
11.79/3.27	    , 6: gcd^#(s(x), 0()) -> c_7()
11.79/3.27	    , 7: gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	    , 8: if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	    , 9: if_gcd^#(false(), s(x), s(y)) ->
11.79/3.27	         c_10(gcd^#(minus(y, x), s(x)))
11.79/3.27	    , 10: minus^#(x, 0()) -> c_4() }
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^1)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	  , gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Weak DPs:
11.79/3.27	  { le^#(0(), y) -> c_1()
11.79/3.27	  , le^#(s(x), 0()) -> c_2()
11.79/3.27	  , minus^#(x, 0()) -> c_4()
11.79/3.27	  , gcd^#(0(), y) -> c_6()
11.79/3.27	  , gcd^#(s(x), 0()) -> c_7() }
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^1))
11.79/3.27	
11.79/3.27	The following weak DPs constitute a sub-graph of the DG that is
11.79/3.27	closed under successors. The DPs are removed.
11.79/3.27	
11.79/3.27	{ le^#(0(), y) -> c_1()
11.79/3.27	, le^#(s(x), 0()) -> c_2()
11.79/3.27	, minus^#(x, 0()) -> c_4()
11.79/3.27	, gcd^#(0(), y) -> c_6()
11.79/3.27	, gcd^#(s(x), 0()) -> c_7() }
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^1)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y))
11.79/3.27	  , gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^1))
11.79/3.27	
11.79/3.27	We use the processor 'matrix interpretation of dimension 1' to
11.79/3.27	orient following rules strictly.
11.79/3.27	
11.79/3.27	DPs:
11.79/3.27	  { 1: le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , 2: minus^#(s(x), s(y)) -> c_5(minus^#(x, y)) }
11.79/3.27	
11.79/3.27	Sub-proof:
11.79/3.27	----------
11.79/3.27	  The following argument positions are usable:
11.79/3.27	    Uargs(c_3) = {1}, Uargs(c_5) = {1}, Uargs(c_8) = {1},
11.79/3.27	    Uargs(c_9) = {1}, Uargs(c_10) = {1}
11.79/3.27	  
11.79/3.27	  TcT has computed the following constructor-based matrix
11.79/3.27	  interpretation satisfying not(EDA).
11.79/3.27	  
11.79/3.27	              [le](x1, x2) = [0]         
11.79/3.27	                                         
11.79/3.27	                       [0] = [0]         
11.79/3.27	                                         
11.79/3.27	                    [true] = [0]         
11.79/3.27	                                         
11.79/3.27	                   [s](x1) = [1] x1 + [2]
11.79/3.27	                                         
11.79/3.27	                   [false] = [0]         
11.79/3.27	                                         
11.79/3.27	           [minus](x1, x2) = [0]         
11.79/3.27	                                         
11.79/3.27	            [le^#](x1, x2) = [4] x1 + [0]
11.79/3.27	                                         
11.79/3.27	                 [c_3](x1) = [1] x1 + [1]
11.79/3.27	                                         
11.79/3.27	         [minus^#](x1, x2) = [4] x1 + [0]
11.79/3.27	                                         
11.79/3.27	                 [c_5](x1) = [1] x1 + [3]
11.79/3.27	                                         
11.79/3.27	           [gcd^#](x1, x2) = [0]         
11.79/3.27	                                         
11.79/3.27	                 [c_8](x1) = [2] x1 + [0]
11.79/3.27	                                         
11.79/3.27	    [if_gcd^#](x1, x2, x3) = [0]         
11.79/3.27	                                         
11.79/3.27	                 [c_9](x1) = [1] x1 + [0]
11.79/3.27	                                         
11.79/3.27	                [c_10](x1) = [4] x1 + [0]
11.79/3.27	  
11.79/3.27	  The order satisfies the following ordering constraints:
11.79/3.27	  
11.79/3.27	                       [le(0(), y)] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [true()]                             
11.79/3.27	                                                                            
11.79/3.27	                    [le(s(x), 0())] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [false()]                            
11.79/3.27	                                                                            
11.79/3.27	                   [le(s(x), s(y))] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [le(x, y)]                           
11.79/3.27	                                                                            
11.79/3.27	                    [minus(x, 0())] =  [0]                                  
11.79/3.27	                                    ?  [1] x + [0]                          
11.79/3.27	                                    =  [x]                                  
11.79/3.27	                                                                            
11.79/3.27	                [minus(s(x), s(y))] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [minus(x, y)]                        
11.79/3.27	                                                                            
11.79/3.27	                 [le^#(s(x), s(y))] =  [4] x + [8]                          
11.79/3.27	                                    >  [4] x + [1]                          
11.79/3.27	                                    =  [c_3(le^#(x, y))]                    
11.79/3.27	                                                                            
11.79/3.27	              [minus^#(s(x), s(y))] =  [4] x + [8]                          
11.79/3.27	                                    >  [4] x + [3]                          
11.79/3.27	                                    =  [c_5(minus^#(x, y))]                 
11.79/3.27	                                                                            
11.79/3.27	                [gcd^#(s(x), s(y))] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [c_8(if_gcd^#(le(y, x), s(x), s(y)))]
11.79/3.27	                                                                            
11.79/3.27	     [if_gcd^#(true(), s(x), s(y))] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [c_9(gcd^#(minus(x, y), s(y)))]      
11.79/3.27	                                                                            
11.79/3.27	    [if_gcd^#(false(), s(x), s(y))] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [c_10(gcd^#(minus(y, x), s(x)))]     
11.79/3.27	                                                                            
11.79/3.27	
11.79/3.27	The strictly oriented rules are moved into the weak component.
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^1)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Weak DPs:
11.79/3.27	  { le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	  , minus^#(s(x), s(y)) -> c_5(minus^#(x, y)) }
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^1))
11.79/3.27	
11.79/3.27	The following weak DPs constitute a sub-graph of the DG that is
11.79/3.27	closed under successors. The DPs are removed.
11.79/3.27	
11.79/3.27	{ le^#(s(x), s(y)) -> c_3(le^#(x, y))
11.79/3.27	, minus^#(s(x), s(y)) -> c_5(minus^#(x, y)) }
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(n^1)).
11.79/3.27	
11.79/3.27	Strict DPs:
11.79/3.27	  { gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(n^1))
11.79/3.27	
11.79/3.27	We use the processor 'matrix interpretation of dimension 1' to
11.79/3.27	orient following rules strictly.
11.79/3.27	
11.79/3.27	DPs:
11.79/3.27	  { 2: if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , 3: if_gcd^#(false(), s(x), s(y)) ->
11.79/3.27	       c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Trs: { minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	
11.79/3.27	Sub-proof:
11.79/3.27	----------
11.79/3.27	  The following argument positions are usable:
11.79/3.27	    Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}
11.79/3.27	  
11.79/3.27	  TcT has computed the following constructor-based matrix
11.79/3.27	  interpretation satisfying not(EDA).
11.79/3.27	  
11.79/3.27	              [le](x1, x2) = [0]                  
11.79/3.27	                                                  
11.79/3.27	                       [0] = [0]                  
11.79/3.27	                                                  
11.79/3.27	                    [true] = [0]                  
11.79/3.27	                                                  
11.79/3.27	                   [s](x1) = [1] x1 + [1]         
11.79/3.27	                                                  
11.79/3.27	                   [false] = [0]                  
11.79/3.27	                                                  
11.79/3.27	           [minus](x1, x2) = [1] x1 + [0]         
11.79/3.27	                                                  
11.79/3.27	            [le^#](x1, x2) = [7] x1 + [7] x2 + [0]
11.79/3.27	                                                  
11.79/3.27	                 [c_3](x1) = [7] x1 + [0]         
11.79/3.27	                                                  
11.79/3.27	         [minus^#](x1, x2) = [7] x1 + [7] x2 + [0]
11.79/3.27	                                                  
11.79/3.27	                 [c_5](x1) = [7] x1 + [0]         
11.79/3.27	                                                  
11.79/3.27	           [gcd^#](x1, x2) = [3] x1 + [3] x2 + [2]
11.79/3.27	                                                  
11.79/3.27	                 [c_8](x1) = [1] x1 + [0]         
11.79/3.27	                                                  
11.79/3.27	    [if_gcd^#](x1, x2, x3) = [3] x2 + [3] x3 + [2]
11.79/3.27	                                                  
11.79/3.27	                 [c_9](x1) = [1] x1 + [1]         
11.79/3.27	                                                  
11.79/3.27	                [c_10](x1) = [1] x1 + [1]         
11.79/3.27	  
11.79/3.27	  The order satisfies the following ordering constraints:
11.79/3.27	  
11.79/3.27	                       [le(0(), y)] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [true()]                             
11.79/3.27	                                                                            
11.79/3.27	                    [le(s(x), 0())] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [false()]                            
11.79/3.27	                                                                            
11.79/3.27	                   [le(s(x), s(y))] =  [0]                                  
11.79/3.27	                                    >= [0]                                  
11.79/3.27	                                    =  [le(x, y)]                           
11.79/3.27	                                                                            
11.79/3.27	                    [minus(x, 0())] =  [1] x + [0]                          
11.79/3.27	                                    >= [1] x + [0]                          
11.79/3.27	                                    =  [x]                                  
11.79/3.27	                                                                            
11.79/3.27	                [minus(s(x), s(y))] =  [1] x + [1]                          
11.79/3.27	                                    >  [1] x + [0]                          
11.79/3.27	                                    =  [minus(x, y)]                        
11.79/3.27	                                                                            
11.79/3.27	                [gcd^#(s(x), s(y))] =  [3] y + [3] x + [8]                  
11.79/3.27	                                    >= [3] y + [3] x + [8]                  
11.79/3.27	                                    =  [c_8(if_gcd^#(le(y, x), s(x), s(y)))]
11.79/3.27	                                                                            
11.79/3.27	     [if_gcd^#(true(), s(x), s(y))] =  [3] y + [3] x + [8]                  
11.79/3.27	                                    >  [3] y + [3] x + [6]                  
11.79/3.27	                                    =  [c_9(gcd^#(minus(x, y), s(y)))]      
11.79/3.27	                                                                            
11.79/3.27	    [if_gcd^#(false(), s(x), s(y))] =  [3] y + [3] x + [8]                  
11.79/3.27	                                    >  [3] y + [3] x + [6]                  
11.79/3.27	                                    =  [c_10(gcd^#(minus(y, x), s(x)))]     
11.79/3.27	                                                                            
11.79/3.27	
11.79/3.27	We return to the main proof. Consider the set of all dependency
11.79/3.27	pairs
11.79/3.27	
11.79/3.27	:
11.79/3.27	  { 1: gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , 2: if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , 3: if_gcd^#(false(), s(x), s(y)) ->
11.79/3.27	       c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	
11.79/3.27	Processor 'matrix interpretation of dimension 1' induces the
11.79/3.27	complexity certificate YES(?,O(n^1)) on application of dependency
11.79/3.27	pairs {2,3}. These cover all (indirect) predecessors of dependency
11.79/3.27	pairs {1,2,3}, their number of application is equally bounded. The
11.79/3.27	dependency pairs are shifted into the weak component.
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(1)).
11.79/3.27	
11.79/3.27	Weak DPs:
11.79/3.27	  { gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	  , if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	  , if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(1))
11.79/3.27	
11.79/3.27	The following weak DPs constitute a sub-graph of the DG that is
11.79/3.27	closed under successors. The DPs are removed.
11.79/3.27	
11.79/3.27	{ gcd^#(s(x), s(y)) -> c_8(if_gcd^#(le(y, x), s(x), s(y)))
11.79/3.27	, if_gcd^#(true(), s(x), s(y)) -> c_9(gcd^#(minus(x, y), s(y)))
11.79/3.27	, if_gcd^#(false(), s(x), s(y)) -> c_10(gcd^#(minus(y, x), s(x))) }
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(1)).
11.79/3.27	
11.79/3.27	Weak Trs:
11.79/3.27	  { le(0(), y) -> true()
11.79/3.27	  , le(s(x), 0()) -> false()
11.79/3.27	  , le(s(x), s(y)) -> le(x, y)
11.79/3.27	  , minus(x, 0()) -> x
11.79/3.27	  , minus(s(x), s(y)) -> minus(x, y) }
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(1))
11.79/3.27	
11.79/3.27	No rule is usable, rules are removed from the input problem.
11.79/3.27	
11.79/3.27	We are left with following problem, upon which TcT provides the
11.79/3.27	certificate YES(O(1),O(1)).
11.79/3.27	
11.79/3.27	Rules: Empty
11.79/3.27	Obligation:
11.79/3.27	  innermost runtime complexity
11.79/3.27	Answer:
11.79/3.27	  YES(O(1),O(1))
11.79/3.27	
11.79/3.27	Empty rules are trivially bounded
11.79/3.27	
11.79/3.27	Hurray, we answered YES(O(1),O(n^2))
11.79/3.28	EOF