DONT KNOW Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { 1 -> s_(0), 2 -> s_(s_(0)), 3 -> s_(s_(s_(0))), 4 -> s_(s_(s_(s_(0)))), 5 -> s_(s_(s_(s_(s_(0))))), 6 -> s_(s_(s_(s_(s_(s_(0)))))), 7 -> s_(s_(s_(s_(s_(s_(s_(0))))))), U11(tt,M,N) -> U12(tt,M,N), U12(tt,M,N) -> s_(+(+(*(M,N),M),N)), U21(tt,M,N) -> U22(tt,M,N), U22(tt,M,N) -> s_(s_(+(M,N))), U31(tt,M,N) -> U32(tt,M,N), U32(tt,M,N) -> _gt_(M,N), U41(tt,M,N) -> U42(tt,M,N), U42(tt,M,N) -> _gt_(N,M), U51(tt,M,N) -> U52(tt,M,N), U52(tt,M,N) -> d(M,N), U61(tt,M',N') -> U62(tt,M',N'), U62(tt,M',N') -> U63(equal(_gt_(N',M'),true),M',N'), U63(tt,M',N') -> gcd(d(M',N'),M'), U71(tt,M',N) -> U72(tt,M',N), U72(tt,M',N) -> U73(equal(_gt_(M',N),true)), U73(tt) -> 0, U81(tt,M',N) -> U82(tt,M',N), U82(tt,M',N) -> U83(equal(_gt_(N,M'),true),M',N), U83(tt,M',N) -> s_(quot(d(M',N),M')), *(0,N) -> 0, *(s_(M),s_(N)) -> U11(tt,M,N), +(0,N) -> N, +(s_(M),s_(N)) -> U21(tt,M,N), _lt_(N,M) -> U31(tt,M,N), _gt_(0,M) -> false, _gt_(N',0) -> true, _gt_(s_(N),s_(M)) -> U41(tt,M,N), d(0,N) -> N, d(s_(M),s_(N)) -> U51(tt,M,N), equal(X,X) -> tt, gcd(0,N) -> 0, gcd(M',N') -> U61(tt,M',N'), gcd(N',N') -> N', p_(s_(N)) -> N, quot(M',M') -> s_(0), quot(N,M') -> U71(tt,M',N), quot(N,M') -> U81(tt,M',N) } (44 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: { p_(s_(V_3)) -> V_3 } (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: {} 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: { _gt_(0,V_1) -> false, _gt_(V_2,0) -> true, _gt_(s_(V_3),s_(V_1)) -> U41(tt,V_1,V_3), U42(tt,V_1,V_3) -> _gt_(V_3,V_1), U41(tt,V_1,V_3) -> U42(tt,V_1,V_3) } (5 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: (8 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [0] = 0; [s_](X0) = X0 + 2; [tt] = 0; [true] = 0; [false] = 0; [U41](X0,X1,X2) = 0; [U42](X0,X1,X2) = 0; [_gt_](X0,X1) = 0; ['U41`](X0,X1,X2) = 2*X2 + 2; ['U42`](X0,X1,X2) = 2*X2 + 1; ['_gt_`](X0,X1) = 2*X0; Checking module: { U32(tt,V_1,V_3) -> _gt_(V_1,V_3) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U31(tt,V_1,V_3) -> U32(tt,V_1,V_3) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { _lt_(V_3,V_1) -> U31(tt,V_1,V_3) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { d(0,V_3) -> V_3, d(s_(V_1),s_(V_3)) -> U51(tt,V_1,V_3), U52(tt,V_1,V_3) -> d(V_1,V_3), U51(tt,V_1,V_3) -> U52(tt,V_1,V_3) } (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: (7 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [0] = 0; [s_](X0) = X0 + 1; [tt] = 0; [U51](X0,X1,X2) = X2 + X1; [U52](X0,X1,X2) = X2 + X1; [d](X0,X1) = X1 + X0; ['U51`](X0,X1,X2) = 2*X2 + 2*X1 + 2; ['U52`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['d`](X0,X1) = 2*X1 + 2*X0; Checking module: { equal(V_4,V_4) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U73(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U72(tt,V_0,V_3) -> U73(equal(_gt_(V_0,V_3),true)) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U71(tt,V_0,V_3) -> U72(tt,V_0,V_3) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { quot(V_3,V_0) -> U81(tt,V_0,V_3), quot(V_3,V_0) -> U71(tt,V_0,V_3), quot(V_0,V_0) -> s_(0), U83(tt,V_0,V_3) -> s_(quot(d(V_0,V_3),V_0)), U82(tt,V_0,V_3) -> U83(equal(_gt_(V_3,V_0),true),V_0,V_3), U81(tt,V_0,V_3) -> U82(tt,V_0,V_3) } (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: (23 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. No solution found for these parameters. No solution found for these constraints. Trying strongly connected part criterion. Trying to solve the following constraints: (23 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. No solution found for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Time out for these parameters. No solution found for these constraints. Trying to solve the following constraints: (23 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 to solve the following constraints: (23 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 to solve the following constraints: (23 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. No modular termination proof found. - : unit = () The last proof attempt failed. - : unit = () Quitting. Standard error: