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