(VAR X Y Z V2 P V V1 I)
(STRATEGY CONTEXTSENSITIVE 
  (__ 1 2)
  (nil)
  (U11 1)
  (tt)
  (U21 1)
  (U22 1)
  (isList)
  (U31 1)
  (U41 1)
  (U42 1)
  (isNeList)
  (U51 1)
  (U52 1)
  (U61 1)
  (U71 1)
  (U72 1)
  (isPal)
  (U81 1)
  (isQid)
  (isNePal)
  (a)
  (e)
  (i)
  (o)
  (u)
)
(RULES 
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt) -> tt
U21(tt,V2) -> U22(isList(V2))
U22(tt) -> tt
U31(tt) -> tt
U41(tt,V2) -> U42(isNeList(V2))
U42(tt) -> tt
U51(tt,V2) -> U52(isList(V2))
U52(tt) -> tt
U61(tt) -> tt
U71(tt,P) -> U72(isPal(P))
U72(tt) -> tt
U81(tt) -> tt
isList(V) -> U11(isNeList(V))
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isList(V1),V2)
isNeList(V) -> U31(isQid(V))
isNeList(__(V1,V2)) -> U41(isList(V1),V2)
isNeList(__(V1,V2)) -> U51(isNeList(V1),V2)
isNePal(V) -> U61(isQid(V))
isNePal(__(I,__(P,I))) -> U71(isQid(I),P)
isPal(V) -> U81(isNePal(V))
isPal(nil) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
)

Proving termination of context-sensitive rewriting for PALINDROME_nokinds_noand:

-> Dependency pairs:
nF___(__(X,Y),Z) -> nF___(X,__(Y,Z))
nF___(__(X,Y),Z) -> nF___(Y,Z)
nF_U21(tt,V2) -> nF_U22(isList(V2))
nF_U21(tt,V2) -> nF_isList(V2)
nF_U41(tt,V2) -> nF_U42(isNeList(V2))
nF_U41(tt,V2) -> nF_isNeList(V2)
nF_U51(tt,V2) -> nF_U52(isList(V2))
nF_U51(tt,V2) -> nF_isList(V2)
nF_U71(tt,P) -> nF_U72(isPal(P))
nF_U71(tt,P) -> nF_isPal(P)
nF_isList(V) -> nF_U11(isNeList(V))
nF_isList(V) -> nF_isNeList(V)
nF_isList(__(V1,V2)) -> nF_U21(isList(V1),V2)
nF_isList(__(V1,V2)) -> nF_isList(V1)
nF_isNeList(V) -> nF_U31(isQid(V))
nF_isNeList(V) -> nF_isQid(V)
nF_isNeList(__(V1,V2)) -> nF_U41(isList(V1),V2)
nF_isNeList(__(V1,V2)) -> nF_isList(V1)
nF_isNeList(__(V1,V2)) -> nF_U51(isNeList(V1),V2)
nF_isNeList(__(V1,V2)) -> nF_isNeList(V1)
nF_isNePal(V) -> nF_U61(isQid(V))
nF_isNePal(V) -> nF_isQid(V)
nF_isNePal(__(I,__(P,I))) -> nF_U71(isQid(I),P)
nF_isNePal(__(I,__(P,I))) -> nF_isQid(I)
nF_isPal(V) -> nF_U81(isNePal(V))
nF_isPal(V) -> nF_isNePal(V)

-> Proof of termination for PALINDROME_nokinds_noand_1_1:
-> -> Dependency pairs in cycle:
nF_U71(tt,P) -> nF_isPal(P)
nF_isNePal(__(I,__(P,I))) -> nF_U71(isQid(I),P)
nF_isPal(V) -> nF_isNePal(V)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nokinds_noand_1_2:
-> -> Dependency pairs in cycle:
nF_U21(tt,V2) -> nF_isList(V2)
nF_isList(__(V1,V2)) -> nF_U21(isList(V1),V2)
nF_isNeList(__(V1,V2)) -> nF_isList(V1)
nF_isNeList(__(V1,V2)) -> nF_isNeList(V1)
nF_isList(V) -> nF_isNeList(V)
nF_isList(__(V1,V2)) -> nF_isList(V1)
nF_U51(tt,V2) -> nF_isList(V2)
nF_isNeList(__(V1,V2)) -> nF_U51(isNeList(V1),V2)
nF_U41(tt,V2) -> nF_isNeList(V2)
nF_isNeList(__(V1,V2)) -> nF_U41(isList(V1),V2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_nokinds_noand_1_3:
-> -> Dependency pairs in cycle:
nF___(__(X,Y),Z) -> nF___(X,__(Y,Z))
nF___(__(X,Y),Z) -> nF___(Y,Z)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in CSDG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.