Problem:
a__zeros() -> cons(0(),zeros())
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(0()) -> 0()
a__zeros() -> zeros()
a__tail(X) -> tail(X)
Proof:
Complexity Transformation Processor:
strict:
a__zeros() -> cons(0(),zeros())
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(0()) -> 0()
a__zeros() -> zeros()
a__tail(X) -> tail(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0,
[mark](x0) = x0 + 3,
[a__tail](x0) = x0 + 13,
[cons](x0, x1) = x0 + x1 + 1,
[zeros] = 0,
[0] = 1,
[a__zeros] = 0
orientation:
a__zeros() = 0 >= 2 = cons(0(),zeros())
a__tail(cons(X,XS)) = X + XS + 14 >= XS + 3 = mark(XS)
mark(zeros()) = 3 >= 0 = a__zeros()
mark(tail(X)) = X + 3 >= X + 16 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = cons(mark(X1),X2)
mark(0()) = 4 >= 1 = 0()
a__zeros() = 0 >= 0 = zeros()
a__tail(X) = X + 13 >= X = tail(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
a__zeros() -> zeros()
weak:
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0,
[mark](x0) = x0 + 2,
[a__tail](x0) = x0,
[cons](x0, x1) = x0 + x1 + 2,
[zeros] = 2,
[0] = 14,
[a__zeros] = 4
orientation:
a__zeros() = 4 >= 18 = cons(0(),zeros())
mark(tail(X)) = X + 2 >= X + 2 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = cons(mark(X1),X2)
a__zeros() = 4 >= 2 = zeros()
a__tail(cons(X,XS)) = X + XS + 2 >= XS + 2 = mark(XS)
mark(zeros()) = 4 >= 4 = a__zeros()
mark(0()) = 16 >= 14 = 0()
a__tail(X) = X >= X = tail(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
weak:
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tail](x0) = x0 + 8,
[mark](x0) = x0 + 8,
[a__tail](x0) = x0 + 8,
[cons](x0, x1) = x0 + x1 + 3,
[zeros] = 0,
[0] = 2,
[a__zeros] = 8
orientation:
a__zeros() = 8 >= 5 = cons(0(),zeros())
mark(tail(X)) = X + 16 >= X + 16 = a__tail(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 11 >= X1 + X2 + 11 = cons(mark(X1),X2)
a__zeros() = 8 >= 0 = zeros()
a__tail(cons(X,XS)) = X + XS + 11 >= XS + 8 = mark(XS)
mark(zeros()) = 8 >= 8 = a__zeros()
mark(0()) = 10 >= 2 = 0()
a__tail(X) = X + 8 >= X + 8 = tail(X)
problem:
strict:
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
weak:
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Splitting Processor:
strict:
mark(tail(X)) -> a__tail(mark(X))
weak:
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {7,6,5}
transitions:
a__tail1(9) -> 10*
mark1(25) -> 31*
mark1(17) -> 10*
mark1(2) -> 10*
mark1(24) -> 25*
mark1(4) -> 10*
mark1(16) -> 17*
mark1(1) -> 10*
mark1(28) -> 10*
mark1(18) -> 19*
mark1(8) -> 9*
mark1(3) -> 10*
cons1(19,2) -> 9*
cons1(9,2) -> 9*
cons1(19,4) -> 9*
cons1(9,4) -> 9*
cons1(25,1) -> 9*
cons1(25,3) -> 9*
cons1(10,1) -> 10*
cons1(10,3) -> 10*
cons1(29,28) -> 6*
cons1(25,17) -> 7*
cons1(10,17) -> 10*
cons1(31,28) -> 10*
cons1(9,1) -> 9*
cons1(9,3) -> 9*
cons1(25,2) -> 9*
cons1(25,4) -> 9*
cons1(10,2) -> 10*
cons1(10,4) -> 10*
cons1(25,28) -> 17,5
cons1(17,2) -> 9*
cons1(17,4) -> 9*
tail1(9) -> 10*
01() -> 31,10,25,29
a__zeros1() -> 10,17
zeros1() -> 10,17,28
mark0(2) -> 7,5
mark0(4) -> 7,5
mark0(1) -> 7,5
mark0(3) -> 7,5
tail0(2) -> 7,1
tail0(4) -> 7,1
tail0(1) -> 7,1
tail0(3) -> 7,1
a__tail0(2) -> 7*
a__tail0(4) -> 7*
a__tail0(1) -> 7*
a__tail0(3) -> 7*
a__zeros0() -> 7,5,6
cons0(3,1) -> 2*
cons0(3,3) -> 2*
cons0(4,2) -> 2*
cons0(4,4) -> 2*
cons0(5,1) -> 7,5
cons0(5,3) -> 7,5
cons0(1,2) -> 2*
cons0(1,4) -> 2*
cons0(2,1) -> 2*
cons0(2,3) -> 2*
cons0(3,2) -> 2*
cons0(3,4) -> 2*
cons0(4,1) -> 2*
cons0(4,3) -> 2*
cons0(5,2) -> 7,5
cons0(5,4) -> 7,5
cons0(1,1) -> 2*
cons0(1,3) -> 2*
cons0(2,2) -> 2*
cons0(2,4) -> 2*
00() -> 7,5,3
zeros0() -> 7,5,6,4
1 -> 18*
2 -> 8*
3 -> 24*
4 -> 16*
10 -> 7,19,5
17 -> 9*
19 -> 9*
25 -> 9*
problem:
strict:
weak:
mark(tail(X)) -> a__tail(mark(X))
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
Qed
strict:
mark(cons(X1,X2)) -> cons(mark(X1),X2)
weak:
mark(tail(X)) -> a__tail(mark(X))
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 0]
[0 1 0]
[0 0 0]
interpretation:
[1 0 0]
[tail](x0) = [0 1 0]x0
[0 0 0] ,
[1 1 0] [0]
[mark](x0) = [0 1 0]x0 + [1]
[0 0 0] [0],
[1 0 0]
[a__tail](x0) = [0 1 0]x0
[0 0 0] ,
[1 0 0] [1 1 0] [0]
[cons](x0, x1) = [0 1 0]x0 + [0 1 0]x1 + [1]
[0 0 0] [0 0 0] [0],
[0]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[0]
[a__zeros] = [1]
[0]
orientation:
[1 1 0] [1 2 0] [1] [1 1 0] [1 1 0] [0]
mark(cons(X1,X2)) = [0 1 0]X1 + [0 1 0]X2 + [2] >= [0 1 0]X1 + [0 1 0]X2 + [2] = cons(mark(X1),X2)
[0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0]
[1 1 0] [0] [1 1 0] [0]
mark(tail(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = a__tail(mark(X))
[0 0 0] [0] [0 0 0] [0]
[0] [0]
a__zeros() = [1] >= [1] = cons(0(),zeros())
[0] [0]
[0] [0]
a__zeros() = [1] >= [0] = zeros()
[0] [0]
[1 0 0] [1 1 0] [0] [1 1 0] [0]
a__tail(cons(X,XS)) = [0 1 0]X + [0 1 0]XS + [1] >= [0 1 0]XS + [1] = mark(XS)
[0 0 0] [0 0 0] [0] [0 0 0] [0]
[0] [0]
mark(zeros()) = [1] >= [1] = a__zeros()
[0] [0]
[0] [0]
mark(0()) = [1] >= [0] = 0()
[0] [0]
[1 0 0] [1 0 0]
a__tail(X) = [0 1 0]X >= [0 1 0]X = tail(X)
[0 0 0] [0 0 0]
problem:
strict:
weak:
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(tail(X)) -> a__tail(mark(X))
a__zeros() -> cons(0(),zeros())
a__zeros() -> zeros()
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(0()) -> 0()
a__tail(X) -> tail(X)
Qed