Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 GroundTermsRemoverProof (⇔)
↳6 ITRS
↳7 DuplicateArgsRemoverProof (⇔)
↳8 ITRS
↳9 ITRStoIDPProof (⇔)
↳10 IDP
↳11 UsableRulesProof (⇔)
↳12 IDP
↳13 IDPNonInfProof (⇐)
↳14 AND
    ↳15 IDP
        ↳16 IDependencyGraphProof (⇔)
        ↳17 IDP
        ↳18 IDPNonInfProof (⇐)
        ↳19 AND
            ↳20 IDP
                ↳21 IDependencyGraphProof (⇔)
                ↳22 TRUE
            ↳23 IDP
                ↳24 IDependencyGraphProof (⇔)
                ↳25 TRUE
    ↳26 IDP
        ↳27 IDependencyGraphProof (⇔)
        ↳28 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Log

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 134 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load344(1, i29, i25) → Cond_Load344(i29 > 1, 1, i29, i25)
Cond_Load344(TRUE, 1, i29, i25) → Load475(1, i29, i25, i29, i29, 0)
Load475(1, i29, i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, 1, i29, i25, i29, i41, i38)
Cond_Load475(TRUE, 1, i29, i25, i29, i41, i38) → Load475(1, i29, i25, i29, i41 - 2, i38 + 1)
Load475(1, i29, i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, 1, i29, i25, i29, i41, i38)
Cond_Load4751(TRUE, 1, i29, i25, i29, i41, i38) → Load487(1, i29, i25, i29, i38)
Load487(1, i29, i25, i29, i38) → Load344(1, i38, i25 + 1)
Load475(1, i29, i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, 1, i29, i25, i29, i40, i38)
Cond_Load4752(TRUE, 1, i29, i25, i29, i40, i38) → Load344(1, i38, i25 + 1)
The set Q consists of the following terms:
Load344(1, x0, x1)
Cond_Load344(TRUE, 1, x0, x1)
Load475(1, x0, x1, x0, x2, x3)
Cond_Load475(TRUE, 1, x0, x1, x0, x2, x3)
Cond_Load4751(TRUE, 1, x0, x1, x0, x2, x3)
Load487(1, x0, x1, x0, x2)
Cond_Load4752(TRUE, 1, x0, x1, x0, x2, x3)

(5) GroundTermsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they always contain the same ground term.
We removed the following ground terms:
  • 1

We removed arguments according to the following replacements:

Cond_Load4752(x1, x2, x3, x4, x5, x6, x7) → Cond_Load4752(x1, x3, x4, x5, x6, x7)
Load475(x1, x2, x3, x4, x5, x6) → Load475(x2, x3, x4, x5, x6)
Load344(x1, x2, x3) → Load344(x2, x3)
Load487(x1, x2, x3, x4, x5) → Load487(x2, x3, x4, x5)
Cond_Load4751(x1, x2, x3, x4, x5, x6, x7) → Cond_Load4751(x1, x3, x4, x5, x6, x7)
Cond_Load475(x1, x2, x3, x4, x5, x6, x7) → Cond_Load475(x1, x3, x4, x5, x6, x7)
Cond_Load344(x1, x2, x3, x4) → Cond_Load344(x1, x3, x4)

(6) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load344(i29, i25) → Cond_Load344(i29 > 1, i29, i25)
Cond_Load344(TRUE, i29, i25) → Load475(i29, i25, i29, i29, 0)
Load475(i29, i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, i29, i25, i29, i41, i38)
Cond_Load475(TRUE, i29, i25, i29, i41, i38) → Load475(i29, i25, i29, i41 - 2, i38 + 1)
Load475(i29, i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, i29, i25, i29, i41, i38)
Cond_Load4751(TRUE, i29, i25, i29, i41, i38) → Load487(i29, i25, i29, i38)
Load487(i29, i25, i29, i38) → Load344(i38, i25 + 1)
Load475(i29, i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, i29, i25, i29, i40, i38)
Cond_Load4752(TRUE, i29, i25, i29, i40, i38) → Load344(i38, i25 + 1)
The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x0, x2, x3)
Cond_Load475(TRUE, x0, x1, x0, x2, x3)
Cond_Load4751(TRUE, x0, x1, x0, x2, x3)
Load487(x0, x1, x0, x2)
Cond_Load4752(TRUE, x0, x1, x0, x2, x3)

(7) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Cond_Load4752(x1, x2, x3, x4, x5, x6) → Cond_Load4752(x1, x3, x4, x5, x6)
Load475(x1, x2, x3, x4, x5) → Load475(x2, x3, x4, x5)
Load487(x1, x2, x3, x4) → Load487(x2, x3, x4)
Cond_Load4751(x1, x2, x3, x4, x5, x6) → Cond_Load4751(x1, x3, x4, x5, x6)
Cond_Load475(x1, x2, x3, x4, x5, x6) → Cond_Load475(x1, x3, x4, x5, x6)

(8) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load344(i29, i25) → Cond_Load344(i29 > 1, i29, i25)
Cond_Load344(TRUE, i29, i25) → Load475(i25, i29, i29, 0)
Load475(i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, i25, i29, i41, i38)
Cond_Load475(TRUE, i25, i29, i41, i38) → Load475(i25, i29, i41 - 2, i38 + 1)
Load475(i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, i25, i29, i41, i38)
Cond_Load4751(TRUE, i25, i29, i41, i38) → Load487(i25, i29, i38)
Load487(i25, i29, i38) → Load344(i38, i25 + 1)
Load475(i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, i25, i29, i40, i38)
Cond_Load4752(TRUE, i25, i29, i40, i38) → Load344(i38, i25 + 1)
The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(9) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


The ITRS R consists of the following rules:
Load344(i29, i25) → Cond_Load344(i29 > 1, i29, i25)
Cond_Load344(TRUE, i29, i25) → Load475(i25, i29, i29, 0)
Load475(i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, i25, i29, i41, i38)
Cond_Load475(TRUE, i25, i29, i41, i38) → Load475(i25, i29, i41 - 2, i38 + 1)
Load475(i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, i25, i29, i41, i38)
Cond_Load4751(TRUE, i25, i29, i41, i38) → Load487(i25, i29, i38)
Load487(i25, i29, i38) → Load344(i38, i25 + 1)
Load475(i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, i25, i29, i40, i38)
Cond_Load4752(TRUE, i25, i29, i40, i38) → Load344(i38, i25 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD344(i29[0], i25[0]) → COND_LOAD344(i29[0] > 1, i29[0], i25[0])
(1): COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
(2): LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(i41[2] > 1 && i38[2] + 1 > 0, i25[2], i29[2], i41[2], i38[2])
(3): COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], i41[3] - 2, i38[3] + 1)
(4): LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(i41[4] > 0 && i41[4] <= 1, i25[4], i29[4], i41[4], i38[4])
(5): COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5])
(6): LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], i25[6] + 1)
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])
(8): COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], i25[8] + 1)

(0) -> (1), if ((i29[0] > 1 →* TRUE)∧(i29[0] →* i29[1])∧(i25[0] →* i25[1]))


(1) -> (2), if ((i25[1] →* i25[2])∧(0 →* i38[2])∧(i29[1] →* i29[2])∧(i29[1] →* i41[2]))


(1) -> (4), if ((i29[1] →* i29[4])∧(0 →* i38[4])∧(i29[1] →* i41[4])∧(i25[1] →* i25[4]))


(1) -> (7), if ((i25[1] →* i25[7])∧(i29[1] →* i40[7])∧(i29[1] →* i29[7])∧(0 →* i38[7]))


(2) -> (3), if ((i41[2] →* i41[3])∧(i38[2] →* i38[3])∧(i29[2] →* i29[3])∧(i25[2] →* i25[3])∧(i41[2] > 1 && i38[2] + 1 > 0 →* TRUE))


(3) -> (2), if ((i29[3] →* i29[2])∧(i41[3] - 2 →* i41[2])∧(i25[3] →* i25[2])∧(i38[3] + 1 →* i38[2]))


(3) -> (4), if ((i25[3] →* i25[4])∧(i38[3] + 1 →* i38[4])∧(i29[3] →* i29[4])∧(i41[3] - 2 →* i41[4]))


(3) -> (7), if ((i41[3] - 2 →* i40[7])∧(i25[3] →* i25[7])∧(i38[3] + 1 →* i38[7])∧(i29[3] →* i29[7]))


(4) -> (5), if ((i38[4] →* i38[5])∧(i41[4] →* i41[5])∧(i41[4] > 0 && i41[4] <= 1 →* TRUE)∧(i29[4] →* i29[5])∧(i25[4] →* i25[5]))


(5) -> (6), if ((i25[5] →* i25[6])∧(i38[5] →* i38[6])∧(i29[5] →* i29[6]))


(6) -> (0), if ((i38[6] →* i29[0])∧(i25[6] + 1 →* i25[0]))


(7) -> (8), if ((i38[7] →* i38[8])∧(i40[7] →* i40[8])∧(i25[7] →* i25[8])∧(i29[7] →* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0 →* TRUE))


(8) -> (0), if ((i25[8] + 1 →* i25[0])∧(i38[8] →* i29[0]))



The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(11) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD344(i29[0], i25[0]) → COND_LOAD344(i29[0] > 1, i29[0], i25[0])
(1): COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
(2): LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(i41[2] > 1 && i38[2] + 1 > 0, i25[2], i29[2], i41[2], i38[2])
(3): COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], i41[3] - 2, i38[3] + 1)
(4): LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(i41[4] > 0 && i41[4] <= 1, i25[4], i29[4], i41[4], i38[4])
(5): COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5])
(6): LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], i25[6] + 1)
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])
(8): COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], i25[8] + 1)

(0) -> (1), if ((i29[0] > 1 →* TRUE)∧(i29[0] →* i29[1])∧(i25[0] →* i25[1]))


(1) -> (2), if ((i25[1] →* i25[2])∧(0 →* i38[2])∧(i29[1] →* i29[2])∧(i29[1] →* i41[2]))


(1) -> (4), if ((i29[1] →* i29[4])∧(0 →* i38[4])∧(i29[1] →* i41[4])∧(i25[1] →* i25[4]))


(1) -> (7), if ((i25[1] →* i25[7])∧(i29[1] →* i40[7])∧(i29[1] →* i29[7])∧(0 →* i38[7]))


(2) -> (3), if ((i41[2] →* i41[3])∧(i38[2] →* i38[3])∧(i29[2] →* i29[3])∧(i25[2] →* i25[3])∧(i41[2] > 1 && i38[2] + 1 > 0 →* TRUE))


(3) -> (2), if ((i29[3] →* i29[2])∧(i41[3] - 2 →* i41[2])∧(i25[3] →* i25[2])∧(i38[3] + 1 →* i38[2]))


(3) -> (4), if ((i25[3] →* i25[4])∧(i38[3] + 1 →* i38[4])∧(i29[3] →* i29[4])∧(i41[3] - 2 →* i41[4]))


