YES(O(1),O(n^1))
0.00/0.41	YES(O(1),O(n^1))
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(n^1)).
0.00/0.41	
0.00/0.41	Strict Trs:
0.00/0.41	  { loop(Cons(x', xs'), Cons(x, xs), pp, ss) ->
0.00/0.41	    loop[Ite][False][Ite][False][Ite](!EQ(x', x),
0.00/0.41	                                      Cons(x', xs'),
0.00/0.41	                                      Cons(x, xs),
0.00/0.41	                                      pp,
0.00/0.41	                                      ss)
0.00/0.41	  , loop(Cons(x, xs), Nil(), pp, ss) -> False()
0.00/0.41	  , loop(Nil(), s, pp, ss) -> True()
0.00/0.41	  , match1(p, s) -> loop(p, s, p, s) }
0.00/0.41	Weak Trs:
0.00/0.41	  { !EQ(S(x), S(y)) -> !EQ(x, y)
0.00/0.41	  , !EQ(S(x), 0()) -> False()
0.00/0.41	  , !EQ(0(), S(y)) -> False()
0.00/0.41	  , !EQ(0(), 0()) -> True() }
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(n^1))
0.00/0.41	
0.00/0.41	We add the following weak dependency pairs:
0.00/0.41	
0.00/0.41	Strict DPs:
0.00/0.41	  { loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	  , loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	  , loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	  , match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	Weak DPs:
0.00/0.41	  { !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	  , !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	  , !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	  , !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	
0.00/0.41	and mark the set of starting terms.
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(n^1)).
0.00/0.41	
0.00/0.41	Strict DPs:
0.00/0.41	  { loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	  , loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	  , loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	  , match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	Strict Trs:
0.00/0.41	  { loop(Cons(x', xs'), Cons(x, xs), pp, ss) ->
0.00/0.41	    loop[Ite][False][Ite][False][Ite](!EQ(x', x),
0.00/0.41	                                      Cons(x', xs'),
0.00/0.41	                                      Cons(x, xs),
0.00/0.41	                                      pp,
0.00/0.41	                                      ss)
0.00/0.41	  , loop(Cons(x, xs), Nil(), pp, ss) -> False()
0.00/0.41	  , loop(Nil(), s, pp, ss) -> True()
0.00/0.41	  , match1(p, s) -> loop(p, s, p, s) }
0.00/0.41	Weak DPs:
0.00/0.41	  { !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	  , !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	  , !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	  , !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	Weak Trs:
0.00/0.41	  { !EQ(S(x), S(y)) -> !EQ(x, y)
0.00/0.41	  , !EQ(S(x), 0()) -> False()
0.00/0.41	  , !EQ(0(), S(y)) -> False()
0.00/0.41	  , !EQ(0(), 0()) -> True() }
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(n^1))
0.00/0.41	
0.00/0.41	No rule is usable, rules are removed from the input problem.
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(n^1)).
0.00/0.41	
0.00/0.41	Strict DPs:
0.00/0.41	  { loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	  , loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	  , loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	  , match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	Weak DPs:
0.00/0.41	  { !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	  , !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	  , !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	  , !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(n^1))
0.00/0.41	
0.00/0.41	The weightgap principle applies (using the following constant
0.00/0.41	growth matrix-interpretation)
0.00/0.41	
0.00/0.41	The following argument positions are usable:
0.00/0.41	  Uargs(c_1) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}
0.00/0.41	
0.00/0.41	TcT has computed the following constructor-restricted matrix
0.00/0.41	interpretation.
0.00/0.41	
0.00/0.41	                   [S](x1) = [1 0] x1 + [0]           
0.00/0.41	                             [0 0]      [0]           
0.00/0.41	                                                      
0.00/0.41	            [Cons](x1, x2) = [1 0] x1 + [0]           
0.00/0.41	                             [0 0]      [0]           
0.00/0.41	                                                      
0.00/0.41	                     [Nil] = [0]                      
0.00/0.41	                             [0]                      
0.00/0.41	                                                      
0.00/0.41	                       [0] = [0]                      
0.00/0.41	                             [0]                      
0.00/0.41	                                                      
0.00/0.41	  [loop^#](x1, x2, x3, x4) = [1 1] x3 + [1 1] x4 + [2]
0.00/0.41	                             [2 2]      [2 2]      [0]
0.00/0.41	                                                      
0.00/0.41	                 [c_1](x1) = [1 0] x1 + [1]           
0.00/0.41	                             [0 1]      [1]           
0.00/0.41	                                                      
0.00/0.41	           [!EQ^#](x1, x2) = [0]                      
0.00/0.41	                             [1]                      
0.00/0.41	                                                      
0.00/0.41	                     [c_2] = [1]                      
0.00/0.41	                             [0]                      
0.00/0.41	                                                      
0.00/0.41	                     [c_3] = [1]                      
0.00/0.41	                             [0]                      
0.00/0.41	                                                      
0.00/0.41	        [match1^#](x1, x2) = [1 1] x1 + [2 2] x2 + [2]
0.00/0.41	                             [2 2]      [2 2]      [2]
0.00/0.41	                                                      
0.00/0.41	                 [c_4](x1) = [1 0] x1 + [1]           
0.00/0.41	                             [0 1]      [2]           
0.00/0.41	                                                      
0.00/0.41	                 [c_5](x1) = [1 0] x1 + [0]           
0.00/0.41	                             [0 1]      [0]           
0.00/0.41	                                                      
0.00/0.41	                     [c_6] = [0]                      
0.00/0.41	                             [1]                      
0.00/0.41	                                                      
0.00/0.41	                     [c_7] = [0]                      
0.00/0.41	                             [1]                      
0.00/0.41	                                                      
0.00/0.41	                     [c_8] = [0]                      
0.00/0.41	                             [1]                      
0.00/0.41	
0.00/0.41	The order satisfies the following ordering constraints:
0.00/0.41	
0.00/0.41	  [loop^#(Cons(x', xs'), Cons(x, xs), pp, ss)] =  [1 1] pp + [1 1] ss + [2]
0.00/0.41	                                                  [2 2]      [2 2]      [0]
0.00/0.41	                                               ?  [1]                      
0.00/0.41	                                                  [2]                      
0.00/0.41	                                               =  [c_1(!EQ^#(x', x))]      
0.00/0.41	                                                                           
0.00/0.41	          [loop^#(Cons(x, xs), Nil(), pp, ss)] =  [1 1] pp + [1 1] ss + [2]
0.00/0.41	                                                  [2 2]      [2 2]      [0]
0.00/0.41	                                               >  [1]                      
0.00/0.41	                                                  [0]                      
0.00/0.41	                                               =  [c_2()]                  
0.00/0.41	                                                                           
0.00/0.41	                    [loop^#(Nil(), s, pp, ss)] =  [1 1] pp + [1 1] ss + [2]
0.00/0.41	                                                  [2 2]      [2 2]      [0]
0.00/0.41	                                               >  [1]                      
0.00/0.41	                                                  [0]                      
0.00/0.41	                                               =  [c_3()]                  
0.00/0.41	                                                                           
0.00/0.41	                           [!EQ^#(S(x), S(y))] =  [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               >= [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               =  [c_5(!EQ^#(x, y))]       
0.00/0.41	                                                                           
0.00/0.41	                            [!EQ^#(S(x), 0())] =  [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               >= [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               =  [c_6()]                  
0.00/0.41	                                                                           
0.00/0.41	                            [!EQ^#(0(), S(y))] =  [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               >= [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               =  [c_7()]                  
0.00/0.41	                                                                           
0.00/0.41	                             [!EQ^#(0(), 0())] =  [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               >= [0]                      
0.00/0.41	                                                  [1]                      
0.00/0.41	                                               =  [c_8()]                  
0.00/0.41	                                                                           
0.00/0.41	                              [match1^#(p, s)] =  [2 2] s + [1 1] p + [2]  
0.00/0.41	                                                  [2 2]     [2 2]     [2]  
0.00/0.41	                                               ?  [1 1] s + [1 1] p + [3]  
0.00/0.41	                                                  [2 2]     [2 2]     [2]  
0.00/0.41	                                               =  [c_4(loop^#(p, s, p, s))]
0.00/0.41	                                                                           
0.00/0.41	
0.00/0.41	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(1)).
0.00/0.41	
0.00/0.41	Strict DPs:
0.00/0.41	  { loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	  , match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	Weak DPs:
0.00/0.41	  { loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	  , loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	  , !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	  , !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	  , !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	  , !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(1))
0.00/0.41	
0.00/0.41	We estimate the number of application of {1} by applications of
0.00/0.41	Pre({1}) = {2}. Here rules are labeled as follows:
0.00/0.41	
0.00/0.41	  DPs:
0.00/0.41	    { 1: loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) ->
0.00/0.41	         c_1(!EQ^#(x', x))
0.00/0.41	    , 2: match1^#(p, s) -> c_4(loop^#(p, s, p, s))
0.00/0.41	    , 3: loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	    , 4: loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	    , 5: !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	    , 6: !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	    , 7: !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	    , 8: !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(1)).
0.00/0.41	
0.00/0.41	Strict DPs: { match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	Weak DPs:
0.00/0.41	  { loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	  , loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	  , loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	  , !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	  , !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	  , !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	  , !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(1))
0.00/0.41	
0.00/0.41	We estimate the number of application of {1} by applications of
0.00/0.41	Pre({1}) = {}. Here rules are labeled as follows:
0.00/0.41	
0.00/0.41	  DPs:
0.00/0.41	    { 1: match1^#(p, s) -> c_4(loop^#(p, s, p, s))
0.00/0.41	    , 2: loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) ->
0.00/0.41	         c_1(!EQ^#(x', x))
0.00/0.41	    , 3: loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	    , 4: loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	    , 5: !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	    , 6: !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	    , 7: !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	    , 8: !EQ^#(0(), 0()) -> c_8() }
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(1)).
0.00/0.41	
0.00/0.41	Weak DPs:
0.00/0.41	  { loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	  , loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	  , loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	  , !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	  , !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	  , !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	  , !EQ^#(0(), 0()) -> c_8()
0.00/0.41	  , match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(1))
0.00/0.41	
0.00/0.41	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.41	closed under successors. The DPs are removed.
0.00/0.41	
0.00/0.41	{ loop^#(Cons(x', xs'), Cons(x, xs), pp, ss) -> c_1(!EQ^#(x', x))
0.00/0.41	, loop^#(Cons(x, xs), Nil(), pp, ss) -> c_2()
0.00/0.41	, loop^#(Nil(), s, pp, ss) -> c_3()
0.00/0.41	, !EQ^#(S(x), S(y)) -> c_5(!EQ^#(x, y))
0.00/0.41	, !EQ^#(S(x), 0()) -> c_6()
0.00/0.41	, !EQ^#(0(), S(y)) -> c_7()
0.00/0.41	, !EQ^#(0(), 0()) -> c_8()
0.00/0.41	, match1^#(p, s) -> c_4(loop^#(p, s, p, s)) }
0.00/0.41	
0.00/0.41	We are left with following problem, upon which TcT provides the
0.00/0.41	certificate YES(O(1),O(1)).
0.00/0.41	
0.00/0.41	Rules: Empty
0.00/0.41	Obligation:
0.00/0.41	  innermost runtime complexity
0.00/0.41	Answer:
0.00/0.41	  YES(O(1),O(1))
0.00/0.41	
0.00/0.41	Empty rules are trivially bounded
0.00/0.41	
0.00/0.41	Hurray, we answered YES(O(1),O(n^1))
0.00/0.41	EOF