```* Step 1: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(from(X)) -> a__from(X)
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 + 
p(a__and) =  x1 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 + 
p(add) =  x1 + 
p(and) =  x1 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 + 
p(mark) = 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
> 
= mark(X)

a__first(0(),X) =  X + 
> 
= nil()

mark(cons(X1,X2)) = 
> 
= cons(X1,X2)

mark(false()) = 
> 
= false()

mark(from(X)) = 
> 
= a__from(X)

mark(nil()) = 
> 
= nil()

mark(s(X)) = 
> 
= s(X)

mark(true()) = 
> 
= true()

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 + 
>=  X1 + 

>= 

a__and(X1,X2) =   X1 + 
>=  X1 + 
=  and(X1,X2)

a__and(false(),Y) =  
>= 
=  false()

a__and(true(),X) =  
>= 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

a__if(X1,X2,X3) =   X1 + 
>=  X1 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =  
>= 
=  mark(Y)

a__if(true(),X,Y) =  
>= 
=  mark(X)

mark(0()) =  
>= 
=  0()

>= 

mark(and(X1,X2)) =  
>= 
=  a__and(mark(X1),X2)

mark(first(X1,X2)) =  
>= 
=  a__first(mark(X1),mark(X2))

mark(if(X1,X2,X3)) =  
>= 
=  a__if(mark(X1),X2,X3)

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:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
- Weak TRS:
a__first(0(),X) -> nil()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 + 
p(a__and) =  x1 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 + 
p(add) =  x1 + 
p(and) =  x1 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 + 
p(mark) = 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
a__add(X1,X2) =  X1 + 
>  X1 + 

> 

a__if(X1,X2,X3) =  X1 + 
>  X1 + 
= if(X1,X2,X3)

a__if(false(),X,Y) = 
> 
= mark(Y)

a__if(true(),X,Y) = 
> 
= mark(X)

Following rules are (at-least) weakly oriented:
>= 
=  mark(X)

a__and(X1,X2) =   X1 + 
>=  X1 + 
=  and(X1,X2)

a__and(false(),Y) =  
>= 
=  false()

a__and(true(),X) =  
>= 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

mark(0()) =  
>= 
=  0()

>= 

mark(and(X1,X2)) =  
>= 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =  
>= 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =  
>= 
=  a__from(X)

mark(if(X1,X2,X3)) =  
>= 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

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:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
- Weak TRS:
a__first(0(),X) -> nil()
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 + 
p(a__and) =  x1 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 + 
p(add) =  x1 + 
p(and) =  x1 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 + 
p(mark) = 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
a__and(X1,X2) =  X1 + 
>  X1 + 
= and(X1,X2)

a__and(false(),Y) = 
> 
= false()

a__and(true(),X) = 
> 
= mark(X)

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 + 
>=  X1 + 

>= 
=  mark(X)

>= 

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

a__if(X1,X2,X3) =   X1 + 
>=  X1 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =  
>= 
=  mark(Y)

a__if(true(),X,Y) =  
>= 
=  mark(X)

mark(0()) =  
>= 
=  0()

>= 

mark(and(X1,X2)) =  
>= 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =  
>= 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =  
>= 
=  a__from(X)

mark(if(X1,X2,X3)) =  
>= 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  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:
a__first(X1,X2) -> first(X1,X2)
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(0(),X) -> nil()
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 + 
p(a__and) =  x1 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 + 
p(add) =  x1 + 
p(and) =  x1 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 + 
p(mark) = 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
a__first(X1,X2) =  X1 +  X2 + 
>  X1 +  X2 + 
= first(X1,X2)

a__first(s(X),cons(Y,Z)) = 
> 
= cons(Y,first(X,Z))

a__from(X) = 
> 
= cons(X,from(s(X)))

a__from(X) = 
> 
= from(X)

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 + 
>=  X1 + 

>= 
=  mark(X)

>= 

a__and(X1,X2) =   X1 + 
>=  X1 + 
=  and(X1,X2)

a__and(false(),Y) =  
>= 
=  false()

a__and(true(),X) =  
>= 
=  mark(X)

a__first(0(),X) =   X + 
>= 
=  nil()

a__if(X1,X2,X3) =   X1 + 
>=  X1 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =  
>= 
=  mark(Y)

a__if(true(),X,Y) =  
>= 
=  mark(X)

mark(0()) =  
>= 
=  0()

>= 

mark(and(X1,X2)) =  
>= 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =  
>= 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =  
>= 
=  a__from(X)

mark(if(X1,X2,X3)) =  
>= 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 + 
p(a__and) =  x1 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 + 
p(add) =  x1 + 
p(and) =  x1 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 + 
p(mark) = 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
mark(0()) = 
> 
= 0()

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 + 
>=  X1 + 

>= 
=  mark(X)

>= 

a__and(X1,X2) =   X1 + 
>=  X1 + 
=  and(X1,X2)

a__and(false(),Y) =  
>= 
=  false()

a__and(true(),X) =  
>= 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

a__if(X1,X2,X3) =   X1 + 
>=  X1 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =  
>= 
=  mark(Y)

a__if(true(),X,Y) =  
>= 
=  mark(X)

>= 

mark(and(X1,X2)) =  
>= 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =  
>= 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =  
>= 
=  a__from(X)

mark(if(X1,X2,X3)) =  
>= 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 +  x2 + 
p(a__and) =  x1 +  x2 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 +  x2 +  x3 + 
p(add) =  x1 +  x2 + 
p(and) =  x1 +  x2 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 +  x2 +  x3 + 
p(mark) =  x1 + 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
mark(if(X1,X2,X3)) =  X1 +  X2 +  X3 + 
>  X1 +  X2 +  X3 + 
= a__if(mark(X1),X2,X3)

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 

a__add(0(),X) =   X + 
>=  X + 
=  mark(X)

a__add(s(X),Y) =   Y + 
>= 

a__and(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  and(X1,X2)

a__and(false(),Y) =   Y + 
>= 
=  false()

a__and(true(),X) =   X + 
>=  X + 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

a__if(X1,X2,X3) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =   X +  Y + 
>=  Y + 
=  mark(Y)

a__if(true(),X,Y) =   X +  Y + 
>=  X + 
=  mark(X)

mark(0()) =  
>= 
=  0()

mark(add(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 

mark(and(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =  
>= 
=  a__from(X)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 +  x2 + 
p(a__and) =  x1 +  x2 + 
p(a__first) =  x1 +  x2 + 
p(a__from) =  x1 + 
p(a__if) =  x1 +  x2 +  x3 + 
p(add) =  x1 +  x2 + 
p(and) =  x1 +  x2 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) =  x1 + 
p(if) =  x1 +  x2 +  x3 + 
p(mark) =  x1 + 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
mark(and(X1,X2)) =  X1 +  X2 + 
>  X1 +  X2 + 
= a__and(mark(X1),X2)

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 

a__add(0(),X) =   X + 
>=  X + 
=  mark(X)

a__add(s(X),Y) =   Y + 
>= 

a__and(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  and(X1,X2)

a__and(false(),Y) =   Y + 
>= 
=  false()

a__and(true(),X) =   X + 
>=  X + 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =   X + 
>= 
=  cons(X,from(s(X)))

a__from(X) =   X + 
>=  X + 
=  from(X)

a__if(X1,X2,X3) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =   X +  Y + 
>=  Y + 
=  mark(Y)

a__if(true(),X,Y) =   X +  Y + 
>=  X + 
=  mark(X)

mark(0()) =  
>= 
=  0()

mark(add(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =   X + 
>=  X + 
=  a__from(X)

mark(if(X1,X2,X3)) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 +  x2 + 
p(a__and) =  x1 +  x2 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 +  x2 +  x3 + 
p(add) =  x1 +  x2 + 
p(and) =  x1 +  x2 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 +  x2 +  x3 + 
p(mark) =  x1 + 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
mark(add(X1,X2)) =  X1 +  X2 + 
>  X1 +  X2 + 

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 

a__add(0(),X) =   X + 
>=  X + 
=  mark(X)

a__add(s(X),Y) =   Y + 
>= 

a__and(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  and(X1,X2)

a__and(false(),Y) =   Y + 
>= 
=  false()

a__and(true(),X) =   X + 
>=  X + 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

a__if(X1,X2,X3) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =   X +  Y + 
>=  Y + 
=  mark(Y)

a__if(true(),X,Y) =   X +  Y + 
>=  X + 
=  mark(X)

mark(0()) =  
>= 
=  0()

mark(and(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(first(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  a__first(mark(X1),mark(X2))

mark(from(X)) =  
>= 
=  a__from(X)

mark(if(X1,X2,X3)) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(from(X)) -> a__from(X)
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature:
,if/3,nil/0,s/1,true/0}
- Obligation:
,and,cons,false,first,from,if,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(a__and) = {1},
uargs(a__first) = {1,2},
uargs(a__if) = {1},
uargs(and) = {1},
uargs(first) = {1,2},
uargs(if) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = 
p(a__add) =  x1 +  x2 + 
p(a__and) =  x1 +  x2 + 
p(a__first) =  x1 +  x2 + 
p(a__from) = 
p(a__if) =  x1 +  x2 +  x3 + 
p(add) =  x1 +  x2 + 
p(and) =  x1 +  x2 + 
p(cons) = 
p(false) = 
p(first) =  x1 +  x2 + 
p(from) = 
p(if) =  x1 +  x2 +  x3 + 
p(mark) =  x1 + 
p(nil) = 
p(s) = 
p(true) = 

Following rules are strictly oriented:
mark(first(X1,X2)) =  X1 +  X2 + 
>  X1 +  X2 + 
= a__first(mark(X1),mark(X2))

Following rules are (at-least) weakly oriented:
a__add(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 

a__add(0(),X) =   X + 
>=  X + 
=  mark(X)

a__add(s(X),Y) =   Y + 
>= 

a__and(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  and(X1,X2)

a__and(false(),Y) =   Y + 
>= 
=  false()

a__and(true(),X) =   X + 
>=  X + 
=  mark(X)

a__first(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  first(X1,X2)

a__first(0(),X) =   X + 
>= 
=  nil()

a__first(s(X),cons(Y,Z)) =  
>= 
=  cons(Y,first(X,Z))

a__from(X) =  
>= 
=  cons(X,from(s(X)))

a__from(X) =  
>= 
=  from(X)

a__if(X1,X2,X3) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  if(X1,X2,X3)

a__if(false(),X,Y) =   X +  Y + 
>=  Y + 
=  mark(Y)

a__if(true(),X,Y) =   X +  Y + 
>=  X + 
=  mark(X)

mark(0()) =  
>= 
=  0()

mark(add(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 

mark(and(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  a__and(mark(X1),X2)

mark(cons(X1,X2)) =  
>= 
=  cons(X1,X2)

mark(false()) =  
>= 
=  false()

mark(from(X)) =  
>= 
=  a__from(X)

mark(if(X1,X2,X3)) =   X1 +  X2 +  X3 + 
>=  X1 +  X2 +  X3 + 
=  a__if(mark(X1),X2,X3)

mark(nil()) =  
>= 
=  nil()

mark(s(X)) =  
>= 
=  s(X)

mark(true()) =  
>= 
=  true()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 10: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
a__and(X1,X2) -> and(X1,X2)
a__and(false(),Y) -> false()
a__and(true(),X) -> mark(X)
a__first(X1,X2) -> first(X1,X2)
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
a__from(X) -> cons(X,from(s(X)))
a__from(X) -> from(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
a__if(false(),X,Y) -> mark(Y)
a__if(true(),X,Y) -> mark(X)
mark(0()) -> 0()
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(cons(X1,X2)) -> cons(X1,X2)
mark(false()) -> false()
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(from(X)) -> a__from(X)
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
mark(nil()) -> nil()
mark(s(X)) -> s(X)
mark(true()) -> true()
- Signature: