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

Strict Trs:
  { f(0()) -> true()
  , f(1()) -> false()
  , f(s(x)) -> f(x)
  , if(true(), x, y) -> x
  , if(false(), x, y) -> y
  , g(x, c(y)) -> g(x, g(s(c(y)), y))
  , g(s(x), s(y)) -> if(f(x), s(x), s(y)) }
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(if) = {1}, Uargs(g) = {2}

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

           [f](x1) = [0]                           
                                                   
               [0] = [0]                           
                                                   
            [true] = [0]                           
                                                   
               [1] = [0]                           
                                                   
           [false] = [4]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
                                                   
       [g](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                   
           [c](x1) = [1] x1 + [0]                  

The order satisfies the following ordering constraints:

             [f(0())] =  [0]                   
                      >= [0]                   
                      =  [true()]              
                                               
             [f(1())] =  [0]                   
                      ?  [4]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [0]                   
                      >= [0]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [1]   
                      >  [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [5]   
                      >  [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] x + [1] y + [0]   
                      >= [1] x + [1] y + [0]   
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [0]                   
                      ?  [1]                   
                      =  [if(f(x), s(x), s(y))]
                                               

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(n^1)).

Strict Trs:
  { f(0()) -> true()
  , f(1()) -> false()
  , f(s(x)) -> f(x)
  , g(x, c(y)) -> g(x, g(s(c(y)), y))
  , g(s(x), s(y)) -> if(f(x), s(x), s(y)) }
Weak Trs:
  { if(true(), x, y) -> x
  , if(false(), x, y) -> y }
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(if) = {1}, Uargs(g) = {2}

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

           [f](x1) = [1]                           
                                                   
               [0] = [0]                           
                                                   
            [true] = [0]                           
                                                   
               [1] = [0]                           
                                                   
           [false] = [0]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
                                                   
       [g](x1, x2) = [1] x2 + [0]                  
                                                   
           [c](x1) = [1] x1 + [2]                  

The order satisfies the following ordering constraints:

             [f(0())] =  [1]                   
                      >  [0]                   
                      =  [true()]              
                                               
             [f(1())] =  [1]                   
                      >  [0]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [1]                   
                      >= [1]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [0]   
                      >= [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [0]   
                      >= [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] y + [2]           
                      >  [1] y + [0]           
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [0]                   
                      ?  [1]                   
                      =  [if(f(x), s(x), s(y))]
                                               

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(n^1)).

Strict Trs:
  { f(s(x)) -> f(x)
  , g(s(x), s(y)) -> if(f(x), s(x), s(y)) }
Weak Trs:
  { f(0()) -> true()
  , f(1()) -> false()
  , if(true(), x, y) -> x
  , if(false(), x, y) -> y
  , g(x, c(y)) -> g(x, g(s(c(y)), y)) }
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(if) = {1}, Uargs(g) = {2}

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

           [f](x1) = [1]                           
                                                   
               [0] = [0]                           
                                                   
            [true] = [0]                           
                                                   
               [1] = [0]                           
                                                   
           [false] = [0]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
                                                   
       [g](x1, x2) = [1] x2 + [4]                  
                                                   
           [c](x1) = [1] x1 + [7]                  

The order satisfies the following ordering constraints:

             [f(0())] =  [1]                   
                      >  [0]                   
                      =  [true()]              
                                               
             [f(1())] =  [1]                   
                      >  [0]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [1]                   
                      >= [1]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [0]   
                      >= [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [0]   
                      >= [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] y + [11]          
                      >  [1] y + [8]           
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [4]                   
                      >  [1]                   
                      =  [if(f(x), s(x), s(y))]
                                               

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(n^1)).

Strict Trs: { f(s(x)) -> f(x) }
Weak Trs:
  { f(0()) -> true()
  , f(1()) -> false()
  , if(true(), x, y) -> x
  , if(false(), x, y) -> y
  , g(x, c(y)) -> g(x, g(s(c(y)), y))
  , g(s(x), s(y)) -> if(f(x), s(x), s(y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

Trs: { f(s(x)) -> f(x) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(if) = {1}, Uargs(g) = {2}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA) and not(IDA(1)).
  
             [f](x1) = [0 1] x1 + [0]                      
                       [0 5]      [4]                      
                                                           
                 [0] = [0]                                 
                       [0]                                 
                                                           
              [true] = [0]                                 
                       [0]                                 
                                                           
                 [1] = [0]                                 
                       [0]                                 
                                                           
             [false] = [0]                                 
                       [0]                                 
                                                           
             [s](x1) = [0 4] x1 + [0]                      
                       [0 1]      [1]                      
                                                           
    [if](x1, x2, x3) = [2 0] x1 + [2 0] x2 + [1 0] x3 + [0]
                       [0 2]      [0 1]      [0 4]      [0]
                                                           
         [g](x1, x2) = [3 1] x1 + [1 0] x2 + [0]           
                       [1 7]      [1 0]      [6]           
                                                           
             [c](x1) = [1 0] x1 + [7]                      
                       [0 0]      [0]                      
  
  The order satisfies the following ordering constraints:
  
               [f(0())] =  [0]                      
                           [4]                      
                        >= [0]                      
                           [0]                      
                        =  [true()]                 
                                                    
               [f(1())] =  [0]                      
                           [4]                      
                        >= [0]                      
                           [0]                      
                        =  [false()]                
                                                    
              [f(s(x))] =  [0 1] x + [1]            
                           [0 5]     [9]            
                        >  [0 1] x + [0]            
                           [0 5]     [4]            
                        =  [f(x)]                   
                                                    
     [if(true(), x, y)] =  [2 0] x + [1 0] y + [0]  
                           [0 1]     [0 4]     [0]  
                        >= [1 0] x + [0]            
                           [0 1]     [0]            
                        =  [x]                      
                                                    
    [if(false(), x, y)] =  [2 0] x + [1 0] y + [0]  
                           [0 1]     [0 4]     [0]  
                        >= [1 0] y + [0]            
                           [0 1]     [0]            
                        =  [y]                      
                                                    
           [g(x, c(y))] =  [3 1] x + [1 0] y + [7]  
                           [1 7]     [1 0]     [13] 
                        >  [3 1] x + [1 0] y + [1]  
                           [1 7]     [1 0]     [7]  
                        =  [g(x, g(s(c(y)), y))]    
                                                    
        [g(s(x), s(y))] =  [0 13] x + [0 4] y + [1] 
                           [0 11]     [0 4]     [13]
                        >  [0 10] x + [0 4] y + [0] 
                           [0 11]     [0 4]     [13]
                        =  [if(f(x), s(x), s(y))]   
                                                    

We return to the main proof.

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

Weak Trs:
  { f(0()) -> true()
  , f(1()) -> false()
  , f(s(x)) -> f(x)
  , if(true(), x, y) -> x
  , if(false(), x, y) -> y
  , g(x, c(y)) -> g(x, g(s(c(y)), y))
  , g(s(x), s(y)) -> if(f(x), s(x), s(y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

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