Problem:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(adx(X)) -> a__adx(mark(X))
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__nats() -> nats()
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Proof:
Complexity Transformation Processor:
strict:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(adx(X)) -> a__adx(mark(X))
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__nats() -> nats()
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0,
[hd](x0) = x0 + 2,
[nats] = 1,
[a__tl](x0) = x0 + 13,
[mark](x0) = x0 + 1,
[a__hd](x0) = x0 + 8,
[adx](x0) = x0 + 2,
[incr](x0) = x0 + 4,
[s](x0) = x0 + 5,
[a__incr](x0) = x0 + 15,
[cons](x0, x1) = x0 + x1 + 10,
[zeros] = 7,
[0] = 2,
[a__adx](x0) = x0 + 15,
[a__zeros] = 5,
[a__nats] = 0
orientation:
a__nats() = 0 >= 20 = a__adx(a__zeros())
a__zeros() = 5 >= 19 = cons(0(),zeros())
a__incr(cons(X,Y)) = X + Y + 25 >= X + Y + 19 = cons(s(X),incr(Y))
a__adx(cons(X,Y)) = X + Y + 25 >= X + Y + 27 = a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) = X + Y + 18 >= X + 1 = mark(X)
a__tl(cons(X,Y)) = X + Y + 23 >= Y + 1 = mark(Y)
mark(nats()) = 2 >= 0 = a__nats()
mark(adx(X)) = X + 3 >= X + 16 = a__adx(mark(X))
mark(zeros()) = 8 >= 5 = a__zeros()
mark(incr(X)) = X + 5 >= X + 16 = a__incr(mark(X))
mark(hd(X)) = X + 3 >= X + 9 = a__hd(mark(X))
mark(tl(X)) = X + 1 >= X + 14 = a__tl(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 11 >= X1 + X2 + 10 = cons(X1,X2)
mark(0()) = 3 >= 2 = 0()
mark(s(X)) = X + 6 >= X + 5 = s(X)
a__nats() = 0 >= 1 = nats()
a__adx(X) = X + 15 >= X + 2 = adx(X)
a__zeros() = 5 >= 7 = zeros()
a__incr(X) = X + 15 >= X + 4 = incr(X)
a__hd(X) = X + 8 >= X + 2 = hd(X)
a__tl(X) = X + 13 >= X = tl(X)
problem:
strict:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__nats() -> nats()
a__zeros() -> zeros()
weak:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0,
[hd](x0) = x0,
[nats] = 14,
[a__tl](x0) = x0,
[mark](x0) = x0,
[a__hd](x0) = x0,
[adx](x0) = x0,
[incr](x0) = x0,
[s](x0) = x0 + 8,
[a__incr](x0) = x0 + 8,
[cons](x0, x1) = x0 + x1,
[zeros] = 8,
[0] = 6,
[a__adx](x0) = x0 + 9,
[a__zeros] = 8,
[a__nats] = 14
orientation:
a__nats() = 14 >= 17 = a__adx(a__zeros())
a__zeros() = 8 >= 14 = cons(0(),zeros())
a__adx(cons(X,Y)) = X + Y + 9 >= X + Y + 8 = a__incr(cons(X,adx(Y)))
mark(adx(X)) = X >= X + 9 = a__adx(mark(X))
mark(incr(X)) = X >= X + 8 = a__incr(mark(X))
mark(hd(X)) = X >= X = a__hd(mark(X))
mark(tl(X)) = X >= X = a__tl(mark(X))
a__nats() = 14 >= 14 = nats()
a__zeros() = 8 >= 8 = zeros()
a__incr(cons(X,Y)) = X + Y + 8 >= X + Y + 8 = cons(s(X),incr(Y))
a__hd(cons(X,Y)) = X + Y >= X = mark(X)
a__tl(cons(X,Y)) = X + Y >= Y = mark(Y)
mark(nats()) = 14 >= 14 = a__nats()
mark(zeros()) = 8 >= 8 = a__zeros()
mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
mark(0()) = 6 >= 6 = 0()
mark(s(X)) = X + 8 >= X + 8 = s(X)
a__adx(X) = X + 9 >= X = adx(X)
a__incr(X) = X + 8 >= X = incr(X)
a__hd(X) = X >= X = hd(X)
a__tl(X) = X >= X = tl(X)
problem:
strict:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__nats() -> nats()
a__zeros() -> zeros()
weak:
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0,
[hd](x0) = x0,
[nats] = 14,
[a__tl](x0) = x0,
[mark](x0) = x0,
[a__hd](x0) = x0,
[adx](x0) = x0,
[incr](x0) = x0 + 2,
[s](x0) = x0,
[a__incr](x0) = x0 + 2,
[cons](x0, x1) = x0 + x1,
[zeros] = 0,
[0] = 0,
[a__adx](x0) = x0 + 2,
[a__zeros] = 0,
[a__nats] = 14
orientation:
a__nats() = 14 >= 2 = a__adx(a__zeros())
a__zeros() = 0 >= 0 = cons(0(),zeros())
mark(adx(X)) = X >= X + 2 = a__adx(mark(X))
mark(incr(X)) = X + 2 >= X + 2 = a__incr(mark(X))
mark(hd(X)) = X >= X = a__hd(mark(X))
mark(tl(X)) = X >= X = a__tl(mark(X))
a__nats() = 14 >= 14 = nats()
a__zeros() = 0 >= 0 = zeros()
a__adx(cons(X,Y)) = X + Y + 2 >= X + Y + 2 = a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) = X + Y + 2 >= X + Y + 2 = cons(s(X),incr(Y))
a__hd(cons(X,Y)) = X + Y >= X = mark(X)
a__tl(cons(X,Y)) = X + Y >= Y = mark(Y)
mark(nats()) = 14 >= 14 = a__nats()
mark(zeros()) = 0 >= 0 = a__zeros()
mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
mark(0()) = 0 >= 0 = 0()
mark(s(X)) = X >= X = s(X)
a__adx(X) = X + 2 >= X = adx(X)
a__incr(X) = X + 2 >= X + 2 = incr(X)
a__hd(X) = X >= X = hd(X)
a__tl(X) = X >= X = tl(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__nats() -> nats()
a__zeros() -> zeros()
weak:
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0,
[hd](x0) = x0,
[nats] = 8,
[a__tl](x0) = x0,
[mark](x0) = x0 + 4,
[a__hd](x0) = x0,
[adx](x0) = x0,
[incr](x0) = x0 + 5,
[s](x0) = x0 + 3,
[a__incr](x0) = x0 + 9,
[cons](x0, x1) = x0 + x1 + 13,
[zeros] = 0,
[0] = 15,
[a__adx](x0) = x0 + 9,
[a__zeros] = 3,
[a__nats] = 12
orientation:
a__zeros() = 3 >= 28 = cons(0(),zeros())
mark(adx(X)) = X + 4 >= X + 13 = a__adx(mark(X))
mark(incr(X)) = X + 9 >= X + 13 = a__incr(mark(X))
mark(hd(X)) = X + 4 >= X + 4 = a__hd(mark(X))
mark(tl(X)) = X + 4 >= X + 4 = a__tl(mark(X))
a__nats() = 12 >= 8 = nats()
a__zeros() = 3 >= 0 = zeros()
a__nats() = 12 >= 12 = a__adx(a__zeros())
a__adx(cons(X,Y)) = X + Y + 22 >= X + Y + 22 = a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) = X + Y + 22 >= X + Y + 21 = cons(s(X),incr(Y))
a__hd(cons(X,Y)) = X + Y + 13 >= X + 4 = mark(X)
a__tl(cons(X,Y)) = X + Y + 13 >= Y + 4 = mark(Y)
mark(nats()) = 12 >= 12 = a__nats()
mark(zeros()) = 4 >= 3 = a__zeros()
mark(cons(X1,X2)) = X1 + X2 + 17 >= X1 + X2 + 13 = cons(X1,X2)
mark(0()) = 19 >= 15 = 0()
mark(s(X)) = X + 7 >= X + 3 = s(X)
a__adx(X) = X + 9 >= X = adx(X)
a__incr(X) = X + 9 >= X + 5 = incr(X)
a__hd(X) = X >= X = hd(X)
a__tl(X) = X >= X = tl(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
weak:
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0 + 4,
[hd](x0) = x0 + 8,
[nats] = 3,
[a__tl](x0) = x0 + 4,
[mark](x0) = x0 + 2,
[a__hd](x0) = x0 + 8,
[adx](x0) = x0,
[incr](x0) = x0,
[s](x0) = x0,
[a__incr](x0) = x0,
[cons](x0, x1) = x0 + x1,
[zeros] = 0,
[0] = 0,
[a__adx](x0) = x0,
[a__zeros] = 1,
[a__nats] = 4
orientation:
a__zeros() = 1 >= 0 = cons(0(),zeros())
mark(adx(X)) = X + 2 >= X + 2 = a__adx(mark(X))
mark(incr(X)) = X + 2 >= X + 2 = a__incr(mark(X))
mark(hd(X)) = X + 10 >= X + 10 = a__hd(mark(X))
mark(tl(X)) = X + 6 >= X + 6 = a__tl(mark(X))
a__nats() = 4 >= 3 = nats()
a__zeros() = 1 >= 0 = zeros()
a__nats() = 4 >= 1 = a__adx(a__zeros())
a__adx(cons(X,Y)) = X + Y >= X + Y = a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) = X + Y >= X + Y = cons(s(X),incr(Y))
a__hd(cons(X,Y)) = X + Y + 8 >= X + 2 = mark(X)
a__tl(cons(X,Y)) = X + Y + 4 >= Y + 2 = mark(Y)
mark(nats()) = 5 >= 4 = a__nats()
mark(zeros()) = 2 >= 1 = a__zeros()
mark(cons(X1,X2)) = X1 + X2 + 2 >= X1 + X2 = cons(X1,X2)
mark(0()) = 2 >= 0 = 0()
mark(s(X)) = X + 2 >= X = s(X)
a__adx(X) = X >= X = adx(X)
a__incr(X) = X >= X = incr(X)
a__hd(X) = X + 8 >= X + 8 = hd(X)
a__tl(X) = X + 4 >= X + 4 = tl(X)
problem:
strict:
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
weak:
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 1 1]
[0 0 0]
interpretation:
[1 0 0] [0]
[tl](x0) = [0 1 0]x0 + [1]
[0 0 0] [0],
[1 1 0]
[hd](x0) = [0 1 0]x0
[0 0 0] ,
[0]
[nats] = [0]
[0],
[1 0 0] [0]
[a__tl](x0) = [0 1 0]x0 + [1]
[0 0 0] [0],
[1 1 0]
[mark](x0) = [0 1 0]x0
[0 0 0] ,
[1 1 1]
[a__hd](x0) = [0 1 0]x0
[0 0 0] ,
[1 0 0]
[adx](x0) = [0 1 0]x0
[0 0 0] ,
[1 0 0]
[incr](x0) = [0 1 0]x0
[0 0 0] ,
[1 0 0]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[a__incr](x0) = [0 1 1]x0
[0 0 0] ,
[1 0 0] [1 1 0]
[cons](x0, x1) = [0 1 0]x0 + [0 1 0]x1
[0 0 0] [0 0 0] ,
[0]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[1 0 0]
[a__adx](x0) = [0 1 0]x0
[0 0 0] ,
[0]
[a__zeros] = [0]
[0],
[0]
[a__nats] = [0]
[0]
orientation:
[1 1 0] [1 1 0]
mark(adx(X)) = [0 1 0]X >= [0 1 0]X = a__adx(mark(X))
[0 0 0] [0 0 0]
[1 1 0] [1 1 0]
mark(incr(X)) = [0 1 0]X >= [0 1 0]X = a__incr(mark(X))
[0 0 0] [0 0 0]
[1 2 0] [1 2 0]
mark(hd(X)) = [0 1 0]X >= [0 1 0]X = a__hd(mark(X))
[0 0 0] [0 0 0]
[1 1 0] [1] [1 1 0] [0]
mark(tl(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = a__tl(mark(X))
[0 0 0] [0] [0 0 0] [0]
[0] [0]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[0] [0]
a__nats() = [0] >= [0] = nats()
[0] [0]
[0] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[0] [0]
a__nats() = [0] >= [0] = a__adx(a__zeros())
[0] [0]
[1 0 0] [1 1 0] [1 0 0] [1 1 0]
a__adx(cons(X,Y)) = [0 1 0]X + [0 1 0]Y >= [0 1 0]X + [0 1 0]Y = a__incr(cons(X,adx(Y)))
[0 0 0] [0 0 0] [0 0 0] [0 0 0]
[1 0 0] [1 1 0] [1 0 0] [1 1 0]
a__incr(cons(X,Y)) = [0 1 0]X + [0 1 0]Y >= [0 0 0]X + [0 1 0]Y = cons(s(X),incr(Y))
[0 0 0] [0 0 0] [0 0 0] [0 0 0]
[1 1 0] [1 2 0] [1 1 0]
a__hd(cons(X,Y)) = [0 1 0]X + [0 1 0]Y >= [0 1 0]X = mark(X)
[0 0 0] [0 0 0] [0 0 0]
[1 0 0] [1 1 0] [0] [1 1 0]
a__tl(cons(X,Y)) = [0 1 0]X + [0 1 0]Y + [1] >= [0 1 0]Y = mark(Y)
[0 0 0] [0 0 0] [0] [0 0 0]
[0] [0]
mark(nats()) = [0] >= [0] = a__nats()
[0] [0]
[0] [0]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 1 0] [1 2 0] [1 0 0] [1 1 0]
mark(cons(X1,X2)) = [0 1 0]X1 + [0 1 0]X2 >= [0 1 0]X1 + [0 1 0]X2 = cons(X1,X2)
[0 0 0] [0 0 0] [0 0 0] [0 0 0]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 0 0] [1 0 0]
mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(X)
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
a__adx(X) = [0 1 0]X >= [0 1 0]X = adx(X)
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
a__incr(X) = [0 1 1]X >= [0 1 0]X = incr(X)
[0 0 0] [0 0 0]
[1 1 1] [1 1 0]
a__hd(X) = [0 1 0]X >= [0 1 0]X = hd(X)
[0 0 0] [0 0 0]
[1 0 0] [0] [1 0 0] [0]
a__tl(X) = [0 1 0]X + [1] >= [0 1 0]X + [1] = tl(X)
[0 0 0] [0] [0 0 0] [0]
problem:
strict:
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
weak:
mark(tl(X)) -> a__tl(mark(X))
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Splitting Processor:
strict:
mark(hd(X)) -> a__hd(mark(X))
weak:
mark(tl(X)) -> a__tl(mark(X))
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 0 0]
[0 0 1]
interpretation:
[1 0 1] [1]
[tl](x0) = [0 0 0]x0 + [0]
[0 0 1] [0],
[1 0 0] [0]
[hd](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[1]
[nats] = [0]
[0],
[1 0 1] [1]
[a__tl](x0) = [0 0 0]x0 + [1]
[0 0 1] [0],
[1 0 1] [0]
[mark](x0) = [0 0 0]x0 + [1]
[0 0 1] [0],
[1 0 0] [0]
[a__hd](x0) = [0 0 0]x0 + [1]
[0 0 1] [1],
[1 0 0]
[adx](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0] [0]
[a__incr](x0) = [0 0 0]x0 + [1]
[0 0 1] [0],
[1 1 1] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 1] [0 0 1] ,
[0]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[1 0 0] [0]
[a__adx](x0) = [0 0 0]x0 + [1]
[0 0 1] [0],
[0]
[a__zeros] = [0]
[0],
[1]
[a__nats] = [1]
[0]
orientation:
[1 0 1] [1] [1 0 1] [0]
mark(hd(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = a__hd(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 0 2] [1] [1 0 2] [1]
mark(tl(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = a__tl(mark(X))
[0 0 1] [0] [0 0 1] [0]
[0] [0]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [1]
a__nats() = [1] >= [0] = nats()
[0] [0]
[0] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1] [0]
a__nats() = [1] >= [1] = a__adx(a__zeros())
[0] [0]
[1 1 1] [1 0 0] [0] [1 1 1] [1 0 0] [0]
a__adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]X + [0 0 0]Y + [1] = a__incr(cons(X,adx(Y)))
[0 0 1] [0 0 1] [0] [0 0 1] [0 0 1] [0]
[1 1 1] [1 0 0] [0] [1 0 0] [1 0 0]
a__incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]X + [0 0 0]Y = cons(s(X),incr(Y))
[0 0 1] [0 0 1] [0] [0 0 0] [0 0 1]
[1 1 1] [1 0 0] [0] [1 0 1] [0]
a__hd(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]X + [1] = mark(X)
[0 0 1] [0 0 1] [1] [0 0 1] [0]
[1 1 2] [1 0 1] [1] [1 0 1] [0]
a__tl(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]Y + [1] = mark(Y)
[0 0 1] [0 0 1] [0] [0 0 1] [0]
[1] [1]
mark(nats()) = [1] >= [1] = a__nats()
[0] [0]
[0] [0]
mark(zeros()) = [1] >= [0] = a__zeros()
[0] [0]
[1 1 2] [1 0 1] [0] [1 1 1] [1 0 0]
mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [1] >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
[0 0 1] [0 0 1] [0] [0 0 1] [0 0 1]
[0] [0]
mark(0()) = [1] >= [0] = 0()
[0] [0]
[1 0 0] [0] [1 0 0]
mark(s(X)) = [0 0 0]X + [1] >= [0 0 0]X = s(X)
[0 0 0] [0] [0 0 0]
[1 0 0] [0] [1 0 0]
a__adx(X) = [0 0 0]X + [1] >= [0 0 0]X = adx(X)
[0 0 1] [0] [0 0 1]
[1 0 0] [0] [1 0 0]
a__incr(X) = [0 0 0]X + [1] >= [0 0 0]X = incr(X)
[0 0 1] [0] [0 0 1]
[1 0 0] [0] [1 0 0] [0]
a__hd(X) = [0 0 0]X + [1] >= [0 0 0]X + [0] = hd(X)
[0 0 1] [1] [0 0 1] [1]
[1 0 1] [1] [1 0 1] [1]
a__tl(X) = [0 0 0]X + [1] >= [0 0 0]X + [0] = tl(X)
[0 0 1] [0] [0 0 1] [0]
[1 0 1] [0] [1 0 1] [0]
mark(adx(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = a__adx(mark(X))
[0 0 1] [0] [0 0 1] [0]
[1 0 1] [0] [1 0 1] [0]
mark(incr(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = a__incr(mark(X))
[0 0 1] [0] [0 0 1] [0]
problem:
strict:
weak:
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
Qed
strict:
mark(adx(X)) -> a__adx(mark(X))
mark(incr(X)) -> a__incr(mark(X))
weak:
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 0 0]
[0 0 1]
interpretation:
[1 0 1]
[tl](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0] [1]
[hd](x0) = [0 0 0]x0 + [0]
[0 0 1] [0],
[0]
[nats] = [0]
[1],
[1 0 1]
[a__tl](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 1]
[mark](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0] [1]
[a__hd](x0) = [0 0 0]x0 + [0]
[0 0 1] [0],
[1 0 0] [0]
[adx](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[a__incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 1 1] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 1] [0 0 1] ,
[0]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[1 0 0] [0]
[a__adx](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[0]
[a__zeros] = [0]
[0],
[1]
[a__nats] = [0]
[1]
orientation:
[1 0 1] [1] [1 0 1] [0]
mark(adx(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__adx(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 0 1] [1 0 1]
mark(incr(X)) = [0 0 0]X >= [0 0 0]X = a__incr(mark(X))
[0 0 1] [0 0 1]
[1 0 1] [1] [1 0 1] [1]
mark(hd(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__hd(mark(X))
[0 0 1] [0] [0 0 1] [0]
[1 0 2] [1 0 2]
mark(tl(X)) = [0 0 0]X >= [0 0 0]X = a__tl(mark(X))
[0 0 1] [0 0 1]
[0] [0]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [0]
a__nats() = [0] >= [0] = nats()
[1] [1]
[0] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1] [0]
a__nats() = [0] >= [0] = a__adx(a__zeros())
[1] [1]
[1 1 1] [1 0 0] [0] [1 1 1] [1 0 0] [0]
a__adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]X + [0 0 0]Y + [0] = a__incr(cons(X,adx(Y)))
[0 0 1] [0 0 1] [1] [0 0 1] [0 0 1] [1]
[1 1 1] [1 0 0] [1 0 0] [1 0 0]
a__incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = cons(s(X),incr(Y))
[0 0 1] [0 0 1] [0 0 0] [0 0 1]
[1 1 1] [1 0 0] [1] [1 0 1]
a__hd(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]X = mark(X)
[0 0 1] [0 0 1] [0] [0 0 1]
[1 1 2] [1 0 1] [1 0 1]
a__tl(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]Y = mark(Y)
[0 0 1] [0 0 1] [0 0 1]
[1] [1]
mark(nats()) = [0] >= [0] = a__nats()
[1] [1]
[0] [0]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 1 2] [1 0 1] [1 1 1] [1 0 0]
mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
[0 0 1] [0 0 1] [0 0 1] [0 0 1]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 0 0] [1 0 0]
mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(X)
[0 0 0] [0 0 0]
[1 0 0] [0] [1 0 0] [0]
a__adx(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = adx(X)
[0 0 1] [1] [0 0 1] [1]
[1 0 0] [1 0 0]
a__incr(X) = [0 0 0]X >= [0 0 0]X = incr(X)
[0 0 1] [0 0 1]
[1 0 0] [1] [1 0 0] [1]
a__hd(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = hd(X)
[0 0 1] [0] [0 0 1] [0]
[1 0 1] [1 0 1]
a__tl(X) = [0 0 0]X >= [0 0 0]X = tl(X)
[0 0 1] [0 0 1]
problem:
strict:
mark(incr(X)) -> a__incr(mark(X))
weak:
mark(adx(X)) -> a__adx(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 0]
[0 1 1]
[0 0 1]
interpretation:
[1 1 0]
[tl](x0) = [0 1 1]x0
[0 0 1] ,
[1]
[hd](x0) = x0 + [1]
[1],
[0]
[nats] = [1]
[1],
[1 1 0]
[a__tl](x0) = [0 1 1]x0
[0 0 1] ,
[1 1 0]
[mark](x0) = [0 1 1]x0
[0 0 1] ,
[1]
[a__hd](x0) = x0 + [1]
[1],
[0]
[adx](x0) = x0 + [0]
[1],
[0]
[incr](x0) = x0 + [1]
[0],
[1 0 0]
[s](x0) = [0 1 0]x0
[0 0 0] ,
[0]
[a__incr](x0) = x0 + [1]
[0],
[1 1 0]
[cons](x0, x1) = [0 1 1]x0 + x1
[0 0 1] ,
[0]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[0]
[a__adx](x0) = x0 + [1]
[1],
[0]
[a__zeros] = [0]
[0],
[1]
[a__nats] = [1]
[1]
orientation:
[1 1 0] [1] [1 1 0] [0]
mark(incr(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = a__incr(mark(X))
[0 0 1] [0] [0 0 1] [0]
[1 1 0] [0] [1 1 0] [0]
mark(adx(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = a__adx(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 1 0] [2] [1 1 0] [1]
mark(hd(X)) = [0 1 1]X + [2] >= [0 1 1]X + [1] = a__hd(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 2 1] [1 2 1]
mark(tl(X)) = [0 1 2]X >= [0 1 2]X = a__tl(mark(X))
[0 0 1] [0 0 1]
[0] [0]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [0]
a__nats() = [1] >= [1] = nats()
[1] [1]
[0] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1] [0]
a__nats() = [1] >= [1] = a__adx(a__zeros())
[1] [1]
[1 1 0] [0] [1 1 0] [0]
a__adx(cons(X,Y)) = [0 1 1]X + Y + [1] >= [0 1 1]X + Y + [1] = a__incr(cons(X,adx(Y)))
[0 0 1] [1] [0 0 1] [1]
[1 1 0] [0] [1 1 0] [0]
a__incr(cons(X,Y)) = [0 1 1]X + Y + [1] >= [0 1 0]X + Y + [1] = cons(s(X),incr(Y))
[0 0 1] [0] [0 0 0] [0]
[1 1 0] [1] [1 1 0]
a__hd(cons(X,Y)) = [0 1 1]X + Y + [1] >= [0 1 1]X = mark(X)
[0 0 1] [1] [0 0 1]
[1 2 1] [1 1 0] [1 1 0]
a__tl(cons(X,Y)) = [0 1 2]X + [0 1 1]Y >= [0 1 1]Y = mark(Y)
[0 0 1] [0 0 1] [0 0 1]
[1] [1]
mark(nats()) = [2] >= [1] = a__nats()
[1] [1]
[0] [0]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 2 1] [1 1 0] [1 1 0]
mark(cons(X1,X2)) = [0 1 2]X1 + [0 1 1]X2 >= [0 1 1]X1 + X2 = cons(X1,X2)
[0 0 1] [0 0 1] [0 0 1]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 1 0] [1 0 0]
mark(s(X)) = [0 1 0]X >= [0 1 0]X = s(X)
[0 0 0] [0 0 0]
[0] [0]
a__adx(X) = X + [1] >= X + [0] = adx(X)
[1] [1]
[0] [0]
a__incr(X) = X + [1] >= X + [1] = incr(X)
[0] [0]
[1] [1]
a__hd(X) = X + [1] >= X + [1] = hd(X)
[1] [1]
[1 1 0] [1 1 0]
a__tl(X) = [0 1 1]X >= [0 1 1]X = tl(X)
[0 0 1] [0 0 1]
problem:
strict:
weak:
mark(incr(X)) -> a__incr(mark(X))
mark(adx(X)) -> a__adx(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__zeros() -> zeros()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Qed