We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  half(0()) -> 0()
       , half(s(0())) -> 0()
       , half(s(s(x))) -> s(half(x))
       , lastbit(0()) -> 0()
       , lastbit(s(0())) -> s(0())
       , lastbit(s(s(x))) -> lastbit(x)
       , conv(0()) -> cons(nil(), 0())
       , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    The weightgap principle applies, where following rules are oriented strictly:
    
    TRS Component:
      {  half(0()) -> 0()
       , half(s(0())) -> 0()
       , lastbit(0()) -> 0()
       , lastbit(s(0())) -> s(0())}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
        Uargs(conv) = {1}, Uargs(cons) = {1, 2}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       half(x1) = [0 0] x1 + [1]
                  [0 0]      [1]
       0() = [0]
             [0]
       s(x1) = [1 0] x1 + [0]
               [0 0]      [1]
       lastbit(x1) = [0 0] x1 + [1]
                     [0 0]      [1]
       conv(x1) = [1 0] x1 + [1]
                  [0 0]      [1]
       cons(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                      [0 0]      [0 0]      [1]
       nil() = [0]
               [0]
    
    The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  half(s(s(x))) -> s(half(x))
         , lastbit(s(s(x))) -> lastbit(x)
         , conv(0()) -> cons(nil(), 0())
         , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
      Weak Trs:
        {  half(0()) -> 0()
         , half(s(0())) -> 0()
         , lastbit(0()) -> 0()
         , lastbit(s(0())) -> s(0())}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {conv(0()) -> cons(nil(), 0())}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
          Uargs(conv) = {1}, Uargs(cons) = {1, 2}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         half(x1) = [0 0] x1 + [1]
                    [0 0]      [1]
         0() = [0]
               [0]
         s(x1) = [1 0] x1 + [0]
                 [0 0]      [1]
         lastbit(x1) = [0 0] x1 + [1]
                       [0 0]      [1]
         conv(x1) = [1 0] x1 + [1]
                    [0 0]      [1]
         cons(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                        [0 0]      [0 0]      [1]
         nil() = [0]
                 [0]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs:
          {  half(s(s(x))) -> s(half(x))
           , lastbit(s(s(x))) -> lastbit(x)
           , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
        Weak Trs:
          {  conv(0()) -> cons(nil(), 0())
           , half(0()) -> 0()
           , half(s(0())) -> 0()
           , lastbit(0()) -> 0()
           , lastbit(s(0())) -> s(0())}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component: {lastbit(s(s(x))) -> lastbit(x)}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
            Uargs(conv) = {1}, Uargs(cons) = {1, 2}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           half(x1) = [1 0] x1 + [2]
                      [0 0]      [2]
           0() = [0]
                 [2]
           s(x1) = [1 0] x1 + [2]
                   [0 1]      [1]
           lastbit(x1) = [0 1] x1 + [0]
                         [0 0]      [3]
           conv(x1) = [1 2] x1 + [0]
                      [0 0]      [1]
           cons(x1, x2) = [1 0] x1 + [1 1] x2 + [1]
                          [0 0]      [0 0]      [1]
           nil() = [0]
                   [0]
        
        The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Strict Trs:
            {  half(s(s(x))) -> s(half(x))
             , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
          Weak Trs:
            {  lastbit(s(s(x))) -> lastbit(x)
             , conv(0()) -> cons(nil(), 0())
             , half(0()) -> 0()
             , half(s(0())) -> 0()
             , lastbit(0()) -> 0()
             , lastbit(s(0())) -> s(0())}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^1))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component: {half(s(s(x))) -> s(half(x))}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
              Uargs(conv) = {1}, Uargs(cons) = {1, 2}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             half(x1) = [1 0] x1 + [3]
                        [1 0]      [0]
             0() = [1]
                   [0]
             s(x1) = [1 0] x1 + [2]
                     [0 0]      [0]
             lastbit(x1) = [0 0] x1 + [3]
                           [0 0]      [1]
             conv(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
             cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                            [1 0]      [0 0]      [0]
             nil() = [0]
                     [0]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict Trs: {conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
            Weak Trs:
              {  half(s(s(x))) -> s(half(x))
               , lastbit(s(s(x))) -> lastbit(x)
               , conv(0()) -> cons(nil(), 0())
               , half(0()) -> 0()
               , half(s(0())) -> 0()
               , lastbit(0()) -> 0()
               , lastbit(s(0())) -> s(0())}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^1))
          
          Proof:
            We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
            
              The weightgap principle does not apply
            
            We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
            
            Strict Trs: {conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
            Weak Trs:
              {  half(s(s(x))) -> s(half(x))
               , lastbit(s(s(x))) -> lastbit(x)
               , conv(0()) -> cons(nil(), 0())
               , half(0()) -> 0()
               , half(s(0())) -> 0()
               , lastbit(0()) -> 0()
               , lastbit(s(0())) -> s(0())}
            StartTerms: basic terms
            Strategy: innermost
            
              The weightgap principle applies, where following rules are oriented strictly:
              
              TRS Component:
                {conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
              
              Interpretation of nonconstant growth:
              -------------------------------------
                The following argument positions are usable:
                  Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
                  Uargs(conv) = {1}, Uargs(cons) = {1, 2}
                We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                Interpretation Functions:
                 half(x1) = [0 0 0] x1 + [0]
                            [0 0 1]      [0]
                            [0 0 1]      [0]
                 0() = [0]
                       [0]
                       [0]
                 s(x1) = [1 0 0] x1 + [0]
                         [0 0 1]      [2]
                         [0 0 1]      [1]
                 lastbit(x1) = [0 0 0] x1 + [0]
                               [0 0 0]      [2]
                               [0 0 1]      [0]
                 conv(x1) = [1 2 0] x1 + [0]
                            [0 0 0]      [1]
                            [0 0 0]      [0]
                 cons(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
                                [0 0 0]      [0 0 0]      [1]
                                [0 0 0]      [0 0 0]      [0]
                 nil() = [0]
                         [0]
                         [0]
              
              The strictly oriented rules are moved into the weak component.
            
            We consider the following Problem:
            
              Weak Trs:
                {  conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
                 , half(s(s(x))) -> s(half(x))
                 , lastbit(s(s(x))) -> lastbit(x)
                 , conv(0()) -> cons(nil(), 0())
                 , half(0()) -> 0()
                 , half(s(0())) -> 0()
                 , lastbit(0()) -> 0()
                 , lastbit(s(0())) -> s(0())}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: YES(O(1),O(1))
            
            Proof:
              We consider the following Problem:
              
                Weak Trs:
                  {  conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
                   , half(s(s(x))) -> s(half(x))
                   , lastbit(s(s(x))) -> lastbit(x)
                   , conv(0()) -> cons(nil(), 0())
                   , half(0()) -> 0()
                   , half(s(0())) -> 0()
                   , lastbit(0()) -> 0()
                   , lastbit(s(0())) -> s(0())}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(O(1),O(1))
              
              Proof:
                Empty rules are trivially bounded

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