YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { loop(Cons(x', xs'), Cons(x, xs), pp, ss) ->
    loop[Ite][False][Ite][False][Ite](!EQ(x', x),
                                      Cons(x', xs'),
                                      Cons(x, xs),
                                      pp,
                                      ss)
  , loop(Cons(x, xs), Nil(), pp, ss) -> False()
  , loop(Nil(), s, pp, ss) -> True()
  , match1(p, s) -> loop(p, s, p, s) }
Weak Trs:
  { !EQ(S(x), S(y)) -> !EQ(x, y)
  , !EQ(S(x), 0()) -> False()
  , !EQ(0(), S(y)) -> False()
  , !EQ(0(), 0()) -> True() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(loop[Ite][False][Ite][False][Ite]) = {1}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

                                            [!EQ](x1, x2) = [1] x1 + [1] x2 + [1]
                                                                                 
                                                   [True] = [7]                  
                                                                                 
                                                  [S](x1) = [1] x1 + [7]         
                                                                                 
                                   [loop](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1]
                                                                                 
                                           [Cons](x1, x2) = [1] x1 + [1] x2 + [7]
                                                                                 
                                                    [Nil] = [7]                  
                                                                                 
                                                      [0] = [7]                  
                                                                                 
  [loop[Ite][False][Ite][False][Ite]](x1, x2, x3, x4, x5) = [1] x1 + [7]         
                                                                                 
                                                  [False] = [6]                  
                                                                                 
                                         [match1](x1, x2) = [1] x1 + [1] x2 + [7]

The following symbols are considered usable

  {!EQ, loop, match1}

The order satisfies the following ordering constraints:

                           [!EQ(S(x), S(y))] = [1] x + [1] y + [15]                             
                                             > [1] x + [1] y + [1]                              
                                             = [!EQ(x, y)]                                      
                                                                                                
                            [!EQ(S(x), 0())] = [1] x + [15]                                     
                                             > [6]                                              
                                             = [False()]                                        
                                                                                                
                            [!EQ(0(), S(y))] = [1] y + [15]                                     
                                             > [6]                                              
                                             = [False()]                                        
                                                                                                
                             [!EQ(0(), 0())] = [15]                                             
                                             > [7]                                              
                                             = [True()]                                         
                                                                                                
  [loop(Cons(x', xs'), Cons(x, xs), pp, ss)] = [1] x + [1] xs + [1] x' + [1] xs' + [15]         
                                             > [1] x + [1] x' + [8]                             
                                             = [loop[Ite][False][Ite][False][Ite](!EQ(x', x),   
                                                                                  Cons(x', xs'),
                                                                                  Cons(x, xs),  
                                                                                  pp,           
                                                                                  ss)]          
                                                                                                
          [loop(Cons(x, xs), Nil(), pp, ss)] = [1] x + [1] xs + [15]                            
                                             > [6]                                              
                                             = [False()]                                        
                                                                                                
                    [loop(Nil(), s, pp, ss)] = [1] s + [8]                                      
                                             > [7]                                              
                                             = [True()]                                         
                                                                                                
                              [match1(p, s)] = [1] s + [1] p + [7]                              
                                             > [1] s + [1] p + [1]                              
                                             = [loop(p, s, p, s)]                               
                                                                                                

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { !EQ(S(x), S(y)) -> !EQ(x, y)
  , !EQ(S(x), 0()) -> False()
  , !EQ(0(), S(y)) -> False()
  , !EQ(0(), 0()) -> True()
  , loop(Cons(x', xs'), Cons(x, xs), pp, ss) ->
    loop[Ite][False][Ite][False][Ite](!EQ(x', x),
                                      Cons(x', xs'),
                                      Cons(x, xs),
                                      pp,
                                      ss)
  , loop(Cons(x, xs), Nil(), pp, ss) -> False()
  , loop(Nil(), s, pp, ss) -> True()
  , match1(p, s) -> loop(p, s, p, s) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))