Termination proof of /tmp/tmpEpBps1/Carre.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 GroundTermsRemoverProof (⇔)

        ↳7 ITRS

        ↳8 DuplicateArgsRemoverProof (⇔)

        ↳9 ITRS

        ↳10 ITRStoIDPProof (⇔)

        ↳11 IDP

        ↳12 UsableRulesProof (⇔)

        ↳13 IDP

        ↳14 ItpfGraphProof (⇔)

        ↳15 IDP

        ↳16 IDPNonInfProof (⇐)

        ↳17 AND

            ↳18 IDP

                ↳19 IDependencyGraphProof (⇔)

                ↳20 IDP

                ↳21 IDPNonInfProof (⇐)

                ↳22 AND

                    ↳23 IDP

                        ↳24 IDependencyGraphProof (⇔)

                        ↳25 TRUE

                    ↳26 IDP

                        ↳27 IDependencyGraphProof (⇔)

                        ↳28 TRUE

            ↳29 IDP

                ↳30 IDependencyGraphProof (⇔)

                ↳31 IDP

                ↳32 IDPNonInfProof (⇐)

                ↳33 AND

                    ↳34 IDP

                        ↳35 IDependencyGraphProof (⇔)

                        ↳36 TRUE

                    ↳37 IDP

                        ↳38 IDependencyGraphProof (⇔)

                        ↳39 TRUE

    ↳40 ITRS

        ↳41 GroundTermsRemoverProof (⇔)

        ↳42 ITRS

        ↳43 DuplicateArgsRemoverProof (⇔)

        ↳44 ITRS

        ↳45 ITRStoIDPProof (⇔)

        ↳46 IDP

        ↳47 UsableRulesProof (⇔)

        ↳48 IDP

        ↳49 ItpfGraphProof (⇔)

        ↳50 IDP

        ↳51 IDPNonInfProof (⇐)

        ↳52 IDP

        ↳53 IDependencyGraphProof (⇔)

        ↳54 IDP

        ↳55 IDPNonInfProof (⇐)

        ↳56 AND

            ↳57 IDP

                ↳58 IDependencyGraphProof (⇔)

                ↳59 TRUE

            ↳60 IDP

                ↳61 IDependencyGraphProof (⇔)

                ↳62 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Carre

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 511 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) 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:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98) → Cond_Load2692(i98 >= 0 && i98 < i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, 0)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99) → Cond_Load3135(i99 >= 0 && i99 < i17 && i99 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99 + 1)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99) → Cond_Load31351(i17 > 0 && i99 >= i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98, i99) → Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17, 1)))), i98 + 1)
The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0, 1)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0, 1)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0, 1)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0, 1)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0, 1)))), x4, x5)

(6) GroundTermsRemoverProof (EQUIVALENT transformation)

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

We removed arguments according to the following replacements:

Curseur(x1, x2, x3, x4, x5) → Curseur(x1, x2, x3, x4)

(7) 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:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98) → Cond_Load2692(i98 >= 0 && i98 < i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, 0)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99) → Cond_Load3135(i99 >= 0 && i99 < i17 && i99 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99 + 1)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99) → Cond_Load31351(i17 > 0 && i99 >= i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98, i99) → Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17, i17)))), i98 + 1)
The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0, x0)))), x4, x5)

(8) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

Curseur(x1, x2, x3, x4) → Curseur(x1, x2, x4)

(9) 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:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → Cond_Load2692(i98 >= 0 && i98 < i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, 0)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Cond_Load3135(i99 >= 0 && i99 < i17 && i99 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99 + 1)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Cond_Load31351(i17 > 0 && i99 >= i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98 + 1)
The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)

(10) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(11) 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

The ITRS R consists of the following rules:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → Cond_Load2692(i98 >= 0 && i98 < i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, 0)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Cond_Load3135(i99 >= 0 && i99 < i17 && i99 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99 + 1)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Cond_Load31351(i17 > 0 && i99 >= i17, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0]) → COND_LOAD2692(i98[0] >= 0 && i98[0] < i17[0], java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])
(1): COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)
(2): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])
(3): COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3] + 1)
(4): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4]) → COND_LOAD31351(i17[4] > 0 && i99[4] >= i17[4], java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])
(5): COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5]) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5] + 1)

(0) -> (1), if ((i98[0] >= 0 && i98[0] < i17[0] →^* TRUE)∧(i98[0] →^* i98[1])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1]))))))

(1) -> (2), if ((java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))))∧(i98[1] →^* i98[2])∧(0 →^* i99[2]))

(1) -> (4), if ((java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))))∧(0 →^* i99[4])∧(i98[1] →^* i98[4]))

(2) -> (3), if ((i98[2] →^* i98[3])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))))∧(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0 →^* TRUE)∧(i99[2] →^* i99[3]))

(3) -> (2), if ((i99[3] + 1 →^* i99[2])∧(i98[3] →^* i98[2])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2]))))))

(3) -> (4), if ((i98[3] →^* i98[4])∧(i99[3] + 1 →^* i99[4])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4]))))))

(4) -> (5), if ((java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))))∧(i99[4] →^* i99[5])∧(i98[4] →^* i98[5])∧(i17[4] > 0 && i99[4] >= i17[4] →^* TRUE))

(5) -> (0), if ((i98[5] + 1 →^* i98[0])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0]))))))

The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)

(12) 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.

(13) 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:
(0): LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0]) → COND_LOAD2692(i98[0] >= 0 && i98[0] < i17[0], java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])
(1): COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)
(2): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])
(3): COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3] + 1)
(4): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4]) → COND_LOAD31351(i17[4] > 0 && i99[4] >= i17[4], java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])
(5): COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5]) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5] + 1)

(14) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(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:

Boolean, Integer

(0) -> (1), if ((i98[0] >= 0 && i98[0] < i17[0] →^* TRUE)∧(i98[0] →^* i98[1])∧((i17[0] →^* i17[1])∧(a1782data[0] →^* a1782data[1])∧(i54[0] →^* i54[1])∧(i56[0] →^* i56[1])))

(1) -> (2), if (((i17[1] →^* i17[2])∧(a1782data[1] →^* a2145data[2])∧(i54[1] →^* i54[2])∧(i56[1] →^* i56[2]))∧(i98[1] →^* i98[2])∧(0 →^* i99[2]))

(1) -> (4), if (((i17[1] →^* i17[4])∧(a1782data[1] →^* a2145data[4])∧(i54[1] →^* i54[4])∧(i56[1] →^* i56[4]))∧(0 →^* i99[4])∧(i98[1] →^* i98[4]))

(2) -> (3), if ((i98[2] →^* i98[3])∧((i17[2] →^* i17[3])∧(a2145data[2] →^* a2145data[3])∧(i54[2] →^* i54[3])∧(i56[2] →^* i56[3]))∧(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0 →^* TRUE)∧(i99[2] →^* i99[3]))

(3) -> (2), if ((i99[3] + 1 →^* i99[2])∧(i98[3] →^* i98[2])∧((i17[3] →^* i17[2])∧(a2145data[3] →^* a2145data[2])∧(i54[3] →^* i54[2])∧(i56[3] →^* i56[2])))

(3) -> (4), if ((i98[3] →^* i98[4])∧(i99[3] + 1 →^* i99[4])∧((i17[3] →^* i17[4])∧(a2145data[3] →^* a2145data[4])∧(i54[3] →^* i54[4])∧(i56[3] →^* i56[4])))

(4) -> (5), if (((i17[4] →^* i17[5])∧(a2145data[4] →^* a2145data[5])∧(i54[4] →^* i54[5])∧(i56[4] →^* i56[5]))∧(i99[4] →^* i99[5])∧(i98[4] →^* i98[5])∧(i17[4] > 0 && i99[4] >= i17[4] →^* TRUE))

(5) -> (0), if ((i98[5] + 1 →^* i98[0])∧((i17[5] →^* i17[0])∧(a2145data[5] →^* a1782data[0])∧(i54[5] →^* i54[0])∧(i56[5] →^* i56[0])))

(16) 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 LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → COND_LOAD2692(&&(>=(i98, 0), <(i98, i17)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) the following chains were created:

We consider the chain LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0]) → COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0]), COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0) which results in the following constraint:
(1)    (&&(>=(i98[0], 0), <(i98[0], i17[0]))=TRUE∧i98[0]=i98[1]∧i17[0]=i17[1]∧a1782data[0]=a1782data[1]∧i54[0]=i54[1]∧i56[0]=i56[1] ⇒ LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])≥NonInfC∧LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])≥COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])∧(U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>=(i98[0], 0)=TRUE∧<(i98[0], i17[0])=TRUE ⇒ LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])≥NonInfC∧LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])≥COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])∧(U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (i98[0] ≥ 0∧i17[0] + [-1] + [-1]i98[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]i98[0] + [bni_21]i17[0] ≥ 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (i98[0] ≥ 0∧i17[0] + [-1] + [-1]i98[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]i98[0] + [bni_21]i17[0] ≥ 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (i98[0] ≥ 0∧i17[0] + [-1] + [-1]i98[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]i98[0] + [bni_21]i17[0] ≥ 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (i98[0] ≥ 0∧i17[0] + [-1] + [-1]i98[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]i98[0] + [bni_21]i17[0] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (i98[0] ≥ 0∧i17[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_21 + (-1)Bound*bni_21] + [bni_21]i17[0] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

For Pair COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, 0) the following chains were created:

We consider the chain COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0) which results in the following constraint:
(8)    (COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1])≥NonInfC∧COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1])≥LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)∧(U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)), ≥)∧[(-1)bso_24] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)), ≥)∧[(-1)bso_24] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)), ≥)∧[(-1)bso_24] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_24] ≥ 0)

For Pair LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → COND_LOAD3135(&&(&&(>=(i99, 0), <(i99, i17)), >(+(i99, 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) the following chains were created:

We consider the chain LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]), COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) which results in the following constraint:
(13)    (i98[2]=i98[3]∧i17[2]=i17[3]∧a2145data[2]=a2145data[3]∧i54[2]=i54[3]∧i56[2]=i56[3]∧&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0))=TRUE∧i99[2]=i99[3] ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])∧(U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥))

We simplified constraint (13) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(14)    (>(+(i99[2], 1), 0)=TRUE∧>=(i99[2], 0)=TRUE∧<(i99[2], i17[2])=TRUE ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])∧(U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]i98[2] + [bni_25]i17[2] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]i98[2] + [bni_25]i17[2] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]i98[2] + [bni_25]i17[2] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-1)bni_25] = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_25 + (-1)Bound*bni_25] + [bni_25]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (18) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(19)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-1)bni_25] = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_25 + (-1)Bound*bni_25] + [bni_25]i99[2] + [bni_25]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

For Pair COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, +(i99, 1)) the following chains were created:

We consider the chain COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) which results in the following constraint:
(20)    (COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3])≥NonInfC∧COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3])≥LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))∧(U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[(-1)bso_28] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[(-1)bso_28] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[(-1)bso_28] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)

For Pair LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → COND_LOAD31351(&&(>(i17, 0), >=(i99, i17)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) the following chains were created:

We consider the chain LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4]) → COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4]), COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5]) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1)) which results in the following constraint:
(25)    (i17[4]=i17[5]∧a2145data[4]=a2145data[5]∧i54[4]=i54[5]∧i56[4]=i56[5]∧i99[4]=i99[5]∧i98[4]=i98[5]∧&&(>(i17[4], 0), >=(i99[4], i17[4]))=TRUE ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])≥COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])∧(U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥))

We simplified constraint (25) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(26)    (>(i17[4], 0)=TRUE∧>=(i99[4], i17[4])=TRUE ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])≥COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])∧(U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (i17[4] + [-1] ≥ 0∧i99[4] + [-1]i17[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i98[4] + [bni_29]i17[4] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (i17[4] + [-1] ≥ 0∧i99[4] + [-1]i17[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i98[4] + [bni_29]i17[4] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (i17[4] + [-1] ≥ 0∧i99[4] + [-1]i17[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i98[4] + [bni_29]i17[4] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (i17[4] + [-1] ≥ 0∧i99[4] + [-1]i17[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[(-1)bni_29] = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_29 + (-1)Bound*bni_29] + [bni_29]i17[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(31)    (i17[4] ≥ 0∧i99[4] + [-1] + [-1]i17[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[(-1)bni_29] = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_29 + (-1)Bound*bni_29] + [bni_29]i17[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (31) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(32)    (i17[4] ≥ 0∧i99[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[(-1)bni_29] = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_29 + (-1)Bound*bni_29] + [bni_29]i17[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)

For Pair COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), +(i98, 1)) the following chains were created:

We consider the chain COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5]) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1)) which results in the following constraint:
(33)    (COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5])≥NonInfC∧COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5])≥LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))∧(U^Increasing(LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))), ≥))

We simplified constraint (33) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(34)    ((U^Increasing(LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))), ≥)∧[1 + (-1)bso_32] ≥ 0)

We simplified constraint (34) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(35)    ((U^Increasing(LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))), ≥)∧[1 + (-1)bso_32] ≥ 0)

We simplified constraint (35) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(36)    ((U^Increasing(LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))), ≥)∧[1 + (-1)bso_32] ≥ 0)

We simplified constraint (36) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(37)    ((U^Increasing(LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_32] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → COND_LOAD2692(&&(>=(i98, 0), <(i98, i17)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98)
- (i98[0] ≥ 0∧i17[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_21 + (-1)Bound*bni_21] + [bni_21]i17[0] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)
COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1782data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, 0)
- ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_24] ≥ 0)
LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → COND_LOAD3135(&&(&&(>=(i99, 0), <(i99, i17)), >(+(i99, 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99)
- (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-1)bni_25] = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_25 + (-1)Bound*bni_25] + [bni_25]i99[2] + [bni_25]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, +(i99, 1))
- ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)
LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → COND_LOAD31351(&&(>(i17, 0), >=(i99, i17)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99)
- (i17[4] ≥ 0∧i99[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])), ≥)∧[(-1)bni_29] = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_29 + (-1)Bound*bni_29] + [bni_29]i17[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)
COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), i98, i99) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a2145data)), i17, java.lang.Object(Curseur(i54, i56, i17)))), +(i98, 1))
- ((U^Increasing(LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_32] ≥ 0)

The constraints for P_> respective P_bound 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 P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD2692(x₁, x₂)) = [-1] + [-1]x₂ + x₁
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁, x₂, x₃)) = [-1]x₃ + [-1]x₂ + [-1]x₁
POL(ARRAY(x₁, x₂)) = [-1] + [-1]x₁
POL(Curseur(x₁, x₂, x₃)) = [-1] + [-1]x₃
POL(COND_LOAD2692(x₁, x₂, x₃)) = [-1] + [-1]x₃ + x₂
POL(&&(x₁, x₂)) = [-1]
POL(>=(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = [-1]
POL(LOAD3135(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁
POL(COND_LOAD3135(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂
POL(>(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_LOAD31351(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂

The following pairs are in P_>:

COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5]) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), +(i98[5], 1))

The following pairs are in P_bound:

LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0]) → COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])

The following pairs are in P_≥:

LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0]) → COND_LOAD2692(&&(>=(i98[0], 0), <(i98[0], i17[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a1782data[0])), i17[0], java.lang.Object(Curseur(i54[0], i56[0], i17[0])))), i98[0])
COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)
LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])
COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))
LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4]) → COND_LOAD31351(&&(>(i17[4], 0), >=(i99[4], i17[4])), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])

There are no usable rules.

(17) Complex Obligation (AND)

(18) 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

(0) -> (1), if ((i98[0] >= 0 && i98[0] < i17[0] →^* TRUE)∧(i98[0] →^* i98[1])∧((i17[0] →^* i17[1])∧(a1782data[0] →^* a1782data[1])∧(i54[0] →^* i54[1])∧(i56[0] →^* i56[1])))

(1) -> (2), if (((i17[1] →^* i17[2])∧(a1782data[1] →^* a2145data[2])∧(i54[1] →^* i54[2])∧(i56[1] →^* i56[2]))∧(i98[1] →^* i98[2])∧(0 →^* i99[2]))

(3) -> (2), if ((i99[3] + 1 →^* i99[2])∧(i98[3] →^* i98[2])∧((i17[3] →^* i17[2])∧(a2145data[3] →^* a2145data[2])∧(i54[3] →^* i54[2])∧(i56[3] →^* i56[2])))

(1) -> (4), if (((i17[1] →^* i17[4])∧(a1782data[1] →^* a2145data[4])∧(i54[1] →^* i54[4])∧(i56[1] →^* i56[4]))∧(0 →^* i99[4])∧(i98[1] →^* i98[4]))

(3) -> (4), if ((i98[3] →^* i98[4])∧(i99[3] + 1 →^* i99[4])∧((i17[3] →^* i17[4])∧(a2145data[3] →^* a2145data[4])∧(i54[3] →^* i54[4])∧(i56[3] →^* i56[4])))

(19) IDependencyGraphProof (EQUIVALENT transformation)

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

(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, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3] + 1)
(2): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])

(3) -> (2), if ((i99[3] + 1 →^* i99[2])∧(i98[3] →^* i98[2])∧((i17[3] →^* i17[2])∧(a2145data[3] →^* a2145data[2])∧(i54[3] →^* i54[2])∧(i56[3] →^* i56[2])))

(21) 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_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) the following chains were created:

We consider the chain COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) which results in the following constraint:
(1)    (COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3])≥NonInfC∧COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3])≥LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))∧(U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

For Pair LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) the following chains were created:

We consider the chain LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]), COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) which results in the following constraint:
(6)    (i98[2]=i98[3]∧i17[2]=i17[3]∧a2145data[2]=a2145data[3]∧i54[2]=i54[3]∧i56[2]=i56[3]∧&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0))=TRUE∧i99[2]=i99[3] ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])∧(U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥))

We simplified constraint (6) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (>(+(i99[2], 1), 0)=TRUE∧>=(i99[2], 0)=TRUE∧<(i99[2], i17[2])=TRUE ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])∧(U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-2)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]i99[2] + [bni_14]i17[2] ≥ 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-2)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]i99[2] + [bni_14]i17[2] ≥ 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-2)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]i99[2] + [bni_14]i17[2] ≥ 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-2)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]i99[2] + [bni_14]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))
- ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])
- (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_LOAD3135(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₂ + [-1]x₄
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(ARRAY(x₁, x₂)) = [-1] + x₁
POL(Curseur(x₁, x₂, x₃)) = [-1] + [-1]x₃
POL(LOAD3135(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(&&(x₁, x₂)) = [-1]
POL(>=(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(>(x₁, x₂)) = 0

The following pairs are in P_>:

COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))

The following pairs are in P_bound:

LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])

The following pairs are in P_≥:

LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])

There are no usable rules.

(22) Complex Obligation (AND)

(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:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])

The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)

(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:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3] + 1)

The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(28) TRUE

(29) 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:
(1): COND_LOAD2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a1782data[1])), i17[1], java.lang.Object(Curseur(i54[1], i56[1], i17[1])))), i98[1], 0)
(2): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(i99[2] >= 0 && i99[2] < i17[2] && i99[2] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])
(3): COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3] + 1)
(4): LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4]) → COND_LOAD31351(i17[4] > 0 && i99[4] >= i17[4], java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a2145data[4])), i17[4], java.lang.Object(Curseur(i54[4], i56[4], i17[4])))), i98[4], i99[4])
(5): COND_LOAD31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5], i99[5]) → LOAD2692(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a2145data[5])), i17[5], java.lang.Object(Curseur(i54[5], i56[5], i17[5])))), i98[5] + 1)

(1) -> (2), if (((i17[1] →^* i17[2])∧(a1782data[1] →^* a2145data[2])∧(i54[1] →^* i54[2])∧(i56[1] →^* i56[2]))∧(i98[1] →^* i98[2])∧(0 →^* i99[2]))

(3) -> (2), if ((i99[3] + 1 →^* i99[2])∧(i98[3] →^* i98[2])∧((i17[3] →^* i17[2])∧(a2145data[3] →^* a2145data[2])∧(i54[3] →^* i54[2])∧(i56[3] →^* i56[2])))

(1) -> (4), if (((i17[1] →^* i17[4])∧(a1782data[1] →^* a2145data[4])∧(i54[1] →^* i54[4])∧(i56[1] →^* i56[4]))∧(0 →^* i99[4])∧(i98[1] →^* i98[4]))

(3) -> (4), if ((i98[3] →^* i98[4])∧(i99[3] + 1 →^* i99[4])∧((i17[3] →^* i17[4])∧(a2145data[3] →^* a2145data[4])∧(i54[3] →^* i54[4])∧(i56[3] →^* i56[4])))

(30) IDependencyGraphProof (EQUIVALENT transformation)

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

(31) 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

(3) -> (2), if ((i99[3] + 1 →^* i99[2])∧(i98[3] →^* i98[2])∧((i17[3] →^* i17[2])∧(a2145data[3] →^* a2145data[2])∧(i54[3] →^* i54[2])∧(i56[3] →^* i56[2])))

(32) 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_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) the following chains were created:

We consider the chain COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) which results in the following constraint:
(1)    (COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3])≥NonInfC∧COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3])≥LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))∧(U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

We consider the chain LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]), COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1)) which results in the following constraint:
(6)    (i98[2]=i98[3]∧i17[2]=i17[3]∧a2145data[2]=a2145data[3]∧i54[2]=i54[3]∧i56[2]=i56[3]∧&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0))=TRUE∧i99[2]=i99[3] ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])∧(U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥))

We simplified constraint (6) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (>(+(i99[2], 1), 0)=TRUE∧>=(i99[2], 0)=TRUE∧<(i99[2], i17[2])=TRUE ⇒ LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥NonInfC∧LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])≥COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])∧(U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i99[2] + [bni_16]i17[2] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i99[2] + [bni_16]i17[2] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i99[2] + [bni_16]i17[2] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] + [-1] + [-1]i99[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i99[2] + [bni_16]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))
- ((U^Increasing(LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])
- (i99[2] ≥ 0∧i99[2] ≥ 0∧i17[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]i17[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_LOAD3135(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₂ + [-1]x₄
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁, x₂, x₃)) = [1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(ARRAY(x₁, x₂)) = [1] + x₁
POL(Curseur(x₁, x₂, x₃)) = [-1] + [-1]x₃
POL(LOAD3135(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(&&(x₁, x₂)) = 0
POL(>=(x₁, x₂)) = 0
POL(0) = 0
POL(<(x₁, x₂)) = [1]
POL(>(x₁, x₂)) = [-1]

The following pairs are in P_>:

COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], +(i99[3], 1))

The following pairs are in P_bound:

LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])

The following pairs are in P_≥:

LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2]) → COND_LOAD3135(&&(&&(>=(i99[2], 0), <(i99[2], i17[2])), >(+(i99[2], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a2145data[2])), i17[2], java.lang.Object(Curseur(i54[2], i56[2], i17[2])))), i98[2], i99[2])

There are no usable rules.

(33) Complex Obligation (AND)

(34) 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

(35) IDependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE

(37) 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:
(3): COND_LOAD3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3]) → LOAD3135(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a2145data[3])), i17[3], java.lang.Object(Curseur(i54[3], i56[3], i17[3])))), i98[3], i99[3] + 1)

The set Q consists of the following terms:
Load2692(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Cond_Load2692(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4)
Load3135(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load3135(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)
Cond_Load31351(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x2, x3, x0)))), x4, x5)

