YES(?,O(n^1))
14.23/4.50	YES(?,O(n^1))
14.23/4.50	
14.23/4.50	We are left with following problem, upon which TcT provides the
14.23/4.50	certificate YES(?,O(n^1)).
14.23/4.50	
14.23/4.50	Strict Trs:
14.23/4.50	  { h(x, c(y, z)) -> h(c(s(y), x), z)
14.23/4.50	  , h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z))) }
14.23/4.50	Obligation:
14.23/4.50	  runtime complexity
14.23/4.50	Answer:
14.23/4.50	  YES(?,O(n^1))
14.23/4.50	
14.23/4.50	The input is overlay and right-linear. Switching to innermost
14.23/4.50	rewriting.
14.23/4.50	
14.23/4.50	We are left with following problem, upon which TcT provides the
14.23/4.50	certificate YES(?,O(n^1)).
14.23/4.50	
14.23/4.50	Strict Trs:
14.23/4.50	  { h(x, c(y, z)) -> h(c(s(y), x), z)
14.23/4.50	  , h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z))) }
14.23/4.50	Obligation:
14.23/4.50	  innermost runtime complexity
14.23/4.50	Answer:
14.23/4.50	  YES(?,O(n^1))
14.23/4.50	
14.23/4.50	The problem is match-bounded by 2. The enriched problem is
14.23/4.50	compatible with the following automaton.
14.23/4.50	{ h_0(2, 2) -> 1
14.23/4.50	, h_1(2, 5) -> 1
14.23/4.50	, h_1(3, 2) -> 1
14.23/4.50	, h_1(3, 5) -> 1
14.23/4.50	, h_1(9, 5) -> 1
14.23/4.50	, h_1(11, 5) -> 1
14.23/4.50	, h_2(9, 5) -> 1
14.23/4.50	, h_2(9, 7) -> 1
14.23/4.50	, h_2(11, 2) -> 1
14.23/4.50	, h_2(11, 5) -> 1
14.23/4.50	, c_0(2, 2) -> 2
14.23/4.50	, c_1(2, 2) -> 7
14.23/4.50	, c_1(2, 5) -> 7
14.23/4.50	, c_1(4, 2) -> 3
14.23/4.50	, c_1(4, 3) -> 3
14.23/4.50	, c_1(4, 11) -> 3
14.23/4.50	, c_1(6, 5) -> 5
14.23/4.50	, c_1(6, 7) -> 5
14.23/4.51	, c_2(10, 2) -> 9
14.23/4.51	, c_2(10, 3) -> 9
14.23/4.51	, c_2(10, 9) -> 9
14.23/4.51	, c_2(10, 11) -> 9
14.23/4.51	, c_2(12, 9) -> 11
14.23/4.51	, s_0(2) -> 2
14.23/4.51	, s_1(2) -> 4
14.23/4.51	, s_1(8) -> 6
14.23/4.51	, s_2(2) -> 12
14.23/4.51	, s_2(6) -> 10
14.23/4.51	, 0_0() -> 2
14.23/4.51	, 0_1() -> 8 }
14.23/4.51	
14.23/4.51	Hurray, we answered YES(?,O(n^1))
14.23/4.53	EOF