Problem:
active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
active(__(X,nil())) -> mark(X)
active(__(nil(),X)) -> mark(X)
active(and(tt(),X)) -> mark(X)
active(isList(V)) -> mark(isNeList(V))
active(isList(nil())) -> mark(tt())
active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
active(isNeList(V)) -> mark(isQid(V))
active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
active(isNePal(V)) -> mark(isQid(V))
active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
active(isPal(V)) -> mark(isNePal(V))
active(isPal(nil())) -> mark(tt())
active(isQid(a())) -> mark(tt())
active(isQid(e())) -> mark(tt())
active(isQid(i())) -> mark(tt())
active(isQid(o())) -> mark(tt())
active(isQid(u())) -> mark(tt())
mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
mark(nil()) -> active(nil())
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(tt()) -> active(tt())
mark(isList(X)) -> active(isList(X))
mark(isNeList(X)) -> active(isNeList(X))
mark(isQid(X)) -> active(isQid(X))
mark(isNePal(X)) -> active(isNePal(X))
mark(isPal(X)) -> active(isPal(X))
mark(a()) -> active(a())
mark(e()) -> active(e())
mark(i()) -> active(i())
mark(o()) -> active(o())
mark(u()) -> active(u())
__(mark(X1),X2) -> __(X1,X2)
__(X1,mark(X2)) -> __(X1,X2)
__(active(X1),X2) -> __(X1,X2)
__(X1,active(X2)) -> __(X1,X2)
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
isList(mark(X)) -> isList(X)
isList(active(X)) -> isList(X)
isNeList(mark(X)) -> isNeList(X)
isNeList(active(X)) -> isNeList(X)
isQid(mark(X)) -> isQid(X)
isQid(active(X)) -> isQid(X)
isNePal(mark(X)) -> isNePal(X)
isNePal(active(X)) -> isNePal(X)
isPal(mark(X)) -> isPal(X)
isPal(active(X)) -> isPal(X)
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {26,16,15,14,13,12,11,10,9,8}
transitions:
active0(30) -> 8*
active0(5) -> 8*
active0(32) -> 8*
active0(27) -> 8*
active0(7) -> 8*
active0(2) -> 8*
active0(29) -> 8*
active0(4) -> 8*
active0(31) -> 8*
active0(6) -> 8*
active0(1) -> 8*
active0(28) -> 8*
active0(3) -> 8*
__0(6,31) -> 10*
__0(1,31) -> 10*
__0(28,1) -> 10*
__0(28,3) -> 10*
__0(28,5) -> 10*
__0(3,1) -> 10*
__0(28,7) -> 10*
__0(32,28) -> 10*
__0(3,3) -> 10*
__0(27,28) -> 10*
__0(32,30) -> 10*
__0(3,5) -> 10*
__0(27,30) -> 10*
__0(32,32) -> 10*
__0(3,7) -> 10*
__0(27,32) -> 10*
__0(7,28) -> 10*
__0(2,28) -> 10*
__0(7,30) -> 10*
__0(2,30) -> 10*
__0(7,32) -> 10*
__0(2,32) -> 10*
__0(29,2) -> 10*
__0(29,4) -> 10*
__0(29,6) -> 10*
__0(4,2) -> 10*
__0(28,27) -> 10*
__0(4,4) -> 10*
__0(28,29) -> 10*
__0(4,6) -> 10*
__0(28,31) -> 10*
__0(3,27) -> 10*
__0(3,29) -> 10*
__0(3,31) -> 10*
__0(30,1) -> 10*
__0(30,3) -> 10*
__0(30,5) -> 10*
__0(5,1) -> 10*
__0(30,7) -> 10*
__0(5,3) -> 10*
__0(29,28) -> 10*
__0(5,5) -> 10*
__0(29,30) -> 10*
__0(5,7) -> 10*
__0(29,32) -> 10*
__0(4,28) -> 10*
__0(4,30) -> 10*
__0(4,32) -> 10*
__0(31,2) -> 10*
__0(31,4) -> 10*
__0(31,6) -> 10*
__0(6,2) -> 10*
__0(30,27) -> 10*
__0(1,2) -> 10*
__0(6,4) -> 10*
__0(30,29) -> 10*
__0(1,4) -> 10*
__0(6,6) -> 10*
__0(30,31) -> 10*
__0(1,6) -> 10*
__0(5,27) -> 10*
__0(5,29) -> 10*
__0(5,31) -> 10*
__0(32,1) -> 10*
__0(27,1) -> 10*
__0(32,3) -> 10*
__0(27,3) -> 10*
__0(32,5) -> 10*
__0(27,5) -> 10*
__0(7,1) -> 10*
__0(32,7) -> 10*
__0(2,1) -> 10*
__0(27,7) -> 10*
__0(7,3) -> 10*
__0(31,28) -> 10*
__0(2,3) -> 10*
__0(7,5) -> 10*
__0(31,30) -> 10*
__0(2,5) -> 10*
__0(7,7) -> 10*
__0(31,32) -> 10*
__0(2,7) -> 10*
__0(6,28) -> 10*
__0(1,28) -> 10*
__0(6,30) -> 10*
__0(1,30) -> 10*
__0(6,32) -> 10*
__0(1,32) -> 10*
__0(28,2) -> 10*
__0(28,4) -> 10*
__0(28,6) -> 10*
__0(32,27) -> 10*
__0(3,2) -> 10*
__0(27,27) -> 10*
__0(32,29) -> 10*
__0(3,4) -> 10*
__0(27,29) -> 10*
__0(32,31) -> 10*
__0(3,6) -> 10*
__0(7,27) -> 10*
__0(27,31) -> 10*
__0(2,27) -> 10*
__0(7,29) -> 10*
__0(2,29) -> 10*
__0(7,31) -> 10*
__0(2,31) -> 10*
__0(29,1) -> 10*
__0(29,3) -> 10*
__0(29,5) -> 10*
__0(4,1) -> 10*
__0(29,7) -> 10*
__0(4,3) -> 10*
__0(28,28) -> 10*
__0(4,5) -> 10*
__0(28,30) -> 10*
__0(4,7) -> 10*
__0(28,32) -> 10*
__0(3,28) -> 10*
__0(3,30) -> 10*
__0(3,32) -> 10*
__0(30,2) -> 10*
__0(30,4) -> 10*
__0(30,6) -> 10*
__0(5,2) -> 10*
__0(29,27) -> 10*
__0(5,4) -> 10*
__0(29,29) -> 10*
__0(5,6) -> 10*
__0(29,31) -> 10*
__0(4,27) -> 10*
__0(4,29) -> 10*
__0(4,31) -> 10*
__0(31,1) -> 10*
__0(31,3) -> 10*
__0(31,5) -> 10*
__0(6,1) -> 10*
__0(31,7) -> 10*
__0(1,1) -> 10*
__0(6,3) -> 10*
__0(30,28) -> 10*
__0(1,3) -> 10*
__0(6,5) -> 10*
__0(30,30) -> 10*
__0(1,5) -> 10*
__0(6,7) -> 10*
__0(30,32) -> 10*
__0(1,7) -> 10*
__0(5,28) -> 10*
__0(5,30) -> 10*
__0(5,32) -> 10*
__0(32,2) -> 10*
__0(27,2) -> 10*
__0(32,4) -> 10*
__0(27,4) -> 10*
__0(32,6) -> 10*
__0(27,6) -> 10*
__0(7,2) -> 10*
__0(31,27) -> 10*
__0(2,2) -> 10*
__0(7,4) -> 10*
__0(31,29) -> 10*
__0(2,4) -> 10*
__0(7,6) -> 10*
__0(31,31) -> 10*
__0(2,6) -> 10*
__0(6,27) -> 10*
__0(1,27) -> 10*
__0(6,29) -> 10*
__0(1,29) -> 10*
mark0(30) -> 9*
mark0(5) -> 9*
mark0(32) -> 9*
mark0(27) -> 9*
mark0(7) -> 9*
mark0(2) -> 9*
mark0(29) -> 9*
mark0(4) -> 9*
mark0(31) -> 9*
mark0(6) -> 9*
mark0(1) -> 9*
mark0(28) -> 9*
mark0(3) -> 9*
nil0() -> 1*
and0(1,29) -> 11*
and0(6,31) -> 11*
and0(1,31) -> 11*
and0(28,1) -> 11*
and0(28,3) -> 11*
and0(28,5) -> 11*
and0(3,1) -> 11*
and0(28,7) -> 11*
and0(32,28) -> 11*
and0(3,3) -> 11*
and0(27,28) -> 11*
and0(32,30) -> 11*
and0(3,5) -> 11*
and0(27,30) -> 11*
and0(32,32) -> 11*
and0(3,7) -> 11*
and0(27,32) -> 11*
and0(7,28) -> 11*
and0(2,28) -> 11*
and0(7,30) -> 11*
and0(2,30) -> 11*
and0(7,32) -> 11*
and0(2,32) -> 11*
and0(29,2) -> 11*
and0(29,4) -> 11*
and0(29,6) -> 11*
and0(4,2) -> 11*
and0(28,27) -> 11*
and0(4,4) -> 11*
and0(28,29) -> 11*
and0(4,6) -> 11*
and0(28,31) -> 11*
and0(3,27) -> 11*
and0(3,29) -> 11*
and0(3,31) -> 11*
and0(30,1) -> 11*
and0(30,3) -> 11*
and0(30,5) -> 11*
and0(5,1) -> 11*
and0(30,7) -> 11*
and0(5,3) -> 11*
and0(29,28) -> 11*
and0(5,5) -> 11*
and0(29,30) -> 11*
and0(5,7) -> 11*
and0(29,32) -> 11*
and0(4,28) -> 11*
and0(4,30) -> 11*
and0(4,32) -> 11*
and0(31,2) -> 11*
and0(31,4) -> 11*
and0(31,6) -> 11*
and0(6,2) -> 11*
and0(30,27) -> 11*
and0(1,2) -> 11*
and0(6,4) -> 11*
and0(30,29) -> 11*
and0(1,4) -> 11*
and0(6,6) -> 11*
and0(30,31) -> 11*
and0(1,6) -> 11*
and0(5,27) -> 11*
and0(5,29) -> 11*
and0(5,31) -> 11*
and0(32,1) -> 11*
and0(27,1) -> 11*
and0(32,3) -> 11*
and0(27,3) -> 11*
and0(32,5) -> 11*
and0(27,5) -> 11*
and0(7,1) -> 11*
and0(32,7) -> 11*
and0(2,1) -> 11*
and0(27,7) -> 11*
and0(7,3) -> 11*
and0(31,28) -> 11*
and0(2,3) -> 11*
and0(7,5) -> 11*
and0(31,30) -> 11*
and0(2,5) -> 11*
and0(7,7) -> 11*
and0(31,32) -> 11*
and0(2,7) -> 11*
and0(6,28) -> 11*
and0(1,28) -> 11*
and0(6,30) -> 11*
and0(1,30) -> 11*
and0(6,32) -> 11*
and0(1,32) -> 11*
and0(28,2) -> 11*
and0(28,4) -> 11*
and0(28,6) -> 11*
and0(32,27) -> 11*
and0(3,2) -> 11*
and0(27,27) -> 11*
and0(32,29) -> 11*
and0(3,4) -> 11*
and0(27,29) -> 11*
and0(32,31) -> 11*
and0(3,6) -> 11*
and0(7,27) -> 11*
and0(27,31) -> 11*
and0(2,27) -> 11*
and0(7,29) -> 11*
and0(2,29) -> 11*
and0(7,31) -> 11*
and0(2,31) -> 11*
and0(29,1) -> 11*
and0(29,3) -> 11*
and0(29,5) -> 11*
and0(4,1) -> 11*
and0(29,7) -> 11*
and0(4,3) -> 11*
and0(28,28) -> 11*
and0(4,5) -> 11*
and0(28,30) -> 11*
and0(4,7) -> 11*
and0(28,32) -> 11*
and0(3,28) -> 11*
and0(3,30) -> 11*
and0(3,32) -> 11*
and0(30,2) -> 11*
and0(30,4) -> 11*
and0(30,6) -> 11*
and0(5,2) -> 11*
and0(29,27) -> 11*
and0(5,4) -> 11*
and0(29,29) -> 11*
and0(5,6) -> 11*
and0(29,31) -> 11*
and0(4,27) -> 11*
and0(4,29) -> 11*
and0(4,31) -> 11*
and0(31,1) -> 11*
and0(31,3) -> 11*
and0(31,5) -> 11*
and0(6,1) -> 11*
and0(31,7) -> 11*
and0(1,1) -> 11*
and0(6,3) -> 11*
and0(30,28) -> 11*
and0(1,3) -> 11*
and0(6,5) -> 11*
and0(30,30) -> 11*
and0(1,5) -> 11*
and0(6,7) -> 11*
and0(30,32) -> 11*
and0(1,7) -> 11*
and0(5,28) -> 11*
and0(5,30) -> 11*
and0(5,32) -> 11*
and0(32,2) -> 11*
and0(27,2) -> 11*
and0(32,4) -> 11*
and0(27,4) -> 11*
and0(32,6) -> 11*
and0(27,6) -> 11*
and0(7,2) -> 11*
and0(31,27) -> 11*
and0(2,2) -> 11*
and0(7,4) -> 11*
and0(31,29) -> 11*
and0(2,4) -> 11*
and0(7,6) -> 11*
and0(31,31) -> 11*
and0(2,6) -> 11*
and0(6,27) -> 11*
and0(1,27) -> 11*
and0(6,29) -> 11*
tt0() -> 2*
isList0(30) -> 12*
isList0(5) -> 12*
isList0(32) -> 12*
isList0(27) -> 12*
isList0(7) -> 12*
isList0(2) -> 12*
isList0(29) -> 12*
isList0(4) -> 12*
isList0(31) -> 12*
isList0(6) -> 12*
isList0(1) -> 12*
isList0(28) -> 12*
isList0(3) -> 12*
isNeList0(30) -> 13*
isNeList0(5) -> 13*
isNeList0(32) -> 13*
isNeList0(27) -> 13*
isNeList0(7) -> 13*
isNeList0(2) -> 13*
isNeList0(29) -> 13*
isNeList0(4) -> 13*
isNeList0(31) -> 13*
isNeList0(6) -> 13*
isNeList0(1) -> 13*
isNeList0(28) -> 13*
isNeList0(3) -> 13*
isQid0(30) -> 14*
isQid0(5) -> 14*
isQid0(32) -> 14*
isQid0(27) -> 14*
isQid0(7) -> 14*
isQid0(2) -> 14*
isQid0(29) -> 14*
isQid0(4) -> 14*
isQid0(31) -> 14*
isQid0(6) -> 14*
isQid0(1) -> 14*
isQid0(28) -> 14*
isQid0(3) -> 14*
isNePal0(30) -> 15*
isNePal0(5) -> 15*
isNePal0(32) -> 15*
isNePal0(27) -> 15*
isNePal0(7) -> 15*
isNePal0(2) -> 15*
isNePal0(29) -> 15*
isNePal0(4) -> 15*
isNePal0(31) -> 15*
isNePal0(6) -> 15*
isNePal0(1) -> 15*
isNePal0(28) -> 15*
isNePal0(3) -> 15*
isPal0(30) -> 16*
isPal0(5) -> 16*
isPal0(32) -> 16*
isPal0(27) -> 16*
isPal0(7) -> 16*
isPal0(2) -> 16*
isPal0(29) -> 16*
isPal0(4) -> 16*
isPal0(31) -> 16*
isPal0(6) -> 16*
isPal0(1) -> 16*
isPal0(28) -> 16*
isPal0(3) -> 16*
a0() -> 3*
e0() -> 4*
i0() -> 5*
o0() -> 6*
u0() -> 7*
active1(30) -> 8,26*
active1(32) -> 8,26*
active1(27) -> 8,26*
active1(29) -> 8,26*
active1(31) -> 8,26*
active1(1) -> 26*,8,9
active1(28) -> 8,26*
u1() -> 27*,7,1
o1() -> 28*,6,1
i1() -> 29*,5,1
e1() -> 30*,4,1
a1() -> 31*,3,1
tt1() -> 32*,2,1
nil1() -> 1*
problem:
Qed