(38) IDependencyGraphProof (EQUIVALENT transformation)

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

(39) TRUE

(40) 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:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53) → Cond_Load1654(i53 >= 0 && i53 < 3, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, 0)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67) → Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Cond_Load1939ARR1(i67 >= 0 && i67 < i79 && i53 >= 0 && i53 < i17 && i67 < 3 && i67 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67 + 1)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67) → Cond_Load1939(i67 >= 3 && i53 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67)
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53, i67) → Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(0, 0, i17, i17, 1)))), i53 + 1)
The set Q consists of the following terms:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), x2)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), x2)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), x2, x3)
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(0, 0, x0, x0, 1)))), x2, x3)

(41) GroundTermsRemoverProof (EQUIVALENT transformation)

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

We removed arguments according to the following replacements:

Curseur(x1, x2, x3, x4, x5) → Curseur(x3, x4)

(42) 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:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), i53) → Cond_Load1654(i53 >= 0 && i53 < 3, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), i53)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), i53) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, 0)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67) → Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Cond_Load1939ARR1(i67 >= 0 && i67 < i79 && i53 >= 0 && i53 < i17 && i67 < 3 && i67 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67 + 1)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67) → Cond_Load1939(i67 >= 3 && i53 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67)
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53, i67) → Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17, i17)))), i53 + 1)
The set Q consists of the following terms:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), x2)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), x2)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), x2, x3)
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0, x0)))), x2, x3)

(43) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

Load1654(x1, x2, x3, x4) → Load1654(x3, x4)
Curseur(x1, x2) → Curseur(x2)
Cond_Load1939(x1, x2, x3, x4, x5, x6) → Cond_Load1939(x1, x4, x5, x6)
Load1939(x1, x2, x3, x4, x5) → Load1939(x3, x4, x5)
Cond_Load1939ARR1(x1, x2, x3, x4, x5, x6, x7) → Cond_Load1939ARR1(x1, x4, x5, x6, x7)
Load1939ARR1(x1, x2, x3, x4, x5, x6) → Load1939ARR1(x3, x4, x5, x6)
Cond_Load1654(x1, x2, x3, x4, x5) → Cond_Load1654(x1, x4, x5)

(44) 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:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → Cond_Load1654(i53 >= 0 && i53 < 3, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53, 0)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Cond_Load1939ARR1(i67 >= 0 && i67 < i79 && i53 >= 0 && i53 < i17 && i67 < 3 && i67 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67 + 1)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → Cond_Load1939(i67 >= 3 && i53 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67)
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53 + 1)
The set Q consists of the following terms:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3)
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3)

(45) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(46) 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

The ITRS R consists of the following rules:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → Cond_Load1654(i53 >= 0 && i53 < 3, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53, 0)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Cond_Load1939ARR1(i67 >= 0 && i67 < i79 && i53 >= 0 && i53 < i17 && i67 < 3 && i67 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67 + 1)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → Cond_Load1939(i67 >= 3 && i53 + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67)
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0]) → COND_LOAD1654(i53[0] >= 0 && i53[0] < 3, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])
(1): COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1]) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)
(2): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))
(3): LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
(4): COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4] + 1)
(5): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5]) → COND_LOAD1939(i67[5] >= 3 && i53[5] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])
(6): COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6]) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6] + 1)

(0) -> (1), if ((i53[0] →^* i53[1])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))))∧(i53[0] >= 0 && i53[0] < 3 →^* TRUE))

(1) -> (2), if ((0 →^* i67[2])∧(i53[1] →^* i53[2])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2]))))))

(1) -> (5), if ((0 →^* i67[5])∧(i53[1] →^* i53[5])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5]))))))

(2) -> (3), if ((java.lang.Object(ARRAY(i79[2], a1323data[2])) →^* java.lang.Object(ARRAY(i79[3], a1323data[3])))∧(i53[2] →^* i53[3])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))))∧(i67[2] →^* i67[3]))

(3) -> (4), if ((java.lang.Object(ARRAY(i79[3], a1323data[3])) →^* java.lang.Object(ARRAY(i79[4], a1323data[4])))∧(i53[3] →^* i53[4])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))))∧(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0 →^* TRUE)∧(i67[3] →^* i67[4]))

(4) -> (2), if ((i53[4] →^* i53[2])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))))∧(i67[4] + 1 →^* i67[2]))

(4) -> (5), if ((i67[4] + 1 →^* i67[5])∧(i53[4] →^* i53[5])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5]))))))

(5) -> (6), if ((i67[5] →^* i67[6])∧(i53[5] →^* i53[6])∧(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))))∧(i67[5] >= 3 && i53[5] + 1 > 0 →^* TRUE))

(6) -> (0), if ((java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))))∧(i53[6] + 1 →^* i53[0]))

The set Q consists of the following terms:
Load1654(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2)
Cond_Load1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2)
Load1939(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3)
Load1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3, java.lang.Object(ARRAY(x4, x5)))
Cond_Load1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0, x1)), x0, java.lang.Object(Curseur(x0)))), x2, x3)

(47) 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.

(48) 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:
(0): LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0]) → COND_LOAD1654(i53[0] >= 0 && i53[0] < 3, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])
(1): COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1]) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)
(2): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))
(3): LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
(4): COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4] + 1)
(5): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5]) → COND_LOAD1939(i67[5] >= 3 && i53[5] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])
(6): COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6]) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6] + 1)

(49) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(50) 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

(0) -> (1), if ((i53[0] →^* i53[1])∧((i17[0] →^* i17[1])∧(a997data[0] →^* a997data[1]))∧(i53[0] >= 0 && i53[0] < 3 →^* TRUE))

(1) -> (2), if ((0 →^* i67[2])∧(i53[1] →^* i53[2])∧((i17[1] →^* i17[2])∧(a997data[1] →^* a1225data[2])))

(1) -> (5), if ((0 →^* i67[5])∧(i53[1] →^* i53[5])∧((i17[1] →^* i17[5])∧(a997data[1] →^* a1225data[5])))

(2) -> (3), if (((i79[2] →^* i79[3])∧(a1323data[2] →^* a1323data[3]))∧(i53[2] →^* i53[3])∧((i17[2] →^* i17[3])∧(a1225data[2] →^* a1225data[3]))∧(i67[2] →^* i67[3]))

(3) -> (4), if (((i79[3] →^* i79[4])∧(a1323data[3] →^* a1323data[4]))∧(i53[3] →^* i53[4])∧((i17[3] →^* i17[4])∧(a1225data[3] →^* a1225data[4]))∧(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0 →^* TRUE)∧(i67[3] →^* i67[4]))

(4) -> (2), if ((i53[4] →^* i53[2])∧((i17[4] →^* i17[2])∧(a1225data[4] →^* a1225data[2]))∧(i67[4] + 1 →^* i67[2]))

(4) -> (5), if ((i67[4] + 1 →^* i67[5])∧(i53[4] →^* i53[5])∧((i17[4] →^* i17[5])∧(a1225data[4] →^* a1225data[5])))

(5) -> (6), if ((i67[5] →^* i67[6])∧(i53[5] →^* i53[6])∧((i17[5] →^* i17[6])∧(a1225data[5] →^* a1225data[6]))∧(i67[5] >= 3 && i53[5] + 1 > 0 →^* TRUE))

(6) -> (0), if (((i17[6] →^* i17[0])∧(a1225data[6] →^* a997data[0]))∧(i53[6] + 1 →^* i53[0]))

(51) 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 LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → COND_LOAD1654(&&(>=(i53, 0), <(i53, 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) the following chains were created:

We consider the chain LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0]) → COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0]), COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1]) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0) which results in the following constraint:
(1)    (i53[0]=i53[1]∧i17[0]=i17[1]∧a997data[0]=a997data[1]∧&&(>=(i53[0], 0), <(i53[0], 3))=TRUE ⇒ LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])≥NonInfC∧LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])≥COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])∧(U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>=(i53[0], 0)=TRUE∧<(i53[0], 3)=TRUE ⇒ LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])≥NonInfC∧LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])≥COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])∧(U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (i53[0] ≥ 0∧[2] + [-1]i53[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i53[0] ≥ 0∧[1 + (-1)bso_25] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (i53[0] ≥ 0∧[2] + [-1]i53[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i53[0] ≥ 0∧[1 + (-1)bso_25] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (i53[0] ≥ 0∧[2] + [-1]i53[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥)∧[bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i53[0] ≥ 0∧[1 + (-1)bso_25] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (i53[0] ≥ 0∧[2] + [-1]i53[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥)∧0 = 0∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i53[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)

For Pair COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53, 0) the following chains were created:

We consider the chain COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1]) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0) which results in the following constraint:
(7)    (COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1])≥NonInfC∧COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1])≥LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)∧(U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)), ≥)∧[(-1)bso_27] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)), ≥)∧[(-1)bso_27] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)), ≥)∧[(-1)bso_27] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) the following chains were created:

We consider the chain LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2]))) which results in the following constraint:
(12)    (LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2])≥NonInfC∧LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2])≥LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))∧(U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67, 0), <(i67, i79)), >=(i53, 0)), <(i53, i17)), <(i67, 3)), >(+(i67, 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) the following chains were created:

We consider the chain LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))), COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1)) which results in the following constraint:
(17)    (i79[3]=i79[4]∧a1323data[3]=a1323data[4]∧i53[3]=i53[4]∧i17[3]=i17[4]∧a1225data[3]=a1225data[4]∧&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0))=TRUE∧i67[3]=i67[4] ⇒ LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥NonInfC∧LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))∧(U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥))

We simplified constraint (17) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(18)    (>(+(i67[3], 1), 0)=TRUE∧<(i67[3], 3)=TRUE∧<(i53[3], i17[3])=TRUE∧>=(i53[3], 0)=TRUE∧>=(i67[3], 0)=TRUE∧<(i67[3], i79[3])=TRUE ⇒ LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥NonInfC∧LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))∧(U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(22)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(23)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (23) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(24)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

For Pair COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, +(i67, 1)) the following chains were created:

We consider the chain COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1)) which results in the following constraint:
(25)    (COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4])))≥NonInfC∧COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4])))≥LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))∧(U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥))

We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(26)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧[(-1)bso_33] ≥ 0)

We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(27)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧[(-1)bso_33] ≥ 0)

We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧[(-1)bso_33] ≥ 0)

We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(29)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → COND_LOAD1939(&&(>=(i67, 3), >(+(i53, 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) the following chains were created:

We consider the chain LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5]) → COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5]), COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6]) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1)) which results in the following constraint:
(30)    (i67[5]=i67[6]∧i53[5]=i53[6]∧i17[5]=i17[6]∧a1225data[5]=a1225data[6]∧&&(>=(i67[5], 3), >(+(i53[5], 1), 0))=TRUE ⇒ LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])≥NonInfC∧LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])≥COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])∧(U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥))

We simplified constraint (30) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(31)    (>=(i67[5], 3)=TRUE∧>(+(i53[5], 1), 0)=TRUE ⇒ LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])≥NonInfC∧LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])≥COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])∧(U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥))

We simplified constraint (31) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(32)    (i67[5] + [-3] ≥ 0∧i53[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥)∧[(-1)Bound*bni_34] + [(-1)bni_34]i53[5] ≥ 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (32) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(33)    (i67[5] + [-3] ≥ 0∧i53[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥)∧[(-1)Bound*bni_34] + [(-1)bni_34]i53[5] ≥ 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (33) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(34)    (i67[5] + [-3] ≥ 0∧i53[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥)∧[(-1)Bound*bni_34] + [(-1)bni_34]i53[5] ≥ 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (34) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(35)    (i67[5] + [-3] ≥ 0∧i53[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_34] + [(-1)bni_34]i53[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(36)    (i67[5] ≥ 0∧i53[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_34] + [(-1)bni_34]i53[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

For Pair COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), +(i53, 1)) the following chains were created:

We consider the chain COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6]) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1)) which results in the following constraint:
(37)    (COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6])≥NonInfC∧COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6])≥LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))∧(U^Increasing(LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))), ≥))

