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