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())

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