(3) -> (7), if ((i41[3] - 2 →* i40[7])∧(i25[3] →* i25[7])∧(i38[3] + 1 →* i38[7])∧(i29[3] →* i29[7]))


(4) -> (5), if ((i38[4] →* i38[5])∧(i41[4] →* i41[5])∧(i41[4] > 0 && i41[4] <= 1 →* TRUE)∧(i29[4] →* i29[5])∧(i25[4] →* i25[5]))


(5) -> (6), if ((i25[5] →* i25[6])∧(i38[5] →* i38[6])∧(i29[5] →* i29[6]))


(6) -> (0), if ((i38[6] →* i29[0])∧(i25[6] + 1 →* i25[0]))


(7) -> (8), if ((i38[7] →* i38[8])∧(i40[7] →* i40[8])∧(i25[7] →* i25[8])∧(i29[7] →* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0 →* TRUE))


(8) -> (0), if ((i25[8] + 1 →* i25[0])∧(i38[8] →* i29[0]))



The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(13) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD344(i29, i25) → COND_LOAD344(>(i29, 1), i29, i25) the following chains were created:
  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

    (1)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1] ⇒ LOAD344(i29[0], i25[0])≥NonInfC∧LOAD344(i29[0], i25[0])≥COND_LOAD344(>(i29[0], 1), i29[0], i25[0])∧(UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (>(i29[0], 1)=TRUE ⇒ LOAD344(i29[0], i25[0])≥NonInfC∧LOAD344(i29[0], i25[0])≥COND_LOAD344(>(i29[0], 1), i29[0], i25[0])∧(UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧[(-1)bso_41] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧[(-1)bso_41] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧[(-1)bso_41] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)







For Pair COND_LOAD344(TRUE, i29, i25) → LOAD475(i25, i29, i29, 0) the following chains were created:
  • We consider the chain COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)) which results in the following constraint:

    (8)    (i25[5]=i25[6]∧i38[5]=i38[6]∧i29[5]=i29[6]∧i38[6]=i29[0]∧+(i25[6], 1)=i25[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[2]∧0=i38[2]∧i29[1]=i29[2]∧i29[1]=i41[2]∧i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (8) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (9)    (>(i29[0], 1)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], +(i25[6], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[6], 1))≥LOAD475(+(i25[6], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (10)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (11)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (12)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (13)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)



  • We consider the chain COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]) which results in the following constraint:

    (15)    (i25[5]=i25[6]∧i38[5]=i38[6]∧i29[5]=i29[6]∧i38[6]=i29[0]∧+(i25[6], 1)=i25[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i29[1]=i29[4]∧0=i38[4]∧i29[1]=i41[4]∧i25[1]=i25[4]∧i38[4]=i38[5]1∧i41[4]=i41[5]1∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]1∧i25[4]=i25[5]1 ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (15) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (16)    (>(i29[0], 1)=TRUE∧>(i29[0], 0)=TRUE∧<=(i29[0], 1)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], +(i25[6], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[6], 1))≥LOAD475(+(i25[6], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (17)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (18)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (19)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (19) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (20)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)



    We solved constraint (20) using rule (IDP_SMT_SPLIT).
  • We consider the chain COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

    (21)    (i25[5]=i25[6]∧i38[5]=i38[6]∧i29[5]=i29[6]∧i38[6]=i29[0]∧+(i25[6], 1)=i25[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[7]∧i29[1]=i40[7]∧i29[1]=i29[7]∧0=i38[7]∧i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (21) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (22)    (>(i29[0], 1)=TRUE∧<=(i29[0], 1)=TRUE∧>(+(+(i25[6], 1), 1), 0)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], +(i25[6], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[6], 1))≥LOAD475(+(i25[6], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (23)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (24)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (25)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We solved constraint (25) using rule (IDP_SMT_SPLIT).
  • We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)) which results in the following constraint:

    (26)    (i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE∧+(i25[8], 1)=i25[0]∧i38[8]=i29[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[2]∧0=i38[2]∧i29[1]=i29[2]∧i29[1]=i41[2]∧i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (26) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (27)    (>(i29[0], 1)=TRUE∧<=(i40[7], 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥LOAD475(+(i25[7], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (27) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (28)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (28) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (29)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (29) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (30)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (31)    (i29[0] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (31) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (32)    (i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



  • We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]) which results in the following constraint:

    (33)    (i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE∧+(i25[8], 1)=i25[0]∧i38[8]=i29[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i29[1]=i29[4]∧0=i38[4]∧i29[1]=i41[4]∧i25[1]=i25[4]∧i38[4]=i38[5]∧i41[4]=i41[5]∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]∧i25[4]=i25[5] ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (33) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (34)    (>(i29[0], 1)=TRUE∧<=(i40[7], 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE∧>(i29[0], 0)=TRUE∧<=(i29[0], 1)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥LOAD475(+(i25[7], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (35)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (36)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (37)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We solved constraint (37) using rule (IDP_SMT_SPLIT).
  • We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

    (38)    (i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE∧+(i25[8], 1)=i25[0]∧i38[8]=i29[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[7]1∧i29[1]=i40[7]1∧i29[1]=i29[7]1∧0=i38[7]1∧i38[7]1=i38[8]1∧i40[7]1=i40[8]1∧i25[7]1=i25[8]1∧i29[7]1=i29[8]1∧&&(<=(i40[7]1, 1), >(+(i25[7]1, 1), 0))=TRUE ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (38) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (39)    (>(i29[0], 1)=TRUE∧<=(i40[7], 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE∧<=(i29[0], 1)=TRUE∧>(+(+(i25[7], 1), 1), 0)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥LOAD475(+(i25[7], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (39) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (40)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (40) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (41)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We simplified constraint (41) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (42)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)



    We solved constraint (42) using rule (IDP_SMT_SPLIT).




For Pair LOAD475(i25, i29, i41, i38) → COND_LOAD475(&&(>(i41, 1), >(+(i38, 1), 0)), i25, i29, i41, i38) the following chains were created:
  • We consider the chain LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)) which results in the following constraint:

    (43)    (i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE ⇒ LOAD475(i25[2], i29[2], i41[2], i38[2])≥NonInfC∧LOAD475(i25[2], i29[2], i41[2], i38[2])≥COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])∧(UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥))



    We simplified constraint (43) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (44)    (>(i41[2], 1)=TRUE∧>(+(i38[2], 1), 0)=TRUE ⇒ LOAD475(i25[2], i29[2], i41[2], i38[2])≥NonInfC∧LOAD475(i25[2], i29[2], i41[2], i38[2])≥COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])∧(UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥))



    We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (45)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧[(-1)bso_45] ≥ 0)



    We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (46)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧[(-1)bso_45] ≥ 0)



    We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (47)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧[(-1)bso_45] ≥ 0)



    We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (48)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)



    We simplified constraint (48) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (49)    (i41[2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧0 = 0∧0 = 0∧[bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)







For Pair COND_LOAD475(TRUE, i25, i29, i41, i38) → LOAD475(i25, i29, -(i41, 2), +(i38, 1)) the following chains were created:
  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)) which results in the following constraint:

    (50)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[2]∧0=i38[2]∧i29[1]=i29[2]∧i29[1]=i41[2]∧i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧i29[3]=i29[2]1∧-(i41[3], 2)=i41[2]1∧i25[3]=i25[2]1∧+(i38[3], 1)=i38[2]1∧i41[2]1=i41[3]1∧i38[2]1=i38[3]1∧i29[2]1=i29[3]1∧i25[2]1=i25[3]1∧&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUE ⇒ COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥NonInfC∧COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))



    We simplified constraint (50) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (51)    (>(i29[0], 1)=TRUE∧>(-(i29[0], 2), 1)=TRUE ⇒ COND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥NonInfC∧COND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥LOAD475(i25[0], i29[0], -(i29[0], 2), +(0, 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))



    We simplified constraint (51) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (52)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (52) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (53)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (53) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (54)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (54) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (55)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (55) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (56)    (i29[0] ≥ 0∧[-2] + i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (56) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (57)    ([2] + i29[0] ≥ 0∧i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]) which results in the following constraint:

    (58)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[2]∧0=i38[2]∧i29[1]=i29[2]∧i29[1]=i41[2]∧i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧i25[3]=i25[4]∧+(i38[3], 1)=i38[4]∧i29[3]=i29[4]∧-(i41[3], 2)=i41[4]∧i38[4]=i38[5]∧i41[4]=i41[5]∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]∧i25[4]=i25[5] ⇒ COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥NonInfC∧COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))



    We simplified constraint (58) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (59)    (>(i29[0], 1)=TRUE∧>(-(i29[0], 2), 0)=TRUE∧<=(-(i29[0], 2), 1)=TRUE ⇒ COND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥NonInfC∧COND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥LOAD475(i25[0], i29[0], -(i29[0], 2), +(0, 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))



    We simplified constraint (59) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (60)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (60) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (61)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (61) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (62)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (62) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (63)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (63) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (64)    (i29[0] ≥ 0∧[-1] + i29[0] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (64) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (65)    ([1] + i29[0] ≥ 0∧i29[0] ≥ 0∧[-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (65) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (66)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

    (67)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[2]∧0=i38[2]∧i29[1]=i29[2]∧i29[1]=i41[2]∧i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧-(i41[3], 2)=i40[7]∧i25[3]=i25[7]∧+(i38[3], 1)=i38[7]∧i29[3]=i29[7]∧i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE ⇒ COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥NonInfC∧COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))



    We simplified constraint (67) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (68)    (>(i29[0], 1)=TRUE∧<=(-(i29[0], 2), 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ COND_LOAD475(TRUE, i25[7], i29[0], i29[0], 0)≥NonInfC∧COND_LOAD475(TRUE, i25[7], i29[0], i29[0], 0)≥LOAD475(i25[7], i29[0], -(i29[0], 2), +(0, 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))



    We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (69)    (i29[0] + [-2] ≥ 0∧[3] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (70)    (i29[0] + [-2] ≥ 0∧[3] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (71)    (i29[0] + [-2] ≥ 0∧[3] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (71) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (72)    (i29[0] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



  • We consider the chain LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)) which results in the following constraint:

    (73)    (i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧i29[3]=i29[2]1∧-(i41[3], 2)=i41[2]1∧i25[3]=i25[2]1∧+(i38[3], 1)=i38[2]1∧i41[2]1=i41[3]1∧i38[2]1=i38[3]1∧i29[2]1=i29[3]1∧i25[2]1=i25[3]1∧&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUE∧i29[3]1=i29[2]2∧-(i41[3]1, 2)=i41[2]2∧i25[3]1=i25[2]2∧+(i38[3]1, 1)=i38[2]2∧i41[2]2=i41[3]2∧i38[2]2=i38[3]2∧i29[2]2=i29[3]2∧i25[2]2=i25[3]2∧&&(>(i41[2]2, 1), >(+(i38[2]2, 1), 0))=TRUE ⇒ COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥NonInfC∧COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))



    We simplified constraint (73) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (74)    (>(i41[2], 1)=TRUE∧>(+(i38[2], 1), 0)=TRUE∧>(-(i41[2], 2), 1)=TRUE∧>(+(+(i38[2], 1), 1), 0)=TRUE∧>(-(-(i41[2], 2), 2), 1)=TRUE∧>(+(+(+(i38[2], 1), 1), 1), 0)=TRUE ⇒ COND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD475(i25[2], i29[2], -(-(i41[2], 2), 2), +(+(i38[2], 1), 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))



    We simplified constraint (74) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (75)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (75) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (76)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (76) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (77)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (77) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (78)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (78) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (79)    (i41[2] ≥ 0∧i38[2] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-4] + i41[2] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (79) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (80)    ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (80) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (81)    ([4] + i41[2] ≥ 0∧i38[2] ≥ 0∧[2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (81) using rule (IDP_POLY_GCD) which results in the following new constraint:

    (82)    ([4] + i41[2] ≥ 0∧i38[2] ≥ 0∧[2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



  • We consider the chain LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]) which results in the following constraint:

    (83)    (i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧i29[3]=i29[2]1∧-(i41[3], 2)=i41[2]1∧i25[3]=i25[2]1∧+(i38[3], 1)=i38[2]1∧i41[2]1=i41[3]1∧i38[2]1=i38[3]1∧i29[2]1=i29[3]1∧i25[2]1=i25[3]1∧&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUE∧i25[3]1=i25[4]∧+(i38[3]1, 1)=i38[4]∧i29[3]1=i29[4]∧-(i41[3]1, 2)=i41[4]∧i38[4]=i38[5]∧i41[4]=i41[5]∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]∧i25[4]=i25[5] ⇒ COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥NonInfC∧COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))



    We simplified constraint (83) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (84)    (>(i41[2], 1)=TRUE∧>(+(i38[2], 1), 0)=TRUE∧>(-(i41[2], 2), 1)=TRUE∧>(+(+(i38[2], 1), 1), 0)=TRUE∧>(-(-(i41[2], 2), 2), 0)=TRUE∧<=(-(-(i41[2], 2), 2), 1)=TRUE ⇒ COND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD475(i25[2], i29[2], -(-(i41[2], 2), 2), +(+(i38[2], 1), 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))



    We simplified constraint (84) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (85)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (85) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (86)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (86) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (87)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (87) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (88)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (88) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (89)    (i41[2] ≥ 0∧i38[2] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-3] + i41[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (89) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (90)    ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-1] + i41[2] ≥ 0∧[1] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (90) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (91)    ([3] + i41[2] ≥ 0∧i38[2] ≥ 0∧[1] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧[-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (91) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (92)    ([3] ≥ 0∧i38[2] ≥ 0∧[1] ≥ 0∧i38[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (92) using rule (IDP_POLY_GCD) which results in the following new constraint:

    (93)    (i38[2] ≥ 0∧[1] ≥ 0∧i38[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



  • We consider the chain LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

    (94)    (i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧i29[3]=i29[2]1∧-(i41[3], 2)=i41[2]1∧i25[3]=i25[2]1∧+(i38[3], 1)=i38[2]1∧i41[2]1=i41[3]1∧i38[2]1=i38[3]1∧i29[2]1=i29[3]1∧i25[2]1=i25[3]1∧&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUE∧-(i41[3]1, 2)=i40[7]∧i25[3]1=i25[7]∧+(i38[3]1, 1)=i38[7]∧i29[3]1=i29[7]∧i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE ⇒ COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥NonInfC∧COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))



    We simplified constraint (94) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (95)    (>(i41[2], 1)=TRUE∧>(+(i38[2], 1), 0)=TRUE∧>(-(i41[2], 2), 1)=TRUE∧>(+(+(i38[2], 1), 1), 0)=TRUE∧<=(-(-(i41[2], 2), 2), 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ COND_LOAD475(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD475(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD475(i25[7], i29[2], -(-(i41[2], 2), 2), +(+(i38[2], 1), 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))



    We simplified constraint (95) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (96)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (96) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (97)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (97) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (98)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (98) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (99)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (99) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (100)    (i41[2] ≥ 0∧i38[2] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (100) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (101)    ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)







For Pair LOAD475(i25, i29, i41, i38) → COND_LOAD4751(&&(>(i41, 0), <=(i41, 1)), i25, i29, i41, i38) the following chains were created:
  • We consider the chain LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]) which results in the following constraint:

    (102)    (i38[4]=i38[5]∧i41[4]=i41[5]∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]∧i25[4]=i25[5] ⇒ LOAD475(i25[4], i29[4], i41[4], i38[4])≥NonInfC∧LOAD475(i25[4], i29[4], i41[4], i38[4])≥COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])∧(UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥))



    We simplified constraint (102) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (103)    (>(i41[4], 0)=TRUE∧<=(i41[4], 1)=TRUE ⇒ LOAD475(i25[4], i29[4], i41[4], i38[4])≥NonInfC∧LOAD475(i25[4], i29[4], i41[4], i38[4])≥COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])∧(UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥))



    We simplified constraint (103) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (104)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i38[4] + [bni_48]i41[4] ≥ 0∧[(-1)bso_49] + i41[4] ≥ 0)



    We simplified constraint (104) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (105)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i38[4] + [bni_48]i41[4] ≥ 0∧[(-1)bso_49] + i41[4] ≥ 0)



    We simplified constraint (105) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (106)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i38[4] + [bni_48]i41[4] ≥ 0∧[(-1)bso_49] + i41[4] ≥ 0)



    We simplified constraint (106) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (107)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i41[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] + i41[4] ≥ 0)



    We simplified constraint (107) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (108)    (i41[4] ≥ 0∧[-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] + [bni_48]i41[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] + i41[4] ≥ 0)



    We simplified constraint (108) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (109)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] ≥ 0)







For Pair COND_LOAD4751(TRUE, i25, i29, i41, i38) → LOAD487(i25, i29, i38) the following chains were created:
  • We consider the chain COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)) which results in the following constraint:

    (110)    (i25[5]=i25[6]∧i38[5]=i38[6]∧i29[5]=i29[6] ⇒ COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5])≥NonInfC∧COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5])≥LOAD487(i25[5], i29[5], i38[5])∧(UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥))



    We simplified constraint (110) using rule (IV) which results in the following new constraint:

    (111)    (COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5])≥NonInfC∧COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5])≥LOAD487(i25[5], i29[5], i38[5])∧(UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥))



    We simplified constraint (111) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (112)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧[(-1)bso_51] ≥ 0)



    We simplified constraint (112) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (113)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧[(-1)bso_51] ≥ 0)



    We simplified constraint (113) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (114)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧[(-1)bso_51] ≥ 0)



    We simplified constraint (114) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (115)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)







For Pair LOAD487(i25, i29, i38) → LOAD344(i38, +(i25, 1)) the following chains were created:
  • We consider the chain COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

    (116)    (i29[1]=i29[4]∧0=i38[4]∧i29[1]=i41[4]∧i25[1]=i25[4]∧i38[4]=i38[5]∧i41[4]=i41[5]∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]∧i25[4]=i25[5]∧i25[5]=i25[6]∧i38[5]=i38[6]∧i29[5]=i29[6]∧i38[6]=i29[0]∧+(i25[6], 1)=i25[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]1∧i25[0]=i25[1]1 ⇒ LOAD487(i25[6], i29[6], i38[6])≥NonInfC∧LOAD487(i25[6], i29[6], i38[6])≥LOAD344(i38[6], +(i25[6], 1))∧(UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥))



    We solved constraint (116) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (IDP_BOOLEAN).
  • We consider the chain COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

    (117)    (i25[3]=i25[4]∧+(i38[3], 1)=i38[4]∧i29[3]=i29[4]∧-(i41[3], 2)=i41[4]∧i38[4]=i38[5]∧i41[4]=i41[5]∧&&(>(i41[4], 0), <=(i41[4], 1))=TRUE∧i29[4]=i29[5]∧i25[4]=i25[5]∧i25[5]=i25[6]∧i38[5]=i38[6]∧i29[5]=i29[6]∧i38[6]=i29[0]∧+(i25[6], 1)=i25[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1] ⇒ LOAD487(i25[6], i29[6], i38[6])≥NonInfC∧LOAD487(i25[6], i29[6], i38[6])≥LOAD344(i38[6], +(i25[6], 1))∧(UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥))



    We simplified constraint (117) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (118)    (>(+(i38[3], 1), 1)=TRUE∧>(-(i41[3], 2), 0)=TRUE∧<=(-(i41[3], 2), 1)=TRUE ⇒ LOAD487(i25[3], i29[3], +(i38[3], 1))≥NonInfC∧LOAD487(i25[3], i29[3], +(i38[3], 1))≥LOAD344(+(i38[3], 1), +(i25[3], 1))∧(UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥))



    We simplified constraint (118) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (119)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧[(-1)bso_53] ≥ 0)



    We simplified constraint (119) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (120)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧[(-1)bso_53] ≥ 0)



    We simplified constraint (120) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (121)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧[(-1)bso_53] ≥ 0)



    We simplified constraint (121) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (122)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)



    We simplified constraint (122) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (123)    (i38[3] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52 + bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)



    We simplified constraint (123) using rule (IDP_POLY_GCD) which results in the following new constraint:

    (124)    (i38[3] ≥ 0∧[3] + [-1]i41[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52 + bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)







For Pair LOAD475(i25, i29, i40, i38) → COND_LOAD4752(&&(<=(i40, 1), >(+(i25, 1), 0)), i25, i29, i40, i38) the following chains were created:
  • We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

    (125)    (i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE ⇒ LOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))



    We simplified constraint (125) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (126)    (<=(i40[7], 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ LOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))



    We simplified constraint (126) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (127)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i38[7] + [bni_54]i40[7] ≥ 0∧[(-1)bso_55] ≥ 0)



    We simplified constraint (127) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (128)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i38[7] + [bni_54]i40[7] ≥ 0∧[(-1)bso_55] ≥ 0)



    We simplified constraint (128) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (129)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i38[7] + [bni_54]i40[7] ≥ 0∧[(-1)bso_55] ≥ 0)



    We simplified constraint (129) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (130)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)



    We simplified constraint (130) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (131)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)


    (132)    ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)







