YES(O(1),O(n^1))
6.23/3.32	YES(O(1),O(n^1))
6.23/3.32	
6.23/3.32	We are left with following problem, upon which TcT provides the
6.23/3.32	certificate YES(O(1),O(n^1)).
6.23/3.32	
6.23/3.32	Strict Trs:
6.23/3.32	  { admit(x, nil()) -> nil()
6.23/3.32	  , admit(x, .(u, .(v, .(w(), z)))) ->
6.23/3.32	    cond(=(sum(x, u, v), w()),
6.23/3.32	         .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
6.23/3.32	  , cond(true(), y) -> y }
6.23/3.32	Obligation:
6.23/3.32	  runtime complexity
6.23/3.32	Answer:
6.23/3.32	  YES(O(1),O(n^1))
6.23/3.32	
6.23/3.32	We add the following weak dependency pairs:
6.23/3.32	
6.23/3.32	Strict DPs:
6.23/3.32	  { admit^#(x, nil()) -> c_1()
6.23/3.32	  , admit^#(x, .(u, .(v, .(w(), z)))) ->
6.23/3.32	    c_2(cond^#(=(sum(x, u, v), w()),
6.23/3.32	               .(u, .(v, .(w(), admit(carry(x, u, v), z))))))
6.23/3.32	  , cond^#(true(), y) -> c_3(y) }
6.23/3.32	
6.23/3.32	and mark the set of starting terms.
6.23/3.32	
6.23/3.32	We are left with following problem, upon which TcT provides the
6.23/3.32	certificate YES(O(1),O(n^1)).
6.23/3.32	
6.23/3.32	Strict DPs:
6.23/3.32	  { admit^#(x, nil()) -> c_1()
6.23/3.32	  , admit^#(x, .(u, .(v, .(w(), z)))) ->
6.23/3.32	    c_2(cond^#(=(sum(x, u, v), w()),
6.23/3.32	               .(u, .(v, .(w(), admit(carry(x, u, v), z))))))
6.23/3.32	  , cond^#(true(), y) -> c_3(y) }
6.23/3.32	Strict Trs:
6.23/3.32	  { admit(x, nil()) -> nil()
6.23/3.32	  , admit(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	    cond(=(sum(x, u, v), w()),
6.23/3.33	         .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
6.23/3.33	  , cond(true(), y) -> y }
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(n^1))
6.23/3.33	
6.23/3.33	The weightgap principle applies (using the following constant
6.23/3.33	growth matrix-interpretation)
6.23/3.33	
6.23/3.33	The following argument positions are usable:
6.23/3.33	  Uargs(.) = {2}, Uargs(cond) = {2}, Uargs(c_2) = {1},
6.23/3.33	  Uargs(cond^#) = {2}, Uargs(c_3) = {1}
6.23/3.33	
6.23/3.33	TcT has computed the following constructor-restricted matrix
6.23/3.33	interpretation.
6.23/3.33	
6.23/3.33	      [admit](x1, x2) = [2 0] x2 + [0]                      
6.23/3.33	                        [0 0]      [0]                      
6.23/3.33	                                                            
6.23/3.33	                [nil] = [2]                                 
6.23/3.33	                        [0]                                 
6.23/3.33	                                                            
6.23/3.33	          [.](x1, x2) = [1 0] x1 + [1 0] x2 + [0]           
6.23/3.33	                        [0 0]      [0 0]      [0]           
6.23/3.33	                                                            
6.23/3.33	                  [w] = [2]                                 
6.23/3.33	                        [0]                                 
6.23/3.33	                                                            
6.23/3.33	       [cond](x1, x2) = [0 1] x1 + [1 0] x2 + [0]           
6.23/3.33	                        [0 0]      [0 2]      [0]           
6.23/3.33	                                                            
6.23/3.33	          [=](x1, x2) = [0]                                 
6.23/3.33	                        [0]                                 
6.23/3.33	                                                            
6.23/3.33	    [sum](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [0]
6.23/3.33	                        [0 0]      [0 0]      [0 0]      [0]
6.23/3.33	                                                            
6.23/3.33	  [carry](x1, x2, x3) = [0]                                 
6.23/3.33	                        [0]                                 
6.23/3.33	                                                            
6.23/3.33	               [true] = [0]                                 
6.23/3.33	                        [1]                                 
6.23/3.33	                                                            
6.23/3.33	    [admit^#](x1, x2) = [2 1] x1 + [2 0] x2 + [2]           
6.23/3.33	                        [1 1]      [0 0]      [2]           
6.23/3.33	                                                            
6.23/3.33	                [c_1] = [1]                                 
6.23/3.33	                        [1]                                 
6.23/3.33	                                                            
6.23/3.33	            [c_2](x1) = [1 0] x1 + [2]                      
6.23/3.33	                        [0 1]      [2]                      
6.23/3.33	                                                            
6.23/3.33	     [cond^#](x1, x2) = [1 0] x2 + [2]                      
6.23/3.33	                        [0 0]      [2]                      
6.23/3.33	                                                            
6.23/3.33	            [c_3](x1) = [1 0] x1 + [1]                      
6.23/3.33	                        [0 1]      [1]                      
6.23/3.33	
6.23/3.33	The order satisfies the following ordering constraints:
6.23/3.33	
6.23/3.33	                    [admit(x, nil())] = [4]                                                        
6.23/3.33	                                        [0]                                                        
6.23/3.33	                                      > [2]                                                        
6.23/3.33	                                        [0]                                                        
6.23/3.33	                                      = [nil()]                                                    
6.23/3.33	                                                                                                   
6.23/3.33	    [admit(x, .(u, .(v, .(w(), z))))] = [2 0] u + [2 0] v + [2 0] z + [4]                          
6.23/3.33	                                        [0 0]     [0 0]     [0 0]     [0]                          
6.23/3.33	                                      > [1 0] u + [1 0] v + [2 0] z + [2]                          
6.23/3.33	                                        [0 0]     [0 0]     [0 0]     [0]                          
6.23/3.33	                                      = [cond(=(sum(x, u, v), w()),                                
6.23/3.33	                                              .(u, .(v, .(w(), admit(carry(x, u, v), z)))))]       
6.23/3.33	                                                                                                   
6.23/3.33	                    [cond(true(), y)] = [1 0] y + [1]                                              
6.23/3.33	                                        [0 2]     [0]                                              
6.23/3.33	                                      > [1 0] y + [0]                                              
6.23/3.33	                                        [0 1]     [0]                                              
6.23/3.33	                                      = [y]                                                        
6.23/3.33	                                                                                                   
6.23/3.33	                  [admit^#(x, nil())] = [2 1] x + [6]                                              
6.23/3.33	                                        [1 1]     [2]                                              
6.23/3.33	                                      > [1]                                                        
6.23/3.33	                                        [1]                                                        
6.23/3.33	                                      = [c_1()]                                                    
6.23/3.33	                                                                                                   
6.23/3.33	  [admit^#(x, .(u, .(v, .(w(), z))))] = [2 1] x + [2 0] u + [2 0] v + [2 0] z + [6]                
6.23/3.33	                                        [1 1]     [0 0]     [0 0]     [0 0]     [2]                
6.23/3.33	                                      ? [1 0] u + [1 0] v + [2 0] z + [6]                          
6.23/3.33	                                        [0 0]     [0 0]     [0 0]     [4]                          
6.23/3.33	                                      = [c_2(cond^#(=(sum(x, u, v), w()),                          
6.23/3.33	                                                    .(u, .(v, .(w(), admit(carry(x, u, v), z))))))]
6.23/3.33	                                                                                                   
6.23/3.33	                  [cond^#(true(), y)] = [1 0] y + [2]                                              
6.23/3.33	                                        [0 0]     [2]                                              
6.23/3.33	                                      ? [1 0] y + [1]                                              
6.23/3.33	                                        [0 1]     [1]                                              
6.23/3.33	                                      = [c_3(y)]                                                   
6.23/3.33	                                                                                                   
6.23/3.33	
6.23/3.33	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
6.23/3.33	
6.23/3.33	We are left with following problem, upon which TcT provides the
6.23/3.33	certificate YES(O(1),O(1)).
6.23/3.33	
6.23/3.33	Strict DPs:
6.23/3.33	  { admit^#(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	    c_2(cond^#(=(sum(x, u, v), w()),
6.23/3.33	               .(u, .(v, .(w(), admit(carry(x, u, v), z))))))
6.23/3.33	  , cond^#(true(), y) -> c_3(y) }
6.23/3.33	Weak DPs: { admit^#(x, nil()) -> c_1() }
6.23/3.33	Weak Trs:
6.23/3.33	  { admit(x, nil()) -> nil()
6.23/3.33	  , admit(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	    cond(=(sum(x, u, v), w()),
6.23/3.33	         .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
6.23/3.33	  , cond(true(), y) -> y }
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(1))
6.23/3.33	
6.23/3.33	We estimate the number of application of {1} by applications of
6.23/3.33	Pre({1}) = {2}. Here rules are labeled as follows:
6.23/3.33	
6.23/3.33	  DPs:
6.23/3.33	    { 1: admit^#(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	         c_2(cond^#(=(sum(x, u, v), w()),
6.23/3.33	                    .(u, .(v, .(w(), admit(carry(x, u, v), z))))))
6.23/3.33	    , 2: cond^#(true(), y) -> c_3(y)
6.23/3.33	    , 3: admit^#(x, nil()) -> c_1() }
6.23/3.33	
6.23/3.33	We are left with following problem, upon which TcT provides the
6.23/3.33	certificate YES(O(1),O(1)).
6.23/3.33	
6.23/3.33	Strict DPs: { cond^#(true(), y) -> c_3(y) }
6.23/3.33	Weak DPs:
6.23/3.33	  { admit^#(x, nil()) -> c_1()
6.23/3.33	  , admit^#(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	    c_2(cond^#(=(sum(x, u, v), w()),
6.23/3.33	               .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) }
6.23/3.33	Weak Trs:
6.23/3.33	  { admit(x, nil()) -> nil()
6.23/3.33	  , admit(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	    cond(=(sum(x, u, v), w()),
6.23/3.33	         .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
6.23/3.33	  , cond(true(), y) -> y }
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(1))
6.23/3.33	
6.23/3.33	The following weak DPs constitute a sub-graph of the DG that is
6.23/3.33	closed under successors. The DPs are removed.
6.23/3.33	
6.23/3.33	{ admit^#(x, nil()) -> c_1()
6.23/3.33	, admit^#(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	  c_2(cond^#(=(sum(x, u, v), w()),
6.23/3.33	             .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) }
6.23/3.33	
6.23/3.33	We are left with following problem, upon which TcT provides the
6.23/3.33	certificate YES(O(1),O(1)).
6.23/3.33	
6.23/3.33	Strict DPs: { cond^#(true(), y) -> c_3(y) }
6.23/3.33	Weak Trs:
6.23/3.33	  { admit(x, nil()) -> nil()
6.23/3.33	  , admit(x, .(u, .(v, .(w(), z)))) ->
6.23/3.33	    cond(=(sum(x, u, v), w()),
6.23/3.33	         .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
6.23/3.33	  , cond(true(), y) -> y }
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(1))
6.23/3.33	
6.23/3.33	No rule is usable, rules are removed from the input problem.
6.23/3.33	
6.23/3.33	We are left with following problem, upon which TcT provides the
6.23/3.33	certificate YES(O(1),O(1)).
6.23/3.33	
6.23/3.33	Strict DPs: { cond^#(true(), y) -> c_3(y) }
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(1))
6.23/3.33	
6.23/3.33	We use the processor 'matrix interpretation of dimension 1' to
6.23/3.33	orient following rules strictly.
6.23/3.33	
6.23/3.33	DPs:
6.23/3.33	  { 1: cond^#(true(), y) -> c_3(y) }
6.23/3.33	
6.23/3.33	Sub-proof:
6.23/3.33	----------
6.23/3.33	  The following argument positions are usable:
6.23/3.33	    none
6.23/3.33	  
6.23/3.33	  TcT has computed the following constructor-restricted matrix
6.23/3.33	  interpretation. Note that the diagonal of the component-wise maxima
6.23/3.33	  of interpretation-entries (of constructors) contains no more than 0
6.23/3.33	  non-zero entries.
6.23/3.33	  
6.23/3.33	              [true] = [5]                  
6.23/3.33	                                            
6.23/3.33	    [cond^#](x1, x2) = [3] x1 + [7] x2 + [0]
6.23/3.33	                                            
6.23/3.33	           [c_3](x1) = [7] x1 + [3]         
6.23/3.33	  
6.23/3.33	  The order satisfies the following ordering constraints:
6.23/3.33	  
6.23/3.33	    [cond^#(true(), y)] = [7] y + [15]
6.23/3.33	                        > [7] y + [3] 
6.23/3.33	                        = [c_3(y)]    
6.23/3.33	                                      
6.23/3.33	
6.23/3.33	The strictly oriented rules are moved into the weak component.
6.23/3.33	
6.23/3.33	We are left with following problem, upon which TcT provides the
6.23/3.33	certificate YES(O(1),O(1)).
6.23/3.33	
6.23/3.33	Weak DPs: { cond^#(true(), y) -> c_3(y) }
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(1))
6.23/3.33	
6.23/3.33	The following weak DPs constitute a sub-graph of the DG that is
6.23/3.33	closed under successors. The DPs are removed.
6.23/3.33	
6.23/3.33	{ cond^#(true(), y) -> c_3(y) }
6.23/3.33	
6.23/3.33	We are left with following problem, upon which TcT provides the
6.23/3.33	certificate YES(O(1),O(1)).
6.23/3.33	
6.23/3.33	Rules: Empty
6.23/3.33	Obligation:
6.23/3.33	  runtime complexity
6.23/3.33	Answer:
6.23/3.33	  YES(O(1),O(1))
6.23/3.33	
6.23/3.33	Empty rules are trivially bounded
6.23/3.33	
6.23/3.33	Hurray, we answered YES(O(1),O(n^1))
6.23/3.34	EOF