MAYBE
* Step 1: WeightGap MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(0()) -> 0()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(nil()) -> nil()
mark(s(X)) -> s(mark(X))
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ 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__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(U11) = [1] x1 + [0]
p(U12) = [1] x1 + [0]
p(a__U11) = [1] x1 + [0]
p(a__U12) = [1] x1 + [0]
p(a__length) = [1] x1 + [0]
p(a__zeros) = [0]
p(cons) = [1] x1 + [0]
p(length) = [1] x1 + [0]
p(mark) = [11]
p(nil) = [0]
p(s) = [1] x1 + [0]
p(tt) = [0]
p(zeros) = [0]
Following rules are strictly oriented:
mark(0()) = [11]
> [0]
= 0()
mark(nil()) = [11]
> [0]
= nil()
mark(tt()) = [11]
> [0]
= tt()
mark(zeros()) = [11]
> [0]
= a__zeros()
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1] X1 + [0]
>= [1] X1 + [0]
= U11(X1,X2)
a__U11(tt(),L) = [0]
>= [0]
= a__U12(tt(),L)
a__U12(X1,X2) = [1] X1 + [0]
>= [1] X1 + [0]
= U12(X1,X2)
a__U12(tt(),L) = [0]
>= [11]
= s(a__length(mark(L)))
a__length(X) = [1] X + [0]
>= [1] X + [0]
= length(X)
a__length(cons(N,L)) = [1] N + [0]
>= [0]
= a__U11(tt(),L)
a__length(nil()) = [0]
>= [0]
= 0()
a__zeros() = [0]
>= [0]
= cons(0(),zeros())
a__zeros() = [0]
>= [0]
= zeros()
mark(U11(X1,X2)) = [11]
>= [11]
= a__U11(mark(X1),X2)
mark(U12(X1,X2)) = [11]
>= [11]
= a__U12(mark(X1),X2)
mark(cons(X1,X2)) = [11]
>= [11]
= cons(mark(X1),X2)
mark(length(X)) = [11]
>= [11]
= a__length(mark(X))
mark(s(X)) = [11]
>= [11]
= s(mark(X))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(s(X)) -> s(mark(X))
- Weak TRS:
mark(0()) -> 0()
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ 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__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(U11) = [0]
p(U12) = [0]
p(a__U11) = [1] x1 + [0]
p(a__U12) = [1] x1 + [9]
p(a__length) = [1] x1 + [0]
p(a__zeros) = [0]
p(cons) = [1] x1 + [0]
p(length) = [0]
p(mark) = [0]
p(nil) = [0]
p(s) = [1] x1 + [0]
p(tt) = [0]
p(zeros) = [0]
Following rules are strictly oriented:
a__U12(X1,X2) = [1] X1 + [9]
> [0]
= U12(X1,X2)
a__U12(tt(),L) = [9]
> [0]
= s(a__length(mark(L)))
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1] X1 + [0]
>= [0]
= U11(X1,X2)
a__U11(tt(),L) = [0]
>= [9]
= a__U12(tt(),L)
a__length(X) = [1] X + [0]
>= [0]
= length(X)
a__length(cons(N,L)) = [1] N + [0]
>= [0]
= a__U11(tt(),L)
a__length(nil()) = [0]
>= [0]
= 0()
a__zeros() = [0]
>= [0]
= cons(0(),zeros())
a__zeros() = [0]
>= [0]
= zeros()
mark(0()) = [0]
>= [0]
= 0()
mark(U11(X1,X2)) = [0]
>= [0]
= a__U11(mark(X1),X2)
mark(U12(X1,X2)) = [0]
>= [9]
= a__U12(mark(X1),X2)
mark(cons(X1,X2)) = [0]
>= [0]
= cons(mark(X1),X2)
mark(length(X)) = [0]
>= [0]
= a__length(mark(X))
mark(nil()) = [0]
>= [0]
= nil()
mark(s(X)) = [0]
>= [0]
= s(mark(X))
mark(tt()) = [0]
>= [0]
= tt()
mark(zeros()) = [0]
>= [0]
= a__zeros()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
mark(0()) -> 0()
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ 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__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(U11) = [0]
p(U12) = [0]
p(a__U11) = [1] x1 + [0]
p(a__U12) = [1] x1 + [13]
p(a__length) = [1] x1 + [7]
p(a__zeros) = [1]
p(cons) = [1] x1 + [2]
p(length) = [0]
p(mark) = [1]
p(nil) = [1]
p(s) = [1] x1 + [2]
p(tt) = [1]
p(zeros) = [0]
Following rules are strictly oriented:
a__length(X) = [1] X + [7]
> [0]
= length(X)
a__length(cons(N,L)) = [1] N + [9]
> [1]
= a__U11(tt(),L)
a__length(nil()) = [8]
> [1]
= 0()
a__zeros() = [1]
> [0]
= zeros()
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1] X1 + [0]
>= [0]
= U11(X1,X2)
a__U11(tt(),L) = [1]
>= [14]
= a__U12(tt(),L)
a__U12(X1,X2) = [1] X1 + [13]
>= [0]
= U12(X1,X2)
a__U12(tt(),L) = [14]
>= [10]
= s(a__length(mark(L)))
a__zeros() = [1]
>= [3]
= cons(0(),zeros())
mark(0()) = [1]
>= [1]
= 0()
mark(U11(X1,X2)) = [1]
>= [1]
= a__U11(mark(X1),X2)
mark(U12(X1,X2)) = [1]
>= [14]
= a__U12(mark(X1),X2)
mark(cons(X1,X2)) = [1]
>= [3]
= cons(mark(X1),X2)
mark(length(X)) = [1]
>= [8]
= a__length(mark(X))
mark(nil()) = [1]
>= [1]
= nil()
mark(s(X)) = [1]
>= [3]
= s(mark(X))
mark(tt()) = [1]
>= [1]
= tt()
mark(zeros()) = [1]
>= [1]
= a__zeros()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
a__zeros() -> cons(0(),zeros())
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> zeros()
mark(0()) -> 0()
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ 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__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [8]
p(U11) = [1] x1 + [1] x2 + [2]
p(U12) = [1] x1 + [1] x2 + [6]
p(a__U11) = [1] x1 + [1] x2 + [1]
p(a__U12) = [1] x1 + [1] x2 + [6]
p(a__length) = [1] x1 + [6]
p(a__zeros) = [0]
p(cons) = [1] x1 + [1] x2 + [8]
p(length) = [1] x1 + [6]
p(mark) = [1] x1 + [0]
p(nil) = [8]
p(s) = [1] x1 + [0]
p(tt) = [0]
p(zeros) = [0]
Following rules are strictly oriented:
mark(U11(X1,X2)) = [1] X1 + [1] X2 + [2]
> [1] X1 + [1] X2 + [1]
= a__U11(mark(X1),X2)
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [2]
= U11(X1,X2)
a__U11(tt(),L) = [1] L + [1]
>= [1] L + [6]
= a__U12(tt(),L)
a__U12(X1,X2) = [1] X1 + [1] X2 + [6]
>= [1] X1 + [1] X2 + [6]
= U12(X1,X2)
a__U12(tt(),L) = [1] L + [6]
>= [1] L + [6]
= s(a__length(mark(L)))
a__length(X) = [1] X + [6]
>= [1] X + [6]
= length(X)
a__length(cons(N,L)) = [1] L + [1] N + [14]
>= [1] L + [1]
= a__U11(tt(),L)
a__length(nil()) = [14]
>= [8]
= 0()
a__zeros() = [0]
>= [16]
= cons(0(),zeros())
a__zeros() = [0]
>= [0]
= zeros()
mark(0()) = [8]
>= [8]
= 0()
mark(U12(X1,X2)) = [1] X1 + [1] X2 + [6]
>= [1] X1 + [1] X2 + [6]
= a__U12(mark(X1),X2)
mark(cons(X1,X2)) = [1] X1 + [1] X2 + [8]
>= [1] X1 + [1] X2 + [8]
= cons(mark(X1),X2)
mark(length(X)) = [1] X + [6]
>= [1] X + [6]
= a__length(mark(X))
mark(nil()) = [8]
>= [8]
= nil()
mark(s(X)) = [1] X + [0]
>= [1] X + [0]
= s(mark(X))
mark(tt()) = [0]
>= [0]
= tt()
mark(zeros()) = [0]
>= [0]
= a__zeros()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
a__zeros() -> cons(0(),zeros())
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> zeros()
mark(0()) -> 0()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ 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__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(U11) = [4]
p(U12) = [0]
p(a__U11) = [1] x1 + [0]
p(a__U12) = [1] x1 + [4]
p(a__length) = [1] x1 + [0]
p(a__zeros) = [4]
p(cons) = [1] x1 + [0]
p(length) = [0]
p(mark) = [4]
p(nil) = [1]
p(s) = [1] x1 + [0]
p(tt) = [0]
p(zeros) = [4]
Following rules are strictly oriented:
a__zeros() = [4]
> [1]
= cons(0(),zeros())
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1] X1 + [0]
>= [4]
= U11(X1,X2)
a__U11(tt(),L) = [0]
>= [4]
= a__U12(tt(),L)
a__U12(X1,X2) = [1] X1 + [4]
>= [0]
= U12(X1,X2)
a__U12(tt(),L) = [4]
>= [4]
= s(a__length(mark(L)))
a__length(X) = [1] X + [0]
>= [0]
= length(X)
a__length(cons(N,L)) = [1] N + [0]
>= [0]
= a__U11(tt(),L)
a__length(nil()) = [1]
>= [1]
= 0()
a__zeros() = [4]
>= [4]
= zeros()
mark(0()) = [4]
>= [1]
= 0()
mark(U11(X1,X2)) = [4]
>= [4]
= a__U11(mark(X1),X2)
mark(U12(X1,X2)) = [4]
>= [8]
= a__U12(mark(X1),X2)
mark(cons(X1,X2)) = [4]
>= [4]
= cons(mark(X1),X2)
mark(length(X)) = [4]
>= [4]
= a__length(mark(X))
mark(nil()) = [4]
>= [1]
= nil()
mark(s(X)) = [4]
>= [4]
= s(mark(X))
mark(tt()) = [4]
>= [0]
= tt()
mark(zeros()) = [4]
>= [4]
= a__zeros()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: NaturalMI MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(0()) -> 0()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(a__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{a__U11,a__U12,a__length,a__zeros,mark}
TcT has computed the following interpretation:
p(0) = [0]
[0]
p(U11) = [1 0] x1 + [0 4] x2 + [0]
[0 1] [0 1] [0]
p(U12) = [1 0] x1 + [0 4] x2 + [0]
[0 1] [0 1] [0]
p(a__U11) = [1 0] x1 + [0 4] x2 + [0]
[0 1] [0 1] [0]
p(a__U12) = [1 0] x1 + [0 4] x2 + [0]
[0 1] [0 1] [0]
p(a__length) = [1 0] x1 + [0]
[0 1] [0]
p(a__zeros) = [0]
[2]
p(cons) = [1 0] x1 + [0 4] x2 + [0]
[0 1] [0 1] [2]
p(length) = [0 0] x1 + [0]
[0 1] [0]
p(mark) = [0 4] x1 + [0]
[0 1] [2]
p(nil) = [4]
[1]
p(s) = [1 0] x1 + [0]
[0 1] [0]
p(tt) = [0]
[2]
p(zeros) = [0]
[0]
Following rules are strictly oriented:
mark(cons(X1,X2)) = [0 4] X1 + [0 4] X2 + [8]
[0 1] [0 1] [4]
> [0 4] X1 + [0 4] X2 + [0]
[0 1] [0 1] [4]
= cons(mark(X1),X2)
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1 0] X1 + [0 4] X2 + [0]
[0 1] [0 1] [0]
>= [1 0] X1 + [0 4] X2 + [0]
[0 1] [0 1] [0]
= U11(X1,X2)
a__U11(tt(),L) = [0 4] L + [0]
[0 1] [2]
>= [0 4] L + [0]
[0 1] [2]
= a__U12(tt(),L)
a__U12(X1,X2) = [1 0] X1 + [0 4] X2 + [0]
[0 1] [0 1] [0]
>= [1 0] X1 + [0 4] X2 + [0]
[0 1] [0 1] [0]
= U12(X1,X2)
a__U12(tt(),L) = [0 4] L + [0]
[0 1] [2]
>= [0 4] L + [0]
[0 1] [2]
= s(a__length(mark(L)))
a__length(X) = [1 0] X + [0]
[0 1] [0]
>= [0 0] X + [0]
[0 1] [0]
= length(X)
a__length(cons(N,L)) = [0 4] L + [1 0] N + [0]
[0 1] [0 1] [2]
>= [0 4] L + [0]
[0 1] [2]
= a__U11(tt(),L)
a__length(nil()) = [4]
[1]
>= [0]
[0]
= 0()
a__zeros() = [0]
[2]
>= [0]
[2]
= cons(0(),zeros())
a__zeros() = [0]
[2]
>= [0]
[0]
= zeros()
mark(0()) = [0]
[2]
>= [0]
[0]
= 0()
mark(U11(X1,X2)) = [0 4] X1 + [0 4] X2 + [0]
[0 1] [0 1] [2]
>= [0 4] X1 + [0 4] X2 + [0]
[0 1] [0 1] [2]
= a__U11(mark(X1),X2)
mark(U12(X1,X2)) = [0 4] X1 + [0 4] X2 + [0]
[0 1] [0 1] [2]
>= [0 4] X1 + [0 4] X2 + [0]
[0 1] [0 1] [2]
= a__U12(mark(X1),X2)
mark(length(X)) = [0 4] X + [0]
[0 1] [2]
>= [0 4] X + [0]
[0 1] [2]
= a__length(mark(X))
mark(nil()) = [4]
[3]
>= [4]
[1]
= nil()
mark(s(X)) = [0 4] X + [0]
[0 1] [2]
>= [0 4] X + [0]
[0 1] [2]
= s(mark(X))
mark(tt()) = [8]
[4]
>= [0]
[2]
= tt()
mark(zeros()) = [0]
[2]
>= [0]
[2]
= a__zeros()
* Step 7: NaturalMI MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(0()) -> 0()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(a__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{a__U11,a__U12,a__length,a__zeros,mark}
TcT has computed the following interpretation:
p(0) = [0]
[0]
p(U11) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [1]
p(U12) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [1]
p(a__U11) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [1]
p(a__U12) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [1]
p(a__length) = [1 0] x1 + [0]
[0 1] [1]
p(a__zeros) = [0]
[0]
p(cons) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [0]
p(length) = [0 0] x1 + [0]
[0 1] [1]
p(mark) = [0 1] x1 + [0]
[0 1] [0]
p(nil) = [4]
[6]
p(s) = [1 0] x1 + [0]
[0 1] [0]
p(tt) = [0]
[0]
p(zeros) = [0]
[0]
Following rules are strictly oriented:
mark(U12(X1,X2)) = [0 1] X1 + [0 1] X2 + [1]
[0 1] [0 1] [1]
> [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [1]
= a__U12(mark(X1),X2)
mark(length(X)) = [0 1] X + [1]
[0 1] [1]
> [0 1] X + [0]
[0 1] [1]
= a__length(mark(X))
Following rules are (at-least) weakly oriented:
a__U11(X1,X2) = [1 0] X1 + [0 1] X2 + [0]
[0 1] [0 1] [1]
>= [0 0] X1 + [0 0] X2 + [0]
[0 1] [0 1] [1]
= U11(X1,X2)
a__U11(tt(),L) = [0 1] L + [0]
[0 1] [1]
>= [0 1] L + [0]
[0 1] [1]
= a__U12(tt(),L)
a__U12(X1,X2) = [1 0] X1 + [0 1] X2 + [0]
[0 1] [0 1] [1]
>= [0 0] X1 + [0 0] X2 + [0]
[0 1] [0 1] [1]
= U12(X1,X2)
a__U12(tt(),L) = [0 1] L + [0]
[0 1] [1]
>= [0 1] L + [0]
[0 1] [1]
= s(a__length(mark(L)))
a__length(X) = [1 0] X + [0]
[0 1] [1]
>= [0 0] X + [0]
[0 1] [1]
= length(X)
a__length(cons(N,L)) = [0 1] L + [1 0] N + [0]
[0 1] [0 1] [1]
>= [0 1] L + [0]
[0 1] [1]
= a__U11(tt(),L)
a__length(nil()) = [4]
[7]
>= [0]
[0]
= 0()
a__zeros() = [0]
[0]
>= [0]
[0]
= cons(0(),zeros())
a__zeros() = [0]
[0]
>= [0]
[0]
= zeros()
mark(0()) = [0]
[0]
>= [0]
[0]
= 0()
mark(U11(X1,X2)) = [0 1] X1 + [0 1] X2 + [1]
[0 1] [0 1] [1]
>= [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [1]
= a__U11(mark(X1),X2)
mark(cons(X1,X2)) = [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [0]
>= [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [0]
= cons(mark(X1),X2)
mark(nil()) = [6]
[6]
>= [4]
[6]
= nil()
mark(s(X)) = [0 1] X + [0]
[0 1] [0]
>= [0 1] X + [0]
[0 1] [0]
= s(mark(X))
mark(tt()) = [0]
[0]
>= [0]
[0]
= tt()
mark(zeros()) = [0]
[0]
>= [0]
[0]
= a__zeros()
* Step 8: NaturalMI MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U11(tt(),L) -> a__U12(tt(),L)
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(0()) -> 0()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(a__U11) = {1},
uargs(a__U12) = {1},
uargs(a__length) = {1},
uargs(cons) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{a__U11,a__U12,a__length,a__zeros,mark}
TcT has computed the following interpretation:
p(0) = [0]
[0]
p(U11) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [6]
p(U12) = [1 0] x1 + [0 1] x2 + [6]
[0 1] [0 1] [6]
p(a__U11) = [1 0] x1 + [0 1] x2 + [6]
[0 1] [0 1] [6]
p(a__U12) = [1 0] x1 + [0 1] x2 + [6]
[0 1] [0 1] [6]
p(a__length) = [1 0] x1 + [6]
[0 1] [6]
p(a__zeros) = [0]
[0]
p(cons) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [0]
p(length) = [1 0] x1 + [0]
[0 1] [6]
p(mark) = [0 1] x1 + [0]
[0 1] [0]
p(nil) = [4]
[5]
p(s) = [1 0] x1 + [0]
[0 1] [0]
p(tt) = [0]
[0]
p(zeros) = [0]
[0]
Following rules are strictly oriented:
a__U11(X1,X2) = [1 0] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
> [1 0] X1 + [0 1] X2 + [0]
[0 1] [0 1] [6]
= U11(X1,X2)
Following rules are (at-least) weakly oriented:
a__U11(tt(),L) = [0 1] L + [6]
[0 1] [6]
>= [0 1] L + [6]
[0 1] [6]
= a__U12(tt(),L)
a__U12(X1,X2) = [1 0] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
>= [1 0] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
= U12(X1,X2)
a__U12(tt(),L) = [0 1] L + [6]
[0 1] [6]
>= [0 1] L + [6]
[0 1] [6]
= s(a__length(mark(L)))
a__length(X) = [1 0] X + [6]
[0 1] [6]
>= [1 0] X + [0]
[0 1] [6]
= length(X)
a__length(cons(N,L)) = [0 1] L + [1 0] N + [6]
[0 1] [0 1] [6]
>= [0 1] L + [6]
[0 1] [6]
= a__U11(tt(),L)
a__length(nil()) = [10]
[11]
>= [0]
[0]
= 0()
a__zeros() = [0]
[0]
>= [0]
[0]
= cons(0(),zeros())
a__zeros() = [0]
[0]
>= [0]
[0]
= zeros()
mark(0()) = [0]
[0]
>= [0]
[0]
= 0()
mark(U11(X1,X2)) = [0 1] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
>= [0 1] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
= a__U11(mark(X1),X2)
mark(U12(X1,X2)) = [0 1] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
>= [0 1] X1 + [0 1] X2 + [6]
[0 1] [0 1] [6]
= a__U12(mark(X1),X2)
mark(cons(X1,X2)) = [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [0]
>= [0 1] X1 + [0 1] X2 + [0]
[0 1] [0 1] [0]
= cons(mark(X1),X2)
mark(length(X)) = [0 1] X + [6]
[0 1] [6]
>= [0 1] X + [6]
[0 1] [6]
= a__length(mark(X))
mark(nil()) = [5]
[5]
>= [4]
[5]
= nil()
mark(s(X)) = [0 1] X + [0]
[0 1] [0]
>= [0 1] X + [0]
[0 1] [0]
= s(mark(X))
mark(tt()) = [0]
[0]
>= [0]
[0]
= tt()
mark(zeros()) = [0]
[0]
>= [0]
[0]
= a__zeros()
* Step 9: Failure MAYBE
+ Considered Problem:
- Strict TRS:
a__U11(tt(),L) -> a__U12(tt(),L)
mark(s(X)) -> s(mark(X))
- Weak TRS:
a__U11(X1,X2) -> U11(X1,X2)
a__U12(X1,X2) -> U12(X1,X2)
a__U12(tt(),L) -> s(a__length(mark(L)))
a__length(X) -> length(X)
a__length(cons(N,L)) -> a__U11(tt(),L)
a__length(nil()) -> 0()
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
mark(0()) -> 0()
mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(length(X)) -> a__length(mark(X))
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(zeros()) -> a__zeros()
- Signature:
{a__U11/2,a__U12/2,a__length/1,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,cons/2,length/1,nil/0,s/1,tt/0,zeros/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__length,a__zeros
,mark} and constructors {0,U11,U12,cons,length,nil,s,tt,zeros}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE