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