We simplified constraint (37) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(38)    ((U^Increasing(LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))), ≥)∧[(-1)bso_37] ≥ 0)

We simplified constraint (38) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(39)    ((U^Increasing(LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))), ≥)∧[(-1)bso_37] ≥ 0)

We simplified constraint (39) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(40)    ((U^Increasing(LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))), ≥)∧[(-1)bso_37] ≥ 0)

We simplified constraint (40) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(41)    ((U^Increasing(LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → COND_LOAD1654(&&(>=(i53, 0), <(i53, 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53)
- (i53[0] ≥ 0∧[2] + [-1]i53[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])), ≥)∧0 = 0∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i53[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)
COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a997data)), i17, java.lang.Object(Curseur(i17)))), i53, 0)
- ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
- ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67, 0), <(i67, i79)), >=(i53, 0)), <(i53, i17)), <(i67, 3)), >(+(i67, 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data)))
- (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_30] + [(-1)bni_30]i53[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67, java.lang.Object(ARRAY(i79, a1323data))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, +(i67, 1))
- ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → COND_LOAD1939(&&(>=(i67, 3), >(+(i53, 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67)
- (i67[5] ≥ 0∧i53[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_34] + [(-1)bni_34]i53[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), i53, i67) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17, a1225data)), i17, java.lang.Object(Curseur(i17)))), +(i53, 1))
- ((U^Increasing(LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD1654(x₁, x₂)) = [-1]x₂ + [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁, x₂, x₃)) = [-1]
POL(ARRAY(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(Curseur(x₁)) = x₁
POL(COND_LOAD1654(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(>=(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = [-1]
POL(3) = [3]
POL(LOAD1939(x₁, x₂, x₃)) = [-1] + [-1]x₂ + [-1]x₁
POL(LOAD1939ARR1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₂ + [-1]x₁
POL(COND_LOAD1939ARR1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₃ + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_LOAD1939(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂

The following pairs are in P_>:

LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0]) → COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])

The following pairs are in P_bound:

LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0]) → COND_LOAD1654(&&(>=(i53[0], 0), <(i53[0], 3)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[0], a997data[0])), i17[0], java.lang.Object(Curseur(i17[0])))), i53[0])

The following pairs are in P_≥:

COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1]) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)
LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))
LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))
LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5]) → COND_LOAD1939(&&(>=(i67[5], 3), >(+(i53[5], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])
COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6]) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), +(i53[6], 1))

There are no usable rules.

(52) 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:
(1): COND_LOAD1654(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1]) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[1], a997data[1])), i17[1], java.lang.Object(Curseur(i17[1])))), i53[1], 0)
(2): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))
(3): LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
(4): COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4] + 1)
(5): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5]) → COND_LOAD1939(i67[5] >= 3 && i53[5] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[5], a1225data[5])), i17[5], java.lang.Object(Curseur(i17[5])))), i53[5], i67[5])
(6): COND_LOAD1939(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6], i67[6]) → LOAD1654(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[6], a1225data[6])), i17[6], java.lang.Object(Curseur(i17[6])))), i53[6] + 1)

(1) -> (2), if ((0 →^* i67[2])∧(i53[1] →^* i53[2])∧((i17[1] →^* i17[2])∧(a997data[1] →^* a1225data[2])))

(4) -> (2), if ((i53[4] →^* i53[2])∧((i17[4] →^* i17[2])∧(a1225data[4] →^* a1225data[2]))∧(i67[4] + 1 →^* i67[2]))

(2) -> (3), if (((i79[2] →^* i79[3])∧(a1323data[2] →^* a1323data[3]))∧(i53[2] →^* i53[3])∧((i17[2] →^* i17[3])∧(a1225data[2] →^* a1225data[3]))∧(i67[2] →^* i67[3]))

(1) -> (5), if ((0 →^* i67[5])∧(i53[1] →^* i53[5])∧((i17[1] →^* i17[5])∧(a997data[1] →^* a1225data[5])))

(4) -> (5), if ((i67[4] + 1 →^* i67[5])∧(i53[4] →^* i53[5])∧((i17[4] →^* i17[5])∧(a1225data[4] →^* a1225data[5])))

(5) -> (6), if ((i67[5] →^* i67[6])∧(i53[5] →^* i53[6])∧((i17[5] →^* i17[6])∧(a1225data[5] →^* a1225data[6]))∧(i67[5] >= 3 && i53[5] + 1 > 0 →^* TRUE))

(53) IDependencyGraphProof (EQUIVALENT transformation)

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

(54) 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:
(4): COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4] + 1)
(3): LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
(2): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))

(4) -> (2), if ((i53[4] →^* i53[2])∧((i17[4] →^* i17[2])∧(a1225data[4] →^* a1225data[2]))∧(i67[4] + 1 →^* i67[2]))

(2) -> (3), if (((i79[2] →^* i79[3])∧(a1323data[2] →^* a1323data[3]))∧(i53[2] →^* i53[3])∧((i17[2] →^* i17[3])∧(a1225data[2] →^* a1225data[3]))∧(i67[2] →^* i67[3]))

(55) 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_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1)) the following chains were created:

We consider the chain COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1)) which results in the following constraint:
(1)    (COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4])))≥NonInfC∧COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4])))≥LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))∧(U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧[1 + (-1)bso_15] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

For Pair LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) the following chains were created:

We consider the chain LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))), COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1)) which results in the following constraint:
(6)    (i79[3]=i79[4]∧a1323data[3]=a1323data[4]∧i53[3]=i53[4]∧i17[3]=i17[4]∧a1225data[3]=a1225data[4]∧&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0))=TRUE∧i67[3]=i67[4] ⇒ LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥NonInfC∧LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))∧(U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥))