For Pair COND_LOAD4752(TRUE, i25, i29, i40, i38) → LOAD344(i38, +(i25, 1)) the following chains were created:
  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

    (133)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[7]∧i29[1]=i40[7]∧i29[1]=i29[7]∧0=i38[7]∧i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE∧+(i25[8], 1)=i25[0]1∧i38[8]=i29[0]1∧>(i29[0]1, 1)=TRUE∧i29[0]1=i29[1]1∧i25[0]1=i25[1]1 ⇒ COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥NonInfC∧COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥LOAD344(i38[8], +(i25[8], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))



    We solved constraint (133) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (IDP_BOOLEAN).
  • We consider the chain LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

    (134)    (i41[2]=i41[3]∧i38[2]=i38[3]∧i29[2]=i29[3]∧i25[2]=i25[3]∧&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE∧-(i41[3], 2)=i40[7]∧i25[3]=i25[7]∧+(i38[3], 1)=i38[7]∧i29[3]=i29[7]∧i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE∧+(i25[8], 1)=i25[0]∧i38[8]=i29[0]∧>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1] ⇒ COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥NonInfC∧COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥LOAD344(i38[8], +(i25[8], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))



    We simplified constraint (134) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (135)    (>(+(i38[2], 1), 1)=TRUE∧>(i41[2], 1)=TRUE∧>(+(i38[2], 1), 0)=TRUE∧<=(-(i41[2], 2), 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ COND_LOAD4752(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD4752(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD344(+(i38[2], 1), +(i25[7], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))



    We simplified constraint (135) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (136)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)



    We simplified constraint (136) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (137)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)



    We simplified constraint (137) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (138)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)



    We simplified constraint (138) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (139)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)



    We simplified constraint (139) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (140)    (i38[2] ≥ 0∧i41[2] + [-2] ≥ 0∧[1] + i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[(-1)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)



    We simplified constraint (140) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (141)    (i38[2] ≥ 0∧i41[2] ≥ 0∧[1] + i38[2] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[(-1)bso_57] + i41[2] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD344(i29, i25) → COND_LOAD344(>(i29, 1), i29, i25)
    • (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

  • COND_LOAD344(TRUE, i29, i25) → LOAD475(i25, i29, i29, 0)
    • (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)
    • (i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

  • LOAD475(i25, i29, i41, i38) → COND_LOAD475(&&(>(i41, 1), >(+(i38, 1), 0)), i25, i29, i41, i38)
    • (i41[2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧0 = 0∧0 = 0∧[bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

  • COND_LOAD475(TRUE, i25, i29, i41, i38) → LOAD475(i25, i29, -(i41, 2), +(i38, 1))
    • ([2] + i29[0] ≥ 0∧i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
    • ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
    • (i29[0] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)
    • ([4] + i41[2] ≥ 0∧i38[2] ≥ 0∧[2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
    • (i38[2] ≥ 0∧[1] ≥ 0∧i38[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
    • ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

  • LOAD475(i25, i29, i41, i38) → COND_LOAD4751(&&(>(i41, 0), <=(i41, 1)), i25, i29, i41, i38)
    • (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] ≥ 0)

  • COND_LOAD4751(TRUE, i25, i29, i41, i38) → LOAD487(i25, i29, i38)
    • ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

  • LOAD487(i25, i29, i38) → LOAD344(i38, +(i25, 1))
    • (i38[3] ≥ 0∧[3] + [-1]i41[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52 + bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

  • LOAD475(i25, i29, i40, i38) → COND_LOAD4752(&&(<=(i40, 1), >(+(i25, 1), 0)), i25, i29, i40, i38)
    • ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)
    • ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

  • COND_LOAD4752(TRUE, i25, i29, i40, i38) → LOAD344(i38, +(i25, 1))
    • (i38[2] ≥ 0∧i41[2] ≥ 0∧[1] + i38[2] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[(-1)bso_57] + i41[2] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD344(x1, x2)) = [-1] + x1   
POL(COND_LOAD344(x1, x2, x3)) = [-1] + x2   
POL(>(x1, x2)) = [-1]   
POL(1) = [1]   
POL(LOAD475(x1, x2, x3, x4)) = [-1] + x4 + x3   
POL(0) = 0   
POL(COND_LOAD475(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + [-1]x1   
POL(&&(x1, x2)) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(2) = [2]   
POL(COND_LOAD4751(x1, x2, x3, x4, x5)) = [-1] + x5 + [-1]x1   
POL(<=(x1, x2)) = [-1]   
POL(LOAD487(x1, x2, x3)) = [-1] + x3   
POL(COND_LOAD4752(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + [-1]x1   

The following pairs are in P>:

COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))
LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])
LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1))

The following pairs are in Pbound:

LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0])
COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])
COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))
LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1))
COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1))

