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))))))), U101(tt,M,N) -> d(M,N), U11(tt) -> 0, U111(tt) -> 0, U121(tt,M',N') -> U122(equal(_gt_(N',M'),true),M',N'), U122(tt,M',N') -> gcd(d(M',N'),M'), U131(tt,N') -> N', U141(tt,N) -> N, U151(tt) -> s_(0), U161(tt,M',N) -> U162(equal(_gt_(M',N),true)), U162(tt) -> 0, U171(tt,M',N) -> U172(equal(_gt_(N,M'),true),M',N), U172(tt,M',N) -> s_(quot(d(M',N),M')), U21(tt,M,N) -> s_(+(+(*(M,N),M),N)), U31(tt,N) -> N, U41(tt,M,N) -> s_(s_(+(M,N))), U51(tt,M,N) -> _gt_(M,N), U61(tt) -> false, U71(tt) -> true, U81(tt,M,N) -> _gt_(N,M), U91(tt,N) -> N, *(0,N) -> U11(isNat(N)), *(s_(M),s_(N)) -> U21(and(isNat(M),isNat(N)),M,N), +(0,N) -> U31(isNat(N),N), +(s_(M),s_(N)) -> U41(and(isNat(M),isNat(N)),M,N), _lt_(N,M) -> U51(and(isNat(M),isNat(N)),M,N), _gt_(0,M) -> U61(isNat(M)), _gt_(N',0) -> U71(isNzNat(N')), _gt_(s_(N),s_(M)) -> U81(and(isNat(M),isNat(N)),M,N), and(tt,X) -> X, d(0,N) -> U91(isNat(N),N), d(s_(M),s_(N)) -> U101(and(isNat(M),isNat(N)),M,N), equal(X,X) -> tt, gcd(0,N) -> U111(isNat(N)), gcd(M',N') -> U121(and(isNzNat(M'),isNzNat(N')),M',N'), gcd(N',N') -> U131(isNzNat(N'),N'), isBoolean(false) -> tt, isBoolean(true) -> tt, isBoolean(_lt_(V1,V2)) -> and(isNat(V1),isNat(V2)), isBoolean(_gt_(V1,V2)) -> and(isNat(V1),isNat(V2)), isNat(0) -> tt, isNat(V) -> isNzNat(V), isNat(*(V1,V2)) -> and(isNat(V1),isNat(V2)), isNat(+(V1,V2)) -> and(isNat(V1),isNat(V2)), isNat(d(V1,V2)) -> and(isNat(V1),isNat(V2)), isNat(gcd(V1,V2)) -> and(isNat(V1),isNat(V2)), isNat(p_(V1)) -> isNzNat(V1), isNat(quot(V1,V2)) -> and(isNat(V1),isNzNat(V2)), isNzNat(1) -> tt, isNzNat(2) -> tt, isNzNat(3) -> tt, isNzNat(4) -> tt, isNzNat(5) -> tt, isNzNat(6) -> tt, isNzNat(7) -> tt, isNzNat(*(V1,V2)) -> and(isNzNat(V1),isNzNat(V2)), isNzNat(gcd(V1,V2)) -> and(isNzNat(V1),isNzNat(V2)), isNzNat(s_(V1)) -> isNat(V1), p_(s_(N)) -> U141(isNat(N),N), quot(M',M') -> U151(isNzNat(M')), quot(N,M') -> U161(and(isNzNat(M'),isNat(N)),M',N), quot(N,M') -> U171(and(isNzNat(M'),isNat(N)),M',N) } (68 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_7) -> V_7 } (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: { 7 -> s_(s_(s_(s_(s_(s_(s_(0))))))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 6 -> s_(s_(s_(s_(s_(s_(0)))))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 5 -> s_(s_(s_(s_(s_(0))))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 4 -> s_(s_(s_(s_(0)))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 3 -> s_(s_(s_(0))) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 2 -> s_(s_(0)) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { 1 -> s_(0) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U31(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U11(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U131(tt,V_2) -> V_2 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U91(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { equal(V_7,V_7) -> tt } (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: { U71(tt) -> true } (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: { U61(tt) -> false } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U111(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U162(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U151(tt) -> s_(0) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U141(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { p_(s_(V_3)) -> U141(isNat(V_3),V_3), isNat(quot(V_4,V_5)) -> and(isNat(V_4),isNzNat(V_5)), isNat(p_(V_4)) -> isNzNat(V_4), isNat(gcd(V_4,V_5)) -> and(isNat(V_4),isNat(V_5)), isNat(d(V_4,V_5)) -> and(isNat(V_4),isNat(V_5)), isNat(+(V_4,V_5)) -> and(isNat(V_4),isNat(V_5)), isNat(*(V_4,V_5)) -> and(isNat(V_4),isNat(V_5)), isNat(V_6) -> isNzNat(V_6), isNat(0) -> tt, d(0,V_3) -> U91(isNat(V_3),V_3), d(s_(V_1),s_(V_3)) -> U101(and(isNat(V_1),isNat(V_3)),V_1,V_3), U101(tt,V_1,V_3) -> d(V_1,V_3), +(0,V_3) -> U31(isNat(V_3),V_3), +(s_(V_1),s_(V_3)) -> U41(and(isNat(V_1),isNat(V_3)),V_1,V_3), U41(tt,V_1,V_3) -> s_(s_(+(V_1,V_3))), *(0,V_3) -> U11(isNat(V_3)), *(s_(V_1),s_(V_3)) -> U21(and(isNat(V_1),isNat(V_3)),V_1,V_3), U21(tt,V_1,V_3) -> s_(+(+(*(V_1,V_3),V_1),V_3)), isNzNat(1) -> tt, isNzNat(2) -> tt, isNzNat(3) -> tt, isNzNat(4) -> tt, isNzNat(5) -> tt, isNzNat(6) -> tt, isNzNat(7) -> tt, isNzNat(*(V_4,V_5)) -> and(isNzNat(V_4),isNzNat(V_5)), isNzNat(gcd(V_4,V_5)) -> and(isNzNat(V_4),isNzNat(V_5)), isNzNat(s_(V_4)) -> isNat(V_4), _gt_(s_(V_3),s_(V_1)) -> U81(and(isNat(V_1),isNat(V_3)),V_1,V_3), _gt_(V_2,0) -> U71(isNzNat(V_2)), _gt_(0,V_1) -> U61(isNat(V_1)), U121(tt,V_0,V_2) -> U122(equal(_gt_(V_2,V_0),true),V_0,V_2), gcd(V_2,V_2) -> U131(isNzNat(V_2),V_2), gcd(V_0,V_2) -> U121(and(isNzNat(V_0),isNzNat(V_2)),V_0,V_2), gcd(0,V_3) -> U111(isNat(V_3)), U122(tt,V_0,V_2) -> gcd(d(V_0,V_2),V_0), U161(tt,V_0,V_3) -> U162(equal(_gt_(V_0,V_3),true)), U81(tt,V_1,V_3) -> _gt_(V_3,V_1), quot(V_3,V_0) -> U171(and(isNzNat(V_0),isNat(V_3)),V_0,V_3), quot(V_3,V_0) -> U161(and(isNzNat(V_0),isNat(V_3)),V_0,V_3), quot(V_0,V_0) -> U151(isNzNat(V_0)), U172(tt,V_0,V_3) -> s_(quot(d(V_0,V_3),V_0)), U171(tt,V_0,V_3) -> U172(equal(_gt_(V_3,V_0),true),V_0,V_3) } (43 rules) The dependency graph is (1 nodes) Checking each of the 7 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (64 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: (64 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: (64 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. No modular termination proof found. - : unit = () The last proof attempt failed. - : unit = () Quitting. Standard error: