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) -> X, U11(tt) -> z, U111(tt,A,B) -> plus(sum(A),sum(B)), U21(tt,X,Y) -> 0(mult(X,Y)), U31(tt,X,Y) -> plus(0(mult(X,Y)),Y), U41(tt,X) -> X, U51(tt,X,Y) -> 0(plus(X,Y)), U61(tt,X,Y) -> 1(plus(X,Y)), U71(tt,X,Y) -> 0(plus(1(z),X,Y)), U81(tt,X) -> X, U91(tt,A,B) -> mult(prod(A),prod(B)), and(tt,X) -> X, isBag(empty) -> tt, isBag(singl(V1)) -> isBin(V1), isBag(union(V1,V2)) -> and(isBag(V1),isBag(V2)), isBin(z) -> tt, isBin(0(V1)) -> isBin(V1), isBin(1(V1)) -> isBin(V1), isBin(mult(V1,V2)) -> and(isBin(V1),isBin(V2)), isBin(plus(V1,V2)) -> and(isBin(V1),isBin(V2)), isBin(prod(V1)) -> isBag(V1), isBin(sum(V1)) -> isBag(V1), mult(z,X) -> U11(isBin(X)), mult(0(X),Y) -> U21(and(isBin(X),isBin(Y)),X,Y), mult(1(X),Y) -> U31(and(isBin(X),isBin(Y)),X,Y), plus(z,X) -> U41(isBin(X),X), plus(0(X),0(Y)) -> U51(and(isBin(X),isBin(Y)),X,Y), plus(0(X),1(Y)) -> U61(and(isBin(X),isBin(Y)),X,Y), plus(1(X),1(Y)) -> U71(and(isBin(X),isBin(Y)),X,Y), prod(empty) -> 1(z), prod(singl(X)) -> U81(isBin(X),X), prod(union(A,B)) -> U91(and(isBag(A),isBag(B)),A,B), sum(empty) -> 0(z), sum(singl(X)) -> U101(isBin(X),X), sum(union(A,B)) -> U111(and(isBag(A),isBag(B)),A,B) } (38 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: { and(tt,V_4) -> V_4 } (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: {} 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: { U41(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U11(tt) -> z } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U81(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { U101(tt,V_4) -> V_4 } (1 rules) The dependency graph is (0 nodes) Checking each of the 0 strongly connected components : Checking module: { isBin(z) -> tt, isBin(0(V_2)) -> isBin(V_2), isBin(1(V_2)) -> isBin(V_2), isBin(mult(V_2,V_3)) -> and(isBin(V_2),isBin(V_3)), isBin(plus(V_2,V_3)) -> and(isBin(V_2),isBin(V_3)), isBin(prod(V_2)) -> isBag(V_2), isBin(sum(V_2)) -> isBag(V_2), plus(1(V_4),1(V_5)) -> U71(and(isBin(V_4),isBin(V_5)),V_4,V_5), plus(0(V_4),1(V_5)) -> U61(and(isBin(V_4),isBin(V_5)),V_4,V_5), plus(0(V_4),0(V_5)) -> U51(and(isBin(V_4),isBin(V_5)),V_4,V_5), plus(z,V_4) -> U41(isBin(V_4),V_4), U51(tt,V_4,V_5) -> 0(plus(V_4,V_5)), U61(tt,V_4,V_5) -> 1(plus(V_4,V_5)), U71(tt,V_4,V_5) -> 0(plus(1(z),V_4,V_5)), mult(1(V_4),V_5) -> U31(and(isBin(V_4),isBin(V_5)),V_4,V_5), mult(0(V_4),V_5) -> U21(and(isBin(V_4),isBin(V_5)),V_4,V_5), mult(z,V_4) -> U11(isBin(V_4)), U21(tt,V_4,V_5) -> 0(mult(V_4,V_5)), U31(tt,V_4,V_5) -> plus(0(mult(V_4,V_5)),V_5), isBag(empty) -> tt, isBag(singl(V_2)) -> isBin(V_2), isBag(union(V_2,V_3)) -> and(isBag(V_2),isBag(V_3)), sum(union(V_0,V_1)) -> U111(and(isBag(V_0),isBag(V_1)),V_0,V_1), sum(singl(V_4)) -> U101(isBin(V_4),V_4), sum(empty) -> 0(z), U111(tt,V_0,V_1) -> plus(sum(V_0),sum(V_1)), prod(union(V_0,V_1)) -> U91(and(isBag(V_0),isBag(V_1)),V_0,V_1), prod(singl(V_4)) -> U81(isBin(V_4),V_4), prod(empty) -> 1(z), U91(tt,V_0,V_1) -> mult(prod(V_0),prod(V_1)) } (30 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: (40 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [z] = 0; [0](X0) = 0; [tt] = 0; [1](X0) = 0; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 1; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2; [U21](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U71](X0,X1,X2) = 0; [U61](X0,X1,X2) = 0; [U51](X0,X1,X2) = 0; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U111`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['sum`](X0) = 2*X0; Checking component 2 Trying simple graph criterion. Trying to solve the following constraints: (40 termination constraints) Search parameters: linear polynomials, coefficient bound is 2. Solution found for these constraints: [z] = 0; [0](X0) = 0; [tt] = 0; [1](X0) = 0; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 1; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2; [U21](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U71](X0,X1,X2) = 0; [U61](X0,X1,X2) = 0; [U51](X0,X1,X2) = 0; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U91`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['prod`](X0) = 2*X0; Checking component 3 Trying simple graph criterion. Trying to solve the following constraints: (46 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: [z] = 0; [0](X0) = X0 + 1; [tt] = 0; [1](X0) = X0 + 1; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2*X1 + 3*X2 + 2*X1 + 3; [U21](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; [mult](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U71](X0,X1,X2) = X2 + X1 + 2; [U61](X0,X1,X2) = X2 + X1 + 1; [U51](X0,X1,X2) = X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U31`](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; ['U21`](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; Checking component 4 Trying simple graph criterion. Trying to solve the following constraints: (50 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: (50 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: [z] = 0; [0](X0) = X0; [tt] = 0; [1](X0) = X0 + 1; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2*X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2*X1 + X2; [U21](X0,X1,X2) = X2*X1; [mult](X0,X1) = X1*X0; [U71](X0,X1,X2) = X2 + X1 + 1; [U61](X0,X1,X2) = X2 + X1 + 1; [U51](X0,X1,X2) = X2 + X1; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U71`](X0,X1,X2) = X2 + X1 + 1; ['U61`](X0,X1,X2) = X2 + X1; ['U51`](X0,X1,X2) = X2 + X1; The dependency graph is (38 nodes) Checking each of the 1 strongly connected components : Checking component 1 Trying simple graph criterion. Trying to solve the following constraints: (43 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: [z] = 1; [0](X0) = X0 + 1; [tt] = 2; [1](X0) = X0 + 2; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 1; [empty] = 3; [union](X0,X1) = X1*X0 + X1 + X0; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 2; [U31](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U21](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [mult](X0,X1) = X1*X0 + X1 + X0; [U71](X0,X1,X2) = X2 + X1 + 2*X0; [U61](X0,X1,X2) = X2 + X1 + 2; [U51](X0,X1,X2) = X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [isBin](X0) = 2; ['U51`](X0,X1,X2) = X2 + X1 + 1; Checking component 5 Trying simple graph criterion. Trying to solve the following constraints: (48 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: [z] = 0; [0](X0) = X0 + 1; [tt] = 2; [1](X0) = X0 + 2; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 2; [union](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; [singl](X0) = X0 + 2; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = 2*X2*X1 + 2*X2 + 2*X1 + 1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1 + 1; [sum](X0) = X0; [isBag](X0) = 2; [U31](X0,X1,X2) = 2*X2*X1 + 3*X2 + 2*X1 + 3; [U21](X0,X1,X2) = 2*X2*X1 + 2*X2 + 2*X1 + 2; [mult](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; [U71](X0,X1,X2) = X2 + X1 + X0 + 3; [U61](X0,X1,X2) = X2 + X1 + 3; [U51](X0,X1,X2) = X2 + X1 + 2; [plus](X0,X1) = X1 + X0 + 1; [isBin](X0) = 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 { and(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 {} 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 {} 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 { U41(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 { U11(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,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 { U101(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 { isBin(z) -> tt, isBin(0(V_2)) -> isBin(V_2), isBin(1(V_2)) -> isBin(V_2), isBin(mult(V_2,V_3)) -> and(isBin(V_2),isBin(V_3)), isBin(plus(V_2,V_3)) -> and(isBin(V_2),isBin(V_3)), isBin(prod(V_2)) -> isBag(V_2), isBin(sum(V_2)) -> isBag(V_2), plus(1(V_4),1(V_5)) -> U71(and(isBin(V_4),isBin(V_5)),V_4,V_5), plus(0(V_4),1(V_5)) -> U61(and(isBin(V_4),isBin(V_5)),V_4,V_5), plus(0(V_4),0(V_5)) -> U51(and(isBin(V_4),isBin(V_5)),V_4,V_5), plus(z,V_4) -> U41(isBin(V_4),V_4), U51(tt,V_4,V_5) -> 0(plus(V_4,V_5)), U61(tt,V_4,V_5) -> 1(plus(V_4,V_5)), U71(tt,V_4,V_5) -> 0(plus(1(z),V_4,V_5)), mult(1(V_4),V_5) -> U31(and(isBin(V_4),isBin(V_5)),V_4,V_5), mult(0(V_4),V_5) -> U21(and(isBin(V_4),isBin(V_5)),V_4,V_5), mult(z,V_4) -> U11(isBin(V_4)), U21(tt,V_4,V_5) -> 0(mult(V_4,V_5)), U31(tt,V_4,V_5) -> plus(0(mult(V_4,V_5)),V_5), isBag(empty) -> tt, isBag(singl(V_2)) -> isBin(V_2), isBag(union(V_2,V_3)) -> and(isBag(V_2),isBag(V_3)), sum(union(V_0,V_1)) -> U111(and(isBag(V_0),isBag(V_1)),V_0,V_1), sum(singl(V_4)) -> U101(isBin(V_4),V_4), sum(empty) -> 0(z), U111(tt,V_0,V_1) -> plus(sum(V_0),sum(V_1)), prod(union(V_0,V_1)) -> U91(and(isBag(V_0),isBag(V_1)),V_0,V_1), prod(singl(V_4)) -> U81(isBin(V_4),V_4), prod(empty) -> 1(z), U91(tt,V_0,V_1) -> mult(prod(V_0),prod(V_1)) } (30 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 14: 'isBag`(union(V_2,V_3)) ; 'isBag`(V_3) 15: 'isBag`(union(V_2,V_3)) ; 'isBag`(V_2) 16: 'isBag`(singl(V_2)) ; 'isBin`(V_2) 64: 'isBin`(sum(V_2)) ; 'isBag`(V_2) 65: 'isBin`(prod(V_2)) ; 'isBag`(V_2) 66: 'isBin`(plus(V_2,V_3)) ; 'isBin`(V_3) 67: 'isBin`(plus(V_2,V_3)) ; 'isBin`(V_2) 68: 'isBin`(mult(V_2,V_3)) ; 'isBin`(V_3) 69: 'isBin`(mult(V_2,V_3)) ; 'isBin`(V_2) 70: 'isBin`(1(V_2)) ; 'isBin`(V_2) 71: 'isBin`(0(V_2)) ; 'isBin`(V_2) 14 -> 14, 14 -> 15, 14 -> 16, 15 -> 14, 15 -> 15, 15 -> 16, 16 -> 64, 16 -> 65, 16 -> 66, 16 -> 67, 16 -> 68, 16 -> 69, 16 -> 70, 16 -> 71, 64 -> 14, 64 -> 15, 64 -> 16, 65 -> 14, 65 -> 15, 65 -> 16, 66 -> 64, 66 -> 65, 66 -> 66, 66 -> 67, 66 -> 68, 66 -> 69, 66 -> 70, 66 -> 71, 67 -> 64, 67 -> 65, 67 -> 66, 67 -> 67, 67 -> 68, 67 -> 69, 67 -> 70, 67 -> 71, 68 -> 64, 68 -> 65, 68 -> 66, 68 -> 67, 68 -> 68, 68 -> 69, 68 -> 70, 68 -> 71, 69 -> 64, 69 -> 65, 69 -> 66, 69 -> 67, 69 -> 68, 69 -> 69, 69 -> 70, 69 -> 71, 70 -> 64, 70 -> 65, 70 -> 66, 70 -> 67, 70 -> 68, 70 -> 69, 70 -> 70, 70 -> 71, 71 -> 64, 71 -> 65, 71 -> 66, 71 -> 67, 71 -> 68, 71 -> 69, 71 -> 70, 71 -> 71, On this component, the interpretation [z] = 0; [0](X0) = X0 + 1; [tt] = 2; [1](X0) = X0 + 2; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 2; [union](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; [singl](X0) = X0 + 2; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = 2*X2*X1 + 2*X2 + 2*X1 + 1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1 + 1; [sum](X0) = X0; [isBag](X0) = 2; [U31](X0,X1,X2) = 2*X2*X1 + 3*X2 + 2*X1 + 3; [U21](X0,X1,X2) = 2*X2*X1 + 2*X2 + 2*X1 + 2; [mult](X0,X1) = 2*X1*X0 + 2*X1 + 2*X0 + 1; [U71](X0,X1,X2) = X2 + X1 + X0 + 3; [U61](X0,X1,X2) = X2 + X1 + 3; [U51](X0,X1,X2) = X2 + X1 + 2; [plus](X0,X1) = X1 + X0 + 1; [isBin](X0) = 2; ['isBag`](X0) = X0; ['isBin`](X0) = X0 + 1; strictly decreases on every cycle component 2 is 37: 'U71`(tt,V_4,V_5) ; plus(1(z),V_4,V_5) 38: 'U61`(tt,V_4,V_5) ; plus(V_4,V_5) 39: 'U51`(tt,V_4,V_5) ; plus(V_4,V_5) 41: plus(z,V_0,V_4) ; plus(U41(isBin(V_4),V_4),V_0) 45: plus(0(V_4),0(V_5),V_0) ; 'U51`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 46: plus(0(V_4),0(V_5),V_0) ; plus(U51(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 49: plus(0(V_4),0(V_5)) ; 'U51`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 52: plus(0(V_4),1(V_5),V_0) ; 'U61`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 53: plus(0(V_4),1(V_5),V_0) ; plus(U61(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 56: plus(0(V_4),1(V_5)) ; 'U61`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 59: plus(1(V_4),1(V_5),V_0) ; 'U71`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 60: plus(1(V_4),1(V_5),V_0) ; plus(U71(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 63: plus(1(V_4),1(V_5)) ; 'U71`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 37 -> 41, 37 -> 45, 37 -> 46, 37 -> 49, 37 -> 52, 37 -> 53, 37 -> 56, 37 -> 59, 37 -> 60, 37 -> 63, 38 -> 41, 38 -> 45, 38 -> 46, 38 -> 49, 38 -> 52, 38 -> 53, 38 -> 56, 38 -> 59, 38 -> 60, 38 -> 63, 39 -> 41, 39 -> 45, 39 -> 46, 39 -> 49, 39 -> 52, 39 -> 53, 39 -> 56, 39 -> 59, 39 -> 60, 39 -> 63, 41 -> 41, 41 -> 45, 41 -> 46, 41 -> 49, 41 -> 52, 41 -> 53, 41 -> 56, 41 -> 59, 41 -> 60, 41 -> 63, 45 -> 39, 46 -> 41, 46 -> 45, 46 -> 46, 46 -> 49, 46 -> 52, 46 -> 53, 46 -> 56, 46 -> 59, 46 -> 60, 46 -> 63, 49 -> 39, 52 -> 38, 53 -> 41, 53 -> 45, 53 -> 46, 53 -> 49, 53 -> 52, 53 -> 53, 53 -> 56, 53 -> 59, 53 -> 60, 53 -> 63, 56 -> 38, 59 -> 37, 60 -> 41, 60 -> 45, 60 -> 46, 60 -> 49, 60 -> 52, 60 -> 53, 60 -> 56, 60 -> 59, 60 -> 60, 60 -> 63, 63 -> 37, On this component, with the interpretation [z] = 0; [0](X0) = X0; [tt] = 0; [1](X0) = X0 + 1; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + X1 + X0; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2*X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2*X1 + X2; [U21](X0,X1,X2) = X2*X1; [mult](X0,X1) = X1*X0; [U71](X0,X1,X2) = X2 + X1 + 1; [U61](X0,X1,X2) = X2 + X1 + 1; [U51](X0,X1,X2) = X2 + X1; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U71`](X0,X1,X2) = X2 + X1 + 1; ['U61`](X0,X1,X2) = X2 + X1; ['U51`](X0,X1,X2) = X2 + X1; the subgraph of pairs that are only weakly decreasing has one strongly connected component: 39: 'U51`(tt,V_4,V_5) ; plus(V_4,V_5) 41: plus(z,V_0,V_4) ; plus(U41(isBin(V_4),V_4),V_0) 45: plus(0(V_4),0(V_5),V_0) ; 'U51`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 46: plus(0(V_4),0(V_5),V_0) ; plus(U51(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 49: plus(0(V_4),0(V_5)) ; 'U51`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 53: plus(0(V_4),1(V_5),V_0) ; plus(U61(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 39 -> 41, 39 -> 45, 39 -> 46, 39 -> 49, 39 -> 53, 41 -> 41, 41 -> 45, 41 -> 46, 41 -> 49, 41 -> 53, 45 -> 39, 46 -> 41, 46 -> 45, 46 -> 46, 46 -> 49, 46 -> 53, 49 -> 39, 53 -> 41, 53 -> 45, 53 -> 46, 53 -> 49, 53 -> 53, On this component, the interpretation [z] = 1; [0](X0) = X0 + 1; [tt] = 2; [1](X0) = X0 + 2; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 1; [empty] = 3; [union](X0,X1) = X1*X0 + X1 + X0; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2*X1 + X2 + X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 2; [U31](X0,X1,X2) = X2*X1 + 2*X2 + X1 + 1; [U21](X0,X1,X2) = X2*X1 + X2 + X1 + 1; [mult](X0,X1) = X1*X0 + X1 + X0; [U71](X0,X1,X2) = X2 + X1 + 2*X0; [U61](X0,X1,X2) = X2 + X1 + 2; [U51](X0,X1,X2) = X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [isBin](X0) = 2; ['U51`](X0,X1,X2) = X2 + X1 + 1; strictly decreases on every cycle component 3 is 17: 'U31`(tt,V_4,V_5) ; mult(V_4,V_5) 19: 'U21`(tt,V_4,V_5) ; mult(V_4,V_5) 21: mult(z,V_0,V_4) ; mult(U11(isBin(V_4)),V_0) 25: mult(0(V_4),V_0,V_5) ; 'U21`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 26: mult(0(V_4),V_0,V_5) ; mult(U21(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 29: mult(0(V_4),V_5) ; 'U21`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 32: mult(1(V_4),V_0,V_5) ; 'U31`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 33: mult(1(V_4),V_0,V_5) ; mult(U31(and(isBin(V_4),isBin(V_5)),V_4,V_5),V_0) 36: mult(1(V_4),V_5) ; 'U31`(and(isBin(V_4),isBin(V_5)),V_4,V_5) 17 -> 21, 17 -> 25, 17 -> 26, 17 -> 29, 17 -> 32, 17 -> 33, 17 -> 36, 19 -> 21, 19 -> 25, 19 -> 26, 19 -> 29, 19 -> 32, 19 -> 33, 19 -> 36, 21 -> 21, 21 -> 25, 21 -> 26, 21 -> 29, 21 -> 32, 21 -> 33, 21 -> 36, 25 -> 19, 26 -> 21, 26 -> 25, 26 -> 26, 26 -> 29, 26 -> 32, 26 -> 33, 26 -> 36, 29 -> 19, 32 -> 17, 33 -> 21, 33 -> 25, 33 -> 26, 33 -> 29, 33 -> 32, 33 -> 33, 33 -> 36, 36 -> 17, On this component, the interpretation [z] = 0; [0](X0) = X0 + 1; [tt] = 0; [1](X0) = X0 + 1; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 1; [union](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 2; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2*X1 + 3*X2 + 2*X1 + 3; [U21](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; [mult](X0,X1) = X1*X0 + 2*X1 + 2*X0 + 2; [U71](X0,X1,X2) = X2 + X1 + 2; [U61](X0,X1,X2) = X2 + X1 + 1; [U51](X0,X1,X2) = X2 + X1 + 1; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U31`](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; ['U21`](X0,X1,X2) = X2*X1 + 2*X2 + 2*X1 + 3; strictly decreases on every cycle component 4 is 0: 'U91`(tt,V_0,V_1) ; 'prod`(V_1) 1: 'U91`(tt,V_0,V_1) ; 'prod`(V_0) 6: 'prod`(union(V_0,V_1)) ; 'U91`(and(isBag(V_0),isBag(V_1)),V_0,V_1) 0 -> 6, 1 -> 6, 6 -> 0, 6 -> 1, On this component, the interpretation [z] = 0; [0](X0) = 0; [tt] = 0; [1](X0) = 0; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 1; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2; [U21](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U71](X0,X1,X2) = 0; [U61](X0,X1,X2) = 0; [U51](X0,X1,X2) = 0; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U91`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['prod`](X0) = 2*X0; strictly decreases on every cycle component 5 is 7: 'U111`(tt,V_0,V_1) ; 'sum`(V_1) 8: 'U111`(tt,V_0,V_1) ; 'sum`(V_0) 13: 'sum`(union(V_0,V_1)) ; 'U111`(and(isBag(V_0),isBag(V_1)),V_0,V_1) 7 -> 13, 8 -> 13, 13 -> 7, 13 -> 8, On this component, the interpretation [z] = 0; [0](X0) = 0; [tt] = 0; [1](X0) = 0; [and](X0,X1) = X1; [U41](X0,X1) = X1; [U11](X0) = 0; [empty] = 0; [union](X0,X1) = X1 + X0 + 1; [singl](X0) = X0; [U101](X0,X1) = X1; [U81](X0,X1) = X1; [U91](X0,X1,X2) = X2 + X1; [prod](X0) = X0; [U111](X0,X1,X2) = X2 + X1; [sum](X0) = X0; [isBag](X0) = 0; [U31](X0,X1,X2) = X2; [U21](X0,X1,X2) = 0; [mult](X0,X1) = X1 + X0; [U71](X0,X1,X2) = 0; [U61](X0,X1,X2) = 0; [U51](X0,X1,X2) = 0; [plus](X0,X1) = X1 + X0; [isBin](X0) = 0; ['U111`](X0,X1,X2) = 2*X2 + 2*X1 + 1; ['sum`](X0) = 2*X0; strictly decreases on every cycle - : unit = () Quitting. Standard error: