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