```* Step 1: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
++(x,g(y,z)) -> g(++(x,y),z)
++(x,nil()) -> x
f(x,g(y,z)) -> g(f(x,y),z)
f(x,nil()) -> g(nil(),x)
max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
max(g(g(nil(),x),y)) -> max'(x,y)
mem(x,max(x)) -> not(null(x))
mem(g(x,y),z) -> or(=(y,z),mem(x,z))
mem(nil(),y) -> false()
null(g(x,y)) -> false()
null(nil()) -> true()
- Signature:
{++/2,f/2,max/1,mem/2,null/1} / {=/2,false/0,g/2,max'/2,nil/0,not/1,or/2,true/0,u/0}
- Obligation:
runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
,true,u}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(g) = {1},
uargs(max') = {1},
uargs(not) = {1},
uargs(or) = {2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(++) =  x1 +  x2 + 
p(=) = 
p(f) =  x1 +  x2 + 
p(false) = 
p(g) =  x1 +  x2 + 
p(max) =  x1 + 
p(max') =  x1 +  x2 + 
p(mem) = 
p(nil) = 
p(not) =  x1 + 
p(null) = 
p(or) =  x1 +  x2 + 
p(true) = 
p(u) = 

Following rules are strictly oriented:
++(x,nil()) =  x + 
>  x + 
= x

Following rules are (at-least) weakly oriented:
++(x,g(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  g(++(x,y),z)

f(x,g(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  g(f(x,y),z)

f(x,nil()) =   x + 
>=  x + 
=  g(nil(),x)

max(g(g(g(x,y),z),u())) =   x +  y +  z + 
>=  x +  y +  z + 
=  max'(max(g(g(x,y),z)),u())

max(g(g(nil(),x),y)) =   x +  y + 
>=  x +  y + 
=  max'(x,y)

mem(x,max(x)) =  
>= 
=  not(null(x))

mem(g(x,y),z) =  
>= 
=  or(=(y,z),mem(x,z))

mem(nil(),y) =  
>= 
=  false()

null(g(x,y)) =  
>= 
=  false()

null(nil()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
++(x,g(y,z)) -> g(++(x,y),z)
f(x,g(y,z)) -> g(f(x,y),z)
f(x,nil()) -> g(nil(),x)
max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
max(g(g(nil(),x),y)) -> max'(x,y)
mem(x,max(x)) -> not(null(x))
mem(g(x,y),z) -> or(=(y,z),mem(x,z))
mem(nil(),y) -> false()
null(g(x,y)) -> false()
null(nil()) -> true()
- Weak TRS:
++(x,nil()) -> x
- Signature:
{++/2,f/2,max/1,mem/2,null/1} / {=/2,false/0,g/2,max'/2,nil/0,not/1,or/2,true/0,u/0}
- Obligation:
runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
,true,u}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(g) = {1},
uargs(max') = {1},
uargs(not) = {1},
uargs(or) = {2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(++) =  x1 +  x2 + 
p(=) = 
p(f) =  x1 +  x2 + 
p(false) = 
p(g) =  x1 +  x2 + 
p(max) =  x1 + 
p(max') =  x1 + 
p(mem) = 
p(nil) = 
p(not) =  x1 + 
p(null) = 
p(or) =  x1 +  x2 + 
p(true) = 
p(u) = 

Following rules are strictly oriented:
f(x,nil()) =  x + 
>  x + 
= g(nil(),x)

max(g(g(g(x,y),z),u())) =  x +  y +  z + 
>  x +  y +  z + 
= max'(max(g(g(x,y),z)),u())

max(g(g(nil(),x),y)) =  x +  y + 
>  x + 
= max'(x,y)

null(g(x,y)) = 
> 
= false()

null(nil()) = 
> 
= true()

Following rules are (at-least) weakly oriented:
++(x,g(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  g(++(x,y),z)

++(x,nil()) =   x + 
>=  x + 
=  x

f(x,g(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  g(f(x,y),z)

mem(x,max(x)) =  
>= 
=  not(null(x))

mem(g(x,y),z) =  
>= 
=  or(=(y,z),mem(x,z))

mem(nil(),y) =  
>= 
=  false()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
++(x,g(y,z)) -> g(++(x,y),z)
f(x,g(y,z)) -> g(f(x,y),z)
mem(x,max(x)) -> not(null(x))
mem(g(x,y),z) -> or(=(y,z),mem(x,z))
mem(nil(),y) -> false()
- Weak TRS:
++(x,nil()) -> x
f(x,nil()) -> g(nil(),x)
max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
max(g(g(nil(),x),y)) -> max'(x,y)
null(g(x,y)) -> false()
null(nil()) -> true()
- Signature:
{++/2,f/2,max/1,mem/2,null/1} / {=/2,false/0,g/2,max'/2,nil/0,not/1,or/2,true/0,u/0}
- Obligation:
runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
,true,u}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(g) = {1},
uargs(max') = {1},
uargs(not) = {1},
uargs(or) = {2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(++) =  x1 +  x2 + 
p(=) = 
p(f) =  x1 +  x2 + 
p(false) = 
p(g) =  x1 +  x2 + 
p(max) =  x1 + 
p(max') =  x1 + 
p(mem) =  x1 + 
p(nil) = 
p(not) =  x1 + 
p(null) = 
p(or) =  x2 + 
p(true) = 
p(u) = 

Following rules are strictly oriented:
++(x,g(y,z)) =  x +  y +  z + 
>  x +  y +  z + 
= g(++(x,y),z)

f(x,g(y,z)) =  x +  y +  z + 
>  x +  y +  z + 
= g(f(x,y),z)

mem(g(x,y),z) =  x +  y + 
>  x + 
= or(=(y,z),mem(x,z))

mem(nil(),y) = 
> 
= false()

Following rules are (at-least) weakly oriented:
++(x,nil()) =   x + 
>=  x + 
=  x

f(x,nil()) =   x + 
>=  x + 
=  g(nil(),x)

max(g(g(g(x,y),z),u())) =   x +  y +  z + 
>=  x +  y +  z + 
=  max'(max(g(g(x,y),z)),u())

max(g(g(nil(),x),y)) =   x +  y + 
>=  x + 
=  max'(x,y)

mem(x,max(x)) =   x + 
>= 
=  not(null(x))

null(g(x,y)) =  
>= 
=  false()

null(nil()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
mem(x,max(x)) -> not(null(x))
- Weak TRS:
++(x,g(y,z)) -> g(++(x,y),z)
++(x,nil()) -> x
f(x,g(y,z)) -> g(f(x,y),z)
f(x,nil()) -> g(nil(),x)
max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
max(g(g(nil(),x),y)) -> max'(x,y)
mem(g(x,y),z) -> or(=(y,z),mem(x,z))
mem(nil(),y) -> false()
null(g(x,y)) -> false()
null(nil()) -> true()
- Signature:
{++/2,f/2,max/1,mem/2,null/1} / {=/2,false/0,g/2,max'/2,nil/0,not/1,or/2,true/0,u/0}
- Obligation:
runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
,true,u}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(g) = {1},
uargs(max') = {1},
uargs(not) = {1},
uargs(or) = {2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(++) =  x1 +  x2 + 
p(=) =  x1 +  x2 + 
p(f) =  x1 +  x2 + 
p(false) = 
p(g) =  x1 +  x2 + 
p(max) =  x1 + 
p(max') =  x1 + 
p(mem) =  x2 + 
p(nil) = 
p(not) =  x1 + 
p(null) = 
p(or) =  x2 + 
p(true) = 
p(u) = 

Following rules are strictly oriented:
mem(x,max(x)) =  x + 
> 
= not(null(x))

Following rules are (at-least) weakly oriented:
++(x,g(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  g(++(x,y),z)

++(x,nil()) =   x + 
>=  x + 
=  x

f(x,g(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  g(f(x,y),z)

f(x,nil()) =   x + 
>=  x + 
=  g(nil(),x)

max(g(g(g(x,y),z),u())) =   x +  y +  z + 
>=  x +  y +  z + 
=  max'(max(g(g(x,y),z)),u())

max(g(g(nil(),x),y)) =   x +  y + 
>=  x + 
=  max'(x,y)

mem(g(x,y),z) =   z + 
>=  z + 
=  or(=(y,z),mem(x,z))

mem(nil(),y) =   y + 
>= 
=  false()

null(g(x,y)) =  
>= 
=  false()

null(nil()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
++(x,g(y,z)) -> g(++(x,y),z)
++(x,nil()) -> x
f(x,g(y,z)) -> g(f(x,y),z)
f(x,nil()) -> g(nil(),x)
max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
max(g(g(nil(),x),y)) -> max'(x,y)
mem(x,max(x)) -> not(null(x))
mem(g(x,y),z) -> or(=(y,z),mem(x,z))
mem(nil(),y) -> false()
null(g(x,y)) -> false()
null(nil()) -> true()
- Signature:
{++/2,f/2,max/1,mem/2,null/1} / {=/2,false/0,g/2,max'/2,nil/0,not/1,or/2,true/0,u/0}
- Obligation:
runtime complexity wrt. defined symbols {++,f,max,mem,null} and constructors {=,false,g,max',nil,not,or
,true,u}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))
```