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