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