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