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