YES(?,O(n^1))
9.51/5.57	YES(?,O(n^1))
9.51/5.57	
9.51/5.57	We are left with following problem, upon which TcT provides the
9.51/5.57	certificate YES(?,O(n^1)).
9.51/5.57	
9.51/5.57	Strict Trs:
9.51/5.57	  { d(x) -> e(u(x))
9.51/5.57	  , d(u(x)) -> c(x)
9.51/5.57	  , c(u(x)) -> b(x)
9.51/5.57	  , b(u(x)) -> a(e(x))
9.51/5.57	  , v(e(x)) -> x }
9.51/5.57	Obligation:
9.51/5.57	  derivational complexity
9.51/5.57	Answer:
9.51/5.57	  YES(?,O(n^1))
9.51/5.57	
9.51/5.57	TcT has computed the following matrix interpretation satisfying
9.51/5.57	not(EDA) and not(IDA(1)).
9.51/5.57	
9.51/5.57	            [1 1 0 0]      [1]
9.51/5.57	  [d](x1) = [0 0 1 0] x1 + [1]
9.51/5.57	            [0 0 0 1]      [1]
9.51/5.57	            [0 0 0 0]      [1]
9.51/5.57	                              
9.51/5.57	            [1 0 0 0]      [0]
9.51/5.57	  [e](x1) = [0 0 0 1] x1 + [0]
9.51/5.57	            [0 0 1 0]      [0]
9.51/5.57	            [0 1 0 0]      [0]
9.51/5.57	                              
9.51/5.57	            [1 1 0 0]      [0]
9.51/5.57	  [u](x1) = [0 0 0 0] x1 + [1]
9.51/5.57	            [0 0 0 1]      [0]
9.51/5.57	            [0 0 1 0]      [0]
9.51/5.57	                              
9.51/5.57	            [1 0 0 0]      [1]
9.51/5.57	  [c](x1) = [0 0 0 1] x1 + [1]
9.51/5.57	            [0 0 1 0]      [1]
9.51/5.57	            [0 0 0 0]      [1]
9.51/5.57	                              
9.51/5.57	            [1 1 0 0]      [0]
9.51/5.57	  [b](x1) = [0 0 1 0] x1 + [1]
9.51/5.57	            [0 0 0 1]      [1]
9.51/5.57	            [0 0 0 0]      [1]
9.51/5.57	                              
9.51/5.57	            [1 0 0 0]      [1]
9.51/5.57	  [v](x1) = [0 0 0 1] x1 + [1]
9.51/5.57	            [0 0 1 0]      [1]
9.51/5.57	            [0 1 0 0]      [1]
9.51/5.57	                              
9.51/5.57	            [1 0 0 0]      [0]
9.51/5.57	  [a](x1) = [0 0 0 0] x1 + [1]
9.51/5.57	            [0 0 0 0]      [1]
9.51/5.57	            [0 0 0 0]      [1]
9.51/5.57	
9.51/5.57	The order satisfies the following ordering constraints:
9.51/5.57	
9.51/5.57	     [d(x)] = [1 1 0 0]     [1]
9.51/5.57	              [0 0 1 0] x + [1]
9.51/5.57	              [0 0 0 1]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            > [1 1 0 0]     [0]
9.51/5.57	              [0 0 1 0] x + [0]
9.51/5.57	              [0 0 0 1]     [0]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            = [e(u(x))]        
9.51/5.57	                               
9.51/5.57	  [d(u(x))] = [1 1 0 0]     [2]
9.51/5.57	              [0 0 0 1] x + [1]
9.51/5.57	              [0 0 1 0]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            > [1 0 0 0]     [1]
9.51/5.57	              [0 0 0 1] x + [1]
9.51/5.57	              [0 0 1 0]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            = [c(x)]           
9.51/5.57	                               
9.51/5.57	  [c(u(x))] = [1 1 0 0]     [1]
9.51/5.57	              [0 0 1 0] x + [1]
9.51/5.57	              [0 0 0 1]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            > [1 1 0 0]     [0]
9.51/5.57	              [0 0 1 0] x + [1]
9.51/5.57	              [0 0 0 1]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            = [b(x)]           
9.51/5.57	                               
9.51/5.57	  [b(u(x))] = [1 1 0 0]     [1]
9.51/5.57	              [0 0 0 1] x + [1]
9.51/5.57	              [0 0 1 0]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            > [1 0 0 0]     [0]
9.51/5.57	              [0 0 0 0] x + [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	              [0 0 0 0]     [1]
9.51/5.57	            = [a(e(x))]        
9.51/5.57	                               
9.51/5.57	  [v(e(x))] = [1 0 0 0]     [1]
9.51/5.57	              [0 1 0 0] x + [1]
9.51/5.57	              [0 0 1 0]     [1]
9.51/5.57	              [0 0 0 1]     [1]
9.51/5.57	            > [1 0 0 0]     [0]
9.51/5.57	              [0 1 0 0] x + [0]
9.51/5.57	              [0 0 1 0]     [0]
9.51/5.57	              [0 0 0 1]     [0]
9.51/5.57	            = [x]              
9.51/5.57	                               
9.51/5.57	
9.51/5.57	Hurray, we answered YES(?,O(n^1))
9.51/5.59	EOF