Problem:
incr(nil()) -> nil()
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(nil()) -> nil()
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
nats() -> adx(zeros())
zeros() -> cons(0(),n__zeros())
head(cons(X,L)) -> X
tail(cons(X,L)) -> activate(L)
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
zeros() -> n__zeros()
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(n__zeros()) -> zeros()
activate(X) -> X
Proof:
Matrix Interpretation Processor: dim=1
interpretation:
[tail](x0) = 4x0 + 3,
[head](x0) = x0 + 1,
[n__zeros] = 0,
[0] = 0,
[zeros] = 0,
[nats] = 0,
[n__adx](x0) = x0,
[adx](x0) = x0,
[n__incr](x0) = x0,
[activate](x0) = x0,
[s](x0) = x0,
[cons](x0, x1) = 2x0 + 4x1,
[incr](x0) = x0,
[nil] = 4
orientation:
incr(nil()) = 4 >= 4 = nil()
incr(cons(X,L)) = 4L + 2X >= 4L + 2X = cons(s(X),n__incr(activate(L)))
adx(nil()) = 4 >= 4 = nil()
adx(cons(X,L)) = 4L + 2X >= 4L + 2X = incr(cons(X,n__adx(activate(L))))
nats() = 0 >= 0 = adx(zeros())
zeros() = 0 >= 0 = cons(0(),n__zeros())
head(cons(X,L)) = 4L + 2X + 1 >= X = X
tail(cons(X,L)) = 16L + 8X + 3 >= L = activate(L)
incr(X) = X >= X = n__incr(X)
adx(X) = X >= X = n__adx(X)
zeros() = 0 >= 0 = n__zeros()
activate(n__incr(X)) = X >= X = incr(X)
activate(n__adx(X)) = X >= X = adx(X)
activate(n__zeros()) = 0 >= 0 = zeros()
activate(X) = X >= X = X
problem:
incr(nil()) -> nil()
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(nil()) -> nil()
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
nats() -> adx(zeros())
zeros() -> cons(0(),n__zeros())
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
zeros() -> n__zeros()
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(n__zeros()) -> zeros()
activate(X) -> X
Matrix Interpretation Processor: dim=3
interpretation:
[0]
[n__zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[0]
[zeros] = [0]
[0],
[1]
[nats] = [1]
[0],
[1 0 0]
[n__adx](x0) = [0 1 1]x0
[0 1 1] ,
[1 0 0]
[adx](x0) = [0 1 1]x0
[0 1 1] ,
[1 0 0]
[n__incr](x0) = [0 0 0]x0
[0 1 1] ,
[0]
[activate](x0) = x0 + [1]
[0],
[1 0 0]
[s](x0) = [0 0 1]x0
[0 1 0] ,
[1 0 0] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 1 1] [0 0 0] ,
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 1 1] ,
[1]
[nil] = [0]
[1]
orientation:
[1] [1]
incr(nil()) = [0] >= [0] = nil()
[1] [1]
[1 0 0] [1 0 0] [1 0 0] [1 0 0]
incr(cons(X,L)) = [0 0 0]L + [0 0 0]X >= [0 0 0]L + [0 0 0]X = cons(s(X),n__incr(activate(L)))
[0 0 0] [0 1 1] [0 0 0] [0 1 1]
[1] [1]
adx(nil()) = [1] >= [0] = nil()
[1] [1]
[1 0 0] [1 0 0] [1 0 0] [1 0 0]
adx(cons(X,L)) = [0 0 0]L + [0 1 1]X >= [0 0 0]L + [0 0 0]X = incr(cons(X,n__adx(activate(L))))
[0 0 0] [0 1 1] [0 0 0] [0 1 1]
[1] [0]
nats() = [1] >= [0] = adx(zeros())
[0] [0]
[0] [0]
zeros() = [0] >= [0] = cons(0(),n__zeros())
[0] [0]
[1 0 0] [1 0 0]
incr(X) = [0 0 0]X >= [0 0 0]X = n__incr(X)
[0 1 1] [0 1 1]
[1 0 0] [1 0 0]
adx(X) = [0 1 1]X >= [0 1 1]X = n__adx(X)
[0 1 1] [0 1 1]
[0] [0]
zeros() = [0] >= [0] = n__zeros()
[0] [0]
[1 0 0] [0] [1 0 0]
activate(n__incr(X)) = [0 0 0]X + [1] >= [0 0 0]X = incr(X)
[0 1 1] [0] [0 1 1]
[1 0 0] [0] [1 0 0]
activate(n__adx(X)) = [0 1 1]X + [1] >= [0 1 1]X = adx(X)
[0 1 1] [0] [0 1 1]
[0] [0]
activate(n__zeros()) = [1] >= [0] = zeros()
[0] [0]
[0]
activate(X) = X + [1] >= X = X
[0]
problem:
incr(nil()) -> nil()
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(nil()) -> nil()
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
zeros() -> cons(0(),n__zeros())
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
zeros() -> n__zeros()
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(n__zeros()) -> zeros()
activate(X) -> X
Matrix Interpretation Processor: dim=1
interpretation:
[n__zeros] = 0,
[0] = 0,
[zeros] = 0,
[n__adx](x0) = 4x0 + 1,
[adx](x0) = 4x0 + 1,
[n__incr](x0) = x0,
[activate](x0) = x0,
[s](x0) = x0,
[cons](x0, x1) = 4x0 + x1,
[incr](x0) = x0,
[nil] = 0
orientation:
incr(nil()) = 0 >= 0 = nil()
incr(cons(X,L)) = L + 4X >= L + 4X = cons(s(X),n__incr(activate(L)))
adx(nil()) = 1 >= 0 = nil()
adx(cons(X,L)) = 4L + 16X + 1 >= 4L + 4X + 1 = incr(cons(X,n__adx(activate(L))))
zeros() = 0 >= 0 = cons(0(),n__zeros())
incr(X) = X >= X = n__incr(X)
adx(X) = 4X + 1 >= 4X + 1 = n__adx(X)
zeros() = 0 >= 0 = n__zeros()
activate(n__incr(X)) = X >= X = incr(X)
activate(n__adx(X)) = 4X + 1 >= 4X + 1 = adx(X)
activate(n__zeros()) = 0 >= 0 = zeros()
activate(X) = X >= X = X
problem:
incr(nil()) -> nil()
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
zeros() -> cons(0(),n__zeros())
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
zeros() -> n__zeros()
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(n__zeros()) -> zeros()
activate(X) -> X
Matrix Interpretation Processor: dim=3
interpretation:
[0]
[n__zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[0]
[zeros] = [0]
[0],
[1 0 0] [1]
[n__adx](x0) = [0 0 0]x0 + [0]
[0 0 0] [0],
[1 0 0] [1]
[adx](x0) = [0 0 0]x0 + [0]
[0 0 0] [0],
[1 0 1]
[n__incr](x0) = [0 0 1]x0
[0 0 0] ,
[1 0 0]
[activate](x0) = [0 1 0]x0
[0 1 1] ,
[1 0 0]
[s](x0) = [0 1 0]x0
[0 0 0] ,
[1 1 0] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 0] [0 1 1] ,
[1 0 1]
[incr](x0) = [0 0 1]x0
[0 0 1] ,
[0]
[nil] = [0]
[1]
orientation:
[1] [0]
incr(nil()) = [1] >= [0] = nil()
[1] [1]
[1 1 1] [1 1 0] [1 1 1] [1 1 0]
incr(cons(X,L)) = [0 1 1]L + [0 0 0]X >= [0 0 0]L + [0 0 0]X = cons(s(X),n__incr(activate(L)))
[0 1 1] [0 0 0] [0 1 1] [0 0 0]
[1 0 0] [1 1 0] [1] [1 0 0] [1 1 0] [1]
adx(cons(X,L)) = [0 0 0]L + [0 0 0]X + [0] >= [0 0 0]L + [0 0 0]X + [0] = incr(cons(X,n__adx(activate(L))))
[0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0]
[0] [0]
zeros() = [0] >= [0] = cons(0(),n__zeros())
[0] [0]
[1 0 1] [1 0 1]
incr(X) = [0 0 1]X >= [0 0 1]X = n__incr(X)
[0 0 1] [0 0 0]
[1 0 0] [1] [1 0 0] [1]
adx(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = n__adx(X)
[0 0 0] [0] [0 0 0] [0]
[0] [0]
zeros() = [0] >= [0] = n__zeros()
[0] [0]
[1 0 1] [1 0 1]
activate(n__incr(X)) = [0 0 1]X >= [0 0 1]X = incr(X)
[0 0 1] [0 0 1]
[1 0 0] [1] [1 0 0] [1]
activate(n__adx(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = adx(X)
[0 0 0] [0] [0 0 0] [0]
[0] [0]
activate(n__zeros()) = [0] >= [0] = zeros()
[0] [0]
[1 0 0]
activate(X) = [0 1 0]X >= X = X
[0 1 1]
problem:
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
zeros() -> cons(0(),n__zeros())
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
zeros() -> n__zeros()
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(n__zeros()) -> zeros()
activate(X) -> X
Matrix Interpretation Processor: dim=3
interpretation:
[0]
[n__zeros] = [1]
[0],
[0]
[0] = [0]
[1],
[1]
[zeros] = [1]
[0],
[1 0 0] [0]
[n__adx](x0) = [0 0 0]x0 + [0]
[0 0 0] [1],
[1 0 0] [0]
[adx](x0) = [0 0 0]x0 + [1]
[0 0 0] [1],
[1 0 0] [0]
[n__incr](x0) = [0 0 0]x0 + [0]
[0 0 0] [1],
[1 1 0]
[activate](x0) = [0 1 1]x0
[0 0 1] ,
[1 0 0] [0]
[s](x0) = [0 0 0]x0 + [1]
[0 0 0] [1],
[1 0 0] [1 1 0]
[cons](x0, x1) = [0 0 1]x0 + [0 0 0]x1
[0 1 0] [0 0 0] ,
[1 0 0] [0]
[incr](x0) = [0 0 0]x0 + [1]
[0 0 0] [1]
orientation:
[1 1 0] [1 0 0] [0] [1 1 0] [1 0 0] [0]
incr(cons(X,L)) = [0 0 0]L + [0 0 0]X + [1] >= [0 0 0]L + [0 0 0]X + [1] = cons(s(X),n__incr(activate(L)))
[0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [1]
[1 1 0] [1 0 0] [0] [1 1 0] [1 0 0] [0]
adx(cons(X,L)) = [0 0 0]L + [0 0 0]X + [1] >= [0 0 0]L + [0 0 0]X + [1] = incr(cons(X,n__adx(activate(L))))
[0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] [1]
[1] [1]
zeros() = [1] >= [1] = cons(0(),n__zeros())
[0] [0]
[1 0 0] [0] [1 0 0] [0]
incr(X) = [0 0 0]X + [1] >= [0 0 0]X + [0] = n__incr(X)
[0 0 0] [1] [0 0 0] [1]
[1 0 0] [0] [1 0 0] [0]
adx(X) = [0 0 0]X + [1] >= [0 0 0]X + [0] = n__adx(X)
[0 0 0] [1] [0 0 0] [1]
[1] [0]
zeros() = [1] >= [1] = n__zeros()
[0] [0]
[1 0 0] [0] [1 0 0] [0]
activate(n__incr(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = incr(X)
[0 0 0] [1] [0 0 0] [1]
[1 0 0] [0] [1 0 0] [0]
activate(n__adx(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = adx(X)
[0 0 0] [1] [0 0 0] [1]
[1] [1]
activate(n__zeros()) = [1] >= [1] = zeros()
[0] [0]
[1 1 0]
activate(X) = [0 1 1]X >= X = X
[0 0 1]
problem:
incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
zeros() -> cons(0(),n__zeros())
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(n__zeros()) -> zeros()
activate(X) -> X
Unfolding Processor:
loop length: 5
terms:
incr(cons(X,n__adx(cons(x3126,n__zeros()))))
cons(s(X),n__incr(activate(n__adx(cons(x3126,n__zeros())))))
cons(s(X),n__incr(adx(cons(x3126,n__zeros()))))
cons(s(X),n__incr(incr(cons(x3126,n__adx(activate(n__zeros()))))))
cons(s(X),n__incr(incr(cons(x3126,n__adx(zeros())))))
context: cons(s(X),n__incr([]))
substitution:
X -> x3126
x3126 -> 0()
Qed