Problem:
nats() -> adx(zeros())
zeros() -> cons(n__0(),n__zeros())
incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
hd(cons(X,Y)) -> activate(X)
tl(cons(X,Y)) -> activate(Y)
0() -> n__0()
zeros() -> n__zeros()
s(X) -> n__s(X)
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
activate(n__0()) -> 0()
activate(n__zeros()) -> zeros()
activate(n__s(X)) -> s(X)
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(X) -> X
Proof:
Matrix Interpretation Processor: dim=1
interpretation:
[s](x0) = x0,
[0] = 0,
[tl](x0) = 4x0 + 6,
[hd](x0) = 4x0,
[n__adx](x0) = x0,
[n__incr](x0) = x0,
[n__s](x0) = x0,
[activate](x0) = x0,
[incr](x0) = x0,
[cons](x0, x1) = x0 + 2x1,
[n__zeros] = 0,
[n__0] = 0,
[adx](x0) = x0,
[zeros] = 0,
[nats] = 0
orientation:
nats() = 0 >= 0 = adx(zeros())
zeros() = 0 >= 0 = cons(n__0(),n__zeros())
incr(cons(X,Y)) = X + 2Y >= X + 2Y = cons(n__s(activate(X)),n__incr(activate(Y)))
adx(cons(X,Y)) = X + 2Y >= X + 2Y = incr(cons(activate(X),n__adx(activate(Y))))
hd(cons(X,Y)) = 4X + 8Y >= X = activate(X)
tl(cons(X,Y)) = 4X + 8Y + 6 >= Y = activate(Y)
0() = 0 >= 0 = n__0()
zeros() = 0 >= 0 = n__zeros()
s(X) = X >= X = n__s(X)
incr(X) = X >= X = n__incr(X)
adx(X) = X >= X = n__adx(X)
activate(n__0()) = 0 >= 0 = 0()
activate(n__zeros()) = 0 >= 0 = zeros()
activate(n__s(X)) = X >= X = s(X)
activate(n__incr(X)) = X >= X = incr(X)
activate(n__adx(X)) = X >= X = adx(X)
activate(X) = X >= X = X
problem:
nats() -> adx(zeros())
zeros() -> cons(n__0(),n__zeros())
incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
hd(cons(X,Y)) -> activate(X)
0() -> n__0()
zeros() -> n__zeros()
s(X) -> n__s(X)
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
activate(n__0()) -> 0()
activate(n__zeros()) -> zeros()
activate(n__s(X)) -> s(X)
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(X) -> X
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 0]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[0]
[0] = [0]
[0],
[1 0 0] [1]
[hd](x0) = [1 0 1]x0 + [0]
[0 0 1] [0],
[1 0 0] [0]
[n__adx](x0) = [0 0 0]x0 + [1]
[0 1 0] [0],
[1 0 0]
[n__incr](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[n__s](x0) = [0 0 0]x0
[0 0 0] ,
[activate](x0) = x0
,
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 0 0] ,
[1 1 0] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 1 1]x1
[0 0 1] [0 0 0] ,
[0]
[n__zeros] = [1]
[0],
[0]
[n__0] = [0]
[0],
[1 0 0] [0]
[adx](x0) = [0 0 0]x0 + [1]
[0 1 0] [0],
[0]
[zeros] = [1]
[0],
[1]
[nats] = [1]
[1]
orientation:
[1] [0]
nats() = [1] >= [1] = adx(zeros())
[1] [1]
[0] [0]
zeros() = [1] >= [1] = cons(n__0(),n__zeros())
[0] [0]
[1 1 0] [1 0 0] [1 0 0] [1 0 0]
incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = cons(n__s(activate(X)),n__incr(activate(Y)))
[0 0 0] [0 0 0] [0 0 0] [0 0 0]
[1 1 0] [1 0 0] [0] [1 1 0] [1 0 0]
adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [1] >= [0 0 0]X + [0 0 0]Y = incr(cons(activate(X),n__adx(activate(Y))))
[0 0 0] [0 1 1] [0] [0 0 0] [0 0 0]
[1 1 0] [1 0 0] [1]
hd(cons(X,Y)) = [1 1 1]X + [1 0 0]Y + [0] >= X = activate(X)
[0 0 1] [0 0 0] [0]
[0] [0]
0() = [0] >= [0] = n__0()
[0] [0]
[0] [0]
zeros() = [1] >= [1] = n__zeros()
[0] [0]
[1 0 0] [1 0 0]
s(X) = [0 0 0]X >= [0 0 0]X = n__s(X)
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
incr(X) = [0 0 0]X >= [0 0 0]X = n__incr(X)
[0 0 0] [0 0 0]
[1 0 0] [0] [1 0 0] [0]
adx(X) = [0 0 0]X + [1] >= [0 0 0]X + [1] = n__adx(X)
[0 1 0] [0] [0 1 0] [0]
[0] [0]
activate(n__0()) = [0] >= [0] = 0()
[0] [0]
[0] [0]
activate(n__zeros()) = [1] >= [1] = zeros()
[0] [0]
[1 0 0] [1 0 0]
activate(n__s(X)) = [0 0 0]X >= [0 0 0]X = s(X)
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
activate(n__incr(X)) = [0 0 0]X >= [0 0 0]X = incr(X)
[0 0 0] [0 0 0]
[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 1 0] [0] [0 1 0] [0]
activate(X) = X >= X = X
problem:
zeros() -> cons(n__0(),n__zeros())
incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
0() -> n__0()
zeros() -> n__zeros()
s(X) -> n__s(X)
incr(X) -> n__incr(X)
adx(X) -> n__adx(X)
activate(n__0()) -> 0()
activate(n__zeros()) -> zeros()
activate(n__s(X)) -> s(X)
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(X) -> X
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 0]
[s](x0) = [0 1 0]x0
[0 0 0] ,
[0]
[0] = [0]
[0],
[1 0 0] [0]
[n__adx](x0) = [0 1 1]x0 + [1]
[0 1 1] [1],
[1 0 0]
[n__incr](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[n__s](x0) = [0 1 0]x0
[0 0 0] ,
[1 0 1]
[activate](x0) = [1 1 0]x0
[1 0 1] ,
[1 0 0]
[incr](x0) = [1 0 0]x0
[1 0 0] ,
[1 0 1] [1 0 1]
[cons](x0, x1) = [1 0 1]x0 + [1 0 1]x1
[0 0 0] [1 1 0] ,
[0]
[n__zeros] = [0]
[0],
[0]
[n__0] = [0]
[0],
[1 1 1] [1]
[adx](x0) = [1 1 1]x0 + [1]
[1 1 1] [1],
[0]
[zeros] = [0]
[0]
orientation:
[0] [0]
zeros() = [0] >= [0] = cons(n__0(),n__zeros())
[0] [0]
[1 0 1] [1 0 1] [1 0 1] [1 0 1]
incr(cons(X,Y)) = [1 0 1]X + [1 0 1]Y >= [1 0 1]X + [1 0 1]Y = cons(n__s(activate(X)),n__incr(activate(Y)))
[1 0 1] [1 0 1] [0 0 0] [1 0 1]
[2 0 2] [3 1 2] [1] [2 0 2] [3 1 2] [1]
adx(cons(X,Y)) = [2 0 2]X + [3 1 2]Y + [1] >= [2 0 2]X + [3 1 2]Y + [1] = incr(cons(activate(X),n__adx(activate(Y))))
[2 0 2] [3 1 2] [1] [2 0 2] [3 1 2] [1]
[0] [0]
0() = [0] >= [0] = n__0()
[0] [0]
[0] [0]
zeros() = [0] >= [0] = n__zeros()
[0] [0]
[1 0 0] [1 0 0]
s(X) = [0 1 0]X >= [0 1 0]X = n__s(X)
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
incr(X) = [1 0 0]X >= [0 0 0]X = n__incr(X)
[1 0 0] [0 0 0]
[1 1 1] [1] [1 0 0] [0]
adx(X) = [1 1 1]X + [1] >= [0 1 1]X + [1] = n__adx(X)
[1 1 1] [1] [0 1 1] [1]
[0] [0]
activate(n__0()) = [0] >= [0] = 0()
[0] [0]
[0] [0]
activate(n__zeros()) = [0] >= [0] = zeros()
[0] [0]
[1 0 0] [1 0 0]
activate(n__s(X)) = [1 1 0]X >= [0 1 0]X = s(X)
[1 0 0] [0 0 0]
[1 0 0] [1 0 0]
activate(n__incr(X)) = [1 0 0]X >= [1 0 0]X = incr(X)
[1 0 0] [1 0 0]
[1 1 1] [1] [1 1 1] [1]
activate(n__adx(X)) = [1 1 1]X + [1] >= [1 1 1]X + [1] = adx(X)
[1 1 1] [1] [1 1 1] [1]
[1 0 1]
activate(X) = [1 1 0]X >= X = X
[1 0 1]
problem:
zeros() -> cons(n__0(),n__zeros())
incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
0() -> n__0()
zeros() -> n__zeros()
s(X) -> n__s(X)
incr(X) -> n__incr(X)
activate(n__0()) -> 0()
activate(n__zeros()) -> zeros()
activate(n__s(X)) -> s(X)
activate(n__incr(X)) -> incr(X)
activate(n__adx(X)) -> adx(X)
activate(X) -> X
Unfolding Processor:
loop length: 5
terms:
incr(cons(X,n__adx(cons(x23443,n__zeros()))))
cons(n__s(activate(X)),n__incr(activate(n__adx(cons(x23443,n__zeros())))))
cons(n__s(activate(X)),n__incr(adx(cons(x23443,n__zeros()))))
cons(n__s(activate(X)),n__incr(incr(cons(activate(x23443),n__adx(activate(n__zeros()))))))
cons(n__s(activate(X)),n__incr(incr(cons(activate(x23443),n__adx(zeros())))))
context: cons(n__s(activate(X)),n__incr([]))
substitution:
X -> activate(x23443)
x23443 -> n__0()
Qed