YES Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { __(__(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 } (30 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: { 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: { U72(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U81(tt) -> tt } (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: { U61(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { __(nil,V_7) -> V_7, __(V_7,nil) -> V_7, __(__(V_7,V_6),V_5) -> __(V_7,__(V_6,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: { isNePal(V_4) -> U61(isQid(V_4)), isNePal(__(V_0,__(V_1,V_0))) -> U71(isQid(V_0),V_1), isPal(nil) -> tt, isPal(V_4) -> U81(isNePal(V_4)), U71(tt,V_1) -> U72(isPal(V_1)) } (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: (19 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; [isQid](X0) = 0; [U61](X0) = 0; [U81](X0) = 0; [U72](X0) = 0; [U71](X0,X1) = 0; [isPal](X0) = 0; [isNePal](X0) = 0; ['U71`](X0,X1) = 2*X1 + 2; ['isPal`](X0) = 2*X0 + 1; ['isNePal`](X0) = 2*X0; Checking module: { U52(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U42(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U31(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U22(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U11(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U51(tt,V_3) -> U52(isList(V_3)), isNeList(__(V_2,V_3)) -> U51(isNeList(V_2),V_3), isNeList(__(V_2,V_3)) -> U41(isList(V_2),V_3), isNeList(V_4) -> U31(isQid(V_4)), isList(V_4) -> U11(isNeList(V_4)), isList(nil) -> tt, isList(__(V_2,V_3)) -> U21(isList(V_2),V_3), U21(tt,V_3) -> U22(isList(V_3)), U41(tt,V_3) -> U42(isNeList(V_3)) } (9 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: (32 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [tt] = 0; [U52](X0) = 0; [nil] = 0; [__](X0,X1) = X1 + X0 + 2; [U31](X0) = 0; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [U11](X0) = 0; [U22](X0) = 0; [U42](X0) = 0; [U41](X0,X1) = 0; [U21](X0,X1) = 0; [isList](X0) = 0; [isNeList](X0) = 0; [U51](X0,X1) = 0; ['U41`](X0,X1) = 2*X1 + 1; ['U21`](X0,X1) = 2*X1 + 2; ['isList`](X0) = 2*X0 + 1; ['isNeList`](X0) = 2*X0; ['U51`](X0,X1) = 2*X1 + 2; 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 { 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 { 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 { U81(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 {} 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) -> 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 { __(nil,V_7) -> V_7, __(V_7,nil) -> V_7, __(__(V_7,V_6),V_5) -> __(V_7,__(V_6,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_7,V_6),V_5) ; '__`(V_6,V_5) 1: '__`(__(V_7,V_6),V_5) ; '__`(V_7,__(V_6,V_5)) 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 { isNePal(V_4) -> U61(isQid(V_4)), isNePal(__(V_0,__(V_1,V_0))) -> U71(isQid(V_0),V_1), isPal(nil) -> tt, isPal(V_4) -> U81(isNePal(V_4)), U71(tt,V_1) -> U72(isPal(V_1)) } (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_1) ; 'isPal`(V_1) 1: 'isPal`(V_4) ; 'isNePal`(V_4) 2: 'isNePal`(__(V_0,__(V_1,V_0))) ; 'U71`(isQid(V_0),V_1) 0 -> 1, 1 -> 2, 2 -> 0, On this component, the interpretation [tt] = 0; [nil] = 0; [__](X0,X1) = X1 + X0 + 1; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [U61](X0) = 0; [U81](X0) = 0; [U72](X0) = 0; [U71](X0,X1) = 0; [isPal](X0) = 0; [isNePal](X0) = 0; ['U71`](X0,X1) = 2*X1 + 2; ['isPal`](X0) = 2*X0 + 1; ['isNePal`](X0) = 2*X0; strictly decreases on every cycle The module { U52(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 { U42(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) -> 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 { U22(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 { U11(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 { U51(tt,V_3) -> U52(isList(V_3)), isNeList(__(V_2,V_3)) -> U51(isNeList(V_2),V_3), isNeList(__(V_2,V_3)) -> U41(isList(V_2),V_3), isNeList(V_4) -> U31(isQid(V_4)), isList(V_4) -> U11(isNeList(V_4)), isList(nil) -> tt, isList(__(V_2,V_3)) -> U21(isList(V_2),V_3), U21(tt,V_3) -> U22(isList(V_3)), U41(tt,V_3) -> U42(isNeList(V_3)) } (9 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_3) ; 'isNeList`(V_3) 1: 'U21`(tt,V_3) ; 'isList`(V_3) 2: 'isList`(__(V_2,V_3)) ; 'isList`(V_2) 3: 'isList`(__(V_2,V_3)) ; 'U21`(isList(V_2),V_3) 4: 'isList`(V_4) ; 'isNeList`(V_4) 5: 'isNeList`(__(V_2,V_3)) ; 'isList`(V_2) 6: 'isNeList`(__(V_2,V_3)) ; 'U41`(isList(V_2),V_3) 7: 'isNeList`(__(V_2,V_3)) ; 'isNeList`(V_2) 8: 'isNeList`(__(V_2,V_3)) ; 'U51`(isNeList(V_2),V_3) 9: 'U51`(tt,V_3) ; 'isList`(V_3) 0 -> 5, 0 -> 6, 0 -> 7, 0 -> 8, 1 -> 2, 1 -> 3, 1 -> 4, 2 -> 2, 2 -> 3, 2 -> 4, 3 -> 1, 4 -> 5, 4 -> 6, 4 -> 7, 4 -> 8, 5 -> 2, 5 -> 3, 5 -> 4, 6 -> 0, 7 -> 5, 7 -> 6, 7 -> 7, 7 -> 8, 8 -> 9, 9 -> 2, 9 -> 3, 9 -> 4, On this component, the interpretation [tt] = 0; [U52](X0) = 0; [nil] = 0; [__](X0,X1) = X1 + X0 + 2; [U31](X0) = 0; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [U11](X0) = 0; [U22](X0) = 0; [U42](X0) = 0; [U41](X0,X1) = 0; [U21](X0,X1) = 0; [isList](X0) = 0; [isNeList](X0) = 0; [U51](X0,X1) = 0; ['U41`](X0,X1) = 2*X1 + 1; ['U21`](X0,X1) = 2*X1 + 2; ['isList`](X0) = 2*X0 + 1; ['isNeList`](X0) = 2*X0; ['U51`](X0,X1) = 2*X1 + 2; strictly decreases on every cycle - : unit = () Quitting. Standard error: