YES(?,O(n^1))
36.01/20.76	YES(?,O(n^1))
36.01/20.76	
36.01/20.76	We are left with following problem, upon which TcT provides the
36.01/20.76	certificate YES(?,O(n^1)).
36.01/20.76	
36.01/20.76	Strict Trs:
36.01/20.76	  { f(f(a(), a()), x) -> f(f(x, f(a(), f(a(), a()))), a()) }
36.01/20.76	Obligation:
36.01/20.76	  derivational complexity
36.01/20.76	Answer:
36.01/20.76	  YES(?,O(n^1))
36.01/20.76	
36.01/20.76	We uncurry the input using the following uncurry rules.
36.01/20.76	
36.01/20.76	  { f(a(), x_1) -> a_1(x_1)
36.01/20.76	  , f(a_1(x_1), x_2) -> a_2(x_1, x_2) }
36.01/20.76	
36.01/20.76	We are left with following problem, upon which TcT provides the
36.01/20.76	certificate YES(?,O(n^1)).
36.01/20.76	
36.01/20.76	Strict Trs: { a_2(a(), x) -> f(f(x, a_1(a_1(a()))), a()) }
36.01/20.76	Weak Trs:
36.01/20.76	  { f(a(), x_1) -> a_1(x_1)
36.01/20.76	  , f(a_1(x_1), x_2) -> a_2(x_1, x_2) }
36.01/20.76	Obligation:
36.01/20.76	  derivational complexity
36.01/20.76	Answer:
36.01/20.76	  YES(?,O(n^1))
36.01/20.76	
36.01/20.76	The problem is match-bounded by 1. The enriched problem is
36.01/20.76	compatible with the following automaton.
36.01/20.76	{ f_0(1, 1) -> 1
36.01/20.76	, f_1(1, 4) -> 2
36.01/20.76	, f_1(2, 3) -> 1
36.01/20.76	, f_1(4, 4) -> 7
36.01/20.76	, f_1(7, 6) -> 2
36.01/20.76	, a_2_0(1, 1) -> 1
36.01/20.76	, a_2_1(1, 4) -> 2
36.01/20.76	, a_2_1(4, 3) -> 1
36.01/20.76	, a_2_1(5, 4) -> 7
36.01/20.76	, a_0() -> 1
36.01/20.76	, a_1() -> 3
36.01/20.76	, a_1() -> 6
36.01/20.76	, a_1_0(1) -> 1
36.01/20.76	, a_1_1(4) -> 2
36.01/20.76	, a_1_1(5) -> 4
36.01/20.76	, a_1_1(6) -> 5 }
36.01/20.76	
36.01/20.76	Hurray, we answered YES(?,O(n^1))
36.01/20.78	EOF