YES(?,O(n^1))
16.62/9.08	YES(?,O(n^1))
16.62/9.08	
16.62/9.08	We are left with following problem, upon which TcT provides the
16.62/9.08	certificate YES(?,O(n^1)).
16.62/9.08	
16.62/9.08	Strict Trs:
16.62/9.08	  { minus(minus(x)) -> x
16.62/9.08	  , minux(+(x, y)) -> +(minus(y), minus(x))
16.62/9.08	  , +(minus(x), +(x, y)) -> y
16.62/9.08	  , +(+(x, y), minus(y)) -> x }
16.62/9.08	Obligation:
16.62/9.08	  derivational complexity
16.62/9.08	Answer:
16.62/9.08	  YES(?,O(n^1))
16.62/9.08	
16.62/9.08	The problem is match-bounded by 1. The enriched problem is
16.62/9.08	compatible with the following automaton.
16.62/9.08	{ minus_0(1) -> 1
16.62/9.08	, minus_0(1) -> 2
16.62/9.08	, minus_0(1) -> 3
16.62/9.08	, minus_1(1) -> 1
16.62/9.08	, minus_1(1) -> 2
16.62/9.08	, minus_1(1) -> 3
16.62/9.08	, minus_1(2) -> 1
16.62/9.08	, minus_1(2) -> 2
16.62/9.08	, minus_1(2) -> 3
16.62/9.08	, minus_1(3) -> 1
16.62/9.08	, minus_1(3) -> 2
16.62/9.08	, minus_1(3) -> 3
16.62/9.08	, minux_0(1) -> 1
16.62/9.08	, minux_0(1) -> 2
16.62/9.08	, minux_0(1) -> 3
16.62/9.08	, +_0(1, 1) -> 1
16.62/9.08	, +_0(1, 1) -> 2
16.62/9.08	, +_0(1, 1) -> 3
16.62/9.08	, +_1(2, 3) -> 1
16.62/9.08	, +_1(2, 3) -> 2
16.62/9.08	, +_1(2, 3) -> 3 }
16.62/9.08	
16.62/9.08	Hurray, we answered YES(?,O(n^1))
16.62/9.09	EOF