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,V1,V2) -> U142(isNat(V1),V2), U142(tt,V2) -> U143(isNat(V2)), U143(tt) -> tt, U151(tt,V1,V2) -> U152(isNat(V1),V2), U152(tt,V2) -> U153(isNat(V2)), U153(tt) -> tt, U161(tt,V) -> U162(isNzNat(V)), U162(tt) -> tt, U171(tt,V1,V2) -> U172(isNat(V1),V2), U172(tt,V2) -> U173(isNat(V2)), U173(tt) -> tt, U181(tt,V1,V2) -> U182(isNat(V1),V2), U182(tt,V2) -> U183(isNat(V2)), U183(tt) -> tt, U191(tt,V1,V2) -> U192(isNat(V1),V2), U192(tt,V2) -> U193(isNat(V2)), U193(tt) -> tt, U201(tt,V1,V2) -> U202(isNat(V1),V2), U202(tt,V2) -> U203(isNat(V2)), U203(tt) -> tt, U21(tt,M,N) -> s_(+(+(*(M,N),M),N)), U211(tt,V1) -> U212(isNzNat(V1)), U212(tt) -> tt, U221(tt,V1,V2) -> U222(isNat(V1),V2), U222(tt,V2) -> U223(isNzNat(V2)), U223(tt) -> tt, U231(tt,V1,V2) -> U232(isNzNat(V1),V2), U232(tt,V2) -> U233(isNzNat(V2)), U233(tt) -> tt, U241(tt,V1,V2) -> U242(isNzNat(V1),V2), U242(tt,V2) -> U243(isNzNat(V2)), U243(tt) -> tt, U251(tt,V1) -> U252(isNat(V1)), U252(tt) -> tt, U261(tt,N) -> N, U271(tt) -> s_(0), U281(tt,M',N) -> U282(equal(_gt_(M',N),true)), U282(tt) -> 0, U291(tt,M',N) -> U292(equal(_gt_(N,M'),true),M',N), U292(tt,M',N) -> s_(quot(d(M',N),M')), 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(and(isNat(N),isNatKind(N))), *(s_(M),s_(N)) -> U21(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N), +(0,N) -> U31(and(isNat(N),isNatKind(N)),N), +(s_(M),s_(N)) -> U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N), _lt_(N,M) -> U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N), _gt_(0,M) -> U61(and(isNat(M),isNatKind(M))), _gt_(N',0) -> U71(and(isNzNat(N'),isNatKind(N'))), _gt_(s_(N),s_(M)) -> U81(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N), and(tt,X) -> X, d(0,N) -> U91(and(isNat(N),isNatKind(N)),N), d(s_(M),s_(N)) -> U101(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N), equal(X,X) -> tt, gcd(0,N) -> U111(and(isNat(N),isNatKind(N))), gcd(M',N') -> U121(and(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'), isNatKind(N'))),M',N'), gcd(N',N') -> U131(and(isNzNat(N'),isNatKind(N')),N'), isBoolean(false) -> tt, isBoolean(true) -> tt, isBoolean(_lt_(V1,V2)) -> U141(and(isNatKind(V1),isNatKind(V2)),V1,V2), isBoolean(_gt_(V1,V2)) -> U151(and(isNatKind(V1),isNatKind(V2)),V1,V2), isBooleanKind(false) -> tt, isBooleanKind(true) -> tt, isBooleanKind(_lt_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isBooleanKind(_gt_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNat(0) -> tt, isNat(V) -> U161(isNatKind(V),V), isNat(*(V1,V2)) -> U171(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNat(+(V1,V2)) -> U181(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNat(d(V1,V2)) -> U191(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNat(gcd(V1,V2)) -> U201(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNat(p_(V1)) -> U211(isNatKind(V1),V1), isNat(quot(V1,V2)) -> U221(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNatKind(0) -> tt, isNatKind(1) -> tt, isNatKind(2) -> tt, isNatKind(3) -> tt, isNatKind(4) -> tt, isNatKind(5) -> tt, isNatKind(6) -> tt, isNatKind(7) -> tt, isNatKind(*(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNatKind(+(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNatKind(d(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNatKind(gcd(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNatKind(p_(V1)) -> isNatKind(V1), isNatKind(quot(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)), isNatKind(s_(V1)) -> isNatKind(V1), 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(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNzNat(gcd(V1,V2)) -> U241(and(isNatKind(V1),isNatKind(V2)),V1,V2), isNzNat(s_(V1)) -> U251(isNatKind(V1),V1), p_(s_(N)) -> U261(and(isNat(N),isNatKind(N)),N), quot(M',M') -> U271(and(isNzNat(M'),isNatKind(M'))), quot(N,M') -> U281(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N), quot(N,M') -> U291(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) } (120 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: { U91(tt,V_3) -> V_3 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U223(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U252(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U243(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U233(tt) -> 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: { 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: { 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: { U212(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U203(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U193(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U183(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U173(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U162(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U282(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: { U261(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)) -> U261(and(isNat(V_3),isNatKind(V_3)),V_3), isNatKind(s_(V_4)) -> isNatKind(V_4), isNatKind(quot(V_4,V_5)) -> and(isNatKind(V_4),isNatKind(V_5)), isNatKind(p_(V_4)) -> isNatKind(V_4), isNatKind(gcd(V_4,V_5)) -> and(isNatKind(V_4),isNatKind(V_5)), isNatKind(d(V_4,V_5)) -> and(isNatKind(V_4),isNatKind(V_5)), isNatKind(+(V_4,V_5)) -> and(isNatKind(V_4),isNatKind(V_5)), isNatKind(*(V_4,V_5)) -> and(isNatKind(V_4),isNatKind(V_5)), isNatKind(7) -> tt, isNatKind(6) -> tt, isNatKind(5) -> tt, isNatKind(4) -> tt, isNatKind(3) -> tt, isNatKind(2) -> tt, isNatKind(1) -> tt, isNatKind(0) -> tt, quot(V_0,V_0) -> U271(and(isNzNat(V_0),isNatKind(V_0))), quot(V_3,V_0) -> U281(and(and(isNzNat(V_0),isNatKind(V_0)),and(isNat(V_3),isNatKind(V_3))),V_0,V_3), quot(V_3,V_0) -> U291(and(and(isNzNat(V_0),isNatKind(V_0)),and(isNat(V_3),isNatKind(V_3))),V_0,V_3), isNat(quot(V_4,V_5)) -> U221(and(isNatKind(V_4),isNatKind(V_5)),V_4,V_5), isNat(p_(V_4)) -> U211(isNatKind(V_4),V_4), isNat(gcd(V_4,V_5)) -> U201(and(isNatKind(V_4),isNatKind(V_5)),V_4,V_5), isNat(d(V_4,V_5)) -> U191(and(isNatKind(V_4),isNatKind(V_5)),V_4,V_5), isNat(+(V_4,V_5)) -> U181(and(isNatKind(V_4),isNatKind(V_5)),V_4,V_5), isNat(*(V_4,V_5)) -> U171(and(isNatKind(V_4),isNatKind(V_5)),V_4,V_5), isNat(V_6) -> U161(isNatKind(V_6),V_6), isNat(0) -> tt, d(0,V_3) -> U91(and(isNat(V_3),isNatKind(V_3)),V_3), d(s_(V_1),s_(V_3)) -> U101(and(and(isNat(V_1),isNatKind(V_1)),and(isNat(V_3),isNatKind(V_3))),V_1,V_3), U101(tt,V_1,V_3) -> d(V_1,V_3), +(0,V_3) -> U31(and(isNat(V_3),isNatKind(V_3)),V_3), +(s_(V_1),s_(V_3)) -> U41(and(and(isNat(V_1),isNatKind(V_1)),and(isNat(V_3),isNatKind(V_3))),V_1,V_3), U41(tt,V_1,V_3) -> s_(s_(+(V_1,V_3))), *(0,V_3) -> U11(and(isNat(V_3),isNatKind(V_3))), *(s_(V_1),s_(V_3)) -> U21(and(and(isNat(V_1),isNatKind(V_1)),and(isNat(V_3),isNatKind(V_3))),V_1,V_3), U21(tt,V_1,V_3) -> s_(+(+(*(V_1,V_3),V_1),V_3)), U172(tt,V_5) -> U173(isNat(V_5)), U171(tt,V_4,V_5) -> U172(isNat(V_4),V_5), U182(tt,V_5) -> U183(isNat(V_5)), U181(tt,V_4,V_5) -> U182(isNat(V_4),V_5), U192(tt,V_5) -> U193(isNat(V_5)), U191(tt,V_4,V_5) -> U192(isNat(V_4),V_5), U202(tt,V_5) -> U203(isNat(V_5)), U201(tt,V_4,V_5) -> U202(isNat(V_4),V_5), U251(tt,V_4) -> U252(isNat(V_4)), isNzNat(s_(V_4)) -> U251(isNatKind(V_4),V_4), isNzNat(gcd(V_4,V_5)) -> U241(and(isNatKind(V_4),isNatKind(V_5)),V_4,V_5), isNzNat(*(V_4,V_5)) -> U231(and(isNatKind(V_4),isNatKind(V_5)),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, _gt_(0,V_1) -> U61(and(isNat(V_1),isNatKind(V_1))), _gt_(V_2,0) -> U71(and(isNzNat(V_2),isNatKind(V_2))), _gt_(s_(V_3),s_(V_1)) -> U81(and(and(isNat(V_1),isNatKind(V_1)),and(isNat(V_3),isNatKind(V_3))),V_1,V_3), U121(tt,V_0,V_2) -> U122(equal(_gt_(V_2,V_0),true),V_0,V_2), gcd(0,V_3) -> U111(and(isNat(V_3),isNatKind(V_3))), gcd(V_0,V_2) -> U121(and(and(isNzNat(V_0),isNatKind(V_0)),and(isNzNat(V_2),isNatKind(V_2))),V_0,V_2), gcd(V_2,V_2) -> U131(and(isNzNat(V_2),isNatKind(V_2)),V_2), U122(tt,V_0,V_2) -> gcd(d(V_0,V_2),V_0), U281(tt,V_0,V_3) -> U282(equal(_gt_(V_0,V_3),true)), U81(tt,V_1,V_3) -> _gt_(V_3,V_1), U161(tt,V_6) -> U162(isNzNat(V_6)), U211(tt,V_4) -> U212(isNzNat(V_4)), U222(tt,V_5) -> U223(isNzNat(V_5)), U221(tt,V_4,V_5) -> U222(isNat(V_4),V_5), U232(tt,V_5) -> U233(isNzNat(V_5)), U231(tt,V_4,V_5) -> U232(isNzNat(V_4),V_5), U242(tt,V_5) -> U243(isNzNat(V_5)), U241(tt,V_4,V_5) -> U242(isNzNat(V_4),V_5), U292(tt,V_0,V_3) -> s_(quot(d(V_0,V_3),V_0)), U291(tt,V_0,V_3) -> U292(equal(_gt_(V_3,V_0),true),V_0,V_3) } (75 rules) The dependency graph is (1 nodes) Checking each of the 8 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (106 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: (106 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: (106 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: