YES(?,O(n^1))
894.60/297.15	YES(?,O(n^1))
894.60/297.15	
894.60/297.15	We are left with following problem, upon which TcT provides the
894.60/297.15	certificate YES(?,O(n^1)).
894.60/297.15	
894.60/297.15	Strict Trs:
894.60/297.15	  { +(+(x, y), z) -> +(x, +(y, z))
894.60/297.15	  , +(*(x, y), +(*(x, z), u())) -> +(*(x, +(y, z)), u())
894.60/297.15	  , +(*(x, y), *(x, z)) -> *(x, +(y, z)) }
894.60/297.15	Obligation:
894.60/297.15	  runtime complexity
894.60/297.15	Answer:
894.60/297.15	  YES(?,O(n^1))
894.60/297.15	
894.60/297.15	The problem is match-bounded by 1. The enriched problem is
894.60/297.15	compatible with the following automaton.
894.60/297.15	{ +_0(2, 2) -> 1
894.60/297.15	, +_0(2, 3) -> 1
894.60/297.15	, +_0(3, 2) -> 1
894.60/297.15	, +_0(3, 3) -> 1
894.60/297.15	, +_1(2, 2) -> 4
894.60/297.15	, +_1(2, 3) -> 4
894.60/297.15	, +_1(3, 2) -> 4
894.60/297.15	, +_1(3, 3) -> 4
894.60/297.15	, *_0(2, 2) -> 2
894.60/297.15	, *_0(2, 3) -> 2
894.60/297.15	, *_0(3, 2) -> 2
894.60/297.15	, *_0(3, 3) -> 2
894.60/297.15	, *_1(2, 4) -> 1
894.60/297.15	, *_1(2, 4) -> 4
894.60/297.15	, *_1(3, 4) -> 1
894.60/297.15	, *_1(3, 4) -> 4
894.60/297.15	, u_0() -> 3 }
894.60/297.15	
894.60/297.15	Hurray, we answered YES(?,O(n^1))
895.07/297.49	EOF