YES Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { U11(tt,V1,V2) -> U12(isNat(V1),V2), U12(tt,V2) -> U13(isNat(V2)), U13(tt) -> tt, U21(tt,V1) -> U22(isNat(V1)), U22(tt) -> tt, U31(tt,N) -> N, U41(tt,M,N) -> s(plus(N,M)), and(tt,X) -> X, isNat(0) -> tt, isNat(plus(V1,V2)) -> U11(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNat(s(V1)) -> U21(isNatKind(V1),V1), isNatKind(0) -> tt, isNatKind(plus(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNatKind(s(V1)) -> isNatKind(V1), plus(N,0) -> U31(and(isNat(N),isNatKind(N)),N), plus(N,s(M)) -> U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) } (16 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: { and(tt,V_4) -> V_4 } (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: { U31(tt,V_1) -> V_1 } (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: { U13(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { isNatKind(s(V_2)) -> isNatKind(V_2), isNatKind(plus(V_2,V_3)) -> and(isNatKind(V_2),isNatKind(V_3)), isNatKind(0) -> tt, plus(V_1,0) -> U31(and(isNat(V_1),isNatKind(V_1)),V_1), plus(V_1,s(V_0)) -> U41(and(and(isNat(V_0),isNatKind(V_0)),and(isNat(V_1),isNatKind(V_1))),V_0,V_1), isNat(s(V_2)) -> U21(isNatKind(V_2),V_2), isNat(plus(V_2,V_3)) -> U11(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3), isNat(0) -> tt, U12(tt,V_3) -> U13(isNat(V_3)), U11(tt,V_2,V_3) -> U12(isNat(V_2),V_3), U21(tt,V_2) -> U22(isNat(V_2)), U41(tt,V_0,V_1) -> s(plus(V_1,V_0)) } (12 rules) The dependency graph is (1 nodes) Checking each of the 3 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (18 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [tt] = 0; [s](X0) = X0 + 1; [and](X0,X1) = X1; [0] = 0; [U31](X0,X1) = X1; [U13](X0) = 0; [U22](X0) = 0; [U41](X0,X1,X2) = X2 + X1 + 1; [U21](X0,X1) = 0; [U11](X0,X1,X2) = 0; [U12](X0,X1) = 0; [isNat](X0) = 0; [plus](X0,X1) = X1 + X0; [isNatKind](X0) = 0; ['U41`](X0,X1,X2) = 2*X1 + 1; ['plus`](X0,X1) = 2*X1; Checking component 2 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: [tt] = 2; [s](X0) = X0 + 2; [and](X0,X1) = X1; [0] = 2; [U31](X0,X1) = X1; [U13](X0) = X0; [U22](X0) = 2; [U41](X0,X1,X2) = X2 + 2*X1 + 2; [U21](X0,X1) = 2; [U11](X0,X1,X2) = X2; [U12](X0,X1) = X1; [isNat](X0) = X0; [plus](X0,X1) = 2*X1 + X0; [isNatKind](X0) = X0; ['U21`](X0,X1) = 2*X1 + 2; ['U11`](X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; ['U12`](X0,X1) = 2*X1 + 2; ['isNat`](X0) = 2*X0 + 1; Checking component 3 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; [s](X0) = X0 + 1; [and](X0,X1) = X1; [0] = 0; [U31](X0,X1) = X1; [U13](X0) = 0; [U22](X0) = 0; [U41](X0,X1,X2) = X2 + X1 + 2; [U21](X0,X1) = 0; [U11](X0,X1,X2) = 0; [U12](X0,X1) = 0; [isNat](X0) = 0; [plus](X0,X1) = X1 + X0 + 1; [isNatKind](X0) = 0; ['isNatKind`](X0) = 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 { and(tt,V_4) -> 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 {} 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_1) -> V_1 } (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 { U13(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 { isNatKind(s(V_2)) -> isNatKind(V_2), isNatKind(plus(V_2,V_3)) -> and(isNatKind(V_2),isNatKind(V_3)), isNatKind(0) -> tt, plus(V_1,0) -> U31(and(isNat(V_1),isNatKind(V_1)),V_1), plus(V_1,s(V_0)) -> U41(and(and(isNat(V_0),isNatKind(V_0)),and(isNat(V_1),isNatKind(V_1))),V_0,V_1), isNat(s(V_2)) -> U21(isNatKind(V_2),V_2), isNat(plus(V_2,V_3)) -> U11(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3), isNat(0) -> tt, U12(tt,V_3) -> U13(isNat(V_3)), U11(tt,V_2,V_3) -> U12(isNat(V_2),V_3), U21(tt,V_2) -> U22(isNat(V_2)), U41(tt,V_0,V_1) -> s(plus(V_1,V_0)) } (12 rules) is CE-terminating by criterion with marks except on AC-symbols, and with graph; the dependency graph has 3 strongly connected components: component 1 is 17: 'isNatKind`(plus(V_2,V_3)) ; 'isNatKind`(V_3) 18: 'isNatKind`(plus(V_2,V_3)) ; 'isNatKind`(V_2) 19: 'isNatKind`(s(V_2)) ; 'isNatKind`(V_2) 17 -> 17, 17 -> 18, 17 -> 19, 18 -> 17, 18 -> 18, 18 -> 19, 19 -> 17, 19 -> 18, 19 -> 19, On this component, the interpretation [tt] = 0; [s](X0) = X0 + 1; [and](X0,X1) = X1; [0] = 0; [U31](X0,X1) = X1; [U13](X0) = 0; [U22](X0) = 0; [U41](X0,X1,X2) = X2 + X1 + 2; [U21](X0,X1) = 0; [U11](X0,X1,X2) = 0; [U12](X0,X1) = 0; [isNat](X0) = 0; [plus](X0,X1) = X1 + X0 + 1; [isNatKind](X0) = 0; ['isNatKind`](X0) = X0; strictly decreases on every cycle component 2 is 1: 'U21`(tt,V_2) ; 'isNat`(V_2) 2: 'U11`(tt,V_2,V_3) ; 'isNat`(V_2) 3: 'U11`(tt,V_2,V_3) ; 'U12`(isNat(V_2),V_3) 4: 'U12`(tt,V_3) ; 'isNat`(V_3) 7: 'isNat`(plus(V_2,V_3)) ; 'U11`(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3) 9: 'isNat`(s(V_2)) ; 'U21`(isNatKind(V_2),V_2) 1 -> 7, 1 -> 9, 2 -> 7, 2 -> 9, 3 -> 4, 4 -> 7, 4 -> 9, 7 -> 2, 7 -> 3, 9 -> 1, On this component, the interpretation [tt] = 2; [s](X0) = X0 + 2; [and](X0,X1) = X1; [0] = 2; [U31](X0,X1) = X1; [U13](X0) = X0; [U22](X0) = 2; [U41](X0,X1,X2) = X2 + 2*X1 + 2; [U21](X0,X1) = 2; [U11](X0,X1,X2) = X2; [U12](X0,X1) = X1; [isNat](X0) = X0; [plus](X0,X1) = 2*X1 + X0; [isNatKind](X0) = X0; ['U21`](X0,X1) = 2*X1 + 2; ['U11`](X0,X1,X2) = 2*X2 + 2*X1 + 2*X0; ['U12`](X0,X1) = 2*X1 + 2; ['isNat`](X0) = 2*X0 + 1; strictly decreases on every cycle component 3 is 0: 'U41`(tt,V_0,V_1) ; 'plus`(V_1,V_0) 14: 'plus`(V_1,s(V_0)) ; 'U41`(and(and(isNat(V_0),isNatKind(V_0)), and(isNat(V_1),isNatKind(V_1))),V_0,V_1) 0 -> 14, 14 -> 0, On this component, the interpretation [tt] = 0; [s](X0) = X0 + 1; [and](X0,X1) = X1; [0] = 0; [U31](X0,X1) = X1; [U13](X0) = 0; [U22](X0) = 0; [U41](X0,X1,X2) = X2 + X1 + 1; [U21](X0,X1) = 0; [U11](X0,X1,X2) = 0; [U12](X0,X1) = 0; [isNat](X0) = 0; [plus](X0,X1) = X1 + X0; [isNatKind](X0) = 0; ['U41`](X0,X1,X2) = 2*X1 + 1; ['plus`](X0,X1) = 2*X1; strictly decreases on every cycle - : unit = () Quitting. Standard error: