WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(x,true()) -> true()
            or(false(),false()) -> false()
            or(true(),y) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(x,true()) -> true()
            or(false(),false()) -> false()
            or(true(),y) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          mem(x,y){y -> union(y,z)} =
            mem(x,union(y,z)) ->^+ or(mem(x,y),mem(x,z))
              = C[mem(x,y) = mem(x,y){}]

** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(x,true()) -> true()
            or(false(),false()) -> false()
            or(true(),y) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(or) = {1,2}
        
        Following symbols are considered usable:
          {mem,or}
        TcT has computed the following interpretation:
              p(=) = 0        
          p(false) = 0        
            p(mem) = 0        
            p(nil) = 0        
             p(or) = x1 + 2*x2
            p(set) = 1        
           p(true) = 8        
          p(union) = 8        
        
        Following rules are strictly oriented:
        or(x,true()) = 16 + x
                     > 8     
                     = true()
        
        
        Following rules are (at-least) weakly oriented:
               mem(x,nil()) =  0                    
                            >= 0                    
                            =  false()              
        
              mem(x,set(y)) =  0                    
                            >= 0                    
                            =  =(x,y)               
        
          mem(x,union(y,z)) =  0                    
                            >= 0                    
                            =  or(mem(x,y),mem(x,z))
        
        or(false(),false()) =  0                    
                            >= 0                    
                            =  false()              
        
               or(true(),y) =  8 + 2*y              
                            >= 8                    
                            =  true()               
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(false(),false()) -> false()
            or(true(),y) -> true()
        - Weak TRS:
            or(x,true()) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(or) = {1,2}
        
        Following symbols are considered usable:
          {mem,or}
        TcT has computed the following interpretation:
              p(=) = 0          
          p(false) = 0          
            p(mem) = 0          
            p(nil) = 0          
             p(or) = 8*x1 + 4*x2
            p(set) = 2          
           p(true) = 1          
          p(union) = 1          
        
        Following rules are strictly oriented:
        or(true(),y) = 8 + 4*y
                     > 1      
                     = true() 
        
        
        Following rules are (at-least) weakly oriented:
               mem(x,nil()) =  0                    
                            >= 0                    
                            =  false()              
        
              mem(x,set(y)) =  0                    
                            >= 0                    
                            =  =(x,y)               
        
          mem(x,union(y,z)) =  0                    
                            >= 0                    
                            =  or(mem(x,y),mem(x,z))
        
               or(x,true()) =  4 + 8*x              
                            >= 1                    
                            =  true()               
        
        or(false(),false()) =  0                    
                            >= 0                    
                            =  false()              
        
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(false(),false()) -> false()
        - Weak TRS:
            or(x,true()) -> true()
            or(true(),y) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(or) = {1,2}
        
        Following symbols are considered usable:
          {mem,or}
        TcT has computed the following interpretation:
              p(=) = 0           
          p(false) = 0           
            p(mem) = 8*x2        
            p(nil) = 0           
             p(or) = 10 + x1 + x2
            p(set) = 0           
           p(true) = 2           
          p(union) = 2 + x1 + x2 
        
        Following rules are strictly oriented:
          mem(x,union(y,z)) = 16 + 8*y + 8*z       
                            > 10 + 8*y + 8*z       
                            = or(mem(x,y),mem(x,z))
        
        or(false(),false()) = 10                   
                            > 0                    
                            = false()              
        
        
        Following rules are (at-least) weakly oriented:
         mem(x,nil()) =  0      
                      >= 0      
                      =  false()
        
        mem(x,set(y)) =  0      
                      >= 0      
                      =  =(x,y) 
        
         or(x,true()) =  12 + x 
                      >= 2      
                      =  true() 
        
         or(true(),y) =  12 + y 
                      >= 2      
                      =  true() 
        
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
        - Weak TRS:
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(x,true()) -> true()
            or(false(),false()) -> false()
            or(true(),y) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(or) = {1,2}
        
        Following symbols are considered usable:
          {mem,or}
        TcT has computed the following interpretation:
              p(=) = 2 + x2      
          p(false) = 8           
            p(mem) = 1 + 2*x2    
            p(nil) = 9           
             p(or) = 12 + x1 + x2
            p(set) = 6 + x1      
           p(true) = 9           
          p(union) = 8 + x1 + x2 
        
        Following rules are strictly oriented:
         mem(x,nil()) = 19      
                      > 8       
                      = false() 
        
        mem(x,set(y)) = 13 + 2*y
                      > 2 + y   
                      = =(x,y)  
        
        
        Following rules are (at-least) weakly oriented:
          mem(x,union(y,z)) =  17 + 2*y + 2*z       
                            >= 14 + 2*y + 2*z       
                            =  or(mem(x,y),mem(x,z))
        
               or(x,true()) =  21 + x               
                            >= 9                    
                            =  true()               
        
        or(false(),false()) =  28                   
                            >= 8                    
                            =  false()              
        
               or(true(),y) =  21 + y               
                            >= 9                    
                            =  true()               
        
** Step 1.b:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            mem(x,nil()) -> false()
            mem(x,set(y)) -> =(x,y)
            mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
            or(x,true()) -> true()
            or(false(),false()) -> false()
            or(true(),y) -> true()
        - Signature:
            {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {mem,or} and constructors {=,false,nil,set,true,union}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))