The following pairs are in P≥:

LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0])
COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])
COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5])
LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])
COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1

(14) Complex Obligation (AND)

(15) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD344(i29[0], i25[0]) → COND_LOAD344(i29[0] > 1, i29[0], i25[0])
(1): COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
(2): LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(i41[2] > 1 && i38[2] + 1 > 0, i25[2], i29[2], i41[2], i38[2])
(5): COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5])
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])
(8): COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], i25[8] + 1)

(8) -> (0), if ((i25[8] + 1 →* i25[0])∧(i38[8] →* i29[0]))


(0) -> (1), if ((i29[0] > 1 →* TRUE)∧(i29[0] →* i29[1])∧(i25[0] →* i25[1]))


(1) -> (2), if ((i25[1] →* i25[2])∧(0 →* i38[2])∧(i29[1] →* i29[2])∧(i29[1] →* i41[2]))


(1) -> (7), if ((i25[1] →* i25[7])∧(i29[1] →* i40[7])∧(i29[1] →* i29[7])∧(0 →* i38[7]))


(7) -> (8), if ((i38[7] →* i38[8])∧(i40[7] →* i40[8])∧(i25[7] →* i25[8])∧(i29[7] →* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0 →* TRUE))



The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(16) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(8): COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], i25[8] + 1)
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])
(1): COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
(0): LOAD344(i29[0], i25[0]) → COND_LOAD344(i29[0] > 1, i29[0], i25[0])

(8) -> (0), if ((i25[8] + 1 →* i25[0])∧(i38[8] →* i29[0]))


(0) -> (1), if ((i29[0] > 1 →* TRUE)∧(i29[0] →* i29[1])∧(i25[0] →* i25[1]))


(1) -> (7), if ((i25[1] →* i25[7])∧(i29[1] →* i40[7])∧(i29[1] →* i29[7])∧(0 →* i38[7]))


(7) -> (8), if ((i38[7] →* i38[8])∧(i40[7] →* i40[8])∧(i25[7] →* i25[8])∧(i29[7] →* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0 →* TRUE))



The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(18) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) the following chains were created:
  • We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]) which results in the following constraint:

    (1)    (i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE∧+(i25[8], 1)=i25[0]∧i38[8]=i29[0] ⇒ COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥NonInfC∧COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥LOAD344(i38[8], +(i25[8], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))



    We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (<=(i40[7], 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ COND_LOAD4752(TRUE, i25[7], i29[7], i40[7], i38[7])≥NonInfC∧COND_LOAD4752(TRUE, i25[7], i29[7], i40[7], i38[7])≥LOAD344(i38[7], +(i25[7], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (7)    ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)


    (8)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)







For Pair LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]) the following chains were created:
  • We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

    (9)    (i38[7]=i38[8]∧i40[7]=i40[8]∧i25[7]=i25[8]∧i29[7]=i29[8]∧&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE ⇒ LOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))



    We simplified constraint (9) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (10)    (<=(i40[7], 1)=TRUE∧>(+(i25[7], 1), 0)=TRUE ⇒ LOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))



    We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (11)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)



    We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (12)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)



    We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (13)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)



    We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (14)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (15)    ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + i40[7] ≥ 0)


    (16)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)







