YES
Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51

- : unit = ()
- : unit = ()
X : variable_set = <variable set>

F : signature = <signature>
R : HTRS = { __(__(X,Y),Z) -> __(X,__(Y,Z)),
             __(X,nil) -> X,
             __(nil,X) -> X,
             U11(tt,V) -> U12(isNeList(V)),
             U12(tt) -> tt,
             U21(tt,V1,V2) -> U22(isList(V1),V2),
             U22(tt,V2) -> U23(isList(V2)),
             U23(tt) -> tt,
             U31(tt,V) -> U32(isQid(V)),
             U32(tt) -> tt,
             U41(tt,V1,V2) -> U42(isList(V1),V2),
             U42(tt,V2) -> U43(isNeList(V2)),
             U43(tt) -> tt,
             U51(tt,V1,V2) -> U52(isNeList(V1),V2),
             U52(tt,V2) -> U53(isList(V2)),
             U53(tt) -> tt,
             U61(tt,V) -> U62(isQid(V)),
             U62(tt) -> tt,
             U71(tt,V) -> U72(isNePal(V)),
             U72(tt) -> tt,
             and(tt,X) -> X,
             isList(V) -> U11(isPalListKind(V),V),
             isList(nil) -> tt,
             isList(__(V1,V2)) ->
             U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2),
             isNeList(V) -> U31(isPalListKind(V),V),
             isNeList(__(V1,V2)) ->
             U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2),
             isNeList(__(V1,V2)) ->
             U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2),
             isNePal(V) -> U61(isPalListKind(V),V),
             isNePal(__(I,__(P,I))) ->
             and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))),
             isPal(V) -> U71(isPalListKind(V),V),
             isPal(nil) -> tt,
             isPalListKind(a) -> tt,
             isPalListKind(e) -> tt,
             isPalListKind(i) -> tt,
             isPalListKind(nil) -> tt,
             isPalListKind(o) -> tt,
             isPalListKind(u) -> tt,
             isPalListKind(__(V1,V2)) ->
             and(isPalListKind(V1),isPalListKind(V2)),
             isQid(a) -> tt,
             isQid(e) -> tt,
             isQid(i) -> tt,
             isQid(o) -> tt,
             isQid(u) -> tt } (43 rules)
