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