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