YES(O(1),O(n^2))
70.18/26.43	YES(O(1),O(n^2))
70.18/26.43	
70.18/26.43	We are left with following problem, upon which TcT provides the
70.18/26.43	certificate YES(O(1),O(n^2)).
70.18/26.43	
70.18/26.43	Strict Trs:
70.18/26.43	  { overlap(Nil(), ys) -> False()
70.18/26.43	  , overlap(Cons(x, xs), ys) ->
70.18/26.43	    overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
70.18/26.43	  , member(x, Nil()) -> False()
70.18/26.43	  , member(x', Cons(x, xs)) ->
70.18/26.43	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.43	  , notEmpty(Nil()) -> False()
70.18/26.43	  , notEmpty(Cons(x, xs)) -> True()
70.18/26.43	  , goal(xs, ys) -> overlap(xs, ys) }
70.18/26.43	Weak Trs:
70.18/26.43	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.43	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.43	    member(x', xs)
70.18/26.43	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.43	  , !EQ(S(x), 0()) -> False()
70.18/26.43	  , !EQ(0(), S(y)) -> False()
70.18/26.43	  , !EQ(0(), 0()) -> True()
70.18/26.43	  , overlap[Ite][True][Ite](True(), xs, ys) -> True()
70.18/26.43	  , overlap[Ite][True][Ite](False(), Cons(x, xs), ys) ->
70.18/26.43	    overlap(xs, ys) }
70.18/26.43	Obligation:
70.18/26.43	  innermost runtime complexity
70.18/26.43	Answer:
70.18/26.43	  YES(O(1),O(n^2))
70.18/26.43	
70.18/26.43	We add the following dependency tuples:
70.18/26.43	
70.18/26.43	Strict DPs:
70.18/26.43	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.43	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.43	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.43	        member^#(x, ys))
70.18/26.43	  , member^#(x, Nil()) -> c_3()
70.18/26.43	  , member^#(x', Cons(x, xs)) ->
70.18/26.43	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)),
70.18/26.43	        !EQ^#(x, x'))
70.18/26.43	  , notEmpty^#(Nil()) -> c_5()
70.18/26.43	  , notEmpty^#(Cons(x, xs)) -> c_6()
70.18/26.43	  , goal^#(xs, ys) -> c_7(overlap^#(xs, ys)) }
70.18/26.43	Weak DPs:
70.18/26.43	  { overlap[Ite][True][Ite]^#(True(), xs, ys) -> c_14()
70.18/26.43	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.43	    c_15(overlap^#(xs, ys))
70.18/26.43	  , member[Ite][True][Ite]^#(True(), x, xs) -> c_8()
70.18/26.43	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.43	    c_9(member^#(x', xs))
70.18/26.43	  , !EQ^#(S(x), S(y)) -> c_10(!EQ^#(x, y))
70.18/26.43	  , !EQ^#(S(x), 0()) -> c_11()
70.18/26.43	  , !EQ^#(0(), S(y)) -> c_12()
70.18/26.43	  , !EQ^#(0(), 0()) -> c_13() }
70.18/26.43	
70.18/26.43	and mark the set of starting terms.
70.18/26.43	
70.18/26.43	We are left with following problem, upon which TcT provides the
70.18/26.43	certificate YES(O(1),O(n^2)).
70.18/26.43	
70.18/26.43	Strict DPs:
70.18/26.43	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.43	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.43	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.43	        member^#(x, ys))
70.18/26.43	  , member^#(x, Nil()) -> c_3()
70.18/26.43	  , member^#(x', Cons(x, xs)) ->
70.18/26.43	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)),
70.18/26.43	        !EQ^#(x, x'))
70.18/26.43	  , notEmpty^#(Nil()) -> c_5()
70.18/26.43	  , notEmpty^#(Cons(x, xs)) -> c_6()
70.18/26.43	  , goal^#(xs, ys) -> c_7(overlap^#(xs, ys)) }
70.18/26.43	Weak DPs:
70.18/26.43	  { overlap[Ite][True][Ite]^#(True(), xs, ys) -> c_14()
70.18/26.43	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.43	    c_15(overlap^#(xs, ys))
70.18/26.43	  , member[Ite][True][Ite]^#(True(), x, xs) -> c_8()
70.18/26.43	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.43	    c_9(member^#(x', xs))
70.18/26.43	  , !EQ^#(S(x), S(y)) -> c_10(!EQ^#(x, y))
70.18/26.43	  , !EQ^#(S(x), 0()) -> c_11()
70.18/26.43	  , !EQ^#(0(), S(y)) -> c_12()
70.18/26.43	  , !EQ^#(0(), 0()) -> c_13() }
70.18/26.43	Weak Trs:
70.18/26.43	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.43	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.43	    member(x', xs)
70.18/26.43	  , overlap(Nil(), ys) -> False()
70.18/26.43	  , overlap(Cons(x, xs), ys) ->
70.18/26.43	    overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
70.18/26.43	  , member(x, Nil()) -> False()
70.18/26.43	  , member(x', Cons(x, xs)) ->
70.18/26.43	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.43	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.43	  , !EQ(S(x), 0()) -> False()
70.18/26.43	  , !EQ(0(), S(y)) -> False()
70.18/26.43	  , !EQ(0(), 0()) -> True()
70.18/26.43	  , notEmpty(Nil()) -> False()
70.18/26.43	  , notEmpty(Cons(x, xs)) -> True()
70.18/26.43	  , overlap[Ite][True][Ite](True(), xs, ys) -> True()
70.18/26.43	  , overlap[Ite][True][Ite](False(), Cons(x, xs), ys) ->
70.18/26.43	    overlap(xs, ys)
70.18/26.43	  , goal(xs, ys) -> overlap(xs, ys) }
70.18/26.43	Obligation:
70.18/26.43	  innermost runtime complexity
70.18/26.43	Answer:
70.18/26.43	  YES(O(1),O(n^2))
70.18/26.43	
70.18/26.43	We estimate the number of application of {5,6} by applications of
70.18/26.43	Pre({5,6}) = {}. Here rules are labeled as follows:
70.18/26.43	
70.18/26.43	  DPs:
70.18/26.43	    { 1: overlap^#(Nil(), ys) -> c_1()
70.18/26.43	    , 2: overlap^#(Cons(x, xs), ys) ->
70.18/26.43	         c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.43	             member^#(x, ys))
70.18/26.43	    , 3: member^#(x, Nil()) -> c_3()
70.18/26.43	    , 4: member^#(x', Cons(x, xs)) ->
70.18/26.43	         c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)),
70.18/26.43	             !EQ^#(x, x'))
70.18/26.43	    , 5: notEmpty^#(Nil()) -> c_5()
70.18/26.43	    , 6: notEmpty^#(Cons(x, xs)) -> c_6()
70.18/26.43	    , 7: goal^#(xs, ys) -> c_7(overlap^#(xs, ys))
70.18/26.43	    , 8: overlap[Ite][True][Ite]^#(True(), xs, ys) -> c_14()
70.18/26.43	    , 9: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.43	         c_15(overlap^#(xs, ys))
70.18/26.43	    , 10: member[Ite][True][Ite]^#(True(), x, xs) -> c_8()
70.18/26.43	    , 11: member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.43	          c_9(member^#(x', xs))
70.18/26.43	    , 12: !EQ^#(S(x), S(y)) -> c_10(!EQ^#(x, y))
70.18/26.43	    , 13: !EQ^#(S(x), 0()) -> c_11()
70.18/26.43	    , 14: !EQ^#(0(), S(y)) -> c_12()
70.18/26.43	    , 15: !EQ^#(0(), 0()) -> c_13() }
70.18/26.43	
70.18/26.43	We are left with following problem, upon which TcT provides the
70.18/26.43	certificate YES(O(1),O(n^2)).
70.18/26.43	
70.18/26.43	Strict DPs:
70.18/26.43	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.43	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.43	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.43	        member^#(x, ys))
70.18/26.43	  , member^#(x, Nil()) -> c_3()
70.18/26.43	  , member^#(x', Cons(x, xs)) ->
70.18/26.43	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)),
70.18/26.43	        !EQ^#(x, x'))
70.18/26.43	  , goal^#(xs, ys) -> c_7(overlap^#(xs, ys)) }
70.18/26.43	Weak DPs:
70.18/26.43	  { overlap[Ite][True][Ite]^#(True(), xs, ys) -> c_14()
70.18/26.43	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.43	    c_15(overlap^#(xs, ys))
70.18/26.43	  , member[Ite][True][Ite]^#(True(), x, xs) -> c_8()
70.18/26.43	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.43	    c_9(member^#(x', xs))
70.18/26.43	  , !EQ^#(S(x), S(y)) -> c_10(!EQ^#(x, y))
70.18/26.43	  , !EQ^#(S(x), 0()) -> c_11()
70.18/26.43	  , !EQ^#(0(), S(y)) -> c_12()
70.18/26.43	  , !EQ^#(0(), 0()) -> c_13()
70.18/26.43	  , notEmpty^#(Nil()) -> c_5()
70.18/26.43	  , notEmpty^#(Cons(x, xs)) -> c_6() }
70.18/26.43	Weak Trs:
70.18/26.43	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.43	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.43	    member(x', xs)
70.18/26.43	  , overlap(Nil(), ys) -> False()
70.18/26.43	  , overlap(Cons(x, xs), ys) ->
70.18/26.43	    overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
70.18/26.43	  , member(x, Nil()) -> False()
70.18/26.43	  , member(x', Cons(x, xs)) ->
70.18/26.43	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.43	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.43	  , !EQ(S(x), 0()) -> False()
70.18/26.43	  , !EQ(0(), S(y)) -> False()
70.18/26.43	  , !EQ(0(), 0()) -> True()
70.18/26.43	  , notEmpty(Nil()) -> False()
70.18/26.43	  , notEmpty(Cons(x, xs)) -> True()
70.18/26.43	  , overlap[Ite][True][Ite](True(), xs, ys) -> True()
70.18/26.43	  , overlap[Ite][True][Ite](False(), Cons(x, xs), ys) ->
70.18/26.43	    overlap(xs, ys)
70.18/26.43	  , goal(xs, ys) -> overlap(xs, ys) }
70.18/26.43	Obligation:
70.18/26.43	  innermost runtime complexity
70.18/26.43	Answer:
70.18/26.43	  YES(O(1),O(n^2))
70.18/26.43	
70.18/26.43	The following weak DPs constitute a sub-graph of the DG that is
70.18/26.43	closed under successors. The DPs are removed.
70.18/26.43	
70.18/26.43	{ overlap[Ite][True][Ite]^#(True(), xs, ys) -> c_14()
70.18/26.43	, member[Ite][True][Ite]^#(True(), x, xs) -> c_8()
70.18/26.43	, !EQ^#(S(x), S(y)) -> c_10(!EQ^#(x, y))
70.18/26.43	, !EQ^#(S(x), 0()) -> c_11()
70.18/26.43	, !EQ^#(0(), S(y)) -> c_12()
70.18/26.43	, !EQ^#(0(), 0()) -> c_13()
70.18/26.43	, notEmpty^#(Nil()) -> c_5()
70.18/26.43	, notEmpty^#(Cons(x, xs)) -> c_6() }
70.18/26.43	
70.18/26.43	We are left with following problem, upon which TcT provides the
70.18/26.43	certificate YES(O(1),O(n^2)).
70.18/26.43	
70.18/26.43	Strict DPs:
70.18/26.43	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.43	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.43	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.43	        member^#(x, ys))
70.18/26.43	  , member^#(x, Nil()) -> c_3()
70.18/26.43	  , member^#(x', Cons(x, xs)) ->
70.18/26.43	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)),
70.18/26.43	        !EQ^#(x, x'))
70.18/26.43	  , goal^#(xs, ys) -> c_7(overlap^#(xs, ys)) }
70.18/26.43	Weak DPs:
70.18/26.43	  { overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.43	    c_15(overlap^#(xs, ys))
70.18/26.43	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.43	    c_9(member^#(x', xs)) }
70.18/26.43	Weak Trs:
70.18/26.43	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.43	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.43	    member(x', xs)
70.18/26.43	  , overlap(Nil(), ys) -> False()
70.18/26.43	  , overlap(Cons(x, xs), ys) ->
70.18/26.43	    overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
70.18/26.43	  , member(x, Nil()) -> False()
70.18/26.43	  , member(x', Cons(x, xs)) ->
70.18/26.43	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.43	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.43	  , !EQ(S(x), 0()) -> False()
70.18/26.43	  , !EQ(0(), S(y)) -> False()
70.18/26.43	  , !EQ(0(), 0()) -> True()
70.18/26.43	  , notEmpty(Nil()) -> False()
70.18/26.43	  , notEmpty(Cons(x, xs)) -> True()
70.18/26.44	  , overlap[Ite][True][Ite](True(), xs, ys) -> True()
70.18/26.44	  , overlap[Ite][True][Ite](False(), Cons(x, xs), ys) ->
70.18/26.44	    overlap(xs, ys)
70.18/26.44	  , goal(xs, ys) -> overlap(xs, ys) }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	Due to missing edges in the dependency-graph, the right-hand sides
70.18/26.44	of following rules could be simplified:
70.18/26.44	
70.18/26.44	  { member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)),
70.18/26.44	        !EQ^#(x, x')) }
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.44	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , member^#(x, Nil()) -> c_3()
70.18/26.44	  , member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.44	  , goal^#(xs, ys) -> c_5(overlap^#(xs, ys)) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , overlap(Nil(), ys) -> False()
70.18/26.44	  , overlap(Cons(x, xs), ys) ->
70.18/26.44	    overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True()
70.18/26.44	  , notEmpty(Nil()) -> False()
70.18/26.44	  , notEmpty(Cons(x, xs)) -> True()
70.18/26.44	  , overlap[Ite][True][Ite](True(), xs, ys) -> True()
70.18/26.44	  , overlap[Ite][True][Ite](False(), Cons(x, xs), ys) ->
70.18/26.44	    overlap(xs, ys)
70.18/26.44	  , goal(xs, ys) -> overlap(xs, ys) }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	We replace rewrite rules by usable rules:
70.18/26.44	
70.18/26.44	  Weak Usable Rules:
70.18/26.44	    { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	    , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	      member(x', xs)
70.18/26.44	    , member(x, Nil()) -> False()
70.18/26.44	    , member(x', Cons(x, xs)) ->
70.18/26.44	      member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	    , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	    , !EQ(S(x), 0()) -> False()
70.18/26.44	    , !EQ(0(), S(y)) -> False()
70.18/26.44	    , !EQ(0(), 0()) -> True() }
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.44	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , member^#(x, Nil()) -> c_3()
70.18/26.44	  , member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.44	  , goal^#(xs, ys) -> c_5(overlap^#(xs, ys)) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True() }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	Consider the dependency graph
70.18/26.44	
70.18/26.44	  1: overlap^#(Nil(), ys) -> c_1()
70.18/26.44	  
70.18/26.44	  2: overlap^#(Cons(x, xs), ys) ->
70.18/26.44	     c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	         member^#(x, ys))
70.18/26.44	     -->_1 overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	           c_6(overlap^#(xs, ys)) :6
70.18/26.44	     -->_2 member^#(x', Cons(x, xs)) ->
70.18/26.44	           c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) :4
70.18/26.44	     -->_2 member^#(x, Nil()) -> c_3() :3
70.18/26.44	  
70.18/26.44	  3: member^#(x, Nil()) -> c_3()
70.18/26.44	  
70.18/26.44	  4: member^#(x', Cons(x, xs)) ->
70.18/26.44	     c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.44	     -->_1 member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	           c_7(member^#(x', xs)) :7
70.18/26.44	  
70.18/26.44	  5: goal^#(xs, ys) -> c_5(overlap^#(xs, ys))
70.18/26.44	     -->_1 overlap^#(Cons(x, xs), ys) ->
70.18/26.44	           c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	               member^#(x, ys)) :2
70.18/26.44	     -->_1 overlap^#(Nil(), ys) -> c_1() :1
70.18/26.44	  
70.18/26.44	  6: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	     c_6(overlap^#(xs, ys))
70.18/26.44	     -->_1 overlap^#(Cons(x, xs), ys) ->
70.18/26.44	           c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	               member^#(x, ys)) :2
70.18/26.44	     -->_1 overlap^#(Nil(), ys) -> c_1() :1
70.18/26.44	  
70.18/26.44	  7: member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	     c_7(member^#(x', xs))
70.18/26.44	     -->_1 member^#(x', Cons(x, xs)) ->
70.18/26.44	           c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) :4
70.18/26.44	     -->_1 member^#(x, Nil()) -> c_3() :3
70.18/26.44	  
70.18/26.44	
70.18/26.44	Following roots of the dependency graph are removed, as the
70.18/26.44	considered set of starting terms is closed under reduction with
70.18/26.44	respect to these rules (modulo compound contexts).
70.18/26.44	
70.18/26.44	  { goal^#(xs, ys) -> c_5(overlap^#(xs, ys)) }
70.18/26.44	
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.44	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , member^#(x, Nil()) -> c_3()
70.18/26.44	  , member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True() }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	We use the processor 'matrix interpretation of dimension 1' to
70.18/26.44	orient following rules strictly.
70.18/26.44	
70.18/26.44	DPs:
70.18/26.44	  { 5: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	       c_6(overlap^#(xs, ys)) }
70.18/26.44	
70.18/26.44	Sub-proof:
70.18/26.44	----------
70.18/26.44	  The following argument positions are usable:
70.18/26.44	    Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1},
70.18/26.44	    Uargs(c_7) = {1}
70.18/26.44	  
70.18/26.44	  TcT has computed the following constructor-based matrix
70.18/26.44	  interpretation satisfying not(EDA).
70.18/26.44	  
70.18/26.44	                                     [True] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                      [Nil] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	       [member[Ite][True][Ite]](x1, x2, x3) = [3] x2 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                           [member](x1, x2) = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                              [!EQ](x1, x2) = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                    [S](x1) = [1] x1 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                             [Cons](x1, x2) = [1] x2 + [4]         
70.18/26.44	                                                                   
70.18/26.44	                                        [0] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                    [False] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                        [overlap^#](x1, x2) = [2] x1 + [0]         
70.18/26.44	                                                                   
70.18/26.44	    [overlap[Ite][True][Ite]^#](x1, x2, x3) = [2] x2 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                         [member^#](x1, x2) = [0]                  
70.18/26.44	                                                                   
70.18/26.44	     [member[Ite][True][Ite]^#](x1, x2, x3) = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                      [c_1] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                              [c_2](x1, x2) = [1] x1 + [4] x2 + [0]
70.18/26.44	                                                                   
70.18/26.44	                                      [c_3] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                  [c_4](x1) = [2] x1 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                                  [c_6](x1) = [1] x1 + [5]         
70.18/26.44	                                                                   
70.18/26.44	                                  [c_7](x1) = [4] x1 + [0]         
70.18/26.44	  
70.18/26.44	  The order satisfies the following ordering constraints:
70.18/26.44	  
70.18/26.44	                  [member[Ite][True][Ite](True(), x, xs)] =  [3] x + [0]                                                    
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [True()]                                                       
70.18/26.44	                                                                                                                            
70.18/26.44	       [member[Ite][True][Ite](False(), x', Cons(x, xs))] =  [3] x' + [0]                                                   
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [member(x', xs)]                                               
70.18/26.44	                                                                                                                            
70.18/26.44	                                       [member(x, Nil())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [False()]                                                      
70.18/26.44	                                                                                                                            
70.18/26.44	                                [member(x', Cons(x, xs))] =  [0]                                                            
70.18/26.44	                                                          ?  [3] x' + [0]                                                   
70.18/26.44	                                                          =  [member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))]          
70.18/26.44	                                                                                                                            
70.18/26.44	                                        [!EQ(S(x), S(y))] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [!EQ(x, y)]                                                    
70.18/26.44	                                                                                                                            
70.18/26.44	                                         [!EQ(S(x), 0())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [False()]                                                      
70.18/26.44	                                                                                                                            
70.18/26.44	                                         [!EQ(0(), S(y))] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [False()]                                                      
70.18/26.44	                                                                                                                            
70.18/26.44	                                          [!EQ(0(), 0())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [True()]                                                       
70.18/26.44	                                                                                                                            
70.18/26.44	                                   [overlap^#(Nil(), ys)] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [c_1()]                                                        
70.18/26.44	                                                                                                                            
70.18/26.44	                             [overlap^#(Cons(x, xs), ys)] =  [2] xs + [8]                                                   
70.18/26.44	                                                          >= [2] xs + [8]                                                   
70.18/26.44	                                                          =  [c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	                                                                  member^#(x, ys))]                                         
70.18/26.44	                                                                                                                            
70.18/26.44	    [overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys)] =  [2] xs + [8]                                                   
70.18/26.44	                                                          >  [2] xs + [5]                                                   
70.18/26.44	                                                          =  [c_6(overlap^#(xs, ys))]                                       
70.18/26.44	                                                                                                                            
70.18/26.44	                                     [member^#(x, Nil())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [c_3()]                                                        
70.18/26.44	                                                                                                                            
70.18/26.44	                              [member^#(x', Cons(x, xs))] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))]   
70.18/26.44	                                                                                                                            
70.18/26.44	     [member[Ite][True][Ite]^#(False(), x', Cons(x, xs))] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [c_7(member^#(x', xs))]                                        
70.18/26.44	                                                                                                                            
70.18/26.44	
70.18/26.44	We return to the main proof. Consider the set of all dependency
70.18/26.44	pairs
70.18/26.44	
70.18/26.44	:
70.18/26.44	  { 1: overlap^#(Nil(), ys) -> c_1()
70.18/26.44	  , 2: overlap^#(Cons(x, xs), ys) ->
70.18/26.44	       c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	           member^#(x, ys))
70.18/26.44	  , 3: member^#(x, Nil()) -> c_3()
70.18/26.44	  , 4: member^#(x', Cons(x, xs)) ->
70.18/26.44	       c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.44	  , 5: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	       c_6(overlap^#(xs, ys))
70.18/26.44	  , 6: member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	       c_7(member^#(x', xs)) }
70.18/26.44	
70.18/26.44	Processor 'matrix interpretation of dimension 1' induces the
70.18/26.44	complexity certificate YES(?,O(n^1)) on application of dependency
70.18/26.44	pairs {5}. These cover all (indirect) predecessors of dependency
70.18/26.44	pairs {1,2,5}, their number of application is equally bounded. The
70.18/26.44	dependency pairs are shifted into the weak component.
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { member^#(x, Nil()) -> c_3()
70.18/26.44	  , member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap^#(Nil(), ys) -> c_1()
70.18/26.44	  , overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True() }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	The following weak DPs constitute a sub-graph of the DG that is
70.18/26.44	closed under successors. The DPs are removed.
70.18/26.44	
70.18/26.44	{ overlap^#(Nil(), ys) -> c_1() }
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { member^#(x, Nil()) -> c_3()
70.18/26.44	  , member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True() }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	We use the processor 'matrix interpretation of dimension 1' to
70.18/26.44	orient following rules strictly.
70.18/26.44	
70.18/26.44	DPs:
70.18/26.44	  { 1: member^#(x, Nil()) -> c_3() }
70.18/26.44	
70.18/26.44	Sub-proof:
70.18/26.44	----------
70.18/26.44	  The following argument positions are usable:
70.18/26.44	    Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1},
70.18/26.44	    Uargs(c_7) = {1}
70.18/26.44	  
70.18/26.44	  TcT has computed the following constructor-based matrix
70.18/26.44	  interpretation satisfying not(EDA).
70.18/26.44	  
70.18/26.44	                                     [True] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                      [Nil] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	       [member[Ite][True][Ite]](x1, x2, x3) = [3] x2 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                           [member](x1, x2) = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                              [!EQ](x1, x2) = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                    [S](x1) = [1] x1 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                             [Cons](x1, x2) = [1] x2 + [1]         
70.18/26.44	                                                                   
70.18/26.44	                                        [0] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                    [False] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                        [overlap^#](x1, x2) = [1] x1 + [2]         
70.18/26.44	                                                                   
70.18/26.44	    [overlap[Ite][True][Ite]^#](x1, x2, x3) = [1] x2 + [1]         
70.18/26.44	                                                                   
70.18/26.44	                         [member^#](x1, x2) = [1]                  
70.18/26.44	                                                                   
70.18/26.44	     [member[Ite][True][Ite]^#](x1, x2, x3) = [1]                  
70.18/26.44	                                                                   
70.18/26.44	                                      [c_1] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                              [c_2](x1, x2) = [1] x1 + [1] x2 + [0]
70.18/26.44	                                                                   
70.18/26.44	                                      [c_3] = [0]                  
70.18/26.44	                                                                   
70.18/26.44	                                  [c_4](x1) = [1] x1 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                                  [c_6](x1) = [1] x1 + [0]         
70.18/26.44	                                                                   
70.18/26.44	                                  [c_7](x1) = [1] x1 + [0]         
70.18/26.44	  
70.18/26.44	  The order satisfies the following ordering constraints:
70.18/26.44	  
70.18/26.44	                  [member[Ite][True][Ite](True(), x, xs)] =  [3] x + [0]                                                    
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [True()]                                                       
70.18/26.44	                                                                                                                            
70.18/26.44	       [member[Ite][True][Ite](False(), x', Cons(x, xs))] =  [3] x' + [0]                                                   
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [member(x', xs)]                                               
70.18/26.44	                                                                                                                            
70.18/26.44	                                       [member(x, Nil())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [False()]                                                      
70.18/26.44	                                                                                                                            
70.18/26.44	                                [member(x', Cons(x, xs))] =  [0]                                                            
70.18/26.44	                                                          ?  [3] x' + [0]                                                   
70.18/26.44	                                                          =  [member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))]          
70.18/26.44	                                                                                                                            
70.18/26.44	                                        [!EQ(S(x), S(y))] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [!EQ(x, y)]                                                    
70.18/26.44	                                                                                                                            
70.18/26.44	                                         [!EQ(S(x), 0())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [False()]                                                      
70.18/26.44	                                                                                                                            
70.18/26.44	                                         [!EQ(0(), S(y))] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [False()]                                                      
70.18/26.44	                                                                                                                            
70.18/26.44	                                          [!EQ(0(), 0())] =  [0]                                                            
70.18/26.44	                                                          >= [0]                                                            
70.18/26.44	                                                          =  [True()]                                                       
70.18/26.44	                                                                                                                            
70.18/26.44	                             [overlap^#(Cons(x, xs), ys)] =  [1] xs + [3]                                                   
70.18/26.44	                                                          >= [1] xs + [3]                                                   
70.18/26.44	                                                          =  [c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	                                                                  member^#(x, ys))]                                         
70.18/26.44	                                                                                                                            
70.18/26.44	    [overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys)] =  [1] xs + [2]                                                   
70.18/26.44	                                                          >= [1] xs + [2]                                                   
70.18/26.44	                                                          =  [c_6(overlap^#(xs, ys))]                                       
70.18/26.44	                                                                                                                            
70.18/26.44	                                     [member^#(x, Nil())] =  [1]                                                            
70.18/26.44	                                                          >  [0]                                                            
70.18/26.44	                                                          =  [c_3()]                                                        
70.18/26.44	                                                                                                                            
70.18/26.44	                              [member^#(x', Cons(x, xs))] =  [1]                                                            
70.18/26.44	                                                          >= [1]                                                            
70.18/26.44	                                                          =  [c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))]   
70.18/26.44	                                                                                                                            
70.18/26.44	     [member[Ite][True][Ite]^#(False(), x', Cons(x, xs))] =  [1]                                                            
70.18/26.44	                                                          >= [1]                                                            
70.18/26.44	                                                          =  [c_7(member^#(x', xs))]                                        
70.18/26.44	                                                                                                                            
70.18/26.44	
70.18/26.44	The strictly oriented rules are moved into the weak component.
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member^#(x, Nil()) -> c_3()
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True() }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	The following weak DPs constitute a sub-graph of the DG that is
70.18/26.44	closed under successors. The DPs are removed.
70.18/26.44	
70.18/26.44	{ member^#(x, Nil()) -> c_3() }
70.18/26.44	
70.18/26.44	We are left with following problem, upon which TcT provides the
70.18/26.44	certificate YES(O(1),O(n^2)).
70.18/26.44	
70.18/26.44	Strict DPs:
70.18/26.44	  { member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) }
70.18/26.44	Weak DPs:
70.18/26.44	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	Weak Trs:
70.18/26.44	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	    member(x', xs)
70.18/26.44	  , member(x, Nil()) -> False()
70.18/26.44	  , member(x', Cons(x, xs)) ->
70.18/26.44	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	  , !EQ(S(x), 0()) -> False()
70.18/26.44	  , !EQ(0(), S(y)) -> False()
70.18/26.44	  , !EQ(0(), 0()) -> True() }
70.18/26.44	Obligation:
70.18/26.44	  innermost runtime complexity
70.18/26.44	Answer:
70.18/26.44	  YES(O(1),O(n^2))
70.18/26.44	
70.18/26.44	We decompose the input problem according to the dependency graph
70.18/26.44	into the upper component
70.18/26.44	
70.18/26.44	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.44	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	        member^#(x, ys))
70.18/26.44	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	    c_6(overlap^#(xs, ys)) }
70.18/26.44	
70.18/26.44	and lower component
70.18/26.44	
70.18/26.44	  { member^#(x', Cons(x, xs)) ->
70.18/26.44	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.44	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.44	    c_7(member^#(x', xs)) }
70.18/26.44	
70.18/26.44	Further, following extension rules are added to the lower
70.18/26.44	component.
70.18/26.44	
70.18/26.44	{ overlap^#(Cons(x, xs), ys) ->
70.18/26.44	  overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys)
70.18/26.44	, overlap^#(Cons(x, xs), ys) -> member^#(x, ys)
70.18/26.44	, overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	  overlap^#(xs, ys) }
70.18/26.44	
70.18/26.44	TcT solves the upper component with certificate YES(O(1),O(n^1)).
70.18/26.44	
70.18/26.44	Sub-proof:
70.18/26.44	----------
70.18/26.44	  We are left with following problem, upon which TcT provides the
70.18/26.44	  certificate YES(O(1),O(n^1)).
70.18/26.44	  
70.18/26.44	  Strict DPs:
70.18/26.44	    { overlap^#(Cons(x, xs), ys) ->
70.18/26.44	      c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	          member^#(x, ys)) }
70.18/26.44	  Weak DPs:
70.18/26.44	    { overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	      c_6(overlap^#(xs, ys)) }
70.18/26.44	  Weak Trs:
70.18/26.44	    { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.44	    , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.44	      member(x', xs)
70.18/26.44	    , member(x, Nil()) -> False()
70.18/26.44	    , member(x', Cons(x, xs)) ->
70.18/26.44	      member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.44	    , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.44	    , !EQ(S(x), 0()) -> False()
70.18/26.44	    , !EQ(0(), S(y)) -> False()
70.18/26.44	    , !EQ(0(), 0()) -> True() }
70.18/26.44	  Obligation:
70.18/26.44	    innermost runtime complexity
70.18/26.44	  Answer:
70.18/26.44	    YES(O(1),O(n^1))
70.18/26.44	  
70.18/26.44	  We use the processor 'matrix interpretation of dimension 1' to
70.18/26.44	  orient following rules strictly.
70.18/26.44	  
70.18/26.44	  DPs:
70.18/26.44	    { 2: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.44	         c_6(overlap^#(xs, ys)) }
70.18/26.44	  
70.18/26.44	  Sub-proof:
70.18/26.44	  ----------
70.18/26.44	    The following argument positions are usable:
70.18/26.44	      Uargs(c_2) = {1}, Uargs(c_6) = {1}
70.18/26.44	    
70.18/26.44	    TcT has computed the following constructor-based matrix
70.18/26.44	    interpretation satisfying not(EDA).
70.18/26.44	    
70.18/26.44	                                       [True] = [0]                  
70.18/26.44	                                                                     
70.18/26.44	                                        [Nil] = [7]                  
70.18/26.44	                                                                     
70.18/26.44	         [member[Ite][True][Ite]](x1, x2, x3) = [3] x2 + [0]         
70.18/26.44	                                                                     
70.18/26.44	                             [member](x1, x2) = [0]                  
70.18/26.44	                                                                     
70.18/26.44	                                [!EQ](x1, x2) = [0]                  
70.18/26.44	                                                                     
70.18/26.44	                                      [S](x1) = [1] x1 + [0]         
70.18/26.44	                                                                     
70.18/26.44	                               [Cons](x1, x2) = [1] x2 + [1]         
70.18/26.44	                                                                     
70.18/26.44	                                          [0] = [0]                  
70.18/26.44	                                                                     
70.18/26.44	                                      [False] = [0]                  
70.18/26.44	                                                                     
70.18/26.44	                          [overlap^#](x1, x2) = [1] x1 + [0]         
70.18/26.44	                                                                     
70.18/26.44	      [overlap[Ite][True][Ite]^#](x1, x2, x3) = [1] x2 + [0]         
70.18/26.44	                                                                     
70.18/26.44	                           [member^#](x1, x2) = [7] x1 + [7] x2 + [7]
70.18/26.44	                                                                     
70.18/26.44	                                [c_2](x1, x2) = [1] x1 + [0]         
70.18/26.44	                                                                     
70.18/26.44	                                    [c_6](x1) = [1] x1 + [0]         
70.18/26.44	    
70.18/26.44	    The order satisfies the following ordering constraints:
70.18/26.44	    
70.18/26.44	                    [member[Ite][True][Ite](True(), x, xs)] =  [3] x + [0]                                                    
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [True()]                                                       
70.18/26.44	                                                                                                                              
70.18/26.44	         [member[Ite][True][Ite](False(), x', Cons(x, xs))] =  [3] x' + [0]                                                   
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [member(x', xs)]                                               
70.18/26.44	                                                                                                                              
70.18/26.44	                                         [member(x, Nil())] =  [0]                                                            
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [False()]                                                      
70.18/26.44	                                                                                                                              
70.18/26.44	                                  [member(x', Cons(x, xs))] =  [0]                                                            
70.18/26.44	                                                            ?  [3] x' + [0]                                                   
70.18/26.44	                                                            =  [member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))]          
70.18/26.44	                                                                                                                              
70.18/26.44	                                          [!EQ(S(x), S(y))] =  [0]                                                            
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [!EQ(x, y)]                                                    
70.18/26.44	                                                                                                                              
70.18/26.44	                                           [!EQ(S(x), 0())] =  [0]                                                            
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [False()]                                                      
70.18/26.44	                                                                                                                              
70.18/26.44	                                           [!EQ(0(), S(y))] =  [0]                                                            
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [False()]                                                      
70.18/26.44	                                                                                                                              
70.18/26.44	                                            [!EQ(0(), 0())] =  [0]                                                            
70.18/26.44	                                                            >= [0]                                                            
70.18/26.44	                                                            =  [True()]                                                       
70.18/26.44	                                                                                                                              
70.18/26.44	                               [overlap^#(Cons(x, xs), ys)] =  [1] xs + [1]                                                   
70.18/26.44	                                                            >= [1] xs + [1]                                                   
70.18/26.44	                                                            =  [c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.44	                                                                    member^#(x, ys))]                                         
70.18/26.44	                                                                                                                              
70.18/26.44	      [overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys)] =  [1] xs + [1]                                                   
70.18/26.44	                                                            >  [1] xs + [0]                                                   
70.18/26.44	                                                            =  [c_6(overlap^#(xs, ys))]                                       
70.18/26.44	                                                                                                                              
70.18/26.45	  
70.18/26.45	  We return to the main proof. Consider the set of all dependency
70.18/26.45	  pairs
70.18/26.45	  
70.18/26.45	  :
70.18/26.45	    { 1: overlap^#(Cons(x, xs), ys) ->
70.18/26.45	         c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.45	             member^#(x, ys))
70.18/26.45	    , 2: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	         c_6(overlap^#(xs, ys)) }
70.18/26.45	  
70.18/26.45	  Processor 'matrix interpretation of dimension 1' induces the
70.18/26.45	  complexity certificate YES(?,O(n^1)) on application of dependency
70.18/26.45	  pairs {2}. These cover all (indirect) predecessors of dependency
70.18/26.45	  pairs {1,2}, their number of application is equally bounded. The
70.18/26.45	  dependency pairs are shifted into the weak component.
70.18/26.45	  
70.18/26.45	  We are left with following problem, upon which TcT provides the
70.18/26.45	  certificate YES(O(1),O(1)).
70.18/26.45	  
70.18/26.45	  Weak DPs:
70.18/26.45	    { overlap^#(Cons(x, xs), ys) ->
70.18/26.45	      c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.45	          member^#(x, ys))
70.18/26.45	    , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	      c_6(overlap^#(xs, ys)) }
70.18/26.45	  Weak Trs:
70.18/26.45	    { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.45	    , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.45	      member(x', xs)
70.18/26.45	    , member(x, Nil()) -> False()
70.18/26.45	    , member(x', Cons(x, xs)) ->
70.18/26.45	      member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.45	    , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.45	    , !EQ(S(x), 0()) -> False()
70.18/26.45	    , !EQ(0(), S(y)) -> False()
70.18/26.45	    , !EQ(0(), 0()) -> True() }
70.18/26.45	  Obligation:
70.18/26.45	    innermost runtime complexity
70.18/26.45	  Answer:
70.18/26.45	    YES(O(1),O(1))
70.18/26.45	  
70.18/26.45	  The following weak DPs constitute a sub-graph of the DG that is
70.18/26.45	  closed under successors. The DPs are removed.
70.18/26.45	  
70.18/26.45	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.45	    c_2(overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys),
70.18/26.45	        member^#(x, ys))
70.18/26.45	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	    c_6(overlap^#(xs, ys)) }
70.18/26.45	  
70.18/26.45	  We are left with following problem, upon which TcT provides the
70.18/26.45	  certificate YES(O(1),O(1)).
70.18/26.45	  
70.18/26.45	  Weak Trs:
70.18/26.45	    { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.45	    , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.45	      member(x', xs)
70.18/26.45	    , member(x, Nil()) -> False()
70.18/26.45	    , member(x', Cons(x, xs)) ->
70.18/26.45	      member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.45	    , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.45	    , !EQ(S(x), 0()) -> False()
70.18/26.45	    , !EQ(0(), S(y)) -> False()
70.18/26.45	    , !EQ(0(), 0()) -> True() }
70.18/26.45	  Obligation:
70.18/26.45	    innermost runtime complexity
70.18/26.45	  Answer:
70.18/26.45	    YES(O(1),O(1))
70.18/26.45	  
70.18/26.45	  No rule is usable, rules are removed from the input problem.
70.18/26.45	  
70.18/26.45	  We are left with following problem, upon which TcT provides the
70.18/26.45	  certificate YES(O(1),O(1)).
70.18/26.45	  
70.18/26.45	  Rules: Empty
70.18/26.45	  Obligation:
70.18/26.45	    innermost runtime complexity
70.18/26.45	  Answer:
70.18/26.45	    YES(O(1),O(1))
70.18/26.45	  
70.18/26.45	  Empty rules are trivially bounded
70.18/26.45	
70.18/26.45	We return to the main proof.
70.18/26.45	
70.18/26.45	We are left with following problem, upon which TcT provides the
70.18/26.45	certificate YES(O(1),O(n^1)).
70.18/26.45	
70.18/26.45	Strict DPs:
70.18/26.45	  { member^#(x', Cons(x, xs)) ->
70.18/26.45	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs))) }
70.18/26.45	Weak DPs:
70.18/26.45	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.45	    overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys)
70.18/26.45	  , overlap^#(Cons(x, xs), ys) -> member^#(x, ys)
70.18/26.45	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	    overlap^#(xs, ys)
70.18/26.45	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.45	    c_7(member^#(x', xs)) }
70.18/26.45	Weak Trs:
70.18/26.45	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.45	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.45	    member(x', xs)
70.18/26.45	  , member(x, Nil()) -> False()
70.18/26.45	  , member(x', Cons(x, xs)) ->
70.18/26.45	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.45	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.45	  , !EQ(S(x), 0()) -> False()
70.18/26.45	  , !EQ(0(), S(y)) -> False()
70.18/26.45	  , !EQ(0(), 0()) -> True() }
70.18/26.45	Obligation:
70.18/26.45	  innermost runtime complexity
70.18/26.45	Answer:
70.18/26.45	  YES(O(1),O(n^1))
70.18/26.45	
70.18/26.45	We use the processor 'matrix interpretation of dimension 1' to
70.18/26.45	orient following rules strictly.
70.18/26.45	
70.18/26.45	DPs:
70.18/26.45	  { 1: member^#(x', Cons(x, xs)) ->
70.18/26.45	       c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.45	  , 3: overlap^#(Cons(x, xs), ys) -> member^#(x, ys)
70.18/26.45	  , 4: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	       overlap^#(xs, ys)
70.18/26.45	  , 5: member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.45	       c_7(member^#(x', xs)) }
70.18/26.45	
70.18/26.45	Sub-proof:
70.18/26.45	----------
70.18/26.45	  The following argument positions are usable:
70.18/26.45	    Uargs(c_4) = {1}, Uargs(c_7) = {1}
70.18/26.45	  
70.18/26.45	  TcT has computed the following constructor-based matrix
70.18/26.45	  interpretation satisfying not(EDA).
70.18/26.45	  
70.18/26.45	                                     [True] = [0]                  
70.18/26.45	                                                                   
70.18/26.45	                                      [Nil] = [7]                  
70.18/26.45	                                                                   
70.18/26.45	       [member[Ite][True][Ite]](x1, x2, x3) = [3] x2 + [0]         
70.18/26.45	                                                                   
70.18/26.45	                           [member](x1, x2) = [0]                  
70.18/26.45	                                                                   
70.18/26.45	                              [!EQ](x1, x2) = [0]                  
70.18/26.45	                                                                   
70.18/26.45	                                    [S](x1) = [1] x1 + [0]         
70.18/26.45	                                                                   
70.18/26.45	                             [Cons](x1, x2) = [1] x2 + [4]         
70.18/26.45	                                                                   
70.18/26.45	                                        [0] = [0]                  
70.18/26.45	                                                                   
70.18/26.45	                                    [False] = [0]                  
70.18/26.45	                                                                   
70.18/26.45	                        [overlap^#](x1, x2) = [2] x1 + [7] x2 + [0]
70.18/26.45	                                                                   
70.18/26.45	    [overlap[Ite][True][Ite]^#](x1, x2, x3) = [2] x2 + [7] x3 + [0]
70.18/26.45	                                                                   
70.18/26.45	                         [member^#](x1, x2) = [2] x2 + [4]         
70.18/26.45	                                                                   
70.18/26.45	     [member[Ite][True][Ite]^#](x1, x2, x3) = [2] x3 + [0]         
70.18/26.45	                                                                   
70.18/26.45	                                  [c_4](x1) = [1] x1 + [3]         
70.18/26.45	                                                                   
70.18/26.45	                                  [c_7](x1) = [1] x1 + [1]         
70.18/26.45	  
70.18/26.45	  The order satisfies the following ordering constraints:
70.18/26.45	  
70.18/26.45	                  [member[Ite][True][Ite](True(), x, xs)] =  [3] x + [0]                                                 
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [True()]                                                    
70.18/26.45	                                                                                                                         
70.18/26.45	       [member[Ite][True][Ite](False(), x', Cons(x, xs))] =  [3] x' + [0]                                                
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [member(x', xs)]                                            
70.18/26.45	                                                                                                                         
70.18/26.45	                                       [member(x, Nil())] =  [0]                                                         
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [False()]                                                   
70.18/26.45	                                                                                                                         
70.18/26.45	                                [member(x', Cons(x, xs))] =  [0]                                                         
70.18/26.45	                                                          ?  [3] x' + [0]                                                
70.18/26.45	                                                          =  [member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))]       
70.18/26.45	                                                                                                                         
70.18/26.45	                                        [!EQ(S(x), S(y))] =  [0]                                                         
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [!EQ(x, y)]                                                 
70.18/26.45	                                                                                                                         
70.18/26.45	                                         [!EQ(S(x), 0())] =  [0]                                                         
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [False()]                                                   
70.18/26.45	                                                                                                                         
70.18/26.45	                                         [!EQ(0(), S(y))] =  [0]                                                         
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [False()]                                                   
70.18/26.45	                                                                                                                         
70.18/26.45	                                          [!EQ(0(), 0())] =  [0]                                                         
70.18/26.45	                                                          >= [0]                                                         
70.18/26.45	                                                          =  [True()]                                                    
70.18/26.45	                                                                                                                         
70.18/26.45	                             [overlap^#(Cons(x, xs), ys)] =  [2] xs + [7] ys + [8]                                       
70.18/26.45	                                                          >= [2] xs + [7] ys + [8]                                       
70.18/26.45	                                                          =  [overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys)] 
70.18/26.45	                                                                                                                         
70.18/26.45	                             [overlap^#(Cons(x, xs), ys)] =  [2] xs + [7] ys + [8]                                       
70.18/26.45	                                                          >  [2] ys + [4]                                                
70.18/26.45	                                                          =  [member^#(x, ys)]                                           
70.18/26.45	                                                                                                                         
70.18/26.45	    [overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys)] =  [2] xs + [7] ys + [8]                                       
70.18/26.45	                                                          >  [2] xs + [7] ys + [0]                                       
70.18/26.45	                                                          =  [overlap^#(xs, ys)]                                         
70.18/26.45	                                                                                                                         
70.18/26.45	                              [member^#(x', Cons(x, xs))] =  [2] xs + [12]                                               
70.18/26.45	                                                          >  [2] xs + [11]                                               
70.18/26.45	                                                          =  [c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))]
70.18/26.45	                                                                                                                         
70.18/26.45	     [member[Ite][True][Ite]^#(False(), x', Cons(x, xs))] =  [2] xs + [8]                                                
70.18/26.45	                                                          >  [2] xs + [5]                                                
70.18/26.45	                                                          =  [c_7(member^#(x', xs))]                                     
70.18/26.45	                                                                                                                         
70.18/26.45	
70.18/26.45	We return to the main proof. Consider the set of all dependency
70.18/26.45	pairs
70.18/26.45	
70.18/26.45	:
70.18/26.45	  { 1: member^#(x', Cons(x, xs)) ->
70.18/26.45	       c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.45	  , 2: overlap^#(Cons(x, xs), ys) ->
70.18/26.45	       overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys)
70.18/26.45	  , 3: overlap^#(Cons(x, xs), ys) -> member^#(x, ys)
70.18/26.45	  , 4: overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	       overlap^#(xs, ys)
70.18/26.45	  , 5: member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.45	       c_7(member^#(x', xs)) }
70.18/26.45	
70.18/26.45	Processor 'matrix interpretation of dimension 1' induces the
70.18/26.45	complexity certificate YES(?,O(n^1)) on application of dependency
70.18/26.45	pairs {1,3,4,5}. These cover all (indirect) predecessors of
70.18/26.45	dependency pairs {1,2,3,4,5}, their number of application is
70.18/26.45	equally bounded. The dependency pairs are shifted into the weak
70.18/26.45	component.
70.18/26.45	
70.18/26.45	We are left with following problem, upon which TcT provides the
70.18/26.45	certificate YES(O(1),O(1)).
70.18/26.45	
70.18/26.45	Weak DPs:
70.18/26.45	  { overlap^#(Cons(x, xs), ys) ->
70.18/26.45	    overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys)
70.18/26.45	  , overlap^#(Cons(x, xs), ys) -> member^#(x, ys)
70.18/26.45	  , overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	    overlap^#(xs, ys)
70.18/26.45	  , member^#(x', Cons(x, xs)) ->
70.18/26.45	    c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.45	  , member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.45	    c_7(member^#(x', xs)) }
70.18/26.45	Weak Trs:
70.18/26.45	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.45	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.45	    member(x', xs)
70.18/26.45	  , member(x, Nil()) -> False()
70.18/26.45	  , member(x', Cons(x, xs)) ->
70.18/26.45	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.45	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.45	  , !EQ(S(x), 0()) -> False()
70.18/26.45	  , !EQ(0(), S(y)) -> False()
70.18/26.45	  , !EQ(0(), 0()) -> True() }
70.18/26.45	Obligation:
70.18/26.45	  innermost runtime complexity
70.18/26.45	Answer:
70.18/26.45	  YES(O(1),O(1))
70.18/26.45	
70.18/26.45	The following weak DPs constitute a sub-graph of the DG that is
70.18/26.45	closed under successors. The DPs are removed.
70.18/26.45	
70.18/26.45	{ overlap^#(Cons(x, xs), ys) ->
70.18/26.45	  overlap[Ite][True][Ite]^#(member(x, ys), Cons(x, xs), ys)
70.18/26.45	, overlap^#(Cons(x, xs), ys) -> member^#(x, ys)
70.18/26.45	, overlap[Ite][True][Ite]^#(False(), Cons(x, xs), ys) ->
70.18/26.45	  overlap^#(xs, ys)
70.18/26.45	, member^#(x', Cons(x, xs)) ->
70.18/26.45	  c_4(member[Ite][True][Ite]^#(!EQ(x, x'), x', Cons(x, xs)))
70.18/26.45	, member[Ite][True][Ite]^#(False(), x', Cons(x, xs)) ->
70.18/26.45	  c_7(member^#(x', xs)) }
70.18/26.45	
70.18/26.45	We are left with following problem, upon which TcT provides the
70.18/26.45	certificate YES(O(1),O(1)).
70.18/26.45	
70.18/26.45	Weak Trs:
70.18/26.45	  { member[Ite][True][Ite](True(), x, xs) -> True()
70.18/26.45	  , member[Ite][True][Ite](False(), x', Cons(x, xs)) ->
70.18/26.45	    member(x', xs)
70.18/26.45	  , member(x, Nil()) -> False()
70.18/26.45	  , member(x', Cons(x, xs)) ->
70.18/26.45	    member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
70.18/26.45	  , !EQ(S(x), S(y)) -> !EQ(x, y)
70.18/26.45	  , !EQ(S(x), 0()) -> False()
70.18/26.45	  , !EQ(0(), S(y)) -> False()
70.18/26.45	  , !EQ(0(), 0()) -> True() }
70.18/26.45	Obligation:
70.18/26.45	  innermost runtime complexity
70.18/26.45	Answer:
70.18/26.45	  YES(O(1),O(1))
70.18/26.45	
70.18/26.45	No rule is usable, rules are removed from the input problem.
70.18/26.45	
70.18/26.45	We are left with following problem, upon which TcT provides the
70.18/26.45	certificate YES(O(1),O(1)).
70.18/26.45	
70.18/26.45	Rules: Empty
70.18/26.45	Obligation:
70.18/26.45	  innermost runtime complexity
70.18/26.45	Answer:
70.18/26.45	  YES(O(1),O(1))
70.18/26.45	
70.18/26.45	Empty rules are trivially bounded
70.18/26.45	
70.18/26.45	Hurray, we answered YES(O(1),O(n^2))
70.34/26.51	EOF