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