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 = { U11(tt,V1,V2) -> U12(isNatKind(V1),V1,V2),
             U12(tt,V1,V2) -> U13(isNatKind(V2),V1,V2),
             U13(tt,V1,V2) -> U14(isNatKind(V2),V1,V2),
             U14(tt,V1,V2) -> U15(isNat(V1),V2),
             U15(tt,V2) -> U16(isNat(V2)),
             U16(tt) -> tt,
             U21(tt,V1) -> U22(isNatKind(V1),V1),
             U22(tt,V1) -> U23(isNat(V1)),
             U23(tt) -> tt,
             U31(tt,V2) -> U32(isNatKind(V2)),
             U32(tt) -> tt,
             U41(tt) -> tt,
             U51(tt,N) -> U52(isNatKind(N),N),
             U52(tt,N) -> N,
             U61(tt,M,N) -> U62(isNatKind(M),M,N),
             U62(tt,M,N) -> U63(isNat(N),M,N),
             U63(tt,M,N) -> U64(isNatKind(N),M,N),
             U64(tt,M,N) -> s(plus(N,M)),
             isNat(0) -> tt,
             isNat(plus(V1,V2)) -> U11(isNatKind(V1),V1,V2),
             isNat(s(V1)) -> U21(isNatKind(V1),V1),
             isNatKind(0) -> tt,
             isNatKind(plus(V1,V2)) -> U31(isNatKind(V1),V2),
             isNatKind(s(V1)) -> U41(isNatKind(V1)),
             plus(N,0) -> U51(isNat(N),N),
             plus(N,s(M)) -> U61(isNat(M),M,N) } (26 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:
{ U41(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:
{ U23(tt) -> tt } (1 rules)

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

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

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

Checking module:
{ U52(tt,V_1) -> V_1 } (1 rules)

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

Checking module:
{ plus(V_1,0) -> U51(isNat(V_1),V_1),
  plus(V_1,s(V_0)) -> U61(isNat(V_0),V_0,V_1),
  isNatKind(s(V_2)) -> U41(isNatKind(V_2)),
  isNatKind(plus(V_2,V_3)) -> U31(isNatKind(V_2),V_3),
  isNatKind(0) -> tt,
  U31(tt,V_3) -> U32(isNatKind(V_3)),
  U51(tt,V_1) -> U52(isNatKind(V_1),V_1),
  isNat(0) -> tt,
  isNat(plus(V_2,V_3)) -> U11(isNatKind(V_2),V_2,V_3),
  isNat(s(V_2)) -> U21(isNatKind(V_2),V_2),
  U15(tt,V_3) -> U16(isNat(V_3)),
  U14(tt,V_2,V_3) -> U15(isNat(V_2),V_3),
  U13(tt,V_2,V_3) -> U14(isNatKind(V_3),V_2,V_3),
  U12(tt,V_2,V_3) -> U13(isNatKind(V_3),V_2,V_3),
  U11(tt,V_2,V_3) -> U12(isNatKind(V_2),V_2,V_3),
  U22(tt,V_2) -> U23(isNat(V_2)),
  U21(tt,V_2) -> U22(isNatKind(V_2),V_2),
  U64(tt,V_0,V_1) -> s(plus(V_1,V_0)),
  U63(tt,V_0,V_1) -> U64(isNatKind(V_1),V_0,V_1),
  U62(tt,V_0,V_1) -> U63(isNat(V_1),V_0,V_1),
  U61(tt,V_0,V_1) -> U62(isNatKind(V_0),V_0,V_1) } (21 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:
(31 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[s](X0) = 2*X0; 
[0] = 3; 
[tt] = 3; 
[U41](X0) = X0; 
[U32](X0) = X0; 
[U52](X0,X1) = X1; 
[U16](X0) = X0; 
[U23](X0) = X0; 
[U61](X0,X1,X2) = 2*X2*X1; 
[U62](X0,X1,X2) = 2*X2*X1; 
[U63](X0,X1,X2) = 2*X2*X1; 
[U64](X0,X1,X2) = 2*X2*X1; 
[U21](X0,X1) = X1; 
[U22](X0,X1) = X1; 
[U11](X0,X1,X2) = X2*X1; 
[U12](X0,X1,X2) = X2*X1; 
[U13](X0,X1,X2) = X2*X1; 
[U14](X0,X1,X2) = X2*X1; 
[U15](X0,X1) = X1*X0; 
[isNat](X0) = X0; 
[U51](X0,X1) = X1; 
[U31](X0,X1) = X1*X0; 
[isNatKind](X0) = X0; 
[plus](X0,X1) = X1*X0; 
['U61`](X0,X1,X2) = X2*X1 + X2*X0 + X1 + X0; 
['U62`](X0,X1,X2) = X2*X1 + X2 + X1 + 2; 
['U63`](X0,X1,X2) = X2*X1 + X2 + X1 + 1; 
['U64`](X0,X1,X2) = X2*X1 + X1 + X0; 
['plus`](X0,X1) = X1*X0 + X1 + 1; 

Checking component 2
Trying simple graph criterion.
Trying to solve the following constraints:
(36 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[s](X0) = X0 + 3; 
[0] = 3; 
[tt] = 3; 
[U41](X0) = 3; 
[U32](X0) = 3; 
[U52](X0,X1) = X1; 
[U16](X0) = 3; 
[U23](X0) = 3; 
[U61](X0,X1,X2) = X2*X1 + 3*X2; 
[U62](X0,X1,X2) = X2*X1 + 3*X2; 
[U63](X0,X1,X2) = X2*X1 + 3*X2; 
[U64](X0,X1,X2) = X2*X1 + X2 + 2*X0; 
[U21](X0,X1) = 3; 
[U22](X0,X1) = 3; 
[U11](X0,X1,X2) = 3; 
[U12](X0,X1,X2) = 3; 
[U13](X0,X1,X2) = 3; 
[U14](X0,X1,X2) = 3; 
[U15](X0,X1) = 3; 
[isNat](X0) = 3; 
[U51](X0,X1) = X1; 
[U31](X0,X1) = 3; 
[isNatKind](X0) = X0; 
[plus](X0,X1) = X1*X0 + X0 + 3; 
['U21`](X0,X1) = 2*X1 + 2; 
['U22`](X0,X1) = 2*X1 + 1; 
['U11`](X0,X1,X2) = X2*X0 + 2*X1 + 3; 
['U12`](X0,X1,X2) = 3*X2 + 2*X1 + 2; 
['U13`](X0,X1,X2) = 3*X2 + 2*X1 + 1; 
['U14`](X0,X1,X2) = 2*X2 + 2*X1 + X0; 
['U15`](X0,X1) = 2*X1 + 1; 
['isNat`](X0) = 2*X0; 

Checking component 3
Trying simple graph criterion.
Trying to solve the following constraints:
(30 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Solution found for these constraints:
[s](X0) = X0 + 1; 
[0] = 0; 
[tt] = 0; 
[U41](X0) = 0; 
[U32](X0) = 0; 
[U52](X0,X1) = X1; 
[U16](X0) = 0; 
[U23](X0) = 0; 
[U61](X0,X1,X2) = X2 + X1 + 2; 
[U62](X0,X1,X2) = X2 + X1 + 2; 
[U63](X0,X1,X2) = X2 + X1 + 2; 
[U64](X0,X1,X2) = X2 + X1 + 2; 
[U21](X0,X1) = 0; 
[U22](X0,X1) = 0; 
[U11](X0,X1,X2) = 0; 
[U12](X0,X1,X2) = 0; 
[U13](X0,X1,X2) = 0; 
[U14](X0,X1,X2) = 0; 
[U15](X0,X1) = 0; 
[isNat](X0) = 0; 
[U51](X0,X1) = X1; 
[U31](X0,X1) = 0; 
[isNatKind](X0) = 0; 
[plus](X0,X1) = X1 + X0 + 1; 
['U31`](X0,X1) = 2*X1 + 1; 
['isNatKind`](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
  { U41(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
  { 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
  { U16(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
  { U52(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
  { plus(V_1,0) -> U51(isNat(V_1),V_1),
    plus(V_1,s(V_0)) -> U61(isNat(V_0),V_0,V_1),
    isNatKind(s(V_2)) -> U41(isNatKind(V_2)),
    isNatKind(plus(V_2,V_3)) -> U31(isNatKind(V_2),V_3),
    isNatKind(0) -> tt,
    U31(tt,V_3) -> U32(isNatKind(V_3)),
    U51(tt,V_1) -> U52(isNatKind(V_1),V_1),
    isNat(0) -> tt,
    isNat(plus(V_2,V_3)) -> U11(isNatKind(V_2),V_2,V_3),
    isNat(s(V_2)) -> U21(isNatKind(V_2),V_2),
    U15(tt,V_3) -> U16(isNat(V_3)),
    U14(tt,V_2,V_3) -> U15(isNat(V_2),V_3),
    U13(tt,V_2,V_3) -> U14(isNatKind(V_3),V_2,V_3),
    U12(tt,V_2,V_3) -> U13(isNatKind(V_3),V_2,V_3),
    U11(tt,V_2,V_3) -> U12(isNatKind(V_2),V_2,V_3),
    U22(tt,V_2) -> U23(isNat(V_2)),
    U21(tt,V_2) -> U22(isNatKind(V_2),V_2),
    U64(tt,V_0,V_1) -> s(plus(V_1,V_0)),
    U63(tt,V_0,V_1) -> U64(isNatKind(V_1),V_0,V_1),
    U62(tt,V_0,V_1) -> U63(isNat(V_1),V_0,V_1),
    U61(tt,V_0,V_1) -> U62(isNatKind(V_0),V_0,V_1) } (21 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
      24: 'U31`(tt,V_3) ; 'isNatKind`(V_3)
      25: 'isNatKind`(plus(V_2,V_3)) ; 'isNatKind`(V_2)
      26: 'isNatKind`(plus(V_2,V_3)) ; 'U31`(isNatKind(V_2),V_3)
      27: 'isNatKind`(s(V_2)) ; 'isNatKind`(V_2) 
      24 -> 25, 24 -> 26, 24 -> 27, 25 -> 25, 25 -> 26, 25 -> 27, 26 -> 24,
      27 -> 25, 27 -> 26, 27 -> 27, 
      On this component, the interpretation
      [s](X0) = X0 + 1; 
      [0] = 0; 
      [tt] = 0; 
      [U41](X0) = 0; 
      [U32](X0) = 0; 
      [U52](X0,X1) = X1; 
      [U16](X0) = 0; 
      [U23](X0) = 0; 
      [U61](X0,X1,X2) = X2 + X1 + 2; 
      [U62](X0,X1,X2) = X2 + X1 + 2; 
      [U63](X0,X1,X2) = X2 + X1 + 2; 
      [U64](X0,X1,X2) = X2 + X1 + 2; 
      [U21](X0,X1) = 0; 
      [U22](X0,X1) = 0; 
      [U11](X0,X1,X2) = 0; 
      [U12](X0,X1,X2) = 0; 
      [U13](X0,X1,X2) = 0; 
      [U14](X0,X1,X2) = 0; 
      [U15](X0,X1) = 0; 
      [isNat](X0) = 0; 
      [U51](X0,X1) = X1; 
      [U31](X0,X1) = 0; 
      [isNatKind](X0) = 0; 
      [plus](X0,X1) = X1 + X0 + 1; 
      ['U31`](X0,X1) = 2*X1 + 1; 
      ['isNatKind`](X0) = 2*X0; 
       strictly decreases on every cycle
    component 2 is
      8: 'U21`(tt,V_2) ; 'U22`(isNatKind(V_2),V_2)
      9: 'U22`(tt,V_2) ; 'isNat`(V_2)
      11: 'U11`(tt,V_2,V_3) ; 'U12`(isNatKind(V_2),V_2,V_3)
      13: 'U12`(tt,V_2,V_3) ; 'U13`(isNatKind(V_3),V_2,V_3)
      15: 'U13`(tt,V_2,V_3) ; 'U14`(isNatKind(V_3),V_2,V_3)
      16: 'U14`(tt,V_2,V_3) ; 'isNat`(V_2)
      17: 'U14`(tt,V_2,V_3) ; 'U15`(isNat(V_2),V_3)
      18: 'U15`(tt,V_3) ; 'isNat`(V_3)
      20: 'isNat`(s(V_2)) ; 'U21`(isNatKind(V_2),V_2)
      22: 'isNat`(plus(V_2,V_3)) ; 'U11`(isNatKind(V_2),V_2,V_3) 
      8 -> 9, 9 -> 20, 9 -> 22, 11 -> 13, 13 -> 15, 15 -> 16, 15 -> 17,
      16 -> 20, 16 -> 22, 17 -> 18, 18 -> 20, 18 -> 22, 20 -> 8, 22 -> 11, 
      On this component, the interpretation
      [s](X0) = X0 + 3; 
      [0] = 3; 
      [tt] = 3; 
      [U41](X0) = 3; 
      [U32](X0) = 3; 
      [U52](X0,X1) = X1; 
      [U16](X0) = 3; 
      [U23](X0) = 3; 
      [U61](X0,X1,X2) = X2*X1 + 3*X2; 
      [U62](X0,X1,X2) = X2*X1 + 3*X2; 
      [U63](X0,X1,X2) = X2*X1 + 3*X2; 
      [U64](X0,X1,X2) = X2*X1 + X2 + 2*X0; 
      [U21](X0,X1) = 3; 
      [U22](X0,X1) = 3; 
      [U11](X0,X1,X2) = 3; 
      [U12](X0,X1,X2) = 3; 
      [U13](X0,X1,X2) = 3; 
      [U14](X0,X1,X2) = 3; 
      [U15](X0,X1) = 3; 
      [isNat](X0) = 3; 
      [U51](X0,X1) = X1; 
      [U31](X0,X1) = 3; 
      [isNatKind](X0) = X0; 
      [plus](X0,X1) = X1*X0 + X0 + 3; 
      ['U21`](X0,X1) = 2*X1 + 2; 
      ['U22`](X0,X1) = 2*X1 + 1; 
      ['U11`](X0,X1,X2) = X2*X0 + 2*X1 + 3; 
      ['U12`](X0,X1,X2) = 3*X2 + 2*X1 + 2; 
      ['U13`](X0,X1,X2) = 3*X2 + 2*X1 + 1; 
      ['U14`](X0,X1,X2) = 2*X2 + 2*X1 + X0; 
      ['U15`](X0,X1) = 2*X1 + 1; 
      ['isNat`](X0) = 2*X0; 
       strictly decreases on every cycle
    component 3 is
      1: 'U61`(tt,V_0,V_1) ; 'U62`(isNatKind(V_0),V_0,V_1)
      3: 'U62`(tt,V_0,V_1) ; 'U63`(isNat(V_1),V_0,V_1)
      5: 'U63`(tt,V_0,V_1) ; 'U64`(isNatKind(V_1),V_0,V_1)
      6: 'U64`(tt,V_0,V_1) ; 'plus`(V_1,V_0)
      29: 'plus`(V_1,s(V_0)) ; 'U61`(isNat(V_0),V_0,V_1) 
      1 -> 3, 3 -> 5, 5 -> 6, 6 -> 29, 29 -> 1, 
      On this component, the interpretation
      [s](X0) = 2*X0; 
      [0] = 3; 
      [tt] = 3; 
      [U41](X0) = X0; 
      [U32](X0) = X0; 
      [U52](X0,X1) = X1; 
      [U16](X0) = X0; 
      [U23](X0) = X0; 
      [U61](X0,X1,X2) = 2*X2*X1; 
      [U62](X0,X1,X2) = 2*X2*X1; 
      [U63](X0,X1,X2) = 2*X2*X1; 
      [U64](X0,X1,X2) = 2*X2*X1; 
      [U21](X0,X1) = X1; 
      [U22](X0,X1) = X1; 
      [U11](X0,X1,X2) = X2*X1; 
      [U12](X0,X1,X2) = X2*X1; 
      [U13](X0,X1,X2) = X2*X1; 
      [U14](X0,X1,X2) = X2*X1; 
      [U15](X0,X1) = X1*X0; 
      [isNat](X0) = X0; 
      [U51](X0,X1) = X1; 
      [U31](X0,X1) = X1*X0; 
      [isNatKind](X0) = X0; 
      [plus](X0,X1) = X1*X0; 
      ['U61`](X0,X1,X2) = X2*X1 + X2*X0 + X1 + X0; 
      ['U62`](X0,X1,X2) = X2*X1 + X2 + X1 + 2; 
      ['U63`](X0,X1,X2) = X2*X1 + X2 + X1 + 1; 
      ['U64`](X0,X1,X2) = X2*X1 + X1 + X0; 
      ['plus`](X0,X1) = X1*X0 + X1 + 1; 
       strictly decreases on every cycle 

- : unit = ()

Quitting.
Standard error: