```* Step 1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ 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(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [4] x1 + [1] x2 + [0]
p(cons) = [1] x2 + [1]
p(eq) = [0]
p(false) = [2]
p(if) = [5] x1 + [1] x2 + [1] x3 + [5]
p(ifinter) = [1] x1 + [1] x3 + [1] x4 + [0]
p(ifmem) = [1] x1 + [0]
p(inter) = [1] x1 + [1] x2 + [3]
p(mem) = [2]
p(nil) = [2]
p(s) = [1] x1 + [0]
p(true) = [2]

Following rules are strictly oriented:
app(cons(x,l1),l2) = [4] l1 + [1] l2 + [4]
> [4] l1 + [1] l2 + [1]
= cons(x,app(l1,l2))

app(nil(),l) = [1] l + [8]
> [1] l + [0]
= l

if(false(),x,y) = [1] x + [1] y + [15]
> [1] y + [0]
= y

if(true(),x,y) = [1] x + [1] y + [15]
> [1] x + [0]
= x

inter(l1,cons(x,l2)) = [1] l1 + [1] l2 + [4]
> [1] l1 + [1] l2 + [2]
= ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) = [1] x + [5]
> [2]
= nil()

inter(cons(x,l1),l2) = [1] l1 + [1] l2 + [4]
> [1] l1 + [1] l2 + [2]
= ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) = [1] x + [5]
> [2]
= nil()

mem(x,cons(y,l)) = [2]
> [0]
= ifmem(eq(x,y),x,l)

Following rules are (at-least) weakly oriented:
eq(0(),0()) =  [0]
>= [2]
=  true()

eq(0(),s(x)) =  [0]
>= [2]
=  false()

eq(s(x),0()) =  [0]
>= [2]
=  false()

eq(s(x),s(y)) =  [0]
>= [0]
=  eq(x,y)

ifinter(false(),x,l1,l2) =  [1] l1 + [1] l2 + [2]
>= [1] l1 + [1] l2 + [3]
=  inter(l1,l2)

ifinter(true(),x,l1,l2) =  [1] l1 + [1] l2 + [2]
>= [1] l1 + [1] l2 + [4]
=  cons(x,inter(l1,l2))

ifmem(false(),x,l) =  [2]
>= [2]
=  mem(x,l)

ifmem(true(),x,l) =  [2]
>= [2]
=  true()

mem(x,nil()) =  [2]
>= [2]
=  false()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,nil()) -> false()
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
if(false(),x,y) -> y
if(true(),x,y) -> x
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ 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(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [4] x1 + [1] x2 + [3]
p(cons) = [1] x2 + [1]
p(eq) = [1]
p(false) = [5]
p(if) = [2] x2 + [1] x3 + [1]
p(ifinter) = [1] x1 + [0]
p(ifmem) = [1] x1 + [3]
p(inter) = [6]
p(mem) = [6]
p(nil) = [0]
p(s) = [1]
p(true) = [1]

Following rules are strictly oriented:
ifmem(false(),x,l) = [8]
> [6]
= mem(x,l)

ifmem(true(),x,l) = [4]
> [1]
= true()

mem(x,nil()) = [6]
> [5]
= false()

Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) =  [4] l1 + [1] l2 + [7]
>= [4] l1 + [1] l2 + [4]
=  cons(x,app(l1,l2))

app(nil(),l) =  [1] l + [3]
>= [1] l + [0]
=  l

eq(0(),0()) =  [1]
>= [1]
=  true()

eq(0(),s(x)) =  [1]
>= [5]
=  false()

eq(s(x),0()) =  [1]
>= [5]
=  false()

eq(s(x),s(y)) =  [1]
>= [1]
=  eq(x,y)

if(false(),x,y) =  [2] x + [1] y + [1]
>= [1] y + [0]
=  y

if(true(),x,y) =  [2] x + [1] y + [1]
>= [1] x + [0]
=  x

ifinter(false(),x,l1,l2) =  [5]
>= [6]
=  inter(l1,l2)

ifinter(true(),x,l1,l2) =  [1]
>= [7]
=  cons(x,inter(l1,l2))

inter(l1,cons(x,l2)) =  [6]
>= [6]
=  ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) =  [6]
>= [0]
=  nil()

inter(cons(x,l1),l2) =  [6]
>= [6]
=  ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) =  [6]
>= [0]
=  nil()

mem(x,cons(y,l)) =  [6]
>= [4]
=  ifmem(eq(x,y),x,l)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
if(false(),x,y) -> y
if(true(),x,y) -> x
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ 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(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [5] x1 + [4] x2 + [4]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [0]
p(false) = [1]
p(if) = [2] x1 + [4] x2 + [2] x3 + [0]
p(ifinter) = [1] x1 + [3] x2 + [4] x3 + [4] x4 + [0]
p(ifmem) = [1] x1 + [1]
p(inter) = [4] x1 + [4] x2 + [0]
p(mem) = [1]
p(nil) = [1]
p(s) = [1] x1 + [2]
p(true) = [1]

Following rules are strictly oriented:
ifinter(false(),x,l1,l2) = [4] l1 + [4] l2 + [3] x + [1]
> [4] l1 + [4] l2 + [0]
= inter(l1,l2)

Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) =  [5] l1 + [4] l2 + [5] x + [14]
>= [5] l1 + [4] l2 + [1] x + [6]
=  cons(x,app(l1,l2))

app(nil(),l) =  [4] l + [9]
>= [1] l + [0]
=  l

eq(0(),0()) =  [0]
>= [1]
=  true()

eq(0(),s(x)) =  [0]
>= [1]
=  false()

eq(s(x),0()) =  [0]
>= [1]
=  false()

eq(s(x),s(y)) =  [0]
>= [0]
=  eq(x,y)

if(false(),x,y) =  [4] x + [2] y + [2]
>= [1] y + [0]
=  y

if(true(),x,y) =  [4] x + [2] y + [2]
>= [1] x + [0]
=  x

ifinter(true(),x,l1,l2) =  [4] l1 + [4] l2 + [3] x + [1]
>= [4] l1 + [4] l2 + [1] x + [2]
=  cons(x,inter(l1,l2))

ifmem(false(),x,l) =  [2]
>= [1]
=  mem(x,l)

ifmem(true(),x,l) =  [2]
>= [1]
=  true()

inter(l1,cons(x,l2)) =  [4] l1 + [4] l2 + [4] x + [8]
>= [4] l1 + [4] l2 + [3] x + [1]
=  ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) =  [4] x + [4]
>= [1]
=  nil()

inter(cons(x,l1),l2) =  [4] l1 + [4] l2 + [4] x + [8]
>= [4] l1 + [4] l2 + [3] x + [1]
=  ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) =  [4] x + [4]
>= [1]
=  nil()

mem(x,cons(y,l)) =  [1]
>= [1]
=  ifmem(eq(x,y),x,l)

mem(x,nil()) =  [1]
>= [1]
=  false()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ 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(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [1] x2 + [4]
p(cons) = [1] x2 + [0]
p(eq) = [1]
p(false) = [2]
p(if) = [4] x1 + [1] x2 + [1] x3 + [0]
p(ifinter) = [1] x1 + [3]
p(ifmem) = [1] x1 + [1]
p(inter) = [5]
p(mem) = [2]
p(nil) = [5]
p(s) = [1] x1 + [0]
p(true) = [0]

Following rules are strictly oriented:
eq(0(),0()) = [1]
> [0]
= true()

Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) =  [1] l2 + [4]
>= [1] l2 + [4]
=  cons(x,app(l1,l2))

app(nil(),l) =  [1] l + [4]
>= [1] l + [0]
=  l

eq(0(),s(x)) =  [1]
>= [2]
=  false()

eq(s(x),0()) =  [1]
>= [2]
=  false()

eq(s(x),s(y)) =  [1]
>= [1]
=  eq(x,y)

if(false(),x,y) =  [1] x + [1] y + [8]
>= [1] y + [0]
=  y

if(true(),x,y) =  [1] x + [1] y + [0]
>= [1] x + [0]
=  x

ifinter(false(),x,l1,l2) =  [5]
>= [5]
=  inter(l1,l2)

ifinter(true(),x,l1,l2) =  [3]
>= [5]
=  cons(x,inter(l1,l2))

ifmem(false(),x,l) =  [3]
>= [2]
=  mem(x,l)

ifmem(true(),x,l) =  [1]
>= [0]
=  true()

inter(l1,cons(x,l2)) =  [5]
>= [5]
=  ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) =  [5]
>= [5]
=  nil()

inter(cons(x,l1),l2) =  [5]
>= [5]
=  ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) =  [5]
>= [5]
=  nil()

mem(x,cons(y,l)) =  [2]
>= [2]
=  ifmem(eq(x,y),x,l)

mem(x,nil()) =  [2]
>= [2]
=  false()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ 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(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(app) = [5] x1 + [1] x2 + [2]
p(cons) = [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(if) = [4] x1 + [4] x2 + [4] x3 + [2]
p(ifinter) = [1] x1 + [4] x3 + [4] x4 + [5]
p(ifmem) = [1] x1 + [0]
p(inter) = [4] x1 + [4] x2 + [0]
p(mem) = [0]
p(nil) = [2]
p(s) = [0]
p(true) = [0]

Following rules are strictly oriented:
ifinter(true(),x,l1,l2) = [4] l1 + [4] l2 + [5]
> [4] l1 + [4] l2 + [2]
= cons(x,inter(l1,l2))

Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) =  [5] l1 + [1] l2 + [12]
>= [5] l1 + [1] l2 + [4]
=  cons(x,app(l1,l2))

app(nil(),l) =  [1] l + [12]
>= [1] l + [0]
=  l

eq(0(),0()) =  [0]
>= [0]
=  true()

eq(0(),s(x)) =  [0]
>= [0]
=  false()

eq(s(x),0()) =  [0]
>= [0]
=  false()

eq(s(x),s(y)) =  [0]
>= [0]
=  eq(x,y)

if(false(),x,y) =  [4] x + [4] y + [2]
>= [1] y + [0]
=  y

if(true(),x,y) =  [4] x + [4] y + [2]
>= [1] x + [0]
=  x

ifinter(false(),x,l1,l2) =  [4] l1 + [4] l2 + [5]
>= [4] l1 + [4] l2 + [0]
=  inter(l1,l2)

ifmem(false(),x,l) =  [0]
>= [0]
=  mem(x,l)

ifmem(true(),x,l) =  [0]
>= [0]
=  true()

inter(l1,cons(x,l2)) =  [4] l1 + [4] l2 + [8]
>= [4] l1 + [4] l2 + [5]
=  ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) =  [4] x + [8]
>= [2]
=  nil()

inter(cons(x,l1),l2) =  [4] l1 + [4] l2 + [8]
>= [4] l1 + [4] l2 + [5]
=  ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) =  [4] x + [8]
>= [2]
=  nil()

mem(x,cons(y,l)) =  [0]
>= [0]
=  ifmem(eq(x,y),x,l)

mem(x,nil()) =  [0]
>= [0]
=  false()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
{app,eq,if,ifinter,ifmem,inter,mem}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 2 + 2*x1 + x2
p(cons) = x1 + x2
p(eq) = x1*x2
p(false) = 0
p(if) = x1 + 2*x1*x2 + 2*x2 + 2*x3
p(ifinter) = 3 + x1 + 2*x2 + 2*x3 + 2*x3*x4 + 2*x4
p(ifmem) = 2*x1 + 2*x2*x3
p(inter) = 3 + 2*x1 + 2*x1*x2 + 2*x2
p(mem) = 2*x1*x2
p(nil) = 0
p(s) = 1 + x1
p(true) = 0

Following rules are strictly oriented:
eq(s(x),s(y)) = 1 + x + x*y + y
> x*y
= eq(x,y)

Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) =  2 + 2*l1 + l2 + 2*x
>= 2 + 2*l1 + l2 + x
=  cons(x,app(l1,l2))

app(nil(),l) =  2 + l
>= l
=  l

eq(0(),0()) =  0
>= 0
=  true()

eq(0(),s(x)) =  0
>= 0
=  false()

eq(s(x),0()) =  0
>= 0
=  false()

if(false(),x,y) =  2*x + 2*y
>= y
=  y

if(true(),x,y) =  2*x + 2*y
>= x
=  x

ifinter(false(),x,l1,l2) =  3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l2
=  inter(l1,l2)

ifinter(true(),x,l1,l2) =  3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l2 + x
=  cons(x,inter(l1,l2))

ifmem(false(),x,l) =  2*l*x
>= 2*l*x
=  mem(x,l)

ifmem(true(),x,l) =  2*l*x
>= 0
=  true()

inter(l1,cons(x,l2)) =  3 + 2*l1 + 2*l1*l2 + 2*l1*x + 2*l2 + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l1*x + 2*l2 + 2*x
=  ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) =  3 + 2*x
>= 0
=  nil()

inter(cons(x,l1),l2) =  3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*l2*x + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*l2*x + 2*x
=  ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) =  3 + 2*x
>= 0
=  nil()

mem(x,cons(y,l)) =  2*l*x + 2*x*y
>= 2*l*x + 2*x*y
=  ifmem(eq(x,y),x,l)

mem(x,nil()) =  0
>= 0
=  false()

* Step 7: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}

Following symbols are considered usable:
{app,eq,if,ifinter,ifmem,inter,mem}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 1 + 2*x1*x2 + 2*x1^2 + x2 + 2*x2^2
p(cons) = 1 + x2
p(eq) = 1
p(false) = 0
p(if) = 2 + 2*x2 + x2*x3 + x3
p(ifinter) = x1 + 2*x3*x4
p(ifmem) = x1 + x3
p(inter) = 2*x1*x2
p(mem) = x2
p(nil) = 0
p(s) = 0
p(true) = 1

Following rules are strictly oriented:
eq(0(),s(x)) = 1
> 0
= false()

eq(s(x),0()) = 1
> 0
= false()

Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) =  3 + 4*l1 + 2*l1*l2 + 2*l1^2 + 3*l2 + 2*l2^2
>= 2 + 2*l1*l2 + 2*l1^2 + l2 + 2*l2^2
=  cons(x,app(l1,l2))

app(nil(),l) =  1 + l + 2*l^2
>= l
=  l

eq(0(),0()) =  1
>= 1
=  true()

eq(s(x),s(y)) =  1
>= 1
=  eq(x,y)

if(false(),x,y) =  2 + 2*x + x*y + y
>= y
=  y

if(true(),x,y) =  2 + 2*x + x*y + y
>= x
=  x

ifinter(false(),x,l1,l2) =  2*l1*l2
>= 2*l1*l2
=  inter(l1,l2)

ifinter(true(),x,l1,l2) =  1 + 2*l1*l2
>= 1 + 2*l1*l2
=  cons(x,inter(l1,l2))

ifmem(false(),x,l) =  l
>= l
=  mem(x,l)

ifmem(true(),x,l) =  1 + l
>= 1
=  true()

inter(l1,cons(x,l2)) =  2*l1 + 2*l1*l2
>= l1 + 2*l1*l2
=  ifinter(mem(x,l1),x,l2,l1)

inter(x,nil()) =  0
>= 0
=  nil()

inter(cons(x,l1),l2) =  2*l1*l2 + 2*l2
>= 2*l1*l2 + l2
=  ifinter(mem(x,l2),x,l1,l2)

inter(nil(),x) =  0
>= 0
=  nil()

mem(x,cons(y,l)) =  1 + l
>= 1 + l
=  ifmem(eq(x,y),x,l)

mem(x,nil()) =  0
>= 0
=  false()

* Step 8: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

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