WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            *(x,*(y,z)) -> *(otimes(x,y),z)
            *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
            *(+(x,y),z) -> oplus(*(x,z),*(y,z))
            *(1(),y) -> y
        - Signature:
            {*/2} / {+/2,1/0,oplus/2,otimes/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        DependencyPairs {dpKind_ = WIDP}
    + Details:
        We add the following weak innermost dependency pairs:
        
        Strict DPs
          *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
          *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
          *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
          *#(1(),y) -> c_4()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
            *#(1(),y) -> c_4()
        - Strict TRS:
            *(x,*(y,z)) -> *(otimes(x,y),z)
            *(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
            *(+(x,y),z) -> oplus(*(x,z),*(y,z))
            *(1(),y) -> y
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
          *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
          *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
          *#(1(),y) -> c_4()
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
            *#(1(),y) -> c_4()
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {4}
        by application of
          Pre({4}) = {2,3}.
        Here rules are labelled as follows:
          1: *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
          2: *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
          3: *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
          4: *#(1(),y) -> c_4()
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
        - Weak DPs:
            *#(1(),y) -> c_4()
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:*#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
             -->_1 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_1 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
          
          2:S:*#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
             -->_2 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_1 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_2 *#(1(),y) -> c_4():4
             -->_1 *#(1(),y) -> c_4():4
             -->_2 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_1 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_2 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
             -->_1 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
          
          3:S:*#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
             -->_2 *#(1(),y) -> c_4():4
             -->_1 *#(1(),y) -> c_4():4
             -->_2 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_1 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_2 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_1 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_2 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
             -->_1 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
          
          4:W:*#(1(),y) -> c_4()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: *#(1(),y) -> c_4()
* Step 5: PredecessorEstimationCP WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
          2: *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
          3: *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
          
        The strictly oriented rules are moved into the weak component.
** Step 5.a:1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1,2},
          uargs(c_3) = {1,2}
        
        Following symbols are considered usable:
          {*#}
        TcT has computed the following interpretation:
               p(*) = 3 + x1*x2 + x1^2 + 2*x2
               p(+) = 3 + x1 + x2            
               p(1) = 1                      
           p(oplus) = 3 + x1 + x2            
          p(otimes) = 0                      
              p(*#) = 3*x1 + 4*x1*x2 + 3*x2  
             p(c_1) = 6 + x1                 
             p(c_2) = 1 + x1 + x2            
             p(c_3) = 6 + x1 + x2            
             p(c_4) = 0                      
        
        Following rules are strictly oriented:
            *#(x,*(y,z)) = 9 + 15*x + 4*x*y*z + 4*x*y^2 + 8*x*z + 3*y*z + 3*y^2 + 6*z
                         > 6 + 3*z                                                   
                         = c_1(*#(otimes(x,y),z))                                    
        
        *#(x,oplus(y,z)) = 9 + 15*x + 4*x*y + 4*x*z + 3*y + 3*z                      
                         > 1 + 6*x + 4*x*y + 4*x*z + 3*y + 3*z                       
                         = c_2(*#(x,y),*#(x,z))                                      
        
            *#(+(x,y),z) = 9 + 3*x + 4*x*z + 3*y + 4*y*z + 15*z                      
                         > 6 + 3*x + 4*x*z + 3*y + 4*y*z + 6*z                       
                         = c_3(*#(x,z),*#(y,z))                                      
        
        
        Following rules are (at-least) weakly oriented:
        
** Step 5.a:2: Assumption WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
    + Details:
        ()

** Step 5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
            *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
            *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:*#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
             -->_1 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_1 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
          
          2:W:*#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
             -->_2 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_1 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_2 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_1 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_2 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
             -->_1 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
          
          3:W:*#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
             -->_2 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_1 *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z)):3
             -->_2 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_1 *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z)):2
             -->_2 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
             -->_1 *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z)):1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          1: *#(x,*(y,z)) -> c_1(*#(otimes(x,y),z))
          3: *#(+(x,y),z) -> c_3(*#(x,z),*#(y,z))
          2: *#(x,oplus(y,z)) -> c_2(*#(x,y),*#(x,z))
** Step 5.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        
        - Signature:
            {*/2,*#/2} / {+/2,1/0,oplus/2,otimes/2,c_1/1,c_2/2,c_3/2,c_4/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#} and constructors {+,1,oplus,otimes}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))