Problem:
 __(__(X,Y),Z) -> __(X,__(Y,Z))
 __(X,nil()) -> X
 __(nil(),X) -> X
 U11(tt()) -> U12(tt())
 U12(tt()) -> tt()
 isNePal(__(I,__(P,I))) -> U11(tt())
 activate(X) -> X

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {16,11,10,9,7,6,5,4,3}
   transitions:
    tt2() -> 11,10,16*,2,5,7,3
    __0(2,16) -> 3*
    __0(9,2) -> 3*
    __0(9,10) -> 3*
    __0(9,16) -> 3*
    __0(10,1) -> 3*
    __0(10,9) -> 3*
    __0(16,2) -> 3*
    __0(1,2) -> 3*
    __0(16,10) -> 3*
    __0(1,10) -> 3*
    __0(16,16) -> 3*
    __0(1,16) -> 3*
    __0(2,1) -> 3*
    __0(2,9) -> 3*
    __0(9,1) -> 3*
    __0(9,9) -> 3*
    __0(10,2) -> 3*
    __0(10,10) -> 3*
    __0(10,16) -> 3*
    __0(16,1) -> 3*
    __0(1,1) -> 3*
    __0(16,9) -> 3*
    __0(1,9) -> 3*
    __0(2,2) -> 3*
    __0(2,10) -> 3*
    nil0() -> 9*,3,7,1
    U110(10) -> 4*
    U110(2) -> 4*
    U110(9) -> 4*
    U110(16) -> 4*
    U110(1) -> 4*
    U120(9) -> 5*
    U120(1) -> 5*
    isNePal0(10) -> 6*
    isNePal0(2) -> 6*
    isNePal0(9) -> 6*
    isNePal0(16) -> 6*
    isNePal0(1) -> 6*
    activate0(10) -> 7*
    activate0(2) -> 7*
    activate0(9) -> 7*
    activate0(16) -> 7*
    activate0(1) -> 7*
    U121(10) -> 11*
    U121(2) -> 11*,5,4
    U121(16) -> 11*
    1 -> 7,3
    2 -> 7,3
    9 -> 7,3
    10 -> 7,3
    16 -> 7,3
  problem:
   
  Qed