YES(?,O(n^1))
6.44/1.96	YES(?,O(n^1))
6.44/1.96	
6.44/1.96	We are left with following problem, upon which TcT provides the
6.44/1.96	certificate YES(?,O(n^1)).
6.44/1.96	
6.44/1.96	Strict Trs:
6.44/1.96	  { append(@l1, @l2) -> append#1(@l1, @l2)
6.44/1.96	  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
6.44/1.96	  , append#1(nil(), @l2) -> @l2
6.44/1.96	  , appendAll(@l) -> appendAll#1(@l)
6.44/1.96	  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
6.44/1.96	  , appendAll#1(nil()) -> nil()
6.44/1.96	  , appendAll2(@l) -> appendAll2#1(@l)
6.44/1.96	  , appendAll2#1(::(@l1, @ls)) ->
6.44/1.96	    append(appendAll(@l1), appendAll2(@ls))
6.44/1.96	  , appendAll2#1(nil()) -> nil()
6.44/1.96	  , appendAll3(@l) -> appendAll3#1(@l)
6.44/1.96	  , appendAll3#1(::(@l1, @ls)) ->
6.44/1.96	    append(appendAll2(@l1), appendAll3(@ls))
6.44/1.96	  , appendAll3#1(nil()) -> nil() }
6.44/1.96	Obligation:
6.44/1.96	  innermost runtime complexity
6.44/1.96	Answer:
6.44/1.96	  YES(?,O(n^1))
6.44/1.96	
6.44/1.96	The problem is match-bounded by 4. The enriched problem is
6.44/1.96	compatible with the following automaton.
6.44/1.96	{ append_0(2, 2) -> 1
6.44/1.96	, append_1(2, 2) -> 3
6.44/1.96	, append_1(2, 4) -> 1
6.44/1.96	, append_1(2, 4) -> 4
6.44/1.96	, append_1(4, 5) -> 1
6.44/1.96	, append_1(4, 5) -> 5
6.44/1.96	, append_1(4, 5) -> 7
6.44/1.96	, append_1(5, 6) -> 1
6.44/1.96	, append_1(5, 6) -> 6
6.44/1.96	, append_1(5, 6) -> 8
6.44/1.96	, append_2(4, 5) -> 7
6.44/1.96	, append_3(7, 6) -> 8
6.44/1.96	, append#1_0(2, 2) -> 1
6.44/1.96	, append#1_1(2, 2) -> 1
6.44/1.96	, append#1_2(2, 2) -> 3
6.44/1.96	, append#1_2(2, 4) -> 1
6.44/1.96	, append#1_2(2, 4) -> 4
6.44/1.96	, append#1_2(4, 5) -> 1
6.44/1.96	, append#1_2(4, 5) -> 5
6.44/1.96	, append#1_2(4, 5) -> 7
6.44/1.96	, append#1_2(5, 6) -> 1
6.44/1.96	, append#1_2(5, 6) -> 6
6.44/1.96	, append#1_2(5, 6) -> 8
6.44/1.96	, append#1_3(4, 5) -> 7
6.44/1.96	, append#1_4(7, 6) -> 8
6.44/1.96	, ::_0(2, 2) -> 1
6.44/1.96	, ::_0(2, 2) -> 2
6.44/1.96	, ::_0(2, 2) -> 3
6.44/1.96	, ::_1(2, 1) -> 1
6.44/1.96	, ::_1(2, 3) -> 1
6.44/1.96	, ::_1(2, 3) -> 3
6.44/1.96	, ::_1(2, 4) -> 1
6.44/1.96	, ::_1(2, 4) -> 4
6.44/1.96	, ::_2(2, 7) -> 1
6.44/1.96	, ::_2(2, 7) -> 5
6.44/1.96	, ::_2(2, 7) -> 7
6.44/1.96	, ::_3(2, 8) -> 1
6.44/1.96	, ::_3(2, 8) -> 6
6.44/1.96	, ::_3(2, 8) -> 8
6.44/1.96	, nil_0() -> 1
6.44/1.96	, nil_0() -> 2
6.44/1.96	, nil_0() -> 3
6.44/1.96	, nil_1() -> 1
6.44/1.96	, nil_1() -> 4
6.44/1.96	, nil_1() -> 5
6.44/1.96	, nil_1() -> 6
6.44/1.96	, nil_1() -> 7
6.44/1.96	, nil_1() -> 8
6.44/1.96	, appendAll_0(2) -> 1
6.44/1.96	, appendAll_1(2) -> 1
6.44/1.96	, appendAll_1(2) -> 4
6.44/1.96	, appendAll#1_0(2) -> 1
6.44/1.96	, appendAll#1_1(2) -> 1
6.44/1.96	, appendAll#1_2(2) -> 1
6.44/1.96	, appendAll#1_2(2) -> 4
6.44/1.96	, appendAll2_0(2) -> 1
6.44/1.96	, appendAll2_1(2) -> 1
6.44/1.96	, appendAll2_1(2) -> 5
6.44/1.96	, appendAll2_1(2) -> 7
6.44/1.96	, appendAll2#1_0(2) -> 1
6.44/1.96	, appendAll2#1_1(2) -> 1
6.44/1.96	, appendAll2#1_2(2) -> 1
6.44/1.96	, appendAll2#1_2(2) -> 5
6.44/1.96	, appendAll2#1_2(2) -> 7
6.44/1.96	, appendAll3_0(2) -> 1
6.44/1.96	, appendAll3_1(2) -> 1
6.44/1.96	, appendAll3_1(2) -> 6
6.44/1.96	, appendAll3_1(2) -> 8
6.44/1.96	, appendAll3#1_0(2) -> 1
6.44/1.96	, appendAll3#1_1(2) -> 1
6.44/1.96	, appendAll3#1_2(2) -> 1
6.44/1.96	, appendAll3#1_2(2) -> 6
6.44/1.96	, appendAll3#1_2(2) -> 8 }
6.44/1.96	
6.44/1.96	Hurray, we answered YES(?,O(n^1))
6.44/1.96	EOF