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:
  { not(true()) -> false()
  , not(false()) -> true()
  , odd(0()) -> false()
  , odd(s(x)) -> not(odd(x))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , +(s(x), y) -> s(+(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add following weak dependency pairs:

Strict DPs:
  { not^#(true()) -> c_1()
  , not^#(false()) -> c_2()
  , odd^#(0()) -> c_3()
  , odd^#(s(x)) -> c_4(not^#(odd(x)))
  , +^#(x, 0()) -> c_5()
  , +^#(x, s(y)) -> c_6(+^#(x, y))
  , +^#(s(x), y) -> c_7(+^#(x, y)) }

and mark the set of starting terms.

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

Strict DPs:
  { not^#(true()) -> c_1()
  , not^#(false()) -> c_2()
  , odd^#(0()) -> c_3()
  , odd^#(s(x)) -> c_4(not^#(odd(x)))
  , +^#(x, 0()) -> c_5()
  , +^#(x, s(y)) -> c_6(+^#(x, y))
  , +^#(s(x), y) -> c_7(+^#(x, y)) }
Strict Trs:
  { not(true()) -> false()
  , not(false()) -> true()
  , odd(0()) -> false()
  , odd(s(x)) -> not(odd(x))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , +(s(x), y) -> s(+(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { not(true()) -> false()
    , not(false()) -> true()
    , odd(0()) -> false()
    , odd(s(x)) -> not(odd(x)) }

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

Strict DPs:
  { not^#(true()) -> c_1()
  , not^#(false()) -> c_2()
  , odd^#(0()) -> c_3()
  , odd^#(s(x)) -> c_4(not^#(odd(x)))
  , +^#(x, 0()) -> c_5()
  , +^#(x, s(y)) -> c_6(+^#(x, y))
  , +^#(s(x), y) -> c_7(+^#(x, y)) }
Strict Trs:
  { not(true()) -> false()
  , not(false()) -> true()
  , odd(0()) -> false()
  , odd(s(x)) -> not(odd(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

The following argument positions are usable:
  Uargs(not) = {1}, Uargs(not^#) = {1}, Uargs(c_4) = {1},
  Uargs(c_6) = {1}, Uargs(c_7) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

      [not](x1) = [1] x1 + [2]         
                                       
         [true] = [2]                  
                                       
        [false] = [2]                  
                                       
      [odd](x1) = [2] x1 + [0]         
                                       
            [0] = [2]                  
                                       
        [s](x1) = [1] x1 + [2]         
                                       
    [not^#](x1) = [1] x1 + [2]         
                                       
          [c_1] = [1]                  
                                       
          [c_2] = [1]                  
                                       
    [odd^#](x1) = [2] x1 + [2]         
                                       
          [c_3] = [1]                  
                                       
      [c_4](x1) = [1] x1 + [2]         
                                       
  [+^#](x1, x2) = [1] x1 + [1] x2 + [2]
                                       
          [c_5] = [1]                  
                                       
      [c_6](x1) = [1] x1 + [1]         
                                       
      [c_7](x1) = [1] x1 + [1]         

This order satisfies following ordering constraints:

   [not(true())] = [4]          
                 > [2]          
                 = [false()]    
                                
  [not(false())] = [4]          
                 > [2]          
                 = [true()]     
                                
      [odd(0())] = [4]          
                 > [2]          
                 = [false()]    
                                
     [odd(s(x))] = [2] x + [4]  
                 > [2] x + [2]  
                 = [not(odd(x))]
                                

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)).

Weak DPs:
  { not^#(true()) -> c_1()
  , not^#(false()) -> c_2()
  , odd^#(0()) -> c_3()
  , odd^#(s(x)) -> c_4(not^#(odd(x)))
  , +^#(x, 0()) -> c_5()
  , +^#(x, s(y)) -> c_6(+^#(x, y))
  , +^#(s(x), y) -> c_7(+^#(x, y)) }
Weak Trs:
  { not(true()) -> false()
  , not(false()) -> true()
  , odd(0()) -> false()
  , odd(s(x)) -> not(odd(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ not^#(true()) -> c_1()
, not^#(false()) -> c_2()
, odd^#(0()) -> c_3()
, odd^#(s(x)) -> c_4(not^#(odd(x)))
, +^#(x, 0()) -> c_5()
, +^#(x, s(y)) -> c_6(+^#(x, y))
, +^#(s(x), y) -> c_7(+^#(x, y)) }

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

Weak Trs:
  { not(true()) -> false()
  , not(false()) -> true()
  , odd(0()) -> false()
  , odd(s(x)) -> not(odd(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

No rule is usable, rules are removed from the input problem.

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

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS)' as induced by the safe mapping


and precedence

 empty .

Following symbols are considered recursive:

 {}

The recursion depth is 0.

Further, following argument filtering is employed:

 empty

Usable defined function symbols are a subset of:

 {}

For your convenience, here are the satisfied ordering constraints:


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