YES(?,O(1))

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

Strict Trs:
  { rewrite(Op(Op(x, y), y')) ->
    rewrite[Ite][True][Let][Ite](True(), Op(Op(x, y), y'), Op(x, y))
  , rewrite(Op(Val(n), y)) ->
    rewrite[Ite][True][Let][Ite](False(), Op(Val(n), y), Val(n))
  , rewrite(Val(n)) -> Val(n)
  , second(Op(x, y)) -> y
  , isOp(Op(x, y)) -> True()
  , isOp(Val(n)) -> False()
  , first(Op(x, y)) -> x
  , first(Val(n)) -> Val(n)
  , assrewrite(exp) -> rewrite(exp) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

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

 safe(rewrite) = {1}, safe(Op) = {1, 2}, safe(Val) = {1},
 safe(rewrite[Ite][True][Let][Ite]) = {1, 2, 3}, safe(False) = {},
 safe(True) = {}, safe(second) = {}, safe(isOp) = {},
 safe(first) = {}, safe(assrewrite) = {}

and precedence

 rewrite > first, second > rewrite, second > isOp, second > first,
 isOp > first, assrewrite > rewrite, assrewrite > isOp,
 assrewrite > first, rewrite ~ isOp, second ~ assrewrite .

Following symbols are considered recursive:

 {}

The recursion depth is 0.

For your convenience, here are the satisfied ordering constraints:

  rewrite(; Op(; Op(; x,  y),  y')) > rewrite[Ite][True][Let][Ite](; True(),                 
                                                                     Op(; Op(; x,  y),  y'), 
                                                                     Op(; x,  y))            
                                                                                             
      rewrite(; Op(; Val(; n),  y)) > rewrite[Ite][True][Let][Ite](; False(),                
                                                                     Op(; Val(; n),  y),     
                                                                     Val(; n))               
                                                                                             
                rewrite(; Val(; n)) > Val(; n)                                               
                                                                                             
               second(Op(; x,  y);) > y                                                      
                                                                                             
                 isOp(Op(; x,  y);) > True()                                                 
                                                                                             
                    isOp(Val(; n);) > False()                                                
                                                                                             
                first(Op(; x,  y);) > x                                                      
                                                                                             
                   first(Val(; n);) > Val(; n)                                               
                                                                                             
                   assrewrite(exp;) > rewrite(; exp)                                         
                                                                                             

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