For Pair COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) the following chains were created:
  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]) which results in the following constraint:

    (17)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1]∧i25[1]=i25[7]∧i29[1]=i40[7]∧i29[1]=i29[7]∧0=i38[7] ⇒ COND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (17) using rules (III), (IV) which results in the following new constraint:

    (18)    (>(i29[0], 1)=TRUE ⇒ COND_LOAD344(TRUE, i29[0], i25[0])≥NonInfC∧COND_LOAD344(TRUE, i29[0], i25[0])≥LOAD475(i25[0], i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))



    We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (19)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (20)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (21)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (22)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)



    We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (23)    (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)







For Pair LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]) the following chains were created:
  • We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

    (24)    (>(i29[0], 1)=TRUE∧i29[0]=i29[1]∧i25[0]=i25[1] ⇒ LOAD344(i29[0], i25[0])≥NonInfC∧LOAD344(i29[0], i25[0])≥COND_LOAD344(>(i29[0], 1), i29[0], i25[0])∧(UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥))



    We simplified constraint (24) using rule (IV) which results in the following new constraint:

    (25)    (>(i29[0], 1)=TRUE ⇒ LOAD344(i29[0], i25[0])≥NonInfC∧LOAD344(i29[0], i25[0])≥COND_LOAD344(>(i29[0], 1), i29[0], i25[0])∧(UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥))



    We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (26)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)



    We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (27)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)



    We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (28)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)



    We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (29)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 = 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)



    We simplified constraint (29) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (30)    (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 = 0∧[(-1)bso_31] + i29[0] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1))
    • ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
    • ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

  • LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])
    • ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + i40[7] ≥ 0)
    • ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

  • COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
    • (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

  • LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0])
    • (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 = 0∧[(-1)bso_31] + i29[0] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_LOAD4752(x1, x2, x3, x4, x5)) = [-1] + [-1]x1   
POL(LOAD344(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(LOAD475(x1, x2, x3, x4)) = [1] + [-1]x3   
POL(&&(x1, x2)) = 0   
POL(<=(x1, x2)) = [-1]   
POL(>(x1, x2)) = 0   
POL(0) = 0   
POL(COND_LOAD344(x1, x2, x3)) = [1] + [-1]x2   

The following pairs are in P>:

LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])

The following pairs are in Pbound:

COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1))
LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])
LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0])

The following pairs are in P≥:

COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1))
COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1

(19) Complex Obligation (AND)

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(8): COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], i25[8] + 1)
(1): COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)
(0): LOAD344(i29[0], i25[0]) → COND_LOAD344(i29[0] > 1, i29[0], i25[0])

(8) -> (0), if ((i25[8] + 1 →* i25[0])∧(i38[8] →* i29[0]))


(0) -> (1), if ((i29[0] > 1 →* TRUE)∧(i29[0] →* i29[1])∧(i25[0] →* i25[1]))



The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(22) TRUE

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0)


The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(24) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(25) TRUE

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(4): LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(i41[4] > 0 && i41[4] <= 1, i25[4], i29[4], i41[4], i38[4])
(5): COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5])
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])

(4) -> (5), if ((i38[4] →* i38[5])∧(i41[4] →* i41[5])∧(i41[4] > 0 && i41[4] <= 1 →* TRUE)∧(i29[4] →* i29[5])∧(i25[4] →* i25[5]))



The set Q consists of the following terms:
Load344(x0, x1)
Cond_Load344(TRUE, x0, x1)
Load475(x0, x1, x2, x3)
Cond_Load475(TRUE, x0, x1, x2, x3)
Cond_Load4751(TRUE, x0, x1, x2, x3)
Load487(x0, x1, x2)
Cond_Load4752(TRUE, x0, x1, x2, x3)

(27) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(28) TRUE