Problem:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil()) -> X
__(nil(),X) -> X
and(tt(),X) -> activate(X)
isNePal(__(I,__(P,I))) -> tt()
activate(X) -> X
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {16,15,12,11,10,6,5,4,3}
transitions:
activate1(15) -> 4,12*
activate1(10) -> 4,12*
activate1(2) -> 12*,6,4
activate1(16) -> 4,12*
activate1(11) -> 4,12*
activate1(1) -> 12*,6,4
__0(2,16) -> 3*
__0(15,1) -> 3*
__0(10,1) -> 3*
__0(15,11) -> 3*
__0(10,11) -> 3*
__0(15,15) -> 3*
__0(10,15) -> 3*
__0(16,2) -> 3*
__0(11,2) -> 3*
__0(1,2) -> 3*
__0(16,10) -> 3*
__0(11,10) -> 3*
__0(1,10) -> 3*
__0(16,16) -> 3*
__0(11,16) -> 3*
__0(1,16) -> 3*
__0(2,1) -> 3*
__0(2,11) -> 3*
__0(2,15) -> 3*
__0(15,2) -> 3*
__0(10,2) -> 3*
__0(15,10) -> 3*
__0(10,10) -> 3*
__0(15,16) -> 3*
__0(10,16) -> 3*
__0(16,1) -> 3*
__0(11,1) -> 3*
__0(1,1) -> 3*
__0(16,11) -> 3*
__0(11,11) -> 3*
__0(1,11) -> 3*
__0(16,15) -> 3*
__0(11,15) -> 3*
__0(1,15) -> 3*
__0(2,2) -> 3*
__0(2,10) -> 3*
nil0() -> 10,15*,3,6,1
and0(2,16) -> 4*
and0(15,1) -> 4*
and0(10,1) -> 4*
and0(15,11) -> 4*
and0(10,11) -> 4*
and0(15,15) -> 4*
and0(10,15) -> 4*
and0(16,2) -> 4*
and0(11,2) -> 4*
and0(1,2) -> 4*
and0(16,10) -> 4*
and0(11,10) -> 4*
and0(1,10) -> 4*
and0(16,16) -> 4*
and0(11,16) -> 4*
and0(1,16) -> 4*
and0(2,1) -> 4*
and0(2,11) -> 4*
and0(2,15) -> 4*
and0(15,2) -> 4*
and0(10,2) -> 4*
and0(15,10) -> 4*
and0(10,10) -> 4*
and0(15,16) -> 4*
and0(10,16) -> 4*
and0(16,1) -> 4*
and0(11,1) -> 4*
and0(1,1) -> 4*
and0(16,11) -> 4*
and0(11,11) -> 4*
and0(1,11) -> 4*
and0(16,15) -> 4*
and0(11,15) -> 4*
and0(1,15) -> 4*
and0(2,2) -> 4*
and0(2,10) -> 4*
tt0() -> 11,16*,3,6,2
isNePal0(15) -> 5*
isNePal0(10) -> 5*
isNePal0(2) -> 5*
isNePal0(16) -> 5*
isNePal0(11) -> 5*
isNePal0(1) -> 5*
1 -> 12,6,3
2 -> 12,6,3
10 -> 12,3
11 -> 12,3
15 -> 12,3
16 -> 12,3
problem:
Qed