YES(?,O(n^1))
345.65/156.38	YES(?,O(n^1))
345.65/156.38	
345.65/156.38	We are left with following problem, upon which TcT provides the
345.65/156.38	certificate YES(?,O(n^1)).
345.65/156.38	
345.65/156.38	Strict Trs:
345.65/156.38	  { f(g(i(a(), b(), b'()), c()), d()) ->
345.65/156.38	    if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
345.65/156.38	  , f(g(h(a(), b()), c()), d()) ->
345.65/156.38	    if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) }
345.65/156.38	Obligation:
345.65/156.38	  derivational complexity
345.65/156.38	Answer:
345.65/156.38	  YES(?,O(n^1))
345.65/156.38	
345.65/156.38	TcT has computed the following matrix interpretation satisfying
345.65/156.38	not(EDA) and not(IDA(1)).
345.65/156.38	
345.65/156.38	                     [1 1 0 0]      [1 1 0 0]      [0]               
345.65/156.38	       [f](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                                                                     
345.65/156.38	                     [1 0 0 0]      [1 0 0 0]      [0]               
345.65/156.38	       [g](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [1]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                                                                     
345.65/156.38	                     [1 0 0 0]      [1 0 0 0]      [1 0 0 0]      [0]
345.65/156.38	   [i](x1, x2, x3) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0 0] x3 + [0]
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0 0 0 0]      [0]
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0 0 0 0]      [0]
345.65/156.38	                                                                     
345.65/156.38	                     [0]                                             
345.65/156.38	               [a] = [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [0]                                             
345.65/156.38	               [b] = [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [1]                                             
345.65/156.38	              [b'] = [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [0]                                             
345.65/156.38	               [c] = [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [0]                                             
345.65/156.38	               [d] = [1]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [1 0 0 0]      [1 0 0 0]      [1 0 0 0]      [0]
345.65/156.38	  [if](x1, x2, x3) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0 0] x3 + [0]
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0 0 0 0]      [0]
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0 0 0 0]      [0]
345.65/156.38	                                                                     
345.65/156.38	                     [0]                                             
345.65/156.38	               [e] = [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [1 0 0 0]      [1 0 0 0]      [0]               
345.65/156.38	       [.](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                                                                     
345.65/156.38	                     [0]                                             
345.65/156.38	              [d'] = [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                     [0]                                             
345.65/156.38	                                                                     
345.65/156.38	                     [1 0 0 0]      [1 0 0 0]      [0]               
345.65/156.38	       [h](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	                     [0 0 0 0]      [0 0 0 0]      [0]               
345.65/156.38	
345.65/156.38	The order satisfies the following ordering constraints:
345.65/156.38	
345.65/156.38	  [f(g(i(a(), b(), b'()), c()), d())] = [3]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                      > [1]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                      = [if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))]      
345.65/156.38	                                                                                                    
345.65/156.38	        [f(g(h(a(), b()), c()), d())] = [2]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                      > [1]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                        [0]                                                         
345.65/156.38	                                      = [if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))]
345.65/156.38	                                                                                                    
345.65/156.38	
345.65/156.38	Hurray, we answered YES(?,O(n^1))
345.85/156.47	EOF