Termination now uses minimal decomposition
- : unit = ()
Entering the termination expert for modules. Verbose level = 0
Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ and(tt,V_5) -> V_5 } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{}

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ __(__(V_5,V_7),V_6) -> __(V_5,__(V_7,V_6)),
  __(V_5,nil) -> V_5,
  __(nil,V_5) -> V_5 } (3 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(5 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[nil] = 0;  [__](X0,X1) = X1 + X0 + 1;  ['__`](X0,X1) = X0;  

Checking module:
{ isPalListKind(__(V_2,V_3)) -> and(isPalListKind(V_2),isPalListKind(V_3)),
  isPalListKind(u) -> tt,
  isPalListKind(o) -> tt,
  isPalListKind(nil) -> tt,
  isPalListKind(i) -> tt,
  isPalListKind(e) -> tt,
  isPalListKind(a) -> tt } (7 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(13 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[tt] = 0; 
[nil] = 0; 
[__](X0,X1) = X1 + X0 + 1; 
[a] = 0; 
[e] = 0; 
[i] = 0; 
[o] = 0; 
[u] = 0; 
[and](X0,X1) = X1; 
[isPalListKind](X0) = 0; 
['isPalListKind`](X0) = X0; 


Checking module:
{ U72(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U62(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ isQid(a) -> tt,
  isQid(e) -> tt,
  isQid(i) -> tt,
  isQid(o) -> tt,
  isQid(u) -> tt } (5 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U61(tt,V_4) -> U62(isQid(V_4)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ isPal(V_4) -> U71(isPalListKind(V_4),V_4),
  isPal(nil) -> tt,
  isNePal(__(V_0,__(V_1,V_0))) ->
  and(and(isQid(V_0),isPalListKind(V_0)),and(isPal(V_1),isPalListKind(V_1))),
  isNePal(V_4) -> U61(isPalListKind(V_4),V_4),
  U71(tt,V_4) -> U72(isNePal(V_4)) } (5 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(27 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[tt] = 1; 
[nil] = 1; 
[__](X0,X1) = X1 + 2*X0 + 1; 
[a] = 1; 
[e] = 1; 
[i] = 1; 
[o] = 1; 
[u] = 1; 
[isQid](X0) = X0; 
[and](X0,X1) = X1; 
[isPalListKind](X0) = X0; 
[U62](X0) = X0; 
[U61](X0,X1) = X1; 
[U72](X0) = X0; 
[U71](X0,X1) = X1; 
[isNePal](X0) = X0; 
[isPal](X0) = X0; 
['U71`](X0,X1) = X1 + X0; 
['isNePal`](X0) = X0; 
['isPal`](X0) = 2*X0 + 1; 


Checking module:
{ U53(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U23(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U12(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U43(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U32(tt) -> tt } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U31(tt,V_4) -> U32(isQid(V_4)) } (1 rules)

The dependency graph is
(0 nodes)
Checking each of the 0 strongly connected components :

Checking module:
{ U52(tt,V_3) -> U53(isList(V_3)),
  U51(tt,V_2,V_3) -> U52(isNeList(V_2),V_3),
  isNeList(__(V_2,V_3)) ->
  U51(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3),
  isNeList(__(V_2,V_3)) ->
  U41(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3),
  isNeList(V_4) -> U31(isPalListKind(V_4),V_4),
  U11(tt,V_4) -> U12(isNeList(V_4)),
  isList(__(V_2,V_3)) ->
  U21(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3),
  isList(nil) -> tt,
  isList(V_4) -> U11(isPalListKind(V_4),V_4),
  U22(tt,V_3) -> U23(isList(V_3)),
  U21(tt,V_2,V_3) -> U22(isList(V_2),V_3),
  U42(tt,V_3) -> U43(isNeList(V_3)),
  U41(tt,V_2,V_3) -> U42(isList(V_2),V_3) } (13 rules)

The dependency graph is
(1 nodes)
Checking each of the 1 strongly connected components :
Checking component 1
Trying simple graph criterion.
Trying to solve the following constraints:
(49 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[tt] = 2; 
[U53](X0) = X0; 
[nil] = 2; 
[__](X0,X1) = X1 + X0 + 2; 
[a] = 2; 
[e] = 2; 
[i] = 2; 
[o] = 2; 
[u] = 2; 
[isQid](X0) = X0; 
[U32](X0) = X0; 
[U31](X0,X1) = X1; 
[and](X0,X1) = X1; 
[isPalListKind](X0) = 2; 
[U12](X0) = X0; 
[U23](X0) = X0; 
[U43](X0) = X0; 
[U41](X0,X1,X2) = X2; 
[U42](X0,X1) = X1; 
[U21](X0,X1,X2) = X2; 
[U22](X0,X1) = X1; 
[isList](X0) = X0; 
[U11](X0,X1) = X1; 
[isNeList](X0) = X0; 
[U51](X0,X1,X2) = X2; 
[U52](X0,X1) = X1; 
['U41`](X0,X1,X2) = 2*X2 + 2*X1 + X0 + 1; 
['U42`](X0,X1) = 2*X1 + 1; 
['U21`](X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; 
['U22`](X0,X1) = 2*X1 + 2*X0; 
['isList`](X0) = 2*X0 + 2; 
['U11`](X0,X1) = 2*X1 + 1; 
['isNeList`](X0) = 2*X0; 
['U51`](X0,X1,X2) = 2*X2 + 2*X1 + 1; 
['U52`](X0,X1) = 2*X1 + 2*X0; 


Modular termination proof found.
- : unit = ()
The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { and(tt,V_5) -> V_5 } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  {}
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { __(__(V_5,V_7),V_6) -> __(V_5,__(V_7,V_6)),
    __(V_5,nil) -> V_5,
    __(nil,V_5) -> V_5 } (3 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: '__`(__(V_5,V_7),V_6) ; '__`(V_7,V_6)
    1: '__`(__(V_5,V_7),V_6) ; '__`(V_5,__(V_7,V_6)) 
    0 -> 0, 0 -> 1, 1 -> 0, 1 -> 1, 
    On this component, the interpretation
    [nil] = 0;  [__](X0,X1) = X1 + X0 + 1;  ['__`](X0,X1) = X0;  
    strictly decreases on every cycle

The module
  { isPalListKind(__(V_2,V_3)) -> and(isPalListKind(V_2),isPalListKind(V_3)),
    isPalListKind(u) -> tt,
    isPalListKind(o) -> tt,
    isPalListKind(nil) -> tt,
    isPalListKind(i) -> tt,
    isPalListKind(e) -> tt,
    isPalListKind(a) -> tt } (7 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'isPalListKind`(__(V_2,V_3)) ; 'isPalListKind`(V_3)
    1: 'isPalListKind`(__(V_2,V_3)) ; 'isPalListKind`(V_2) 
    0 -> 0, 0 -> 1, 1 -> 0, 1 -> 1, 
    On this component, the interpretation
    [tt] = 0; 
    [nil] = 0; 
    [__](X0,X1) = X1 + X0 + 1; 
    [a] = 0; 
    [e] = 0; 
    [i] = 0; 
    [o] = 0; 
    [u] = 0; 
    [and](X0,X1) = X1; 
    [isPalListKind](X0) = 0; 
    ['isPalListKind`](X0) = X0; 
     strictly decreases on every cycle

The module
  { U72(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U62(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { isQid(a) -> tt,
    isQid(e) -> tt,
    isQid(i) -> tt,
    isQid(o) -> tt,
    isQid(u) -> tt } (5 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U61(tt,V_4) -> U62(isQid(V_4)) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { isPal(V_4) -> U71(isPalListKind(V_4),V_4),
    isPal(nil) -> tt,
    isNePal(__(V_0,__(V_1,V_0))) ->
    and(and(isQid(V_0),isPalListKind(V_0)),and(isPal(V_1),isPalListKind(V_1))),
    isNePal(V_4) -> U61(isPalListKind(V_4),V_4),
    U71(tt,V_4) -> U72(isNePal(V_4)) } (5 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U71`(tt,V_4) ; 'isNePal`(V_4)
    1: 'isNePal`(__(V_0,__(V_1,V_0))) ; 'isPal`(V_1)
    2: 'isPal`(V_4) ; 'U71`(isPalListKind(V_4),V_4) 
    0 -> 1, 1 -> 2, 2 -> 0, 
    On this component, the interpretation
    [tt] = 1; 
    [nil] = 1; 
    [__](X0,X1) = X1 + 2*X0 + 1; 
    [a] = 1; 
    [e] = 1; 
    [i] = 1; 
    [o] = 1; 
    [u] = 1; 
    [isQid](X0) = X0; 
    [and](X0,X1) = X1; 
    [isPalListKind](X0) = X0; 
    [U62](X0) = X0; 
    [U61](X0,X1) = X1; 
    [U72](X0) = X0; 
    [U71](X0,X1) = X1; 
    [isNePal](X0) = X0; 
    [isPal](X0) = X0; 
    ['U71`](X0,X1) = X1 + X0; 
    ['isNePal`](X0) = X0; 
    ['isPal`](X0) = 2*X0 + 1; 
     strictly decreases on every cycle

The module
  { U53(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U23(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U12(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U43(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U32(tt) -> tt } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U31(tt,V_4) -> U32(isQid(V_4)) } (1 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has no strongly connected components.

The module
  { U52(tt,V_3) -> U53(isList(V_3)),
    U51(tt,V_2,V_3) -> U52(isNeList(V_2),V_3),
    isNeList(__(V_2,V_3)) ->
    U51(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3),
    isNeList(__(V_2,V_3)) ->
    U41(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3),
    isNeList(V_4) -> U31(isPalListKind(V_4),V_4),
    U11(tt,V_4) -> U12(isNeList(V_4)),
    isList(__(V_2,V_3)) ->
    U21(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3),
    isList(nil) -> tt,
    isList(V_4) -> U11(isPalListKind(V_4),V_4),
    U22(tt,V_3) -> U23(isList(V_3)),
    U21(tt,V_2,V_3) -> U22(isList(V_2),V_3),
    U42(tt,V_3) -> U43(isNeList(V_3)),
    U41(tt,V_2,V_3) -> U42(isList(V_2),V_3) } (13 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has one strongly connected component:
    0: 'U41`(tt,V_2,V_3) ; 'isList`(V_2)
    1: 'U41`(tt,V_2,V_3) ; 'U42`(isList(V_2),V_3)
    2: 'U42`(tt,V_3) ; 'isNeList`(V_3) 3: 'U21`(tt,V_2,V_3) ; 'isList`(V_2)
    4: 'U21`(tt,V_2,V_3) ; 'U22`(isList(V_2),V_3)
    5: 'U22`(tt,V_3) ; 'isList`(V_3)
    6: 'isList`(V_4) ; 'U11`(isPalListKind(V_4),V_4)
    7: 'isList`(__(V_2,V_3)) ; 'U21`(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3)
    8: 'U11`(tt,V_4) ; 'isNeList`(V_4)
    9: 'isNeList`(__(V_2,V_3)) ; 'U41`(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3)
    10: 'isNeList`(__(V_2,V_3)) ; 'U51`(and(isPalListKind(V_2),isPalListKind(V_3)),V_2,V_3)
    11: 'U51`(tt,V_2,V_3) ; 'isNeList`(V_2)
    12: 'U51`(tt,V_2,V_3) ; 'U52`(isNeList(V_2),V_3)
    13: 'U52`(tt,V_3) ; 'isList`(V_3) 
    0 -> 6, 0 -> 7, 1 -> 2, 2 -> 9, 2 -> 10, 3 -> 6, 3 -> 7, 4 -> 5, 5 -> 6,
    5 -> 7, 6 -> 8, 7 -> 3, 7 -> 4, 8 -> 9, 8 -> 10, 9 -> 0, 9 -> 1,
    10 -> 11, 10 -> 12, 11 -> 9, 11 -> 10, 12 -> 13, 13 -> 6, 13 -> 7, 
    On this component, the interpretation
    [tt] = 2; 
    [U53](X0) = X0; 
    [nil] = 2; 
    [__](X0,X1) = X1 + X0 + 2; 
    [a] = 2; 
    [e] = 2; 
    [i] = 2; 
    [o] = 2; 
    [u] = 2; 
    [isQid](X0) = X0; 
    [U32](X0) = X0; 
    [U31](X0,X1) = X1; 
    [and](X0,X1) = X1; 
    [isPalListKind](X0) = 2; 
    [U12](X0) = X0; 
    [U23](X0) = X0; 
    [U43](X0) = X0; 
    [U41](X0,X1,X2) = X2; 
    [U42](X0,X1) = X1; 
    [U21](X0,X1,X2) = X2; 
    [U22](X0,X1) = X1; 
    [isList](X0) = X0; 
    [U11](X0,X1) = X1; 
    [isNeList](X0) = X0; 
    [U51](X0,X1,X2) = X2; 
    [U52](X0,X1) = X1; 
    ['U41`](X0,X1,X2) = 2*X2 + 2*X1 + X0 + 1; 
    ['U42`](X0,X1) = 2*X1 + 1; 
    ['U21`](X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; 
    ['U22`](X0,X1) = 2*X1 + 2*X0; 
    ['isList`](X0) = 2*X0 + 2; 
    ['U11`](X0,X1) = 2*X1 + 1; 
    ['isNeList`](X0) = 2*X0; 
    ['U51`](X0,X1,X2) = 2*X2 + 2*X1 + 1; 
    ['U52`](X0,X1) = 2*X1 + 2*X0; 
     strictly decreases on every cycle

- : unit = ()

Quitting.
Standard error: