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,N) -> N,
             U21(tt,M,N) -> s(plus(N,M)),
             U31(tt) -> 0,
             U41(tt,M,N) -> plus(x(N,M),N),
             and(tt,X) -> X,
             isNat(0) -> tt,
             isNat(plus(V1,V2)) -> and(isNat(V1),isNat(V2)),
             isNat(s(V1)) -> isNat(V1),
             isNat(x(V1,V2)) -> and(isNat(V1),isNat(V2)),
             plus(N,0) -> U11(isNat(N),N),
             plus(N,s(M)) -> U21(and(isNat(M),isNat(N)),M,N),
             x(N,0) -> U31(isNat(N)),
             x(N,s(M)) -> U41(and(isNat(M),isNat(N)),M,N) } (13 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:
{ U11(tt,V_1) -> V_1 } (1 rules)

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

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

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

Checking module:
{ isNat(0) -> tt,
  isNat(plus(V_2,V_3)) -> and(isNat(V_2),isNat(V_3)),
  isNat(s(V_2)) -> isNat(V_2),
  isNat(x(V_2,V_3)) -> and(isNat(V_2),isNat(V_3)),
  plus(V_1,s(V_0)) -> U21(and(isNat(V_0),isNat(V_1)),V_0,V_1),
  plus(V_1,0) -> U11(isNat(V_1),V_1),
  U21(tt,V_0,V_1) -> s(plus(V_1,V_0)),
  x(V_1,s(V_0)) -> U41(and(isNat(V_0),isNat(V_1)),V_0,V_1),
  x(V_1,0) -> U31(isNat(V_1)),
  U41(tt,V_0,V_1) -> plus(x(V_1,V_0),V_1) } (10 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:
(15 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; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1,X2) = X2*X1 + X2; 
[x](X0,X1) = X1*X0; 
[U21](X0,X1,X2) = X2 + X1 + 1; 
[plus](X0,X1) = X1 + X0; 
[isNat](X0) = 0; 
['U41`](X0,X1,X2) = 2*X1 + 1; 
['x`](X0,X1) = 2*X1; 

Checking component 2
Trying simple graph criterion.
Trying to solve the following constraints:
(15 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; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1,X2) = X2*X1 + X2; 
[x](X0,X1) = X1*X0; 
[U21](X0,X1,X2) = X2 + X1 + 1; 
[plus](X0,X1) = X1 + X0; 
[isNat](X0) = 0; 
['U21`](X0,X1,X2) = 2*X1 + 1; 
['plus`](X0,X1) = 2*X1; 

Checking component 3
Trying simple graph criterion.
Trying to solve the following constraints:
(18 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; 
[U11](X0,X1) = X1; 
[U31](X0) = 0; 
[U41](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 2; 
[x](X0,X1) = X1*X0 + X1 + X0 + 1; 
[U21](X0,X1,X2) = X2 + X1 + 2; 
[plus](X0,X1) = X1 + X0 + 1; 
[isNat](X0) = 0; 
['isNat`](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
  { U11(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
  { U31(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
  { isNat(0) -> tt,
    isNat(plus(V_2,V_3)) -> and(isNat(V_2),isNat(V_3)),
    isNat(s(V_2)) -> isNat(V_2),
    isNat(x(V_2,V_3)) -> and(isNat(V_2),isNat(V_3)),
    plus(V_1,s(V_0)) -> U21(and(isNat(V_0),isNat(V_1)),V_0,V_1),
    plus(V_1,0) -> U11(isNat(V_1),V_1),
    U21(tt,V_0,V_1) -> s(plus(V_1,V_0)),
    x(V_1,s(V_0)) -> U41(and(isNat(V_0),isNat(V_1)),V_0,V_1),
    x(V_1,0) -> U31(isNat(V_1)),
    U41(tt,V_0,V_1) -> plus(x(V_1,V_0),V_1) } (10 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
      11: 'isNat`(x(V_2,V_3)) ; 'isNat`(V_3)
      12: 'isNat`(x(V_2,V_3)) ; 'isNat`(V_2)
      13: 'isNat`(s(V_2)) ; 'isNat`(V_2)
      14: 'isNat`(plus(V_2,V_3)) ; 'isNat`(V_3)
      15: 'isNat`(plus(V_2,V_3)) ; 'isNat`(V_2) 
      11 -> 11, 11 -> 12, 11 -> 13, 11 -> 14, 11 -> 15, 12 -> 11, 12 -> 12,
      12 -> 13, 12 -> 14, 12 -> 15, 13 -> 11, 13 -> 12, 13 -> 13, 13 -> 14,
      13 -> 15, 14 -> 11, 14 -> 12, 14 -> 13, 14 -> 14, 14 -> 15, 15 -> 11,
      15 -> 12, 15 -> 13, 15 -> 14, 15 -> 15, 
      On this component, the interpretation
      [tt] = 0; 
      [s](X0) = X0 + 1; 
      [0] = 0; 
      [and](X0,X1) = X1; 
      [U11](X0,X1) = X1; 
      [U31](X0) = 0; 
      [U41](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 2; 
      [x](X0,X1) = X1*X0 + X1 + X0 + 1; 
      [U21](X0,X1,X2) = X2 + X1 + 2; 
      [plus](X0,X1) = X1 + X0 + 1; 
      [isNat](X0) = 0; 
      ['isNat`](X0) = X0; 
       strictly decreases on every cycle
    component 2 is
      6: 'U21`(tt,V_0,V_1) ; 'plus`(V_1,V_0)
      10: 'plus`(V_1,s(V_0)) ; 'U21`(and(isNat(V_0),isNat(V_1)),V_0,V_1) 
      6 -> 10, 10 -> 6, 
      On this component, the interpretation
      [tt] = 0; 
      [s](X0) = X0 + 1; 
      [0] = 0; 
      [and](X0,X1) = X1; 
      [U11](X0,X1) = X1; 
      [U31](X0) = 0; 
      [U41](X0,X1,X2) = X2*X1 + X2; 
      [x](X0,X1) = X1*X0; 
      [U21](X0,X1,X2) = X2 + X1 + 1; 
      [plus](X0,X1) = X1 + X0; 
      [isNat](X0) = 0; 
      ['U21`](X0,X1,X2) = 2*X1 + 1; 
      ['plus`](X0,X1) = 2*X1; 
       strictly decreases on every cycle
    component 3 is
      0: 'U41`(tt,V_0,V_1) ; 'x`(V_1,V_0)
      5: 'x`(V_1,s(V_0)) ; 'U41`(and(isNat(V_0),isNat(V_1)),V_0,V_1) 
      0 -> 5, 5 -> 0, 
      On this component, the interpretation
      [tt] = 0; 
      [s](X0) = X0 + 1; 
      [0] = 0; 
      [and](X0,X1) = X1; 
      [U11](X0,X1) = X1; 
      [U31](X0) = 0; 
      [U41](X0,X1,X2) = X2*X1 + X2; 
      [x](X0,X1) = X1*X0; 
      [U21](X0,X1,X2) = X2 + X1 + 1; 
      [plus](X0,X1) = X1 + X0; 
      [isNat](X0) = 0; 
      ['U41`](X0,X1,X2) = 2*X1 + 1; 
      ['x`](X0,X1) = 2*X1; 
       strictly decreases on every cycle 

- : unit = ()

Quitting.
Standard error: