YES(?,O(n^1))
841.85/297.03	YES(?,O(n^1))
841.85/297.03	
841.85/297.03	We are left with following problem, upon which TcT provides the
841.85/297.03	certificate YES(?,O(n^1)).
841.85/297.03	
841.85/297.03	Strict Trs:
841.85/297.03	  { +(+(x, y), z) -> +(x, +(y, z))
841.85/297.03	  , +(f(x), +(f(y), z)) -> +(f(+(x, y)), z)
841.85/297.03	  , +(f(x), f(y)) -> f(+(x, y)) }
841.85/297.03	Obligation:
841.85/297.03	  runtime complexity
841.85/297.03	Answer:
841.85/297.03	  YES(?,O(n^1))
841.85/297.03	
841.85/297.03	The problem is match-bounded by 1. The enriched problem is
841.85/297.03	compatible with the following automaton.
841.85/297.03	{ +_0(2, 2) -> 1
841.85/297.03	, +_1(2, 2) -> 3
841.85/297.03	, f_0(2) -> 2
841.85/297.03	, f_1(3) -> 1
841.85/297.03	, f_1(3) -> 3 }
841.85/297.03	
841.85/297.03	Hurray, we answered YES(?,O(n^1))
842.08/297.26	EOF