YES(O(1),O(n^2))
170.22/60.02	YES(O(1),O(n^2))
170.22/60.02	
170.22/60.02	We are left with following problem, upon which TcT provides the
170.22/60.02	certificate YES(O(1),O(n^2)).
170.22/60.02	
170.22/60.02	Strict Trs: { .(.(x, y), z) -> .(x, .(y, z)) }
170.22/60.02	Obligation:
170.22/60.02	  derivational complexity
170.22/60.02	Answer:
170.22/60.02	  YES(O(1),O(n^2))
170.22/60.02	
170.22/60.02	We use the processor 'matrix interpretation of dimension 2' to
170.22/60.02	orient following rules strictly.
170.22/60.02	
170.22/60.02	Trs: { .(.(x, y), z) -> .(x, .(y, z)) }
170.22/60.02	
170.22/60.02	The induced complexity on above rules (modulo remaining rules) is
170.22/60.02	YES(?,O(n^2)) . These rules are moved into the corresponding weak
170.22/60.02	component(s).
170.22/60.02	
170.22/60.02	Sub-proof:
170.22/60.02	----------
170.22/60.02	  TcT has computed the following triangular matrix interpretation.
170.22/60.02	  
170.22/60.02	    [.](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
170.22/60.02	                  [0 1]      [0 1]      [1]
170.22/60.02	  
170.22/60.02	  The order satisfies the following ordering constraints:
170.22/60.02	  
170.22/60.02	    [.(.(x, y), z)] = [1 2] x + [1 1] y + [1 0] z + [1]
170.22/60.02	                      [0 1]     [0 1]     [0 1]     [2]
170.22/60.02	                    > [1 1] x + [1 1] y + [1 0] z + [0]
170.22/60.02	                      [0 1]     [0 1]     [0 1]     [2]
170.22/60.02	                    = [.(x, .(y, z))]                  
170.22/60.02	                                                       
170.22/60.02	
170.22/60.02	We return to the main proof.
170.22/60.02	
170.22/60.02	We are left with following problem, upon which TcT provides the
170.22/60.02	certificate YES(O(1),O(1)).
170.22/60.02	
170.22/60.02	Weak Trs: { .(.(x, y), z) -> .(x, .(y, z)) }
170.22/60.02	Obligation:
170.22/60.02	  derivational complexity
170.22/60.02	Answer:
170.22/60.02	  YES(O(1),O(1))
170.22/60.02	
170.22/60.02	Empty rules are trivially bounded
170.22/60.02	
170.22/60.02	Hurray, we answered YES(O(1),O(n^2))
170.36/60.18	EOF