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) -> U102(isNat(N),M,N), U102(tt,M,N) -> d(M,N), U11(tt) -> 0, U111(tt) -> 0, U121(tt,M',N') -> U122(isNzNat(N'),M',N'), U122(tt,M',N') -> U123(equal(_gt_(N',M'),true),M',N'), U123(tt,M',N') -> gcd(d(M',N'),M'), U131(tt,N') -> N', U141(tt,V2) -> U142(isNat(V2)), U142(tt) -> tt, U151(tt,V2) -> U152(isNat(V2)), U152(tt) -> tt, U161(tt) -> tt, U171(tt,V2) -> U172(isNat(V2)), U172(tt) -> tt, U181(tt,V2) -> U182(isNat(V2)), U182(tt) -> tt, U191(tt,V2) -> U192(isNat(V2)), U192(tt) -> tt, U201(tt,V2) -> U202(isNat(V2)), U202(tt) -> tt, U21(tt,M,N) -> U22(isNat(N),M,N), U211(tt) -> tt, U22(tt,M,N) -> s_(+(+(*(M,N),M),N)), U221(tt,V2) -> U222(isNzNat(V2)), U222(tt) -> tt, U231(tt,V2) -> U232(isNzNat(V2)), U232(tt) -> tt, U241(tt,V2) -> U242(isNzNat(V2)), U242(tt) -> tt, U251(tt) -> tt, U261(tt,N) -> N, U271(tt) -> s_(0), U281(tt,M',N) -> U282(isNat(N),M',N), U282(tt,M',N) -> U283(equal(_gt_(M',N),true)), U283(tt) -> 0, U291(tt,M',N) -> U292(isNat(N),M',N), U292(tt,M',N) -> U293(equal(_gt_(N,M'),true),M',N), U293(tt,M',N) -> s_(quot(d(M',N),M')), U31(tt,N) -> N, U41(tt,M,N) -> U42(isNat(N),M,N), U42(tt,M,N) -> s_(s_(+(M,N))), U51(tt,M,N) -> U52(isNat(N),M,N), U52(tt,M,N) -> _gt_(M,N), U61(tt) -> false, U71(tt) -> true, U81(tt,M,N) -> U82(isNat(N),M,N), U82(tt,M,N) -> _gt_(N,M), U91(tt,N) -> N, *(0,N) -> U11(isNat(N)), *(s_(M),s_(N)) -> U21(isNat(M),M,N), +(0,N) -> U31(isNat(N),N), +(s_(M),s_(N)) -> U41(isNat(M),M,N), _lt_(N,M) -> U51(isNat(M),M,N), _gt_(0,M) -> U61(isNat(M)), _gt_(N',0) -> U71(isNzNat(N')), _gt_(s_(N),s_(M)) -> U81(isNat(M),M,N), d(0,N) -> U91(isNat(N),N), d(s_(M),s_(N)) -> U101(isNat(M),M,N), equal(X,X) -> tt, gcd(0,N) -> U111(isNat(N)), gcd(M',N') -> U121(isNzNat(M'),M',N'), gcd(N',N') -> U131(isNzNat(N'),N'), isBoolean(false) -> tt, isBoolean(true) -> tt, isBoolean(_lt_(V1,V2)) -> U141(isNat(V1),V2), isBoolean(_gt_(V1,V2)) -> U151(isNat(V1),V2), isNat(0) -> tt, isNat(V) -> U161(isNzNat(V)), isNat(*(V1,V2)) -> U171(isNat(V1),V2), isNat(+(V1,V2)) -> U181(isNat(V1),V2), isNat(d(V1,V2)) -> U191(isNat(V1),V2), isNat(gcd(V1,V2)) -> U201(isNat(V1),V2), isNat(p_(V1)) -> U211(isNzNat(V1)), isNat(quot(V1,V2)) -> U221(isNat(V1),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)) -> U231(isNzNat(V1),V2), isNzNat(gcd(V1,V2)) -> U241(isNzNat(V1),V2), isNzNat(s_(V1)) -> U251(isNat(V1)), p_(s_(N)) -> U261(isNat(N),N), quot(M',M') -> U271(isNzNat(M')), quot(N,M') -> U281(isNzNat(M'),M',N), quot(N,M') -> U291(isNzNat(M'),M',N) } (96 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: { U261(tt,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: { U91(tt,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: { 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: { U251(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U242(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U232(tt) -> tt } (1 rules) 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: { U111(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U283(tt) -> 0 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U271(tt) -> s_(0) } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U222(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U211(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U202(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U192(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U182(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U172(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U161(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { p_(s_(V_3)) -> U261(isNat(V_3),V_3), isNat(0) -> tt, isNat(V_6) -> U161(isNzNat(V_6)), isNat(*(V_4,V_5)) -> U171(isNat(V_4),V_5), isNat(+(V_4,V_5)) -> U181(isNat(V_4),V_5), isNat(d(V_4,V_5)) -> U191(isNat(V_4),V_5), isNat(gcd(V_4,V_5)) -> U201(isNat(V_4),V_5), isNat(p_(V_4)) -> U211(isNzNat(V_4)), isNat(quot(V_4,V_5)) -> U221(isNat(V_4),V_5), U101(tt,V_1,V_3) -> U102(isNat(V_3),V_1,V_3), d(0,V_3) -> U91(isNat(V_3),V_3), d(s_(V_1),s_(V_3)) -> U101(isNat(V_1),V_1,V_3), U102(tt,V_1,V_3) -> d(V_1,V_3), U171(tt,V_5) -> U172(isNat(V_5)), U181(tt,V_5) -> U182(isNat(V_5)), U191(tt,V_5) -> U192(isNat(V_5)), U201(tt,V_5) -> U202(isNat(V_5)), U41(tt,V_1,V_3) -> U42(isNat(V_3),V_1,V_3), +(s_(V_1),s_(V_3)) -> U41(isNat(V_1),V_1,V_3), +(0,V_3) -> U31(isNat(V_3),V_3), U22(tt,V_1,V_3) -> s_(+(+(*(V_1,V_3),V_1),V_3)), U21(tt,V_1,V_3) -> U22(isNat(V_3),V_1,V_3), *(0,V_3) -> U11(isNat(V_3)), *(s_(V_1),s_(V_3)) -> U21(isNat(V_1),V_1,V_3), U42(tt,V_1,V_3) -> s_(s_(+(V_1,V_3))), U81(tt,V_1,V_3) -> U82(isNat(V_3),V_1,V_3), _gt_(s_(V_3),s_(V_1)) -> U81(isNat(V_1),V_1,V_3), _gt_(V_2,0) -> U71(isNzNat(V_2)), _gt_(0,V_1) -> U61(isNat(V_1)), U122(tt,V_0,V_2) -> U123(equal(_gt_(V_2,V_0),true),V_0,V_2), U121(tt,V_0,V_2) -> U122(isNzNat(V_2),V_0,V_2), gcd(0,V_3) -> U111(isNat(V_3)), gcd(V_0,V_2) -> U121(isNzNat(V_0),V_0,V_2), gcd(V_2,V_2) -> U131(isNzNat(V_2),V_2), isNzNat(s_(V_4)) -> U251(isNat(V_4)), isNzNat(gcd(V_4,V_5)) -> U241(isNzNat(V_4),V_5), isNzNat(*(V_4,V_5)) -> U231(isNzNat(V_4),V_5), isNzNat(7) -> tt, isNzNat(6) -> tt, isNzNat(5) -> tt, isNzNat(4) -> tt, isNzNat(3) -> tt, isNzNat(2) -> tt, isNzNat(1) -> tt, U221(tt,V_5) -> U222(isNzNat(V_5)), U231(tt,V_5) -> U232(isNzNat(V_5)), U241(tt,V_5) -> U242(isNzNat(V_5)), U123(tt,V_0,V_2) -> gcd(d(V_0,V_2),V_0), U282(tt,V_0,V_3) -> U283(equal(_gt_(V_0,V_3),true)), U281(tt,V_0,V_3) -> U282(isNat(V_3),V_0,V_3), U292(tt,V_0,V_3) -> U293(equal(_gt_(V_3,V_0),true),V_0,V_3), U291(tt,V_0,V_3) -> U292(isNat(V_3),V_0,V_3), quot(V_0,V_0) -> U271(isNzNat(V_0)), quot(V_3,V_0) -> U281(isNzNat(V_0),V_0,V_3), quot(V_3,V_0) -> U291(isNzNat(V_0),V_0,V_3), U293(tt,V_0,V_3) -> s_(quot(d(V_0,V_3),V_0)), U82(tt,V_1,V_3) -> _gt_(V_3,V_1) } (57 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: (88 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 strongly connected part criterion. Trying to solve the following constraints: (88 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: (88 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: (88 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: