Problem:
active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
active(__(X,nil())) -> mark(X)
active(__(nil(),X)) -> mark(X)
active(U11(tt())) -> mark(tt())
active(U21(tt(),V2)) -> mark(U22(isList(V2)))
active(U22(tt())) -> mark(tt())
active(U31(tt())) -> mark(tt())
active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
active(U42(tt())) -> mark(tt())
active(U51(tt(),V2)) -> mark(U52(isList(V2)))
active(U52(tt())) -> mark(tt())
active(U61(tt())) -> mark(tt())
active(U71(tt(),P)) -> mark(U72(isPal(P)))
active(U72(tt())) -> mark(tt())
active(U81(tt())) -> mark(tt())
active(isList(V)) -> mark(U11(isNeList(V)))
active(isList(nil())) -> mark(tt())
active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
active(isNeList(V)) -> mark(U31(isQid(V)))
active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
active(isNePal(V)) -> mark(U61(isQid(V)))
active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
active(isPal(V)) -> mark(U81(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(U11(X)) -> active(U11(mark(X)))
mark(tt()) -> active(tt())
mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
mark(U22(X)) -> active(U22(mark(X)))
mark(isList(X)) -> active(isList(X))
mark(U31(X)) -> active(U31(mark(X)))
mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
mark(U42(X)) -> active(U42(mark(X)))
mark(isNeList(X)) -> active(isNeList(X))
mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
mark(U52(X)) -> active(U52(mark(X)))
mark(U61(X)) -> active(U61(mark(X)))
mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
mark(U72(X)) -> active(U72(mark(X)))
mark(isPal(X)) -> active(isPal(X))
mark(U81(X)) -> active(U81(mark(X)))
mark(isQid(X)) -> active(isQid(X))
mark(isNePal(X)) -> active(isNePal(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)
U11(mark(X)) -> U11(X)
U11(active(X)) -> U11(X)
U21(mark(X1),X2) -> U21(X1,X2)
U21(X1,mark(X2)) -> U21(X1,X2)
U21(active(X1),X2) -> U21(X1,X2)
U21(X1,active(X2)) -> U21(X1,X2)
U22(mark(X)) -> U22(X)
U22(active(X)) -> U22(X)
isList(mark(X)) -> isList(X)
isList(active(X)) -> isList(X)
U31(mark(X)) -> U31(X)
U31(active(X)) -> U31(X)
U41(mark(X1),X2) -> U41(X1,X2)
U41(X1,mark(X2)) -> U41(X1,X2)
U41(active(X1),X2) -> U41(X1,X2)
U41(X1,active(X2)) -> U41(X1,X2)
U42(mark(X)) -> U42(X)
U42(active(X)) -> U42(X)
isNeList(mark(X)) -> isNeList(X)
isNeList(active(X)) -> isNeList(X)
U51(mark(X1),X2) -> U51(X1,X2)
U51(X1,mark(X2)) -> U51(X1,X2)
U51(active(X1),X2) -> U51(X1,X2)
U51(X1,active(X2)) -> U51(X1,X2)
U52(mark(X)) -> U52(X)
U52(active(X)) -> U52(X)
U61(mark(X)) -> U61(X)
U61(active(X)) -> U61(X)
U71(mark(X1),X2) -> U71(X1,X2)
U71(X1,mark(X2)) -> U71(X1,X2)
U71(active(X1),X2) -> U71(X1,X2)
U71(X1,active(X2)) -> U71(X1,X2)
U72(mark(X)) -> U72(X)
U72(active(X)) -> U72(X)
isPal(mark(X)) -> isPal(X)
isPal(active(X)) -> isPal(X)
U81(mark(X)) -> U81(X)
U81(active(X)) -> U81(X)
isQid(mark(X)) -> isQid(X)
isQid(active(X)) -> isQid(X)
isNePal(mark(X)) -> isNePal(X)
isNePal(active(X)) -> isNePal(X)
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {37,27,26,25,24,23,22,21,20,19,18,17,16,15,14,13,12,11,10,9,8}
transitions:
o1() -> 39*,6,1
i1() -> 40*,5,1
e1() -> 41*,4,1
a1() -> 42*,3,1
tt1() -> 43*,2,1
nil1() -> 1*
active0(40) -> 8*
active0(5) -> 8*
active0(42) -> 8*
active0(7) -> 8*
active0(2) -> 8*
active0(39) -> 8*
active0(4) -> 8*
active0(41) -> 8*
active0(6) -> 8*
active0(43) -> 8*
active0(38) -> 8*
active0(3) -> 8*
__0(41,39) -> 10*
__0(43,1) -> 10*
__0(41,41) -> 10*
__0(38,1) -> 10*
__0(43,3) -> 10*
__0(41,43) -> 10*
__0(38,3) -> 10*
__0(43,5) -> 10*
__0(38,5) -> 10*
__0(6,39) -> 10*
__0(43,7) -> 10*
__0(1,39) -> 10*
__0(38,7) -> 10*
__0(6,41) -> 10*
__0(3,1) -> 10*
__0(1,41) -> 10*
__0(6,43) -> 10*
__0(3,3) -> 10*
__0(1,43) -> 10*
__0(3,5) -> 10*
__0(3,7) -> 10*
__0(42,38) -> 10*
__0(42,40) -> 10*
__0(42,42) -> 10*
__0(39,2) -> 10*
__0(39,4) -> 10*
__0(7,38) -> 10*
__0(2,38) -> 10*
__0(39,6) -> 10*
__0(7,40) -> 10*
__0(2,40) -> 10*
__0(7,42) -> 10*
__0(4,2) -> 10*
__0(2,42) -> 10*
__0(4,4) -> 10*
__0(4,6) -> 10*
__0(43,39) -> 10*
__0(38,39) -> 10*
__0(43,41) -> 10*
__0(40,1) -> 10*
__0(38,41) -> 10*
__0(43,43) -> 10*
__0(40,3) -> 10*
__0(38,43) -> 10*
__0(40,5) -> 10*
__0(3,39) -> 10*
__0(40,7) -> 10*
__0(5,1) -> 10*
__0(3,41) -> 10*
__0(5,3) -> 10*
__0(3,43) -> 10*
__0(5,5) -> 10*
__0(5,7) -> 10*
__0(39,38) -> 10*
__0(39,40) -> 10*
__0(41,2) -> 10*
__0(39,42) -> 10*
__0(41,4) -> 10*
__0(4,38) -> 10*
__0(41,6) -> 10*
__0(4,40) -> 10*
__0(6,2) -> 10*
__0(4,42) -> 10*
__0(1,2) -> 10*
__0(6,4) -> 10*
__0(1,4) -> 10*
__0(6,6) -> 10*
__0(1,6) -> 10*
__0(40,39) -> 10*
__0(42,1) -> 10*
__0(40,41) -> 10*
__0(42,3) -> 10*
__0(40,43) -> 10*
__0(42,5) -> 10*
__0(5,39) -> 10*
__0(42,7) -> 10*
__0(7,1) -> 10*
__0(5,41) -> 10*
__0(2,1) -> 10*
__0(7,3) -> 10*
__0(5,43) -> 10*
__0(2,3) -> 10*
__0(7,5) -> 10*
__0(2,5) -> 10*
__0(7,7) -> 10*
__0(2,7) -> 10*
__0(41,38) -> 10*
__0(41,40) -> 10*
__0(43,2) -> 10*
__0(41,42) -> 10*
__0(38,2) -> 10*
__0(43,4) -> 10*
__0(38,4) -> 10*
__0(6,38) -> 10*
__0(43,6) -> 10*
__0(1,38) -> 10*
__0(38,6) -> 10*
__0(6,40) -> 10*
__0(1,40) -> 10*
__0(6,42) -> 10*
__0(3,2) -> 10*
__0(1,42) -> 10*
__0(3,4) -> 10*
__0(3,6) -> 10*
__0(42,39) -> 10*
__0(42,41) -> 10*
__0(39,1) -> 10*
__0(42,43) -> 10*
__0(39,3) -> 10*
__0(39,5) -> 10*
__0(7,39) -> 10*
__0(2,39) -> 10*
__0(39,7) -> 10*
__0(7,41) -> 10*
__0(4,1) -> 10*
__0(2,41) -> 10*
__0(7,43) -> 10*
__0(4,3) -> 10*
__0(2,43) -> 10*
__0(4,5) -> 10*
__0(4,7) -> 10*
__0(43,38) -> 10*
__0(38,38) -> 10*
__0(43,40) -> 10*
__0(38,40) -> 10*
__0(43,42) -> 10*
__0(40,2) -> 10*
__0(38,42) -> 10*
__0(40,4) -> 10*
__0(3,38) -> 10*
__0(40,6) -> 10*
__0(3,40) -> 10*
__0(5,2) -> 10*
__0(3,42) -> 10*
__0(5,4) -> 10*
__0(5,6) -> 10*
__0(39,39) -> 10*
__0(41,1) -> 10*
__0(39,41) -> 10*
__0(41,3) -> 10*
__0(39,43) -> 10*
__0(41,5) -> 10*
__0(4,39) -> 10*
__0(41,7) -> 10*
__0(6,1) -> 10*
__0(4,41) -> 10*
__0(1,1) -> 10*
__0(6,3) -> 10*
__0(4,43) -> 10*
__0(1,3) -> 10*
__0(6,5) -> 10*
__0(1,5) -> 10*
__0(6,7) -> 10*
__0(1,7) -> 10*
__0(40,38) -> 10*
__0(40,40) -> 10*
__0(42,2) -> 10*
__0(40,42) -> 10*
__0(42,4) -> 10*
__0(5,38) -> 10*
__0(42,6) -> 10*
__0(5,40) -> 10*
__0(7,2) -> 10*
__0(5,42) -> 10*
__0(2,2) -> 10*
__0(7,4) -> 10*
__0(2,4) -> 10*
__0(7,6) -> 10*
__0(2,6) -> 10*
mark0(40) -> 9*
mark0(5) -> 9*
mark0(42) -> 9*
mark0(7) -> 9*
mark0(2) -> 9*
mark0(39) -> 9*
mark0(4) -> 9*
mark0(41) -> 9*
mark0(6) -> 9*
mark0(1) -> 9*
mark0(43) -> 9*
mark0(38) -> 9*
mark0(3) -> 9*
U110(40) -> 11*
U110(5) -> 11*
U110(42) -> 11*
U110(7) -> 11*
U110(2) -> 11*
U110(39) -> 11*
U110(4) -> 11*
U110(41) -> 11*
U110(6) -> 11*
U110(1) -> 11*
U110(43) -> 11*
U110(38) -> 11*
U110(3) -> 11*
U210(41,39) -> 12*
U210(43,1) -> 12*
U210(41,41) -> 12*
U210(38,1) -> 12*
U210(43,3) -> 12*
U210(41,43) -> 12*
U210(38,3) -> 12*
U210(43,5) -> 12*
U210(38,5) -> 12*
U210(6,39) -> 12*
U210(43,7) -> 12*
U210(1,39) -> 12*
U210(38,7) -> 12*
U210(6,41) -> 12*
U210(3,1) -> 12*
U210(1,41) -> 12*
U210(6,43) -> 12*
U210(3,3) -> 12*
U210(1,43) -> 12*
U210(3,5) -> 12*
U210(3,7) -> 12*
U210(42,38) -> 12*
U210(42,40) -> 12*
U210(42,42) -> 12*
U210(39,2) -> 12*
U210(39,4) -> 12*
U210(7,38) -> 12*
U210(2,38) -> 12*
U210(39,6) -> 12*
U210(7,40) -> 12*
U210(2,40) -> 12*
U210(7,42) -> 12*
U210(4,2) -> 12*
U210(2,42) -> 12*
U210(4,4) -> 12*
U210(4,6) -> 12*
U210(43,39) -> 12*
U210(38,39) -> 12*
U210(43,41) -> 12*
U210(40,1) -> 12*
U210(38,41) -> 12*
U210(43,43) -> 12*
U210(40,3) -> 12*
U210(38,43) -> 12*
U210(40,5) -> 12*
U210(3,39) -> 12*
U210(40,7) -> 12*
U210(5,1) -> 12*
U210(3,41) -> 12*
U210(5,3) -> 12*
U210(3,43) -> 12*
U210(5,5) -> 12*
U210(5,7) -> 12*
U210(39,38) -> 12*
U210(39,40) -> 12*
U210(41,2) -> 12*
U210(39,42) -> 12*
U210(41,4) -> 12*
U210(4,38) -> 12*
U210(41,6) -> 12*
U210(4,40) -> 12*
U210(6,2) -> 12*
U210(4,42) -> 12*
U210(1,2) -> 12*
U210(6,4) -> 12*
U210(1,4) -> 12*
U210(6,6) -> 12*
U210(1,6) -> 12*
U210(40,39) -> 12*
U210(42,1) -> 12*
U210(40,41) -> 12*
U210(42,3) -> 12*
U210(40,43) -> 12*
U210(42,5) -> 12*
U210(5,39) -> 12*
U210(42,7) -> 12*
U210(7,1) -> 12*
U210(5,41) -> 12*
U210(2,1) -> 12*
U210(7,3) -> 12*
U210(5,43) -> 12*
U210(2,3) -> 12*
U210(7,5) -> 12*
U210(2,5) -> 12*
U210(7,7) -> 12*
U210(2,7) -> 12*
U210(41,38) -> 12*
U210(41,40) -> 12*
U210(43,2) -> 12*
U210(41,42) -> 12*
U210(38,2) -> 12*
U210(43,4) -> 12*
U210(38,4) -> 12*
U210(6,38) -> 12*
U210(43,6) -> 12*
U210(1,38) -> 12*
U210(38,6) -> 12*
U210(6,40) -> 12*
U210(1,40) -> 12*
U210(6,42) -> 12*
U210(3,2) -> 12*
U210(1,42) -> 12*
U210(3,4) -> 12*
U210(3,6) -> 12*
U210(42,39) -> 12*
U210(42,41) -> 12*
U210(39,1) -> 12*
U210(42,43) -> 12*
U210(39,3) -> 12*
U210(39,5) -> 12*
U210(7,39) -> 12*
U210(2,39) -> 12*
U210(39,7) -> 12*
U210(7,41) -> 12*
U210(4,1) -> 12*
U210(2,41) -> 12*
U210(7,43) -> 12*
U210(4,3) -> 12*
U210(2,43) -> 12*
U210(4,5) -> 12*
U210(4,7) -> 12*
U210(43,38) -> 12*
U210(38,38) -> 12*
U210(43,40) -> 12*
U210(38,40) -> 12*
U210(43,42) -> 12*
U210(40,2) -> 12*
U210(38,42) -> 12*
U210(40,4) -> 12*
U210(3,38) -> 12*
U210(40,6) -> 12*
U210(3,40) -> 12*
U210(5,2) -> 12*
U210(3,42) -> 12*
U210(5,4) -> 12*
U210(5,6) -> 12*
U210(39,39) -> 12*
U210(41,1) -> 12*
U210(39,41) -> 12*
U210(41,3) -> 12*
U210(39,43) -> 12*
U210(41,5) -> 12*
U210(4,39) -> 12*
U210(41,7) -> 12*
U210(6,1) -> 12*
U210(4,41) -> 12*
U210(1,1) -> 12*
U210(6,3) -> 12*
U210(4,43) -> 12*
U210(1,3) -> 12*
U210(6,5) -> 12*
U210(1,5) -> 12*
U210(6,7) -> 12*
U210(1,7) -> 12*
U210(40,38) -> 12*
U210(40,40) -> 12*
U210(42,2) -> 12*
U210(40,42) -> 12*
U210(42,4) -> 12*
U210(5,38) -> 12*
U210(42,6) -> 12*
U210(5,40) -> 12*
U210(7,2) -> 12*
U210(5,42) -> 12*
U210(2,2) -> 12*
U210(7,4) -> 12*
U210(2,4) -> 12*
U210(7,6) -> 12*
U210(2,6) -> 12*
U220(40) -> 13*
U220(5) -> 13*
U220(42) -> 13*
U220(7) -> 13*
U220(2) -> 13*
U220(39) -> 13*
U220(4) -> 13*
U220(41) -> 13*
U220(6) -> 13*
U220(1) -> 13*
U220(43) -> 13*
U220(38) -> 13*
U220(3) -> 13*
isList0(40) -> 14*
isList0(5) -> 14*
isList0(42) -> 14*
isList0(7) -> 14*
isList0(2) -> 14*
isList0(39) -> 14*
isList0(4) -> 14*
isList0(41) -> 14*
isList0(6) -> 14*
isList0(1) -> 14*
isList0(43) -> 14*
isList0(38) -> 14*
isList0(3) -> 14*
U310(40) -> 15*
U310(5) -> 15*
U310(42) -> 15*
U310(7) -> 15*
U310(2) -> 15*
U310(39) -> 15*
U310(4) -> 15*
U310(41) -> 15*
U310(6) -> 15*
U310(1) -> 15*
U310(43) -> 15*
U310(38) -> 15*
U310(3) -> 15*
U410(2,6) -> 16*
U410(41,39) -> 16*
U410(43,1) -> 16*
U410(41,41) -> 16*
U410(38,1) -> 16*
U410(43,3) -> 16*
U410(41,43) -> 16*
U410(38,3) -> 16*
U410(43,5) -> 16*
U410(38,5) -> 16*
U410(6,39) -> 16*
U410(43,7) -> 16*
U410(1,39) -> 16*
U410(38,7) -> 16*
U410(6,41) -> 16*
U410(3,1) -> 16*
U410(1,41) -> 16*
U410(6,43) -> 16*
U410(3,3) -> 16*
U410(1,43) -> 16*
U410(3,5) -> 16*
U410(3,7) -> 16*
U410(42,38) -> 16*
U410(42,40) -> 16*
U410(42,42) -> 16*
U410(39,2) -> 16*
U410(39,4) -> 16*
U410(7,38) -> 16*
U410(2,38) -> 16*
U410(39,6) -> 16*
U410(7,40) -> 16*
U410(2,40) -> 16*
U410(7,42) -> 16*
U410(4,2) -> 16*
U410(2,42) -> 16*
U410(4,4) -> 16*
U410(4,6) -> 16*
U410(43,39) -> 16*
U410(38,39) -> 16*
U410(43,41) -> 16*
U410(40,1) -> 16*
U410(38,41) -> 16*
U410(43,43) -> 16*
U410(40,3) -> 16*
U410(38,43) -> 16*
U410(40,5) -> 16*
U410(3,39) -> 16*
U410(40,7) -> 16*
U410(5,1) -> 16*
U410(3,41) -> 16*
U410(5,3) -> 16*
U410(3,43) -> 16*
U410(5,5) -> 16*
U410(5,7) -> 16*
U410(39,38) -> 16*
U410(39,40) -> 16*
U410(41,2) -> 16*
U410(39,42) -> 16*
U410(41,4) -> 16*
U410(4,38) -> 16*
U410(41,6) -> 16*
U410(4,40) -> 16*
U410(6,2) -> 16*
U410(4,42) -> 16*
U410(1,2) -> 16*
U410(6,4) -> 16*
U410(1,4) -> 16*
U410(6,6) -> 16*
U410(1,6) -> 16*
U410(40,39) -> 16*
U410(42,1) -> 16*
U410(40,41) -> 16*
U410(42,3) -> 16*
U410(40,43) -> 16*
U410(42,5) -> 16*
U410(5,39) -> 16*
U410(42,7) -> 16*
U410(7,1) -> 16*
U410(5,41) -> 16*
U410(2,1) -> 16*
U410(7,3) -> 16*
U410(5,43) -> 16*
U410(2,3) -> 16*
U410(7,5) -> 16*
U410(2,5) -> 16*
U410(7,7) -> 16*
U410(2,7) -> 16*
U410(41,38) -> 16*
U410(41,40) -> 16*
U410(43,2) -> 16*
U410(41,42) -> 16*
U410(38,2) -> 16*
U410(43,4) -> 16*
U410(38,4) -> 16*
U410(6,38) -> 16*
U410(43,6) -> 16*
U410(1,38) -> 16*
U410(38,6) -> 16*
U410(6,40) -> 16*
U410(1,40) -> 16*
U410(6,42) -> 16*
U410(3,2) -> 16*
U410(1,42) -> 16*
U410(3,4) -> 16*
U410(3,6) -> 16*
U410(42,39) -> 16*
U410(42,41) -> 16*
U410(39,1) -> 16*
U410(42,43) -> 16*
U410(39,3) -> 16*
U410(39,5) -> 16*
U410(7,39) -> 16*
U410(2,39) -> 16*
U410(39,7) -> 16*
U410(7,41) -> 16*
U410(4,1) -> 16*
U410(2,41) -> 16*
U410(7,43) -> 16*
U410(4,3) -> 16*
U410(2,43) -> 16*
U410(4,5) -> 16*
U410(4,7) -> 16*
U410(43,38) -> 16*
U410(38,38) -> 16*
U410(43,40) -> 16*
U410(38,40) -> 16*
U410(43,42) -> 16*
U410(40,2) -> 16*
U410(38,42) -> 16*
U410(40,4) -> 16*
U410(3,38) -> 16*
U410(40,6) -> 16*
U410(3,40) -> 16*
U410(5,2) -> 16*
U410(3,42) -> 16*
U410(5,4) -> 16*
U410(5,6) -> 16*
U410(39,39) -> 16*
U410(41,1) -> 16*
U410(39,41) -> 16*
U410(41,3) -> 16*
U410(39,43) -> 16*
U410(41,5) -> 16*
U410(4,39) -> 16*
U410(41,7) -> 16*
U410(6,1) -> 16*
U410(4,41) -> 16*
U410(1,1) -> 16*
U410(6,3) -> 16*
U410(4,43) -> 16*
U410(1,3) -> 16*
U410(6,5) -> 16*
U410(1,5) -> 16*
U410(6,7) -> 16*
U410(1,7) -> 16*
U410(40,38) -> 16*
U410(40,40) -> 16*
U410(42,2) -> 16*
U410(40,42) -> 16*
U410(42,4) -> 16*
U410(5,38) -> 16*
U410(42,6) -> 16*
U410(5,40) -> 16*
U410(7,2) -> 16*
U410(5,42) -> 16*
U410(2,2) -> 16*
U410(7,4) -> 16*
U410(2,4) -> 16*
U410(7,6) -> 16*
U420(40) -> 17*
U420(5) -> 17*
U420(42) -> 17*
U420(7) -> 17*
U420(2) -> 17*
U420(39) -> 17*
U420(4) -> 17*
U420(41) -> 17*
U420(6) -> 17*
U420(1) -> 17*
U420(43) -> 17*
U420(38) -> 17*
U420(3) -> 17*
isNeList0(40) -> 18*
isNeList0(5) -> 18*
isNeList0(42) -> 18*
isNeList0(7) -> 18*
isNeList0(2) -> 18*
isNeList0(39) -> 18*
isNeList0(4) -> 18*
isNeList0(41) -> 18*
isNeList0(6) -> 18*
isNeList0(1) -> 18*
isNeList0(43) -> 18*
isNeList0(38) -> 18*
isNeList0(3) -> 18*
U510(7,6) -> 19*
U510(2,6) -> 19*
U510(41,39) -> 19*
U510(43,1) -> 19*
U510(41,41) -> 19*
U510(38,1) -> 19*
U510(43,3) -> 19*
U510(41,43) -> 19*
U510(38,3) -> 19*
U510(43,5) -> 19*
U510(38,5) -> 19*
U510(6,39) -> 19*
U510(43,7) -> 19*
U510(1,39) -> 19*
U510(38,7) -> 19*
U510(6,41) -> 19*
U510(3,1) -> 19*
U510(1,41) -> 19*
U510(6,43) -> 19*
U510(3,3) -> 19*
U510(1,43) -> 19*
U510(3,5) -> 19*
U510(3,7) -> 19*
U510(42,38) -> 19*
U510(42,40) -> 19*
U510(42,42) -> 19*
U510(39,2) -> 19*
U510(39,4) -> 19*
U510(7,38) -> 19*
U510(2,38) -> 19*
U510(39,6) -> 19*
U510(7,40) -> 19*
U510(2,40) -> 19*
U510(7,42) -> 19*
U510(4,2) -> 19*
U510(2,42) -> 19*
U510(4,4) -> 19*
U510(4,6) -> 19*
U510(43,39) -> 19*
U510(38,39) -> 19*
U510(43,41) -> 19*
U510(40,1) -> 19*
U510(38,41) -> 19*
U510(43,43) -> 19*
U510(40,3) -> 19*
U510(38,43) -> 19*
U510(40,5) -> 19*
U510(3,39) -> 19*
U510(40,7) -> 19*
U510(5,1) -> 19*
U510(3,41) -> 19*
U510(5,3) -> 19*
U510(3,43) -> 19*
U510(5,5) -> 19*
U510(5,7) -> 19*
U510(39,38) -> 19*
U510(39,40) -> 19*
U510(41,2) -> 19*
U510(39,42) -> 19*
U510(41,4) -> 19*
U510(4,38) -> 19*
U510(41,6) -> 19*
U510(4,40) -> 19*
U510(6,2) -> 19*
U510(4,42) -> 19*
U510(1,2) -> 19*
U510(6,4) -> 19*
U510(1,4) -> 19*
U510(6,6) -> 19*
U510(1,6) -> 19*
U510(40,39) -> 19*
U510(42,1) -> 19*
U510(40,41) -> 19*
U510(42,3) -> 19*
U510(40,43) -> 19*
U510(42,5) -> 19*
U510(5,39) -> 19*
U510(42,7) -> 19*
U510(7,1) -> 19*
U510(5,41) -> 19*
U510(2,1) -> 19*
U510(7,3) -> 19*
U510(5,43) -> 19*
U510(2,3) -> 19*
U510(7,5) -> 19*
U510(2,5) -> 19*
U510(7,7) -> 19*
U510(2,7) -> 19*
U510(41,38) -> 19*
U510(41,40) -> 19*
U510(43,2) -> 19*
U510(41,42) -> 19*
U510(38,2) -> 19*
U510(43,4) -> 19*
U510(38,4) -> 19*
U510(6,38) -> 19*
U510(43,6) -> 19*
U510(1,38) -> 19*
U510(38,6) -> 19*
U510(6,40) -> 19*
U510(1,40) -> 19*
U510(6,42) -> 19*
U510(3,2) -> 19*
U510(1,42) -> 19*
U510(3,4) -> 19*
U510(3,6) -> 19*
U510(42,39) -> 19*
U510(42,41) -> 19*
U510(39,1) -> 19*
U510(42,43) -> 19*
U510(39,3) -> 19*
U510(39,5) -> 19*
U510(7,39) -> 19*
U510(2,39) -> 19*
U510(39,7) -> 19*
U510(7,41) -> 19*
U510(4,1) -> 19*
U510(2,41) -> 19*
U510(7,43) -> 19*
U510(4,3) -> 19*
U510(2,43) -> 19*
U510(4,5) -> 19*
U510(4,7) -> 19*
U510(43,38) -> 19*
U510(38,38) -> 19*
U510(43,40) -> 19*
U510(38,40) -> 19*
U510(43,42) -> 19*
U510(40,2) -> 19*
U510(38,42) -> 19*
U510(40,4) -> 19*
U510(3,38) -> 19*
U510(40,6) -> 19*
U510(3,40) -> 19*
U510(5,2) -> 19*
U510(3,42) -> 19*
U510(5,4) -> 19*
U510(5,6) -> 19*
U510(39,39) -> 19*
U510(41,1) -> 19*
U510(39,41) -> 19*
U510(41,3) -> 19*
U510(39,43) -> 19*
U510(41,5) -> 19*
U510(4,39) -> 19*
U510(41,7) -> 19*
U510(6,1) -> 19*
U510(4,41) -> 19*
U510(1,1) -> 19*
U510(6,3) -> 19*
U510(4,43) -> 19*
U510(1,3) -> 19*
U510(6,5) -> 19*
U510(1,5) -> 19*
U510(6,7) -> 19*
U510(1,7) -> 19*
U510(40,38) -> 19*
U510(40,40) -> 19*
U510(42,2) -> 19*
U510(40,42) -> 19*
U510(42,4) -> 19*
U510(5,38) -> 19*
U510(42,6) -> 19*
U510(5,40) -> 19*
U510(7,2) -> 19*
U510(5,42) -> 19*
U510(2,2) -> 19*
U510(7,4) -> 19*
U510(2,4) -> 19*
U520(40) -> 20*
U520(5) -> 20*
U520(42) -> 20*
U520(7) -> 20*
U520(2) -> 20*
U520(39) -> 20*
U520(4) -> 20*
U520(41) -> 20*
U520(6) -> 20*
U520(1) -> 20*
U520(43) -> 20*
U520(38) -> 20*
U520(3) -> 20*
U610(40) -> 21*
U610(5) -> 21*
U610(42) -> 21*
U610(7) -> 21*
U610(2) -> 21*
U610(39) -> 21*
U610(4) -> 21*
U610(41) -> 21*
U610(6) -> 21*
U610(1) -> 21*
U610(43) -> 21*
U610(38) -> 21*
U610(3) -> 21*
U710(7,6) -> 22*
U710(2,6) -> 22*
U710(41,39) -> 22*
U710(43,1) -> 22*
U710(41,41) -> 22*
U710(38,1) -> 22*
U710(43,3) -> 22*
U710(41,43) -> 22*
U710(38,3) -> 22*
U710(43,5) -> 22*
U710(38,5) -> 22*
U710(6,39) -> 22*
U710(43,7) -> 22*
U710(1,39) -> 22*
U710(38,7) -> 22*
U710(6,41) -> 22*
U710(3,1) -> 22*
U710(1,41) -> 22*
U710(6,43) -> 22*
U710(3,3) -> 22*
U710(1,43) -> 22*
U710(3,5) -> 22*
U710(3,7) -> 22*
U710(42,38) -> 22*
U710(42,40) -> 22*
U710(42,42) -> 22*
U710(39,2) -> 22*
U710(39,4) -> 22*
U710(7,38) -> 22*
U710(2,38) -> 22*
U710(39,6) -> 22*
U710(7,40) -> 22*
U710(2,40) -> 22*
U710(7,42) -> 22*
U710(4,2) -> 22*
U710(2,42) -> 22*
U710(4,4) -> 22*
U710(4,6) -> 22*
U710(43,39) -> 22*
U710(38,39) -> 22*
U710(43,41) -> 22*
U710(40,1) -> 22*
U710(38,41) -> 22*
U710(43,43) -> 22*
U710(40,3) -> 22*
U710(38,43) -> 22*
U710(40,5) -> 22*
U710(3,39) -> 22*
U710(40,7) -> 22*
U710(5,1) -> 22*
U710(3,41) -> 22*
U710(5,3) -> 22*
U710(3,43) -> 22*
U710(5,5) -> 22*
U710(5,7) -> 22*
U710(39,38) -> 22*
U710(39,40) -> 22*
U710(41,2) -> 22*
U710(39,42) -> 22*
U710(41,4) -> 22*
U710(4,38) -> 22*
U710(41,6) -> 22*
U710(4,40) -> 22*
U710(6,2) -> 22*
U710(4,42) -> 22*
U710(1,2) -> 22*
U710(6,4) -> 22*
U710(1,4) -> 22*
U710(6,6) -> 22*
U710(1,6) -> 22*
U710(40,39) -> 22*
U710(42,1) -> 22*
U710(40,41) -> 22*
U710(42,3) -> 22*
U710(40,43) -> 22*
U710(42,5) -> 22*
U710(5,39) -> 22*
U710(42,7) -> 22*
U710(7,1) -> 22*
U710(5,41) -> 22*
U710(2,1) -> 22*
U710(7,3) -> 22*
U710(5,43) -> 22*
U710(2,3) -> 22*
U710(7,5) -> 22*
U710(2,5) -> 22*
U710(7,7) -> 22*
U710(2,7) -> 22*
U710(41,38) -> 22*
U710(41,40) -> 22*
U710(43,2) -> 22*
U710(41,42) -> 22*
U710(38,2) -> 22*
U710(43,4) -> 22*
U710(38,4) -> 22*
U710(6,38) -> 22*
U710(43,6) -> 22*
U710(1,38) -> 22*
U710(38,6) -> 22*
U710(6,40) -> 22*
U710(1,40) -> 22*
U710(6,42) -> 22*
U710(3,2) -> 22*
U710(1,42) -> 22*
U710(3,4) -> 22*
U710(3,6) -> 22*
U710(42,39) -> 22*
U710(42,41) -> 22*
U710(39,1) -> 22*
U710(42,43) -> 22*
U710(39,3) -> 22*
U710(39,5) -> 22*
U710(7,39) -> 22*
U710(2,39) -> 22*
U710(39,7) -> 22*
U710(7,41) -> 22*
U710(4,1) -> 22*
U710(2,41) -> 22*
U710(7,43) -> 22*
U710(4,3) -> 22*
U710(2,43) -> 22*
U710(4,5) -> 22*
U710(4,7) -> 22*
U710(43,38) -> 22*
U710(38,38) -> 22*
U710(43,40) -> 22*
U710(38,40) -> 22*
U710(43,42) -> 22*
U710(40,2) -> 22*
U710(38,42) -> 22*
U710(40,4) -> 22*
U710(3,38) -> 22*
U710(40,6) -> 22*
U710(3,40) -> 22*
U710(5,2) -> 22*
U710(3,42) -> 22*
U710(5,4) -> 22*
U710(5,6) -> 22*
U710(39,39) -> 22*
U710(41,1) -> 22*
U710(39,41) -> 22*
U710(41,3) -> 22*
U710(39,43) -> 22*
U710(41,5) -> 22*
U710(4,39) -> 22*
U710(41,7) -> 22*
U710(6,1) -> 22*
U710(4,41) -> 22*
U710(1,1) -> 22*
U710(6,3) -> 22*
U710(4,43) -> 22*
U710(1,3) -> 22*
U710(6,5) -> 22*
U710(1,5) -> 22*
U710(6,7) -> 22*
U710(1,7) -> 22*
U710(40,38) -> 22*
U710(40,40) -> 22*
U710(42,2) -> 22*
U710(40,42) -> 22*
U710(42,4) -> 22*
U710(5,38) -> 22*
U710(42,6) -> 22*
U710(5,40) -> 22*
U710(7,2) -> 22*
U710(5,42) -> 22*
U710(2,2) -> 22*
U710(7,4) -> 22*
U710(2,4) -> 22*
U720(40) -> 23*
U720(5) -> 23*
U720(42) -> 23*
U720(7) -> 23*
U720(2) -> 23*
U720(39) -> 23*
U720(4) -> 23*
U720(41) -> 23*
U720(6) -> 23*
U720(1) -> 23*
U720(43) -> 23*
U720(38) -> 23*
U720(3) -> 23*
isPal0(40) -> 24*
isPal0(5) -> 24*
isPal0(42) -> 24*
isPal0(7) -> 24*
isPal0(2) -> 24*
isPal0(39) -> 24*
isPal0(4) -> 24*
isPal0(41) -> 24*
isPal0(6) -> 24*
isPal0(1) -> 24*
isPal0(43) -> 24*
isPal0(38) -> 24*
isPal0(3) -> 24*
U810(40) -> 25*
U810(5) -> 25*
U810(42) -> 25*
U810(7) -> 25*
U810(2) -> 25*
U810(39) -> 25*
U810(4) -> 25*
U810(41) -> 25*
U810(6) -> 25*
U810(1) -> 25*
U810(43) -> 25*
U810(38) -> 25*
U810(3) -> 25*
isQid0(40) -> 26*
isQid0(5) -> 26*
isQid0(42) -> 26*
isQid0(7) -> 26*
isQid0(2) -> 26*
isQid0(39) -> 26*
isQid0(4) -> 26*
isQid0(41) -> 26*
isQid0(6) -> 26*
isQid0(1) -> 26*
isQid0(43) -> 26*
isQid0(38) -> 26*
isQid0(3) -> 26*
isNePal0(40) -> 27*
isNePal0(5) -> 27*
isNePal0(42) -> 27*
isNePal0(7) -> 27*
isNePal0(2) -> 27*
isNePal0(39) -> 27*
isNePal0(4) -> 27*
isNePal0(41) -> 27*
isNePal0(6) -> 27*
isNePal0(1) -> 27*
isNePal0(43) -> 27*
isNePal0(38) -> 27*
isNePal0(3) -> 27*
active1(40) -> 8,37*
active1(42) -> 8,37*
active1(39) -> 8,37*
active1(41) -> 8,37*
active1(1) -> 37*,8,9
active1(43) -> 8,37*
active1(38) -> 8,37*
u1() -> 38*,7,1
problem:
Qed