YES Welcome to CiME version 2.02 - Built on 14/04/2004 13:29:51 - : unit = () - : unit = () X : variable_set = F : signature = R : HTRS = { union(empty,X) -> X, union(empty,X) -> X, 0(z) -> z, U101(tt,X,Y) -> U102(isBin(Y),X,Y), U102(tt,X,Y) -> 0(mult(X,Y)), U11(tt) -> tt, U111(tt,X,Y) -> U112(isBin(Y),X,Y), U112(tt,X,Y) -> plus(0(mult(X,Y)),Y), U121(tt,X) -> X, U131(tt,X,Y) -> U132(isBin(Y),X,Y), U132(tt,X,Y) -> 0(plus(X,Y)), U141(tt,X,Y) -> U142(isBin(Y),X,Y), U142(tt,X,Y) -> 1(plus(X,Y)), U151(tt,X,Y) -> U152(isBin(Y),X,Y), U152(tt,X,Y) -> 0(plus(1(z),X,Y)), U161(tt,X) -> X, U171(tt,A,B) -> U172(isBag(B),A,B), U172(tt,A,B) -> mult(prod(A),prod(B)), U181(tt,X) -> X, U191(tt,A,B) -> U192(isBag(B),A,B), U192(tt,A,B) -> plus(sum(A),sum(B)), U21(tt,V2) -> U22(isBag(V2)), U22(tt) -> tt, U31(tt) -> tt, U41(tt) -> tt, U51(tt,V2) -> U52(isBin(V2)), U52(tt) -> tt, U61(tt,V2) -> U62(isBin(V2)), U62(tt) -> tt, U71(tt) -> tt, U81(tt) -> tt, U91(tt) -> z, isBag(empty) -> tt, isBag(singl(V1)) -> U11(isBin(V1)), isBag(union(V1,V2)) -> U21(isBag(V1),V2), isBin(z) -> tt, isBin(0(V1)) -> U31(isBin(V1)), isBin(1(V1)) -> U41(isBin(V1)), isBin(mult(V1,V2)) -> U51(isBin(V1),V2), isBin(plus(V1,V2)) -> U61(isBin(V1),V2), isBin(prod(V1)) -> U71(isBag(V1)), isBin(sum(V1)) -> U81(isBag(V1)), mult(z,X) -> U91(isBin(X)), mult(0(X),Y) -> U101(isBin(X),X,Y), mult(1(X),Y) -> U111(isBin(X),X,Y), plus(z,X) -> U121(isBin(X),X), plus(0(X),0(Y)) -> U131(isBin(X),X,Y), plus(0(X),1(Y)) -> U141(isBin(X),X,Y), plus(1(X),1(Y)) -> U151(isBin(X),X,Y), prod(empty) -> 1(z), prod(singl(X)) -> U161(isBin(X),X), prod(union(A,B)) -> U171(isBag(A),A,B), sum(empty) -> 0(z), sum(singl(X)) -> U181(isBin(X),X), sum(union(A,B)) -> U191(isBag(A),A,B) } (55 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: {} 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) -> z } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U81(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U71(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U62(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U52(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U41(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U31(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: { 0(z) -> z } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U121(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U22(tt) -> tt } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U11(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: { union(empty,V_4) -> V_4, union(empty,V_4) -> V_4 } (2 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U181(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U161(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U61(tt,V_3) -> U62(isBin(V_3)), isBin(z) -> tt, isBin(0(V_2)) -> U31(isBin(V_2)), isBin(1(V_2)) -> U41(isBin(V_2)), isBin(mult(V_2,V_3)) -> U51(isBin(V_2),V_3), isBin(plus(V_2,V_3)) -> U61(isBin(V_2),V_3), isBin(prod(V_2)) -> U71(isBag(V_2)), isBin(sum(V_2)) -> U81(isBag(V_2)), U151(tt,V_4,V_5) -> U152(isBin(V_5),V_4,V_5), plus(z,V_4) -> U121(isBin(V_4),V_4), plus(0(V_4),0(V_5)) -> U131(isBin(V_4),V_4,V_5), plus(0(V_4),1(V_5)) -> U141(isBin(V_4),V_4,V_5), plus(1(V_4),1(V_5)) -> U151(isBin(V_4),V_4,V_5), U112(tt,V_4,V_5) -> plus(0(mult(V_4,V_5)),V_5), U111(tt,V_4,V_5) -> U112(isBin(V_5),V_4,V_5), mult(1(V_4),V_5) -> U111(isBin(V_4),V_4,V_5), mult(0(V_4),V_5) -> U101(isBin(V_4),V_4,V_5), mult(z,V_4) -> U91(isBin(V_4)), U102(tt,V_4,V_5) -> 0(mult(V_4,V_5)), U101(tt,V_4,V_5) -> U102(isBin(V_5),V_4,V_5), U132(tt,V_4,V_5) -> 0(plus(V_4,V_5)), U131(tt,V_4,V_5) -> U132(isBin(V_5),V_4,V_5), U142(tt,V_4,V_5) -> 1(plus(V_4,V_5)), U141(tt,V_4,V_5) -> U142(isBin(V_5),V_4,V_5), U152(tt,V_4,V_5) -> 0(plus(1(z),V_4,V_5)), isBag(union(V_2,V_3)) -> U21(isBag(V_2),V_3), isBag(singl(V_2)) -> U11(isBin(V_2)), isBag(empty) -> tt, U21(tt,V_3) -> U22(isBag(V_3)), prod(union(V_0,V_1)) -> U171(isBag(V_0),V_0,V_1), prod(singl(V_4)) -> U161(isBin(V_4),V_4), prod(empty) -> 1(z), U172(tt,V_0,V_1) -> mult(prod(V_0),prod(V_1)), U171(tt,V_0,V_1) -> U172(isBag(V_1),V_0,V_1), sum(empty) -> 0(z), sum(singl(V_4)) -> U181(isBin(V_4),V_4), sum(union(V_0,V_1)) -> U191(isBag(V_0),V_0,V_1), U192(tt,V_0,V_1) -> plus(sum(V_0),sum(V_1)), U191(tt,V_0,V_1) -> U192(isBag(V_1),V_0,V_1), U51(tt,V_3) -> U52(isBin(V_3)) } (40 rules) The dependency graph is (1 nodes) Checking each of the 5 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (58 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = 0; [1](X0) = 0; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 2; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2 + X1; [U172](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = 0; [U141](X0,X1,X2) = 0; [U142](X0,X1,X2) = 0; [U131](X0,X1,X2) = 0; [U132](X0,X1,X2) = 0; [U101](X0,X1,X2) = 0; [U102](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U111](X0,X1,X2) = X2; [U112](X0,X1,X2) = X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = 0; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U171`](X0,X1,X2) = 2*X2 + 2*X1 + 2; ['U172`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['prod`](X0) = 2*X0; Checking component 2 Trying simple graph criterion. Trying to solve the following constraints: (65 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: (65 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; [U62](X0) = 0; [z] = 0; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 1; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1; [U132](X0,X1,X2) = X2 + X1; [U101](X0,X1,X2) = X2*X1 + X2 + X1; [U102](X0,X1,X2) = X2*X1 + X2 + X1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 1; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U101`](X0,X1,X2) = X2*X1 + X2 + X1; ['U102`](X0,X1,X2) = X2*X1 + X2 + X1; ['U111`](X0,X1,X2) = X2*X1 + X2 + X1 + 1; ['U112`](X0,X1,X2) = X2*X1 + X2 + X1 + 1; The dependency graph is (30 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (60 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: (60 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; [U62](X0) = 0; [z] = 0; [0](X0) = X0 + 1; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [U102](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U101`](X0,X1,X2) = X2*X1 + X2 + X1; ['U102`](X0,X1,X2) = X2*X1 + X2 + X1; The dependency graph is (30 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (56 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = 0; [1](X0) = 0; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 1; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2 + X1 + 1; [U172](X0,X1,X2) = X2 + X1 + 1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = 0; [U141](X0,X1,X2) = 0; [U142](X0,X1,X2) = 0; [U131](X0,X1,X2) = 0; [U132](X0,X1,X2) = 0; [U101](X0,X1,X2) = 0; [U102](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0 + 1; [U111](X0,X1,X2) = X2; [U112](X0,X1,X2) = X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = 0; [isBin](X0) = 0; [U61](X0,X1) = 0; Checking component 3 Trying simple graph criterion. Trying to solve the following constraints: (58 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = 0; [1](X0) = 0; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 2; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2 + X1; [U172](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = 0; [U141](X0,X1,X2) = 0; [U142](X0,X1,X2) = 0; [U131](X0,X1,X2) = 0; [U132](X0,X1,X2) = 0; [U101](X0,X1,X2) = 0; [U102](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U111](X0,X1,X2) = X2; [U112](X0,X1,X2) = X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = 0; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U191`](X0,X1,X2) = 2*X2 + 2*X1 + 2; ['U192`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['sum`](X0) = 2*X0; Checking component 4 Trying simple graph criterion. Trying to solve the following constraints: (70 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: (70 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; [U62](X0) = 0; [z] = 0; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1; [U172](X0,X1,X2) = X2*X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 1; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1; [U132](X0,X1,X2) = X2 + X1; [U101](X0,X1,X2) = X2*X1; [U102](X0,X1,X2) = X2*X1; [mult](X0,X1) = X1*X0; [U111](X0,X1,X2) = X2*X1 + X2; [U112](X0,X1,X2) = X2*X1 + X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 1; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U152`](X0,X1,X2) = X2 + X1 + 1; ['U141`](X0,X1,X2) = X2 + X1; ['U142`](X0,X1,X2) = X2 + X1; ['U131`](X0,X1,X2) = X2 + X1; ['U132`](X0,X1,X2) = X2 + X1; ['U151`](X0,X1,X2) = X2 + X1 + 2; The dependency graph is (22 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (61 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: (61 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; [U62](X0) = 0; [z] = 1; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 1; [empty] = 2; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1; [U132](X0,X1,X2) = X2 + X1; [U101](X0,X1,X2) = X2*X1 + X2 + X1; [U102](X0,X1,X2) = X2*X1 + X2 + X1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U131`](X0,X1,X2) = X2 + X1; ['U132`](X0,X1,X2) = X2 + X1; The dependency graph is (27 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (60 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: (60 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; [U62](X0) = 0; [z] = 0; [0](X0) = X0 + 1; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [U102](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U131`](X0,X1,X2) = X2 + X1; ['U132`](X0,X1,X2) = X2 + X1; The dependency graph is (27 nodes) Checking each of the 0 strongly connected components : Checking component 5 Trying simple graph criterion. Trying to solve the following constraints: (68 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: (68 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Time out for these parameters. Search parameters: simple polynomials, coefficient bound is 3. Solution found for these constraints: [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1 + 1; [U192](X0,X1,X2) = X2 + X1 + 1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 3; [U141](X0,X1,X2) = X2 + X1 + 2; [U142](X0,X1,X2) = X2 + X1 + 2; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + X2 + X1; [U102](X0,X1,X2) = X2*X1 + X2 + X1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [plus](X0,X1) = X1 + X0 + 1; [U151](X0,X1,X2) = X2 + X1 + 3; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U51`](X0,X1) = X1; ['U21`](X0,X1) = X1; ['isBag`](X0) = X0; ['isBin`](X0) = X0; ['U61`](X0,X1) = X1 + 1; 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: (61 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; [U62](X0) = 0; [z] = 0; [0](X0) = X0 + 1; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U11](X0) = 0; [singl](X0) = X0 + 2; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; [U172](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; [U102](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; [mult](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U111](X0,X1,X2) = X2*X1 + 3*X2 + 2*X1 + 3; [U112](X0,X1,X2) = X2*X1 + 3*X2 + 2*X1 + 3; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U51`](X0,X1) = X1 + 2; ['isBag`](X0) = X0; ['isBin`](X0) = X0 + 1; 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 {} 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 { U91(tt) -> z } (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 { U81(tt) -> tt } (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 { U71(tt) -> tt } (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 { U62(tt) -> tt } (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 { U52(tt) -> tt } (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 { U41(tt) -> tt } (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) -> tt } (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 { 0(z) -> z } (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 { U121(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 { U22(tt) -> tt } (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 { U11(tt) -> tt } (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 { union(empty,V_4) -> V_4, union(empty,V_4) -> V_4 } (2 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 { U181(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 { U161(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 { U61(tt,V_3) -> U62(isBin(V_3)), isBin(z) -> tt, isBin(0(V_2)) -> U31(isBin(V_2)), isBin(1(V_2)) -> U41(isBin(V_2)), isBin(mult(V_2,V_3)) -> U51(isBin(V_2),V_3), isBin(plus(V_2,V_3)) -> U61(isBin(V_2),V_3), isBin(prod(V_2)) -> U71(isBag(V_2)), isBin(sum(V_2)) -> U81(isBag(V_2)), U151(tt,V_4,V_5) -> U152(isBin(V_5),V_4,V_5), plus(z,V_4) -> U121(isBin(V_4),V_4), plus(0(V_4),0(V_5)) -> U131(isBin(V_4),V_4,V_5), plus(0(V_4),1(V_5)) -> U141(isBin(V_4),V_4,V_5), plus(1(V_4),1(V_5)) -> U151(isBin(V_4),V_4,V_5), U112(tt,V_4,V_5) -> plus(0(mult(V_4,V_5)),V_5), U111(tt,V_4,V_5) -> U112(isBin(V_5),V_4,V_5), mult(1(V_4),V_5) -> U111(isBin(V_4),V_4,V_5), mult(0(V_4),V_5) -> U101(isBin(V_4),V_4,V_5), mult(z,V_4) -> U91(isBin(V_4)), U102(tt,V_4,V_5) -> 0(mult(V_4,V_5)), U101(tt,V_4,V_5) -> U102(isBin(V_5),V_4,V_5), U132(tt,V_4,V_5) -> 0(plus(V_4,V_5)), U131(tt,V_4,V_5) -> U132(isBin(V_5),V_4,V_5), U142(tt,V_4,V_5) -> 1(plus(V_4,V_5)), U141(tt,V_4,V_5) -> U142(isBin(V_5),V_4,V_5), U152(tt,V_4,V_5) -> 0(plus(1(z),V_4,V_5)), isBag(union(V_2,V_3)) -> U21(isBag(V_2),V_3), isBag(singl(V_2)) -> U11(isBin(V_2)), isBag(empty) -> tt, U21(tt,V_3) -> U22(isBag(V_3)), prod(union(V_0,V_1)) -> U171(isBag(V_0),V_0,V_1), prod(singl(V_4)) -> U161(isBin(V_4),V_4), prod(empty) -> 1(z), U172(tt,V_0,V_1) -> mult(prod(V_0),prod(V_1)), U171(tt,V_0,V_1) -> U172(isBag(V_1),V_0,V_1), sum(empty) -> 0(z), sum(singl(V_4)) -> U181(isBin(V_4),V_4), sum(union(V_0,V_1)) -> U191(isBag(V_0),V_0,V_1), U192(tt,V_0,V_1) -> plus(sum(V_0),sum(V_1)), U191(tt,V_0,V_1) -> U192(isBag(V_1),V_0,V_1), U51(tt,V_3) -> U52(isBin(V_3)) } (40 rules) is CE-terminating by criterion with marks except on AC-symbols, and with graph; the dependency graph has 5 strongly connected components: component 1 is 0: 'U51`(tt,V_3) ; 'isBin`(V_3) 17: 'U21`(tt,V_3) ; 'isBag`(V_3) 18: 'isBag`(singl(V_2)) ; 'isBin`(V_2) 19: 'isBag`(union(V_2,V_3)) ; 'isBag`(V_2) 20: 'isBag`(union(V_2,V_3)) ; 'U21`(isBag(V_2),V_3) 68: 'isBin`(sum(V_2)) ; 'isBag`(V_2) 69: 'isBin`(prod(V_2)) ; 'isBag`(V_2) 70: 'isBin`(plus(V_2,V_3)) ; 'isBin`(V_2) 71: 'isBin`(plus(V_2,V_3)) ; 'U61`(isBin(V_2),V_3) 72: 'isBin`(mult(V_2,V_3)) ; 'isBin`(V_2) 73: 'isBin`(mult(V_2,V_3)) ; 'U51`(isBin(V_2),V_3) 74: 'isBin`(1(V_2)) ; 'isBin`(V_2) 75: 'isBin`(0(V_2)) ; 'isBin`(V_2) 76: 'U61`(tt,V_3) ; 'isBin`(V_3) 0 -> 68, 0 -> 69, 0 -> 70, 0 -> 71, 0 -> 72, 0 -> 73, 0 -> 74, 0 -> 75, 17 -> 18, 17 -> 19, 17 -> 20, 18 -> 68, 18 -> 69, 18 -> 70, 18 -> 71, 18 -> 72, 18 -> 73, 18 -> 74, 18 -> 75, 19 -> 18, 19 -> 19, 19 -> 20, 20 -> 17, 68 -> 18, 68 -> 19, 68 -> 20, 69 -> 18, 69 -> 19, 69 -> 20, 70 -> 68, 70 -> 69, 70 -> 70, 70 -> 71, 70 -> 72, 70 -> 73, 70 -> 74, 70 -> 75, 71 -> 76, 72 -> 68, 72 -> 69, 72 -> 70, 72 -> 71, 72 -> 72, 72 -> 73, 72 -> 74, 72 -> 75, 73 -> 0, 74 -> 68, 74 -> 69, 74 -> 70, 74 -> 71, 74 -> 72, 74 -> 73, 74 -> 74, 74 -> 75, 75 -> 68, 75 -> 69, 75 -> 70, 75 -> 71, 75 -> 72, 75 -> 73, 75 -> 74, 75 -> 75, 76 -> 68, 76 -> 69, 76 -> 70, 76 -> 71, 76 -> 72, 76 -> 73, 76 -> 74, 76 -> 75, On this component, with the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1 + 1; [U192](X0,X1,X2) = X2 + X1 + 1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 3; [U141](X0,X1,X2) = X2 + X1 + 2; [U142](X0,X1,X2) = X2 + X1 + 2; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + X2 + X1; [U102](X0,X1,X2) = X2*X1 + X2 + X1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [plus](X0,X1) = X1 + X0 + 1; [U151](X0,X1,X2) = X2 + X1 + 3; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U51`](X0,X1) = X1; ['U21`](X0,X1) = X1; ['isBag`](X0) = X0; ['isBin`](X0) = X0; ['U61`](X0,X1) = X1 + 1; the subgraph of pairs that are only weakly decreasing has one strongly connected component: 0: 'U51`(tt,V_3) ; 'isBin`(V_3) 18: 'isBag`(singl(V_2)) ; 'isBin`(V_2) 68: 'isBin`(sum(V_2)) ; 'isBag`(V_2) 69: 'isBin`(prod(V_2)) ; 'isBag`(V_2) 72: 'isBin`(mult(V_2,V_3)) ; 'isBin`(V_2) 73: 'isBin`(mult(V_2,V_3)) ; 'U51`(isBin(V_2),V_3) 75: 'isBin`(0(V_2)) ; 'isBin`(V_2) 0 -> 68, 0 -> 69, 0 -> 72, 0 -> 73, 0 -> 75, 18 -> 68, 18 -> 69, 18 -> 72, 18 -> 73, 18 -> 75, 68 -> 18, 69 -> 18, 72 -> 68, 72 -> 69, 72 -> 72, 72 -> 73, 72 -> 75, 73 -> 0, 75 -> 68, 75 -> 69, 75 -> 72, 75 -> 73, 75 -> 75, On this component, the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0 + 1; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U11](X0) = 0; [singl](X0) = X0 + 2; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; [U172](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; [U102](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; [mult](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U111](X0,X1,X2) = X2*X1 + 3*X2 + 2*X1 + 3; [U112](X0,X1,X2) = X2*X1 + 3*X2 + 2*X1 + 3; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U51`](X0,X1) = X1 + 2; ['isBag`](X0) = X0; ['isBin`](X0) = X0 + 1; strictly decreases on every cycle component 2 is 21: 'U152`(tt,V_4,V_5) ; plus(1(z),V_4,V_5) 23: 'U141`(tt,V_4,V_5) ; 'U142`(isBin(V_5),V_4,V_5) 24: 'U142`(tt,V_4,V_5) ; plus(V_4,V_5) 26: 'U131`(tt,V_4,V_5) ; 'U132`(isBin(V_5),V_4,V_5) 27: 'U132`(tt,V_4,V_5) ; plus(V_4,V_5) 49: plus(1(V_4),1(V_5),V_0) ; 'U151`(isBin(V_4),V_4,V_5) 50: plus(1(V_4),1(V_5),V_0) ; plus(U151(isBin(V_4),V_4,V_5),V_0) 52: plus(1(V_4),1(V_5)) ; 'U151`(isBin(V_4),V_4,V_5) 54: plus(0(V_4),1(V_5),V_0) ; 'U141`(isBin(V_4),V_4,V_5) 55: plus(0(V_4),1(V_5),V_0) ; plus(U141(isBin(V_4),V_4,V_5),V_0) 57: plus(0(V_4),1(V_5)) ; 'U141`(isBin(V_4),V_4,V_5) 59: plus(0(V_4),0(V_5),V_0) ; 'U131`(isBin(V_4),V_4,V_5) 60: plus(0(V_4),0(V_5),V_0) ; plus(U131(isBin(V_4),V_4,V_5),V_0) 62: plus(0(V_4),0(V_5)) ; 'U131`(isBin(V_4),V_4,V_5) 64: plus(z,V_0,V_4) ; plus(U121(isBin(V_4),V_4),V_0) 67: 'U151`(tt,V_4,V_5) ; 'U152`(isBin(V_5),V_4,V_5) 21 -> 49, 21 -> 50, 21 -> 52, 21 -> 54, 21 -> 55, 21 -> 57, 21 -> 59, 21 -> 60, 21 -> 62, 21 -> 64, 23 -> 24, 24 -> 49, 24 -> 50, 24 -> 52, 24 -> 54, 24 -> 55, 24 -> 57, 24 -> 59, 24 -> 60, 24 -> 62, 24 -> 64, 26 -> 27, 27 -> 49, 27 -> 50, 27 -> 52, 27 -> 54, 27 -> 55, 27 -> 57, 27 -> 59, 27 -> 60, 27 -> 62, 27 -> 64, 49 -> 67, 50 -> 49, 50 -> 50, 50 -> 52, 50 -> 54, 50 -> 55, 50 -> 57, 50 -> 59, 50 -> 60, 50 -> 62, 50 -> 64, 52 -> 67, 54 -> 23, 55 -> 49, 55 -> 50, 55 -> 52, 55 -> 54, 55 -> 55, 55 -> 57, 55 -> 59, 55 -> 60, 55 -> 62, 55 -> 64, 57 -> 23, 59 -> 26, 60 -> 49, 60 -> 50, 60 -> 52, 60 -> 54, 60 -> 55, 60 -> 57, 60 -> 59, 60 -> 60, 60 -> 62, 60 -> 64, 62 -> 26, 64 -> 49, 64 -> 50, 64 -> 52, 64 -> 54, 64 -> 55, 64 -> 57, 64 -> 59, 64 -> 60, 64 -> 62, 64 -> 64, 67 -> 21, On this component, with the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1; [U172](X0,X1,X2) = X2*X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 1; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1; [U132](X0,X1,X2) = X2 + X1; [U101](X0,X1,X2) = X2*X1; [U102](X0,X1,X2) = X2*X1; [mult](X0,X1) = X1*X0; [U111](X0,X1,X2) = X2*X1 + X2; [U112](X0,X1,X2) = X2*X1 + X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 1; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U152`](X0,X1,X2) = X2 + X1 + 1; ['U141`](X0,X1,X2) = X2 + X1; ['U142`](X0,X1,X2) = X2 + X1; ['U131`](X0,X1,X2) = X2 + X1; ['U132`](X0,X1,X2) = X2 + X1; ['U151`](X0,X1,X2) = X2 + X1 + 2; the subgraph of pairs that are only weakly decreasing has one strongly connected component: 26: 'U131`(tt,V_4,V_5) ; 'U132`(isBin(V_5),V_4,V_5) 27: 'U132`(tt,V_4,V_5) ; plus(V_4,V_5) 55: plus(0(V_4),1(V_5),V_0) ; plus(U141(isBin(V_4),V_4,V_5),V_0) 59: plus(0(V_4),0(V_5),V_0) ; 'U131`(isBin(V_4),V_4,V_5) 60: plus(0(V_4),0(V_5),V_0) ; plus(U131(isBin(V_4),V_4,V_5),V_0) 62: plus(0(V_4),0(V_5)) ; 'U131`(isBin(V_4),V_4,V_5) 64: plus(z,V_0,V_4) ; plus(U121(isBin(V_4),V_4),V_0) 26 -> 27, 27 -> 55, 27 -> 59, 27 -> 60, 27 -> 62, 27 -> 64, 55 -> 55, 55 -> 59, 55 -> 60, 55 -> 62, 55 -> 64, 59 -> 26, 60 -> 55, 60 -> 59, 60 -> 60, 60 -> 62, 60 -> 64, 62 -> 26, 64 -> 55, 64 -> 59, 64 -> 60, 64 -> 62, 64 -> 64, On this component, with the interpretation [tt] = 0; [U62](X0) = 0; [z] = 1; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 1; [empty] = 2; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1; [U132](X0,X1,X2) = X2 + X1; [U101](X0,X1,X2) = X2*X1 + X2 + X1; [U102](X0,X1,X2) = X2*X1 + X2 + X1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U131`](X0,X1,X2) = X2 + X1; ['U132`](X0,X1,X2) = X2 + X1; the subgraph of pairs that are only weakly decreasing has one strongly connected component: 26: 'U131`(tt,V_4,V_5) ; 'U132`(isBin(V_5),V_4,V_5) 27: 'U132`(tt,V_4,V_5) ; plus(V_4,V_5) 55: plus(0(V_4),1(V_5),V_0) ; plus(U141(isBin(V_4),V_4,V_5),V_0) 59: plus(0(V_4),0(V_5),V_0) ; 'U131`(isBin(V_4),V_4,V_5) 60: plus(0(V_4),0(V_5),V_0) ; plus(U131(isBin(V_4),V_4,V_5),V_0) 62: plus(0(V_4),0(V_5)) ; 'U131`(isBin(V_4),V_4,V_5) 26 -> 27, 27 -> 55, 27 -> 59, 27 -> 60, 27 -> 62, 55 -> 55, 55 -> 59, 55 -> 60, 55 -> 62, 59 -> 26, 60 -> 55, 60 -> 59, 60 -> 60, 60 -> 62, 62 -> 26, On this component, with the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0 + 1; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [U102](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U131`](X0,X1,X2) = X2 + X1; ['U132`](X0,X1,X2) = X2 + X1; the subgraph of pairs that are only weakly decreasing has no strongly connected components. component 3 is 2: 'U191`(tt,V_0,V_1) ; 'U192`(isBag(V_1),V_0,V_1) 3: 'U192`(tt,V_0,V_1) ; 'sum`(V_1) 4: 'U192`(tt,V_0,V_1) ; 'sum`(V_0) 7: 'sum`(union(V_0,V_1)) ; 'U191`(isBag(V_0),V_0,V_1) 2 -> 3, 2 -> 4, 3 -> 7, 4 -> 7, 7 -> 2, On this component, the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = 0; [1](X0) = 0; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 2; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2 + X1; [U172](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = 0; [U141](X0,X1,X2) = 0; [U142](X0,X1,X2) = 0; [U131](X0,X1,X2) = 0; [U132](X0,X1,X2) = 0; [U101](X0,X1,X2) = 0; [U102](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U111](X0,X1,X2) = X2; [U112](X0,X1,X2) = X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = 0; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U191`](X0,X1,X2) = 2*X2 + 2*X1 + 2; ['U192`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['sum`](X0) = 2*X0; strictly decreases on every cycle component 4 is 29: 'U101`(tt,V_4,V_5) ; 'U102`(isBin(V_5),V_4,V_5) 30: 'U102`(tt,V_4,V_5) ; mult(V_4,V_5) 32: mult(z,V_0,V_4) ; mult(U91(isBin(V_4)),V_0) 35: mult(0(V_4),V_0,V_5) ; 'U101`(isBin(V_4),V_4,V_5) 36: mult(0(V_4),V_0,V_5) ; mult(U101(isBin(V_4),V_4,V_5),V_0) 38: mult(0(V_4),V_5) ; 'U101`(isBin(V_4),V_4,V_5) 40: mult(1(V_4),V_0,V_5) ; 'U111`(isBin(V_4),V_4,V_5) 41: mult(1(V_4),V_0,V_5) ; mult(U111(isBin(V_4),V_4,V_5),V_0) 43: mult(1(V_4),V_5) ; 'U111`(isBin(V_4),V_4,V_5) 45: 'U111`(tt,V_4,V_5) ; 'U112`(isBin(V_5),V_4,V_5) 46: 'U112`(tt,V_4,V_5) ; mult(V_4,V_5) 29 -> 30, 30 -> 32, 30 -> 35, 30 -> 36, 30 -> 38, 30 -> 40, 30 -> 41, 30 -> 43, 32 -> 32, 32 -> 35, 32 -> 36, 32 -> 38, 32 -> 40, 32 -> 41, 32 -> 43, 35 -> 29, 36 -> 32, 36 -> 35, 36 -> 36, 36 -> 38, 36 -> 40, 36 -> 41, 36 -> 43, 38 -> 29, 40 -> 45, 41 -> 32, 41 -> 35, 41 -> 36, 41 -> 38, 41 -> 40, 41 -> 41, 41 -> 43, 43 -> 45, 45 -> 46, 46 -> 32, 46 -> 35, 46 -> 36, 46 -> 38, 46 -> 40, 46 -> 41, 46 -> 43, On this component, with the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 1; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1; [U132](X0,X1,X2) = X2 + X1; [U101](X0,X1,X2) = X2*X1 + X2 + X1; [U102](X0,X1,X2) = X2*X1 + X2 + X1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 1; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U101`](X0,X1,X2) = X2*X1 + X2 + X1; ['U102`](X0,X1,X2) = X2*X1 + X2 + X1; ['U111`](X0,X1,X2) = X2*X1 + X2 + X1 + 1; ['U112`](X0,X1,X2) = X2*X1 + X2 + X1 + 1; the subgraph of pairs that are only weakly decreasing has one strongly connected component: 29: 'U101`(tt,V_4,V_5) ; 'U102`(isBin(V_5),V_4,V_5) 30: 'U102`(tt,V_4,V_5) ; mult(V_4,V_5) 32: mult(z,V_0,V_4) ; mult(U91(isBin(V_4)),V_0) 35: mult(0(V_4),V_0,V_5) ; 'U101`(isBin(V_4),V_4,V_5) 36: mult(0(V_4),V_0,V_5) ; mult(U101(isBin(V_4),V_4,V_5),V_0) 38: mult(0(V_4),V_5) ; 'U101`(isBin(V_4),V_4,V_5) 29 -> 30, 30 -> 32, 30 -> 35, 30 -> 36, 30 -> 38, 32 -> 32, 32 -> 35, 32 -> 36, 32 -> 38, 35 -> 29, 36 -> 32, 36 -> 35, 36 -> 36, 36 -> 38, 38 -> 29, On this component, with the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = X0 + 1; [1](X0) = X0 + 1; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2*X1 + X2 + X1; [U172](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = X2 + X1 + 2; [U141](X0,X1,X2) = X2 + X1 + 1; [U142](X0,X1,X2) = X2 + X1 + 1; [U131](X0,X1,X2) = X2 + X1 + 1; [U132](X0,X1,X2) = X2 + X1 + 1; [U101](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [U102](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [mult](X0,X1) = X1*X0 + X1 + X0; [U111](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U112](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = X2 + X1 + 2; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U101`](X0,X1,X2) = X2*X1 + X2 + X1; ['U102`](X0,X1,X2) = X2*X1 + X2 + X1; the subgraph of pairs that are only weakly decreasing has one strongly connected component: 32: mult(z,V_0,V_4) ; mult(U91(isBin(V_4)),V_0) 36: mult(0(V_4),V_0,V_5) ; mult(U101(isBin(V_4),V_4,V_5),V_0) 32 -> 32, 32 -> 36, 36 -> 32, 36 -> 36, On this component, the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = 0; [1](X0) = 0; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 1; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2 + X1 + 1; [U172](X0,X1,X2) = X2 + X1 + 1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = 0; [U141](X0,X1,X2) = 0; [U142](X0,X1,X2) = 0; [U131](X0,X1,X2) = 0; [U132](X0,X1,X2) = 0; [U101](X0,X1,X2) = 0; [U102](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0 + 1; [U111](X0,X1,X2) = X2; [U112](X0,X1,X2) = X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = 0; [isBin](X0) = 0; [U61](X0,X1) = 0; strictly decreases on every cycle component 5 is 10: 'U171`(tt,V_0,V_1) ; 'U172`(isBag(V_1),V_0,V_1) 11: 'U172`(tt,V_0,V_1) ; 'prod`(V_1) 12: 'U172`(tt,V_0,V_1) ; 'prod`(V_0) 16: 'prod`(union(V_0,V_1)) ; 'U171`(isBag(V_0),V_0,V_1) 10 -> 11, 10 -> 12, 11 -> 16, 12 -> 16, 16 -> 10, On this component, the interpretation [tt] = 0; [U62](X0) = 0; [z] = 0; [0](X0) = 0; [1](X0) = 0; [U31](X0) = 0; [U41](X0) = 0; [U71](X0) = 0; [U81](X0) = 0; [U121](X0,X1) = X1; [U91](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 2; [U11](X0) = 0; [singl](X0) = X0; [U22](X0) = 0; [U161](X0,X1) = X1; [U181](X0,X1) = X1; [U52](X0) = 0; [U51](X0,X1) = 0; [U191](X0,X1,X2) = X2 + X1; [U192](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [U171](X0,X1,X2) = X2 + X1; [U172](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U21](X0,X1) = 0; [isBag](X0) = 0; [U152](X0,X1,X2) = 0; [U141](X0,X1,X2) = 0; [U142](X0,X1,X2) = 0; [U131](X0,X1,X2) = 0; [U132](X0,X1,X2) = 0; [U101](X0,X1,X2) = 0; [U102](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U111](X0,X1,X2) = X2; [U112](X0,X1,X2) = X2; [plus](X0,X1) = X1 + X0; [U151](X0,X1,X2) = 0; [isBin](X0) = 0; [U61](X0,X1) = 0; ['U171`](X0,X1,X2) = 2*X2 + 2*X1 + 2; ['U172`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['prod`](X0) = 2*X0; strictly decreases on every cycle - : unit = () Quitting. Standard error: