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, and(tt,X) -> X, isList(V) -> isNeList(V), isList(nil) -> tt, isList(__(V1,V2)) -> and(isList(V1),isList(V2)), isNeList(V) -> isQid(V), isNeList(__(V1,V2)) -> and(isList(V1),isNeList(V2)), isNeList(__(V1,V2)) -> and(isNeList(V1),isList(V2)), isNePal(V) -> isQid(V), isNePal(__(I,__(P,I))) -> and(isQid(I),isPal(P)), isPal(V) -> isNePal(V), isPal(nil) -> tt, isQid(a) -> tt, isQid(e) -> tt, isQid(i) -> tt, isQid(o) -> tt, isQid(u) -> tt } (19 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: { 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: { __(nil,V_5) -> V_5, __(V_5,nil) -> V_5, __(__(V_5,V_7),V_6) -> __(V_5,__(V_7,V_6)) } (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: { isPal(V_4) -> isNePal(V_4), isPal(nil) -> tt, isNePal(__(V_0,__(V_1,V_0))) -> and(isQid(V_0),isPal(V_1)), isNePal(V_4) -> isQid(V_4) } (4 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: (15 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [nil] = 0; [__](X0,X1) = X1 + X0 + 1; [tt] = 0; [and](X0,X1) = X1; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [isNePal](X0) = 0; [isPal](X0) = 0; ['isNePal`](X0) = X0; ['isPal`](X0) = X0 + 1; Checking module: { isNeList(V_4) -> isQid(V_4), isNeList(__(V_2,V_3)) -> and(isList(V_2),isNeList(V_3)), isNeList(__(V_2,V_3)) -> and(isNeList(V_2),isList(V_3)), isList(__(V_2,V_3)) -> and(isList(V_2),isList(V_3)), isList(nil) -> tt, isList(V_4) -> isNeList(V_4) } (6 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: (22 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [nil] = 0; [__](X0,X1) = X1 + X0 + 1; [tt] = 0; [and](X0,X1) = X1; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [isList](X0) = 0; [isNeList](X0) = 0; ['isList`](X0) = 2*X0 + 1; ['isNeList`](X0) = 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 { 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 { 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 { __(nil,V_5) -> V_5, __(V_5,nil) -> V_5, __(__(V_5,V_7),V_6) -> __(V_5,__(V_7,V_6)) } (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 { isPal(V_4) -> isNePal(V_4), isPal(nil) -> tt, isNePal(__(V_0,__(V_1,V_0))) -> and(isQid(V_0),isPal(V_1)), isNePal(V_4) -> isQid(V_4) } (4 rules) is CE-terminating by criterion with marks except on AC-symbols, and with graph; the dependency graph has one strongly connected component: 0: 'isNePal`(__(V_0,__(V_1,V_0))) ; 'isPal`(V_1) 1: 'isPal`(V_4) ; 'isNePal`(V_4) 0 -> 1, 1 -> 0, On this component, the interpretation [nil] = 0; [__](X0,X1) = X1 + X0 + 1; [tt] = 0; [and](X0,X1) = X1; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [isNePal](X0) = 0; [isPal](X0) = 0; ['isNePal`](X0) = X0; ['isPal`](X0) = X0 + 1; strictly decreases on every cycle The module { isNeList(V_4) -> isQid(V_4), isNeList(__(V_2,V_3)) -> and(isList(V_2),isNeList(V_3)), isNeList(__(V_2,V_3)) -> and(isNeList(V_2),isList(V_3)), isList(__(V_2,V_3)) -> and(isList(V_2),isList(V_3)), isList(nil) -> tt, isList(V_4) -> isNeList(V_4) } (6 rules) is CE-terminating by criterion with marks except on AC-symbols, and with graph; the dependency graph has one strongly connected component: 0: 'isList`(V_4) ; 'isNeList`(V_4) 1: 'isList`(__(V_2,V_3)) ; 'isList`(V_3) 2: 'isList`(__(V_2,V_3)) ; 'isList`(V_2) 3: 'isNeList`(__(V_2,V_3)) ; 'isList`(V_3) 4: 'isNeList`(__(V_2,V_3)) ; 'isNeList`(V_2) 5: 'isNeList`(__(V_2,V_3)) ; 'isNeList`(V_3) 6: 'isNeList`(__(V_2,V_3)) ; 'isList`(V_2) 0 -> 3, 0 -> 4, 0 -> 5, 0 -> 6, 1 -> 0, 1 -> 1, 1 -> 2, 2 -> 0, 2 -> 1, 2 -> 2, 3 -> 0, 3 -> 1, 3 -> 2, 4 -> 3, 4 -> 4, 4 -> 5, 4 -> 6, 5 -> 3, 5 -> 4, 5 -> 5, 5 -> 6, 6 -> 0, 6 -> 1, 6 -> 2, On this component, the interpretation [nil] = 0; [__](X0,X1) = X1 + X0 + 1; [tt] = 0; [and](X0,X1) = X1; [a] = 0; [e] = 0; [i] = 0; [o] = 0; [u] = 0; [isQid](X0) = 0; [isList](X0) = 0; [isNeList](X0) = 0; ['isList`](X0) = 2*X0 + 1; ['isNeList`](X0) = 2*X0; strictly decreases on every cycle - : unit = () Quitting. Standard error: