YES(?,O(n^1))
78.48/31.10	YES(?,O(n^1))
78.48/31.10	
78.48/31.10	We are left with following problem, upon which TcT provides the
78.48/31.10	certificate YES(?,O(n^1)).
78.48/31.10	
78.48/31.10	Strict Trs:
78.48/31.10	  { rev(rev(x)) -> x
78.48/31.10	  , rev(nil()) -> nil()
78.48/31.10	  , rev(++(x, y)) -> ++(rev(y), rev(x))
78.48/31.10	  , ++(x, nil()) -> x
78.48/31.10	  , ++(x, ++(y, z)) -> ++(++(x, y), z)
78.48/31.10	  , ++(nil(), y) -> y
78.48/31.10	  , ++(.(x, y), z) -> .(x, ++(y, z))
78.48/31.10	  , make(x) -> .(x, nil()) }
78.48/31.10	Obligation:
78.48/31.10	  innermost runtime complexity
78.48/31.10	Answer:
78.48/31.10	  YES(?,O(n^1))
78.48/31.10	
78.48/31.10	The problem is match-bounded by 1. The enriched problem is
78.48/31.10	compatible with the following automaton.
78.48/31.10	{ rev_0(2) -> 1
78.48/31.10	, nil_0() -> 1
78.48/31.10	, nil_0() -> 2
78.48/31.10	, nil_0() -> 3
78.48/31.10	, nil_1() -> 1
78.48/31.10	, ++_0(2, 2) -> 1
78.48/31.10	, ++_1(2, 2) -> 3
78.48/31.10	, ._0(2, 2) -> 1
78.48/31.10	, ._0(2, 2) -> 2
78.48/31.10	, ._0(2, 2) -> 3
78.48/31.10	, ._1(2, 1) -> 1
78.48/31.10	, ._1(2, 3) -> 1
78.48/31.10	, ._1(2, 3) -> 3
78.48/31.10	, make_0(2) -> 1 }
78.48/31.10	
78.48/31.10	Hurray, we answered YES(?,O(n^1))
78.48/31.17	EOF