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:
  { 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] = [7]                           
                                                   
            [true] = [7]                           
                                                   
               [1] = [7]                           
                                                   
           [false] = [5]                           
                                                   
           [s](x1) = [7]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
                                                   
       [g](x1, x2) = [1] x1 + [1] x2 + [1]         
                                                   
           [c](x1) = [1] x1 + [7]                  

The following symbols are considered usable

  {f, if, g}

The order satisfies the following ordering constraints:

             [f(0())] =  [0]                   
                      ?  [7]                   
                      =  [true()]              
                                               
             [f(1())] =  [0]                   
                      ?  [5]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [0]                   
                      >= [0]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [8]   
                      >  [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [6]   
                      >  [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] x + [1] y + [8]   
                      ?  [1] x + [1] y + [9]   
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [15]                  
                      >= [15]                  
                      =  [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) = [0]                           
                                                   
               [0] = [7]                           
                                                   
            [true] = [3]                           
                                                   
               [1] = [7]                           
                                                   
           [false] = [7]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3]
                                                   
       [g](x1, x2) = [1] x2 + [0]                  
                                                   
           [c](x1) = [1] x1 + [7]                  

The following symbols are considered usable

  {f, if, g}

The order satisfies the following ordering constraints:

             [f(0())] =  [0]                   
                      ?  [3]                   
                      =  [true()]              
                                               
             [f(1())] =  [0]                   
                      ?  [7]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [0]                   
                      >= [0]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [6]   
                      >  [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [10]  
                      >  [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] y + [7]           
                      >  [1] y + [0]           
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [0]                   
                      ?  [3]                   
                      =  [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(s(x), s(y)) -> if(f(x), s(x), s(y)) }
Weak Trs:
  { 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] = [7]                           
                                                   
            [true] = [6]                           
                                                   
               [1] = [7]                           
                                                   
           [false] = [0]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [6]
                                                   
       [g](x1, x2) = [1] x2 + [0]                  
                                                   
           [c](x1) = [1] x1 + [7]                  

The following symbols are considered usable

  {f, if, g}

The order satisfies the following ordering constraints:

             [f(0())] =  [1]                   
                      ?  [6]                   
                      =  [true()]              
                                               
             [f(1())] =  [1]                   
                      >  [0]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [1]                   
                      >= [1]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [12]  
                      >  [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [6]   
                      >  [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] y + [7]           
                      >  [1] y + [0]           
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [0]                   
                      ?  [7]                   
                      =  [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(s(x)) -> f(x)
  , g(s(x), s(y)) -> if(f(x), s(x), s(y)) }
Weak Trs:
  { 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] = [7]                           
                                                   
            [true] = [0]                           
                                                   
               [1] = [7]                           
                                                   
           [false] = [1]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
                                                   
       [g](x1, x2) = [1] x2 + [0]                  
                                                   
           [c](x1) = [1] x1 + [7]                  

The following symbols are considered usable

  {f, if, g}

The order satisfies the following ordering constraints:

             [f(0())] =  [1]                   
                      >  [0]                   
                      =  [true()]              
                                               
             [f(1())] =  [1]                   
                      >= [1]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [1]                   
                      >= [1]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [2]   
                      >  [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [3]   
                      >  [1] y + [0]           
                      =  [y]                   
                                               
         [g(x, c(y))] =  [1] y + [7]           
                      >  [1] y + [0]           
                      =  [g(x, g(s(c(y)), y))] 
                                               
      [g(s(x), s(y))] =  [0]                   
                      ?  [3]                   
                      =  [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] = [7]                           
                                                   
            [true] = [1]                           
                                                   
               [1] = [7]                           
                                                   
           [false] = [1]                           
                                                   
           [s](x1) = [0]                           
                                                   
  [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
                                                   
       [g](x1, x2) = [1] x2 + [4]                  
                                                   
           [c](x1) = [1] x1 + [7]                  

The following symbols are considered usable

  {f, if, g}

The order satisfies the following ordering constraints:

             [f(0())] =  [1]                   
                      >= [1]                   
                      =  [true()]              
                                               
             [f(1())] =  [1]                   
                      >= [1]                   
                      =  [false()]             
                                               
            [f(s(x))] =  [1]                   
                      >= [1]                   
                      =  [f(x)]                
                                               
   [if(true(), x, y)] =  [1] x + [1] y + [3]   
                      >  [1] x + [0]           
                      =  [x]                   
                                               
  [if(false(), x, y)] =  [1] x + [1] y + [3]   
                      >  [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]                   
                      >  [3]                   
                      =  [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 + [4]                      
                       [0 1]      [0]                      
                                                           
                 [0] = [0]                                 
                       [4]                                 
                                                           
              [true] = [0]                                 
                       [0]                                 
                                                           
                 [1] = [0]                                 
                       [4]                                 
                                                           
             [false] = [0]                                 
                       [0]                                 
                                                           
             [s](x1) = [0 1] x1 + [0]                      
                       [0 1]      [1]                      
                                                           
    [if](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [1 0] x3 + [0]
                       [0 1]      [1 2]      [0 1]      [0]
                                                           
         [g](x1, x2) = [0 4] x1 + [1 0] x2 + [0]           
                       [2 2]      [1 0]      [1]           
                                                           
             [c](x1) = [1 0] x1 + [7]                      
                       [0 0]      [0]                      
  
  The following symbols are considered usable
  
    {f, if, g}
  
  The order satisfies the following ordering constraints:
  
               [f(0())] =  [8]                    
                           [4]                    
                        >  [0]                    
                           [0]                    
                        =  [true()]               
                                                  
               [f(1())] =  [8]                    
                           [4]                    
                        >  [0]                    
                           [0]                    
                        =  [false()]              
                                                  
              [f(s(x))] =  [0 1] x + [5]          
                           [0 1]     [1]          
                        >  [0 1] x + [4]          
                           [0 1]     [0]          
                        =  [f(x)]                 
                                                  
     [if(true(), x, y)] =  [1 0] x + [1 0] y + [0]
                           [1 2]     [0 1]     [0]
                        >= [1 0] x + [0]          
                           [0 1]     [0]          
                        =  [x]                    
                                                  
    [if(false(), x, y)] =  [1 0] x + [1 0] y + [0]
                           [1 2]     [0 1]     [0]
                        >= [1 0] y + [0]          
                           [0 1]     [0]          
                        =  [y]                    
                                                  
           [g(x, c(y))] =  [0 4] x + [1 0] y + [7]
                           [2 2]     [1 0]     [8]
                        >  [0 4] x + [1 0] y + [4]
                           [2 2]     [1 0]     [5]
                        =  [g(x, g(s(c(y)), y))]  
                                                  
        [g(s(x), s(y))] =  [0 4] x + [0 1] y + [4]
                           [0 4]     [0 1]     [3]
                        >= [0 3] x + [0 1] y + [4]
                           [0 4]     [0 1]     [3]
                        =  [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))