YES(?,POLY)

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

Strict Trs:
  { sqr(0()) -> 0()
  , sqr(s(x)) -> s(+(sqr(x), double(x)))
  , sqr(s(x)) -> +(sqr(x), s(double(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

We add the following dependency tuples:

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

and mark the set of starting terms.

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

Strict DPs:
  { sqr^#(0()) -> c_1()
  , sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
  , sqr^#(s(x)) ->
    c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x))
  , +^#(x, 0()) -> c_4()
  , +^#(x, s(y)) -> c_5(+^#(x, y))
  , double^#(0()) -> c_6()
  , double^#(s(x)) -> c_7(double^#(x)) }
Weak Trs:
  { sqr(0()) -> 0()
  , sqr(s(x)) -> s(+(sqr(x), double(x)))
  , sqr(s(x)) -> +(sqr(x), s(double(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

We estimate the number of application of {1,4,6} by applications of
Pre({1,4,6}) = {2,3,5,7}. Here rules are labeled as follows:

  DPs:
    { 1: sqr^#(0()) -> c_1()
    , 2: sqr^#(s(x)) ->
         c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
    , 3: sqr^#(s(x)) ->
         c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x))
    , 4: +^#(x, 0()) -> c_4()
    , 5: +^#(x, s(y)) -> c_5(+^#(x, y))
    , 6: double^#(0()) -> c_6()
    , 7: double^#(s(x)) -> c_7(double^#(x)) }

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

Strict DPs:
  { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
  , sqr^#(s(x)) ->
    c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x))
  , +^#(x, s(y)) -> c_5(+^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x)) }
Weak DPs:
  { sqr^#(0()) -> c_1()
  , +^#(x, 0()) -> c_4()
  , double^#(0()) -> c_6() }
Weak Trs:
  { sqr(0()) -> 0()
  , sqr(s(x)) -> s(+(sqr(x), double(x)))
  , sqr(s(x)) -> +(sqr(x), s(double(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

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

{ sqr^#(0()) -> c_1()
, +^#(x, 0()) -> c_4()
, double^#(0()) -> c_6() }

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

Strict DPs:
  { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
  , sqr^#(s(x)) ->
    c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x))
  , +^#(x, s(y)) -> c_5(+^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x)) }
Weak Trs:
  { sqr(0()) -> 0()
  , sqr(s(x)) -> s(+(sqr(x), double(x)))
  , sqr(s(x)) -> +(sqr(x), s(double(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

We decompose the input problem according to the dependency graph
into the upper component

  { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
  , sqr^#(s(x)) ->
    c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x)) }

and lower component

  { +^#(x, s(y)) -> c_5(+^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x)) }

Further, following extension rules are added to the lower
component.

{ sqr^#(s(x)) -> sqr^#(x)
, sqr^#(s(x)) -> +^#(sqr(x), s(double(x)))
, sqr^#(s(x)) -> +^#(sqr(x), double(x))
, sqr^#(s(x)) -> double^#(x) }

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
    , sqr^#(s(x)) ->
      c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x)) }
  Weak Trs:
    { sqr(0()) -> 0()
    , sqr(s(x)) -> s(+(sqr(x), double(x)))
    , sqr(s(x)) -> +(sqr(x), s(double(x)))
    , +(x, 0()) -> x
    , +(x, s(y)) -> s(+(x, y))
    , double(0()) -> 0()
    , double(s(x)) -> s(s(double(x))) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
  to orient following rules strictly.
  
  DPs:
    { 1: sqr^#(s(x)) ->
         c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
    , 2: sqr^#(s(x)) ->
         c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x)) }
  Trs:
    { sqr(0()) -> 0()
    , +(x, 0()) -> x
    , double(0()) -> 0() }
  
  Sub-proof:
  ----------
    The input was oriented with the instance of 'Small Polynomial Path
    Order (PS,1-bounded)' as induced by the safe mapping
    
     safe(sqr) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1, 2},
     safe(double) = {1}, safe(sqr^#) = {}, safe(c_1) = {},
     safe(c_2) = {}, safe(+^#) = {}, safe(double^#) = {},
     safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {},
     safe(c_7) = {}
    
    and precedence
    
     + ~ sqr^# .
    
    Following symbols are considered recursive:
    
     {sqr^#}
    
    The recursion depth is 1.
    
    Further, following argument filtering is employed:
    
     pi(sqr) = [], pi(0) = [], pi(s) = [1], pi(+) = [1, 2],
     pi(double) = [1], pi(sqr^#) = [1], pi(c_1) = [],
     pi(c_2) = [1, 2, 3], pi(+^#) = [], pi(double^#) = [1],
     pi(c_3) = [1, 2, 3], pi(c_4) = [], pi(c_5) = [], pi(c_6) = [],
     pi(c_7) = []
    
    Usable defined function symbols are a subset of:
    
     {sqr^#, +^#, double^#}
    
    For your convenience, here are the satisfied ordering constraints:
    
      pi(sqr^#(s(x))) = sqr^#(s(; x);)                                           
                      > c_2(+^#(),  sqr^#(x;),  double^#(x;);)                   
                      = pi(c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x)))   
                                                                                 
      pi(sqr^#(s(x))) = sqr^#(s(; x);)                                           
                      > c_3(+^#(),  sqr^#(x;),  double^#(x;);)                   
                      = pi(c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x)))
                                                                                 
  
  The strictly oriented rules are moved into the weak component.
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak DPs:
    { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
    , sqr^#(s(x)) ->
      c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x)) }
  Weak Trs:
    { sqr(0()) -> 0()
    , sqr(s(x)) -> s(+(sqr(x), double(x)))
    , sqr(s(x)) -> +(sqr(x), s(double(x)))
    , +(x, 0()) -> x
    , +(x, s(y)) -> s(+(x, y))
    , double(0()) -> 0()
    , double(s(x)) -> s(s(double(x))) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(1))
  
  The following weak DPs constitute a sub-graph of the DG that is
  closed under successors. The DPs are removed.
  
  { sqr^#(s(x)) -> c_2(+^#(sqr(x), double(x)), sqr^#(x), double^#(x))
  , sqr^#(s(x)) ->
    c_3(+^#(sqr(x), s(double(x))), sqr^#(x), double^#(x)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { sqr(0()) -> 0()
    , sqr(s(x)) -> s(+(sqr(x), double(x)))
    , sqr(s(x)) -> +(sqr(x), s(double(x)))
    , +(x, 0()) -> x
    , +(x, s(y)) -> s(+(x, y))
    , double(0()) -> 0()
    , double(s(x)) -> s(s(double(x))) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),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),O(1)).
  
  Rules: Empty
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(1))
  
  Empty rules are trivially bounded

We return to the main proof.

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

Strict DPs:
  { +^#(x, s(y)) -> c_5(+^#(x, y))
  , double^#(s(x)) -> c_7(double^#(x)) }
Weak DPs:
  { sqr^#(s(x)) -> sqr^#(x)
  , sqr^#(s(x)) -> +^#(sqr(x), s(double(x)))
  , sqr^#(s(x)) -> +^#(sqr(x), double(x))
  , sqr^#(s(x)) -> double^#(x) }
Weak Trs:
  { sqr(0()) -> 0()
  , sqr(s(x)) -> s(+(sqr(x), double(x)))
  , sqr(s(x)) -> +(sqr(x), s(double(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , double(0()) -> 0()
  , double(s(x)) -> s(s(double(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

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

 safe(sqr) = {1}, safe(0) = {}, safe(s) = {1}, safe(+) = {2},
 safe(double) = {}, safe(sqr^#) = {}, safe(c_1) = {},
 safe(c_2) = {}, safe(+^#) = {1}, safe(double^#) = {},
 safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {},
 safe(c_7) = {}

and precedence

 sqr > +, double > sqr, double > +, sqr^# > sqr, sqr^# > +,
 sqr^# > double, sqr^# > +^#, sqr^# > double^#, +^# > sqr, +^# > +,
 double^# > sqr, double^# > +, double ~ +^#, double ~ double^#,
 +^# ~ double^# .

Following symbols are considered recursive:

 {sqr, +, double, sqr^#, +^#, double^#}

The recursion depth is 4.

Further, following argument filtering is employed:

 pi(sqr) = [], pi(0) = [], pi(s) = [1], pi(+) = [],
 pi(double) = [1], pi(sqr^#) = [1], pi(c_1) = [], pi(c_2) = [],
 pi(+^#) = [2], pi(double^#) = [1], pi(c_3) = [], pi(c_4) = [],
 pi(c_5) = [1], pi(c_6) = [], pi(c_7) = [1]

Usable defined function symbols are a subset of:

 {double, sqr^#, +^#, double^#}

For your convenience, here are the satisfied ordering constraints:

     pi(sqr^#(s(x))) = sqr^#(s(; x);)               
                     > sqr^#(x;)                    
                     = pi(sqr^#(x))                 
                                                    
     pi(sqr^#(s(x))) = sqr^#(s(; x);)               
                     > +^#(s(; double(x;));)        
                     = pi(+^#(sqr(x), s(double(x))))
                                                    
     pi(sqr^#(s(x))) = sqr^#(s(; x);)               
                     > +^#(double(x;);)             
                     = pi(+^#(sqr(x), double(x)))   
                                                    
     pi(sqr^#(s(x))) = sqr^#(s(; x);)               
                     > double^#(x;)                 
                     = pi(double^#(x))              
                                                    
    pi(+^#(x, s(y))) = +^#(s(; y);)                 
                     > c_5(+^#(y;);)                
                     = pi(c_5(+^#(x, y)))           
                                                    
  pi(double^#(s(x))) = double^#(s(; x);)            
                     > c_7(double^#(x;);)           
                     = pi(c_7(double^#(x)))         
                                                    
     pi(double(0())) = double(0();)                 
                     > 0()                          
                     = pi(0())                      
                                                    
    pi(double(s(x))) = double(s(; x);)              
                     > s(; s(; double(x;)))         
                     = pi(s(s(double(x))))          
                                                    

Hurray, we answered YES(?,POLY)