We simplified constraint (6) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (>(+(i67[3], 1), 0)=TRUE∧<(i67[3], 3)=TRUE∧<(i53[3], i17[3])=TRUE∧>=(i53[3], 0)=TRUE∧>=(i67[3], 0)=TRUE∧<(i67[3], i79[3])=TRUE ⇒ LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥NonInfC∧LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))≥COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))∧(U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] + [-1] + [-1]i53[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] + [-1] + [-1]i67[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(13)    (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2]))) the following chains were created:

We consider the chain LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2]))) which results in the following constraint:
(14)    (LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2])≥NonInfC∧LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2])≥LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))∧(U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧[(-1)bso_19] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧[(-1)bso_19] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧[(-1)bso_19] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))
- ((U^Increasing(LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
- (i67[3] ≥ 0∧[2] + [-1]i67[3] ≥ 0∧i17[3] ≥ 0∧i53[3] ≥ 0∧i67[3] ≥ 0∧i79[3] ≥ 0 ⇒ (U^Increasing(COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i67[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)
LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))
- ((U^Increasing(LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_LOAD1939ARR1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(ARRAY(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(Curseur(x₁)) = x₁
POL(LOAD1939(x₁, x₂, x₃)) = [-1] + [-1]x₃
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(LOAD1939ARR1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(&&(x₁, x₂)) = [-1]
POL(>=(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = [-1]
POL(3) = [3]
POL(>(x₁, x₂)) = [-1]

The following pairs are in P_>:

COND_LOAD1939ARR1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], i67[4], java.lang.Object(ARRAY(i79[4], a1323data[4]))) → LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[4], a1225data[4])), i17[4], java.lang.Object(Curseur(i17[4])))), i53[4], +(i67[4], 1))

The following pairs are in P_bound:

LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))

The following pairs are in P_≥:

LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(&&(&&(&&(&&(&&(>=(i67[3], 0), <(i67[3], i79[3])), >=(i53[3], 0)), <(i53[3], i17[3])), <(i67[3], 3)), >(+(i67[3], 1), 0)), java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))

There are no usable rules.

(56) Complex Obligation (AND)

(57) 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:
(3): LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3]))) → COND_LOAD1939ARR1(i67[3] >= 0 && i67[3] < i79[3] && i53[3] >= 0 && i53[3] < i17[3] && i67[3] < 3 && i67[3] + 1 > 0, java.lang.Object(Carre(java.lang.Object(ARRAY(i17[3], a1225data[3])), i17[3], java.lang.Object(Curseur(i17[3])))), i53[3], i67[3], java.lang.Object(ARRAY(i79[3], a1323data[3])))
(2): LOAD1939(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2]) → LOAD1939ARR1(java.lang.Object(Carre(java.lang.Object(ARRAY(i17[2], a1225data[2])), i17[2], java.lang.Object(Curseur(i17[2])))), i53[2], i67[2], java.lang.Object(ARRAY(i79[2], a1323data[2])))

(2) -> (3), if (((i79[2] →^* i79[3])∧(a1323data[2] →^* a1323data[3]))∧(i53[2] →^* i53[3])∧((i17[2] →^* i17[3])∧(a1225data[2] →^* a1225data[3]))∧(i67[2] →^* i67[3]))

(58) IDependencyGraphProof (EQUIVALENT transformation)

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

(59) TRUE

(60) 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

(4) -> (2), if ((i53[4] →^* i53[2])∧((i17[4] →^* i17[2])∧(a1225data[4] →^* a1225data[2]))∧(i67[4] + 1 →^* i67[2]))

(61) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBC2FIG (SOUND transformation)

(2) Obligation:

(3) FIGtoITRSProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) GroundTermsRemoverProof (EQUIVALENT transformation)

(7) Obligation:

(8) DuplicateArgsRemoverProof (EQUIVALENT transformation)

(9) Obligation:

(10) ITRStoIDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) UsableRulesProof (EQUIVALENT transformation)

(13) Obligation:

(14) ItpfGraphProof (EQUIVALENT transformation)

(15) Obligation:

(16) IDPNonInfProof (SOUND transformation)

(17) Complex Obligation (AND)

(18) Obligation:

(19) IDependencyGraphProof (EQUIVALENT transformation)

(20) Obligation:

(21) IDPNonInfProof (SOUND transformation)

(22) Complex Obligation (AND)

(23) Obligation:

(24) IDependencyGraphProof (EQUIVALENT transformation)

(25) TRUE

(26) Obligation:

(27) IDependencyGraphProof (EQUIVALENT transformation)

(28) TRUE

(29) Obligation:

(30) IDependencyGraphProof (EQUIVALENT transformation)

(31) Obligation:

(32) IDPNonInfProof (SOUND transformation)

(33) Complex Obligation (AND)

(34) Obligation:

(35) IDependencyGraphProof (EQUIVALENT transformation)

(36) TRUE

(37) Obligation:

(38) IDependencyGraphProof (EQUIVALENT transformation)

(39) TRUE

(40) Obligation:

(41) GroundTermsRemoverProof (EQUIVALENT transformation)

(42) Obligation:

(43) DuplicateArgsRemoverProof (EQUIVALENT transformation)

(44) Obligation:

(45) ITRStoIDPProof (EQUIVALENT transformation)

(46) Obligation:

(47) UsableRulesProof (EQUIVALENT transformation)

(48) Obligation:

(49) ItpfGraphProof (EQUIVALENT transformation)

(50) Obligation:

(51) IDPNonInfProof (SOUND transformation)

(52) Obligation:

(53) IDependencyGraphProof (EQUIVALENT transformation)

(54) Obligation:

(55) IDPNonInfProof (SOUND transformation)

(56) Complex Obligation (AND)

(57) Obligation:

(58) IDependencyGraphProof (EQUIVALENT transformation)

(59) TRUE

(60) Obligation:

(61) IDependencyGraphProof (EQUIVALENT transformation)

(62) TRUE