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(isNat(V1),V2),
             U12(tt,V2) -> U13(isNat(V2)),
             U13(tt) -> tt,
             U21(tt,V1) -> U22(isNat(V1)),
             U22(tt) -> tt,
             U31(tt,V1,V2) -> U32(isNat(V1),V2),
             U32(tt,V2) -> U33(isNat(V2)),
             U33(tt) -> tt,
             U41(tt,N) -> N,
             U51(tt,M,N) -> s(plus(N,M)),
             U61(tt) -> 0,
             U71(tt,M,N) -> plus(x(N,M),N),
             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),
             isNat(x(V1,V2)) -> U31(and(isNatKind(V1),isNatKind(V2)),V1,V2),
             isNatKind(0) -> tt,
             isNatKind(plus(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)),
             isNatKind(s(V1)) -> isNatKind(V1),
             isNatKind(x(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)),
             plus(N,0) -> U41(and(isNat(N),isNatKind(N)),N),
             plus(N,s(M)) ->
             U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N),
             x(N,0) -> U61(and(isNat(N),isNatKind(N))),
             x(N,s(M)) ->
             U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) }
             (25 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:
{ 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:
{}

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

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

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

Checking module:
{ U33(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:
{ U13(tt) -> tt } (1 rules)

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

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

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

Checking module:
{ isNatKind(x(V_2,V_3)) -> and(isNatKind(V_2),isNatKind(V_3)),
  isNatKind(s(V_2)) -> isNatKind(V_2),
  isNatKind(plus(V_2,V_3)) -> and(isNatKind(V_2),isNatKind(V_3)),
  isNatKind(0) -> tt,
  x(V_1,0) -> U61(and(isNat(V_1),isNatKind(V_1))),
  x(V_1,s(V_0)) ->
  U71(and(and(isNat(V_0),isNatKind(V_0)),and(isNat(V_1),isNatKind(V_1))),V_0,V_1),
  isNat(x(V_2,V_3)) -> U31(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3),
  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)),
  U32(tt,V_3) -> U33(isNat(V_3)),
  U31(tt,V_2,V_3) -> U32(isNat(V_2),V_3),
  plus(V_1,s(V_0)) ->
  U51(and(and(isNat(V_0),isNatKind(V_0)),and(isNat(V_1),isNatKind(V_1))),V_0,V_1),
  plus(V_1,0) -> U41(and(isNat(V_1),isNatKind(V_1)),V_1),
  U51(tt,V_0,V_1) -> s(plus(V_1,V_0)),
  U71(tt,V_0,V_1) -> plus(x(V_1,V_0),V_1) } (19 rules)

The dependency graph is
(1 nodes)
Checking each of the 4 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.
Time out for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(27 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:
[tt] = 1; 
[s](X0) = X0 + 1; 
[0] = 0; 
[and](X0,X1) = X1*X0; 
[U61](X0) = 0; 
[U13](X0) = 1; 
[U22](X0) = 1; 
[U33](X0) = 1; 
[U41](X0,X1) = X1; 
[U71](X0,X1,X2) = X2*X1 + X2; 
[U51](X0,X1,X2) = X2 + X1 + 1; 
[plus](X0,X1) = X1 + X0; 
[U31](X0,X1,X2) = 1; 
[U32](X0,X1) = 1; 
[U21](X0,X1) = 1; 
[U11](X0,X1,X2) = 1; 
[U12](X0,X1) = 1; 
[isNat](X0) = 1; 
[x](X0,X1) = X1*X0; 
[isNatKind](X0) = 1; 
['U71`](X0,X1,X2) = X1; 
['x`](X0,X1) = X1; 

The dependency graph is
(1 nodes)
Checking each of the 0 strongly connected components :
Checking component 2
Trying simple graph criterion.
Trying to solve the following constraints:
(27 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
Time out for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Time out for these parameters.
No solution found for these constraints.
Trying strongly connected part criterion.
Trying to solve the following constraints:
(27 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:
[tt] = 1; 
[s](X0) = X0 + 1; 
[0] = 0; 
[and](X0,X1) = X1*X0; 
[U61](X0) = 0; 
[U13](X0) = 1; 
[U22](X0) = 1; 
[U33](X0) = 1; 
[U41](X0,X1) = X1; 
[U71](X0,X1,X2) = X2*X1 + X2; 
[U51](X0,X1,X2) = X2 + X1 + 1; 
[plus](X0,X1) = X1 + X0; 
[U31](X0,X1,X2) = 1; 
[U32](X0,X1) = 1; 
[U21](X0,X1) = 1; 
[U11](X0,X1,X2) = 1; 
[U12](X0,X1) = 1; 
[isNat](X0) = 1; 
[x](X0,X1) = X1*X0; 
[isNatKind](X0) = 1; 
['U51`](X0,X1,X2) = X1; 
['plus`](X0,X1) = X1; 

The dependency graph is
(3 nodes)
Checking each of the 0 strongly connected components :
Checking component 3
Trying simple graph criterion.
Trying to solve the following constraints:
(35 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[tt] = 1; 
[s](X0) = X0 + 1; 
[0] = 0; 
[and](X0,X1) = X1*X0; 
[U61](X0) = 0; 
[U13](X0) = 1; 
[U22](X0) = 1; 
[U33](X0) = 1; 
[U41](X0,X1) = X1; 
[U71](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 2; 
[U51](X0,X1,X2) = X2 + X1 + 2; 
[plus](X0,X1) = X1 + X0 + 1; 
[U31](X0,X1,X2) = 1; 
[U32](X0,X1) = 1; 
[U21](X0,X1) = 1; 
[U11](X0,X1,X2) = 1; 
[U12](X0,X1) = 1; 
[isNat](X0) = 1; 
[x](X0,X1) = X1*X0 + X1 + X0 + 1; 
[isNatKind](X0) = 1; 
['U31`](X0,X1,X2) = 3*X2 + 3*X1 + 2; 
['U32`](X0,X1) = 3*X1 + 1; 
['U21`](X0,X1) = 3*X1 + 1; 
['U11`](X0,X1,X2) = 3*X2 + 3*X1 + 2; 
['U12`](X0,X1) = 3*X1 + 1; 
['isNat`](X0) = 3*X0; 

Checking component 4
Trying simple graph criterion.
Trying to solve the following constraints:
(30 termination constraints)
Search parameters: linear polynomials, coefficient bound is 2.
No solution found for these parameters.
Search parameters: simple polynomials, coefficient bound is 3.
Solution found for these constraints:
[tt] = 0; 
[s](X0) = X0 + 1; 
[0] = 0; 
[and](X0,X1) = X1; 
[U61](X0) = 0; 
[U13](X0) = 0; 
[U22](X0) = 0; 
[U33](X0) = 0; 
[U41](X0,X1) = X1; 
[U71](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 2; 
[U51](X0,X1,X2) = X2 + X1 + 2; 
[plus](X0,X1) = X1 + X0 + 1; 
[U31](X0,X1,X2) = 0; 
[U32](X0,X1) = 0; 
[U21](X0,X1) = 0; 
[U11](X0,X1,X2) = 0; 
[U12](X0,X1) = 0; 
[isNat](X0) = 0; 
[x](X0,X1) = X1*X0 + 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
  { 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
  {}
  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,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
  { U33(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
  { 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
  { U61(tt) -> 0 } (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(x(V_2,V_3)) -> and(isNatKind(V_2),isNatKind(V_3)),
    isNatKind(s(V_2)) -> isNatKind(V_2),
    isNatKind(plus(V_2,V_3)) -> and(isNatKind(V_2),isNatKind(V_3)),
    isNatKind(0) -> tt,
    x(V_1,0) -> U61(and(isNat(V_1),isNatKind(V_1))),
    x(V_1,s(V_0)) ->
    U71(and(and(isNat(V_0),isNatKind(V_0)),and(isNat(V_1),isNatKind(V_1))),V_0,V_1),
    isNat(x(V_2,V_3)) -> U31(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3),
    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)),
    U32(tt,V_3) -> U33(isNat(V_3)),
    U31(tt,V_2,V_3) -> U32(isNat(V_2),V_3),
    plus(V_1,s(V_0)) ->
    U51(and(and(isNat(V_0),isNatKind(V_0)),and(isNat(V_1),isNatKind(V_1))),V_0,V_1),
    plus(V_1,0) -> U41(and(isNat(V_1),isNatKind(V_1)),V_1),
    U51(tt,V_0,V_1) -> s(plus(V_1,V_0)),
    U71(tt,V_0,V_1) -> plus(x(V_1,V_0),V_1) } (19 rules)
  is CE-terminating by criterion with marks except on AC-symbols, and with graph;
  the dependency graph has 4 strongly connected components:
    component 1 is
      32: 'isNatKind`(plus(V_2,V_3)) ; 'isNatKind`(V_3)
      33: 'isNatKind`(plus(V_2,V_3)) ; 'isNatKind`(V_2)
      34: 'isNatKind`(s(V_2)) ; 'isNatKind`(V_2)
      35: 'isNatKind`(x(V_2,V_3)) ; 'isNatKind`(V_3)
      36: 'isNatKind`(x(V_2,V_3)) ; 'isNatKind`(V_2) 
      32 -> 32, 32 -> 33, 32 -> 34, 32 -> 35, 32 -> 36, 33 -> 32, 33 -> 33,
      33 -> 34, 33 -> 35, 33 -> 36, 34 -> 32, 34 -> 33, 34 -> 34, 34 -> 35,
      34 -> 36, 35 -> 32, 35 -> 33, 35 -> 34, 35 -> 35, 35 -> 36, 36 -> 32,
      36 -> 33, 36 -> 34, 36 -> 35, 36 -> 36, 
      On this component, the interpretation
      [tt] = 0; 
      [s](X0) = X0 + 1; 
      [0] = 0; 
      [and](X0,X1) = X1; 
      [U61](X0) = 0; 
      [U13](X0) = 0; 
      [U22](X0) = 0; 
      [U33](X0) = 0; 
      [U41](X0,X1) = X1; 
      [U71](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 2; 
      [U51](X0,X1,X2) = X2 + X1 + 2; 
      [plus](X0,X1) = X1 + X0 + 1; 
      [U31](X0,X1,X2) = 0; 
      [U32](X0,X1) = 0; 
      [U21](X0,X1) = 0; 
      [U11](X0,X1,X2) = 0; 
      [U12](X0,X1) = 0; 
      [isNat](X0) = 0; 
      [x](X0,X1) = X1*X0 + X1 + X0 + 1; 
      [isNatKind](X0) = 0; 
      ['isNatKind`](X0) = X0; 
       strictly decreases on every cycle
    component 2 is
      10: 'U31`(tt,V_2,V_3) ; 'isNat`(V_2)
      11: 'U31`(tt,V_2,V_3) ; 'U32`(isNat(V_2),V_3)
      12: 'U32`(tt,V_3) ; 'isNat`(V_3) 13: 'U21`(tt,V_2) ; 'isNat`(V_2)
      14: 'U11`(tt,V_2,V_3) ; 'isNat`(V_2)
      15: 'U11`(tt,V_2,V_3) ; 'U12`(isNat(V_2),V_3)
      16: 'U12`(tt,V_3) ; 'isNat`(V_3)
      19: 'isNat`(plus(V_2,V_3)) ; 'U11`(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3)
      21: 'isNat`(s(V_2)) ; 'U21`(isNatKind(V_2),V_2)
      24: 'isNat`(x(V_2,V_3)) ; 'U31`(and(isNatKind(V_2),isNatKind(V_3)),V_2,V_3)
      
      10 -> 19, 10 -> 21, 10 -> 24, 11 -> 12, 12 -> 19, 12 -> 21, 12 -> 24,
      13 -> 19, 13 -> 21, 13 -> 24, 14 -> 19, 14 -> 21, 14 -> 24, 15 -> 16,
      16 -> 19, 16 -> 21, 16 -> 24, 19 -> 14, 19 -> 15, 21 -> 13, 24 -> 10,
      24 -> 11, 
      On this component, the interpretation
      [tt] = 1; 
      [s](X0) = X0 + 1; 
      [0] = 0; 
      [and](X0,X1) = X1*X0; 
      [U61](X0) = 0; 
      [U13](X0) = 1; 
      [U22](X0) = 1; 
      [U33](X0) = 1; 
      [U41](X0,X1) = X1; 
      [U71](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 2; 
      [U51](X0,X1,X2) = X2 + X1 + 2; 
      [plus](X0,X1) = X1 + X0 + 1; 
      [U31](X0,X1,X2) = 1; 
      [U32](X0,X1) = 1; 
      [U21](X0,X1) = 1; 
      [U11](X0,X1,X2) = 1; 
      [U12](X0,X1) = 1; 
      [isNat](X0) = 1; 
      [x](X0,X1) = X1*X0 + X1 + X0 + 1; 
      [isNatKind](X0) = 1; 
      ['U31`](X0,X1,X2) = 3*X2 + 3*X1 + 2; 
      ['U32`](X0,X1) = 3*X1 + 1; 
      ['U21`](X0,X1) = 3*X1 + 1; 
      ['U11`](X0,X1,X2) = 3*X2 + 3*X1 + 2; 
      ['U12`](X0,X1) = 3*X1 + 1; 
      ['isNat`](X0) = 3*X0; 
       strictly decreases on every cycle
    component 3 is
      2: 'U51`(tt,V_0,V_1) ; 'plus`(V_1,V_0)
      9: 'plus`(V_1,s(V_0)) ; 'U51`(and(and(isNat(V_0),isNatKind(V_0)),
                                    and(isNat(V_1),isNatKind(V_1))),V_0,V_1) 
      2 -> 9, 9 -> 2, 
      On this component, with the interpretation
        [tt] = 1; 
        [s](X0) = X0 + 1; 
        [0] = 0; 
        [and](X0,X1) = X1*X0; 
        [U61](X0) = 0; 
        [U13](X0) = 1; 
        [U22](X0) = 1; 
        [U33](X0) = 1; 
        [U41](X0,X1) = X1; 
        [U71](X0,X1,X2) = X2*X1 + X2; 
        [U51](X0,X1,X2) = X2 + X1 + 1; 
        [plus](X0,X1) = X1 + X0; 
        [U31](X0,X1,X2) = 1; 
        [U32](X0,X1) = 1; 
        [U21](X0,X1) = 1; 
        [U11](X0,X1,X2) = 1; 
        [U12](X0,X1) = 1; 
        [isNat](X0) = 1; 
        [x](X0,X1) = X1*X0; 
        [isNatKind](X0) = 1; 
        ['U51`](X0,X1,X2) = X1; 
        ['plus`](X0,X1) = X1; 
        
      the subgraph of pairs that are only weakly decreasing
      has no strongly connected components.
    component 4 is
      0: 'U71`(tt,V_0,V_1) ; 'x`(V_1,V_0)
      29: 'x`(V_1,s(V_0)) ; 'U71`(and(and(isNat(V_0),isNatKind(V_0)),
                                  and(isNat(V_1),isNatKind(V_1))),V_0,V_1) 
      0 -> 29, 29 -> 0, 
      On this component, with the interpretation
        [tt] = 1; 
        [s](X0) = X0 + 1; 
        [0] = 0; 
        [and](X0,X1) = X1*X0; 
        [U61](X0) = 0; 
        [U13](X0) = 1; 
        [U22](X0) = 1; 
        [U33](X0) = 1; 
        [U41](X0,X1) = X1; 
        [U71](X0,X1,X2) = X2*X1 + X2; 
        [U51](X0,X1,X2) = X2 + X1 + 1; 
        [plus](X0,X1) = X1 + X0; 
        [U31](X0,X1,X2) = 1; 
        [U32](X0,X1) = 1; 
        [U21](X0,X1) = 1; 
        [U11](X0,X1,X2) = 1; 
        [U12](X0,X1) = 1; 
        [isNat](X0) = 1; 
        [x](X0,X1) = X1*X0; 
        [isNatKind](X0) = 1; 
        ['U71`](X0,X1,X2) = X1; 
        ['x`](X0,X1) = X1; 
        
      the subgraph of pairs that are only weakly decreasing
      has no strongly connected components. 

- : unit = ()

Quitting.
Standard error: