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