Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 AND
    ↳5 ITRS
        ↳6 ITRStoIDPProof (⇔)
        ↳7 IDP
        ↳8 UsableRulesProof (⇔)
        ↳9 IDP
        ↳10 IDPNonInfProof (⇐)
        ↳11 AND
            ↳12 IDP
                ↳13 IDependencyGraphProof (⇔)
                ↳14 TRUE
            ↳15 IDP
                ↳16 IDependencyGraphProof (⇔)
                ↳17 TRUE
    ↳18 ITRS
        ↳19 DuplicateArgsRemoverProof (⇔)
        ↳20 ITRS
        ↳21 ITRStoIDPProof (⇔)
        ↳22 IDP
        ↳23 UsableRulesProof (⇔)
        ↳24 IDP
        ↳25 ItpfGraphProof (⇔)
        ↳26 IDP
        ↳27 IDPNonInfProof (⇐)
        ↳28 AND
            ↳29 IDP
                ↳30 IDependencyGraphProof (⇔)
                ↳31 TRUE
            ↳32 IDP
                ↳33 IDependencyGraphProof (⇔)
                ↳34 TRUE
    ↳35 ITRS
        ↳36 ITRStoIDPProof (⇔)
        ↳37 IDP
        ↳38 UsableRulesProof (⇔)
        ↳39 IDP
        ↳40 ItpfGraphProof (⇔)
        ↳41 IDP
        ↳42 IDPNonInfProof (⇐)
        ↳43 AND
            ↳44 IDP
                ↳45 IDependencyGraphProof (⇔)
                ↳46 TRUE
            ↳47 IDP
                ↳48 IDependencyGraphProof (⇔)
                ↳49 TRUE

(0) Obligation:

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

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

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 354 nodes with 3 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:
Load2356(i717) → Cond_Load2356(i717 > 0, i717)
Cond_Load2356(TRUE, i717) → Load2356(i717 + -1)
The set Q consists of the following terms:
Load2356(x0)
Cond_Load2356(TRUE, x0)

(6) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

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


The ITRS R consists of the following rules:
Load2356(i717) → Cond_Load2356(i717 > 0, i717)
Cond_Load2356(TRUE, i717) → Load2356(i717 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD2356(i717[0]) → COND_LOAD2356(i717[0] > 0, i717[0])
(1): COND_LOAD2356(TRUE, i717[1]) → LOAD2356(i717[1] + -1)

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


(1) -> (0), if ((i717[1] + -1 →* i717[0]))



The set Q consists of the following terms:
Load2356(x0)
Cond_Load2356(TRUE, x0)

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

(9) 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:
(0): LOAD2356(i717[0]) → COND_LOAD2356(i717[0] > 0, i717[0])
(1): COND_LOAD2356(TRUE, i717[1]) → LOAD2356(i717[1] + -1)

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


(1) -> (0), if ((i717[1] + -1 →* i717[0]))



The set Q consists of the following terms:
Load2356(x0)
Cond_Load2356(TRUE, x0)

(10) 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 LOAD2356(i717) → COND_LOAD2356(>(i717, 0), i717) the following chains were created:
  • We consider the chain LOAD2356(i717[0]) → COND_LOAD2356(>(i717[0], 0), i717[0]), COND_LOAD2356(TRUE, i717[1]) → LOAD2356(+(i717[1], -1)) which results in the following constraint:

    (1)    (>(i717[0], 0)=TRUE∧i717[0]=i717[1] ⇒ LOAD2356(i717[0])≥NonInfC∧LOAD2356(i717[0])≥COND_LOAD2356(>(i717[0], 0), i717[0])∧(UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥))



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

    (2)    (>(i717[0], 0)=TRUE ⇒ LOAD2356(i717[0])≥NonInfC∧LOAD2356(i717[0])≥COND_LOAD2356(>(i717[0], 0), i717[0])∧(UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥))



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

    (3)    (i717[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)



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

    (4)    (i717[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)



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

    (5)    (i717[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)



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

    (6)    (i717[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)







For Pair COND_LOAD2356(TRUE, i717) → LOAD2356(+(i717, -1)) the following chains were created:
  • We consider the chain COND_LOAD2356(TRUE, i717[1]) → LOAD2356(+(i717[1], -1)) which results in the following constraint:

    (7)    (COND_LOAD2356(TRUE, i717[1])≥NonInfC∧COND_LOAD2356(TRUE, i717[1])≥LOAD2356(+(i717[1], -1))∧(UIncreasing(LOAD2356(+(i717[1], -1))), ≥))



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

    (8)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)



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

    (9)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)



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

    (10)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)



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

    (11)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD2356(i717) → COND_LOAD2356(>(i717, 0), i717)
    • (i717[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)

  • COND_LOAD2356(TRUE, i717) → LOAD2356(+(i717, -1))
    • ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD2356(x1)) = [2]x1   
POL(COND_LOAD2356(x1, x2)) = [2]x2   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   

The following pairs are in P>:

COND_LOAD2356(TRUE, i717[1]) → LOAD2356(+(i717[1], -1))

The following pairs are in Pbound:

LOAD2356(i717[0]) → COND_LOAD2356(>(i717[0], 0), i717[0])

The following pairs are in P≥:

LOAD2356(i717[0]) → COND_LOAD2356(>(i717[0], 0), i717[0])

There are no usable rules.

(11) Complex Obligation (AND)

(12) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2356(i717[0]) → COND_LOAD2356(i717[0] > 0, i717[0])


The set Q consists of the following terms:
Load2356(x0)
Cond_Load2356(TRUE, x0)

(13) IDependencyGraphProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LOAD2356(TRUE, i717[1]) → LOAD2356(i717[1] + -1)


The set Q consists of the following terms:
Load2356(x0)
Cond_Load2356(TRUE, x0)

(16) IDependencyGraphProof (EQUIVALENT transformation)

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

(17) TRUE

(18) 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:
Load2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → Cond_Load2110(i637 > 1, java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676)))
Cond_Load2110(TRUE, java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → JMP2394(java.lang.Object(IntList(o2075, i676)), i637 + -1, o2075)
JMP2394(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Cond_Load21101(i637 > 1, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
Cond_Load21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637 + -1, o2070)
The set Q consists of the following terms:
Cond_Load2110(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x0, x1)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

(19) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

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

(20) 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:
Load2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → Cond_Load2110(i637 > 1, i637, java.lang.Object(IntList(o2075, i676)))
Cond_Load2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394(java.lang.Object(IntList(o2075, i676)), i637 + -1, o2075)
JMP2394(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Cond_Load21101(i637 > 1, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
Cond_Load21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637 + -1, o2070)
The set Q consists of the following terms:
Cond_Load2110(TRUE, x0, java.lang.Object(IntList(x1, x2)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

(21) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

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


The ITRS R consists of the following rules:
Load2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → Cond_Load2110(i637 > 1, i637, java.lang.Object(IntList(o2075, i676)))
Cond_Load2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394(java.lang.Object(IntList(o2075, i676)), i637 + -1, o2075)
JMP2394(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Cond_Load21101(i637 > 1, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
Cond_Load21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637 + -1, o2070)

The integer pair graph contains the following rules and edges:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(3): LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(i637[3] > 1, java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(0) -> (1), if ((java.lang.Object(IntList(o2075[0], i676[0])) →* java.lang.Object(IntList(o2075[1], i676[1])))∧(i637[0] →* i637[1])∧(i637[0] > 1 →* TRUE))


(1) -> (2), if ((i637[1] + -1 →* i650[2])∧(o2075[1] →* o2070[2])∧(java.lang.Object(IntList(o2075[1], i676[1])) →* java.lang.Object(IntList(o1946Field0[2], o1946Field1[2]))))


(2) -> (0), if ((o2070[2] →* java.lang.Object(IntList(o2075[0], i676[0])))∧(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i650[2] →* i637[0]))


(2) -> (3), if ((java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(o2070[2] →* java.lang.Object(IntList(o2070[3], i675[3])))∧(i650[2] →* i637[3]))


(3) -> (4), if ((java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])) →* java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])))∧(i637[3] > 1 →* TRUE)∧(java.lang.Object(IntList(o2070[3], i675[3])) →* java.lang.Object(IntList(o2070[4], i675[4])))∧(i637[3] →* i637[4]))


(4) -> (0), if ((java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(o2070[4] →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i637[4] + -1 →* i637[0]))


(4) -> (3), if ((o2070[4] →* java.lang.Object(IntList(o2070[3], i675[3])))∧(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(i637[4] + -1 →* i637[3]))



The set Q consists of the following terms:
Cond_Load2110(TRUE, x0, java.lang.Object(IntList(x1, x2)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

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

(24) 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:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(3): LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(i637[3] > 1, java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(0) -> (1), if ((java.lang.Object(IntList(o2075[0], i676[0])) →* java.lang.Object(IntList(o2075[1], i676[1])))∧(i637[0] →* i637[1])∧(i637[0] > 1 →* TRUE))


(1) -> (2), if ((i637[1] + -1 →* i650[2])∧(o2075[1] →* o2070[2])∧(java.lang.Object(IntList(o2075[1], i676[1])) →* java.lang.Object(IntList(o1946Field0[2], o1946Field1[2]))))


(2) -> (0), if ((o2070[2] →* java.lang.Object(IntList(o2075[0], i676[0])))∧(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i650[2] →* i637[0]))


(2) -> (3), if ((java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(o2070[2] →* java.lang.Object(IntList(o2070[3], i675[3])))∧(i650[2] →* i637[3]))


(3) -> (4), if ((java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])) →* java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])))∧(i637[3] > 1 →* TRUE)∧(java.lang.Object(IntList(o2070[3], i675[3])) →* java.lang.Object(IntList(o2070[4], i675[4])))∧(i637[3] →* i637[4]))


(4) -> (0), if ((java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(o2070[4] →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i637[4] + -1 →* i637[0]))


(4) -> (3), if ((o2070[4] →* java.lang.Object(IntList(o2070[3], i675[3])))∧(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(i637[4] + -1 →* i637[3]))



The set Q consists of the following terms:
Cond_Load2110(TRUE, x0, java.lang.Object(IntList(x1, x2)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

(25) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(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:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(3): LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(i637[3] > 1, java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(0) -> (1), if (((o2075[0] →* o2075[1])∧(i676[0] →* i676[1]))∧(i637[0] →* i637[1])∧(i637[0] > 1 →* TRUE))


(1) -> (2), if ((i637[1] + -1 →* i650[2])∧(o2075[1] →* o2070[2])∧((o2075[1] →* o1946Field0[2])∧(i676[1] →* o1946Field1[2])))


(2) -> (0), if ((o2070[2] →* java.lang.Object(IntList(o2075[0], i676[0])))∧((o1946Field0[2] →* o2075[0])∧(o1946Field1[2] →* i676[0]))∧(i650[2] →* i637[0]))


(2) -> (3), if (((o1946Field0[2] →* o1946Field0[3])∧(o1946Field1[2] →* o1946Field1[3]))∧(o2070[2] →* java.lang.Object(IntList(o2070[3], i675[3])))∧(i650[2] →* i637[3]))


(3) -> (4), if (((o1946Field0[3] →* o1946Field0[4])∧(o1946Field1[3] →* o1946Field1[4]))∧(i637[3] > 1 →* TRUE)∧((o2070[3] →* o2070[4])∧(i675[3] →* i675[4]))∧(i637[3] →* i637[4]))


(4) -> (0), if (((o1946Field0[4] →* o2075[0])∧(o1946Field1[4] →* i676[0]))∧(o2070[4] →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i637[4] + -1 →* i637[0]))


(4) -> (3), if ((o2070[4] →* java.lang.Object(IntList(o2070[3], i675[3])))∧((o1946Field0[4] →* o1946Field0[3])∧(o1946Field1[4] →* o1946Field1[3]))∧(i637[4] + -1 →* i637[3]))



The set Q consists of the following terms:
Cond_Load2110(TRUE, x0, java.lang.Object(IntList(x1, x2)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

(27) 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 LOAD2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → COND_LOAD2110(>(i637, 1), i637, java.lang.Object(IntList(o2075, i676))) the following chains were created:
  • We consider the chain LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))), COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1]) which results in the following constraint:

    (1)    (o2075[0]=o2075[1]∧i676[0]=i676[1]∧i637[0]=i637[1]∧>(i637[0], 1)=TRUE ⇒ LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))≥NonInfC∧LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))≥COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))∧(UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥))



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

    (2)    (>(i637[0], 1)=TRUE ⇒ LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))≥NonInfC∧LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))≥COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))∧(UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥))



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

    (3)    (i637[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (4)    (i637[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (5)    (i637[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (6)    (i637[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[(5)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)







For Pair COND_LOAD2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394'(java.lang.Object(IntList(o2075, i676)), +(i637, -1), o2075) the following chains were created:
  • We consider the chain COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1]) which results in the following constraint:

    (7)    (COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1])))≥NonInfC∧COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1])))≥JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])∧(UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥))



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

    (8)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧[1 + (-1)bso_17] ≥ 0)



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

    (9)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧[1 + (-1)bso_17] ≥ 0)



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

    (10)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧[1 + (-1)bso_17] ≥ 0)



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

    (11)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧0 = 0∧[1 + (-1)bso_17] ≥ 0)







For Pair JMP2394'(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) the following chains were created:
  • We consider the chain JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]), LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) which results in the following constraint:

    (12)    (o2070[2]=java.lang.Object(IntList(o2075[0], i676[0]))∧o1946Field0[2]=o2075[0]∧o1946Field1[2]=i676[0]∧i650[2]=i637[0] ⇒ JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))



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

    (13)    (JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])))≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])))≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])))∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))



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

    (14)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)



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

    (15)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)



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

    (16)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)



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

    (17)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)



  • We consider the chain JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]), LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) which results in the following constraint:

    (18)    (o1946Field0[2]=o1946Field0[3]∧o1946Field1[2]=o1946Field1[3]∧o2070[2]=java.lang.Object(IntList(o2070[3], i675[3]))∧i650[2]=i637[3] ⇒ JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))



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

    (19)    (JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o2070[3], i675[3])))≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o2070[3], i675[3])))≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o2070[3], i675[3])))∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))



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

    (20)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)



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

    (21)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)



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

    (22)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)



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

    (23)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)







For Pair LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → COND_LOAD21101(>(i637, 1), java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) the following chains were created:
  • We consider the chain LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))), COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4]) which results in the following constraint:

    (24)    (o1946Field0[3]=o1946Field0[4]∧o1946Field1[3]=o1946Field1[4]∧>(i637[3], 1)=TRUE∧o2070[3]=o2070[4]∧i675[3]=i675[4]∧i637[3]=i637[4] ⇒ LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥NonInfC∧LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))∧(UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥))



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

    (25)    (>(i637[3], 1)=TRUE ⇒ LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥NonInfC∧LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))∧(UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥))



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

    (26)    (i637[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)



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

    (27)    (i637[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)



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

    (28)    (i637[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)



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

    (29)    (i637[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[(5)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)







For Pair COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), +(i637, -1), o2070) the following chains were created:
  • We consider the chain COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4]) which results in the following constraint:

    (30)    (COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4])))≥NonInfC∧COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4])))≥LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥))



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

    (31)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧[1 + (-1)bso_23] ≥ 0)



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

    (32)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧[1 + (-1)bso_23] ≥ 0)



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

    (33)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧[1 + (-1)bso_23] ≥ 0)



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

    (34)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧0 = 0∧[1 + (-1)bso_23] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → COND_LOAD2110(>(i637, 1), i637, java.lang.Object(IntList(o2075, i676)))
    • (i637[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[(5)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)

  • COND_LOAD2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394'(java.lang.Object(IntList(o2075, i676)), +(i637, -1), o2075)
    • ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧0 = 0∧[1 + (-1)bso_17] ≥ 0)

  • JMP2394'(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
    • ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
    • ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

  • LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → COND_LOAD21101(>(i637, 1), java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
    • (i637[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[(5)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)

  • COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), +(i637, -1), o2070)
    • ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧0 = 0∧[1 + (-1)bso_23] ≥ 0)




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD2110(x1, x2, x3)) = [1] + [2]x2   
POL(java.lang.Object(x1)) = [-1]   
POL(IntList(x1, x2)) = [-1]   
POL(COND_LOAD2110(x1, x2, x3)) = [1] + [2]x2   
POL(>(x1, x2)) = [-1]   
POL(1) = [1]   
POL(JMP2394'(x1, x2, x3)) = [2] + [2]x2   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(COND_LOAD21101(x1, x2, x3, x4)) = [2]x3   

The following pairs are in P>:

COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])
JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])

The following pairs are in Pbound:

LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))

The following pairs are in P≥:

LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))

There are no usable rules.

(28) Complex Obligation (AND)

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

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))


The set Q consists of the following terms:
Cond_Load2110(TRUE, x0, java.lang.Object(IntList(x1, x2)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

(30) IDependencyGraphProof (EQUIVALENT transformation)

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

(31) TRUE

(32) 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:
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(1) -> (2), if ((i637[1] + -1 →* i650[2])∧(o2075[1] →* o2070[2])∧((o2075[1] →* o1946Field0[2])∧(i676[1] →* o1946Field1[2])))



The set Q consists of the following terms:
Cond_Load2110(TRUE, x0, java.lang.Object(IntList(x1, x2)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Load2110(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

(33) IDependencyGraphProof (EQUIVALENT transformation)

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

(34) TRUE

(35) 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:
Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Cond_Load1206ARR1(i116 > 0 && i116 < i3 && i121 > 0 && i116 + 1 > 0, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116 + 1, i121 + -1)
The set Q consists of the following terms:
Load1206(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(36) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

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

Boolean, Integer


The ITRS R consists of the following rules:
Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Cond_Load1206ARR1(i116 > 0 && i116 < i3 && i121 > 0 && i116 + 1 > 0, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116 + 1, i121 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(0) -> (1), if ((java.lang.Object(ARRAY(i3[0], a1405data[0])) →* java.lang.Object(ARRAY(i3[1], a1405data[1])))∧(i116[0] →* i116[1])∧(java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])) →* java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(i121[0] →* i121[1]))


(1) -> (2), if ((i121[1] →* i121[2])∧(java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])) →* java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))∧(java.lang.Object(ARRAY(i3[1], a1405data[1])) →* java.lang.Object(ARRAY(i3[2], a1405data[2])))∧(i116[1] →* i116[2])∧(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i116[2] + 1 →* i116[0])∧(i121[2] + -1 →* i121[0])∧(java.lang.Object(ARRAY(i3[2], a1405data[2])) →* java.lang.Object(ARRAY(i3[0], a1405data[0]))))



The set Q consists of the following terms:
Load1206(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

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

(39) 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): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(0) -> (1), if ((java.lang.Object(ARRAY(i3[0], a1405data[0])) →* java.lang.Object(ARRAY(i3[1], a1405data[1])))∧(i116[0] →* i116[1])∧(java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])) →* java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(i121[0] →* i121[1]))


(1) -> (2), if ((i121[1] →* i121[2])∧(java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])) →* java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))∧(java.lang.Object(ARRAY(i3[1], a1405data[1])) →* java.lang.Object(ARRAY(i3[2], a1405data[2])))∧(i116[1] →* i116[2])∧(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i116[2] + 1 →* i116[0])∧(i121[2] + -1 →* i121[0])∧(java.lang.Object(ARRAY(i3[2], a1405data[2])) →* java.lang.Object(ARRAY(i3[0], a1405data[0]))))



The set Q consists of the following terms:
Load1206(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(40) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(41) 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): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(0) -> (1), if (((i3[0] →* i3[1])∧(a1405data[0] →* a1405data[1]))∧(i116[0] →* i116[1])∧((i212[0] →* i212[1])∧(i211[0] →* i211[1])∧(i213[0] →* i213[1])∧(a1774[0] →* a1774[1]))∧(i121[0] →* i121[1]))


(1) -> (2), if ((i121[1] →* i121[2])∧((i212[1] →* i212[2])∧(i211[1] →* i211[2])∧(i213[1] →* i213[2])∧(a1774[1] →* a1774[2]))∧((i3[1] →* i3[2])∧(a1405data[1] →* a1405data[2]))∧(i116[1] →* i116[2])∧(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0 →* TRUE))


(2) -> (0), if ((i116[2] + 1 →* i116[0])∧(i121[2] + -1 →* i121[0])∧((i3[2] →* i3[0])∧(a1405data[2] →* a1405data[0])))



The set Q consists of the following terms:
Load1206(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(42) 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 LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) the following chains were created:
  • We consider the chain LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0]))) which results in the following constraint:

    (1)    (LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0])≥NonInfC∧LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0])≥LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))∧(UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥))



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

    (2)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧[(-1)bso_17] ≥ 0)



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

    (3)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧[(-1)bso_17] ≥ 0)



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

    (4)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧[(-1)bso_17] ≥ 0)



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

    (5)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)







For Pair LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116, 0), <(i116, i3)), >(i121, 0)), >(+(i116, 1), 0)), java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) the following chains were created:
  • We consider the chain LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))), COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1)) which results in the following constraint:

    (6)    (i121[1]=i121[2]∧i212[1]=i212[2]∧i211[1]=i211[2]∧i213[1]=i213[2]∧a1774[1]=a1774[2]∧i3[1]=i3[2]∧a1405data[1]=a1405data[2]∧i116[1]=i116[2]∧&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0))=TRUE ⇒ LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥NonInfC∧LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥))



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

    (7)    (>(+(i116[1], 1), 0)=TRUE∧>(i121[1], 0)=TRUE∧>(i116[1], 0)=TRUE∧<(i116[1], i3[1])=TRUE ⇒ LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥NonInfC∧LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥))



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

    (8)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (9)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (10)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (11)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)



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

    (12)    ([1] + i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] ≥ 0∧i3[1] + [-2] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)



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

    (13)    ([1] + i116[1] ≥ 0∧i121[1] ≥ 0∧i116[1] ≥ 0∧i3[1] + [-2] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)



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

    (14)    ([1] + i116[1] ≥ 0∧i121[1] ≥ 0∧i116[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)







For Pair COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), +(i116, 1), +(i121, -1)) the following chains were created:
  • We consider the chain COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1)) which results in the following constraint:

    (15)    (COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))≥NonInfC∧COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))≥LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))∧(UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥))



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

    (16)    ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)



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

    (17)    ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)



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

    (18)    ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)



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

    (19)    ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
    • ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

  • LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116, 0), <(i116, i3)), >(i121, 0)), >(+(i116, 1), 0)), java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
    • ([1] + i116[1] ≥ 0∧i121[1] ≥ 0∧i116[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

  • COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), +(i116, 1), +(i121, -1))
    • ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD1206(x1, x2, x3)) = [1] + x3 + [-1]x2 + [-1]x1   
POL(java.lang.Object(x1)) = x1   
POL(ARRAY(x1, x2)) = [-1] + [-1]x1   
POL(LOAD1206ARR1(x1, x2, x3, x4)) = [1] + x3 + [-1]x2 + [-1]x1   
POL(java.lang.String(x1, x2, x3, x4)) = [-1]   
POL(COND_LOAD1206ARR1(x1, x2, x3, x4, x5)) = [1] + x4 + [-1]x3 + [-1]x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(-1) = [-1]   

The following pairs are in P>:

COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))

The following pairs are in Pbound:

LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))

The following pairs are in P≥:

LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))

There are no usable rules.

(43) Complex Obligation (AND)

(44) 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): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))

(0) -> (1), if (((i3[0] →* i3[1])∧(a1405data[0] →* a1405data[1]))∧(i116[0] →* i116[1])∧((i212[0] →* i212[1])∧(i211[0] →* i211[1])∧(i213[0] →* i213[1])∧(a1774[0] →* a1774[1]))∧(i121[0] →* i121[1]))



The set Q consists of the following terms:
Load1206(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(45) IDependencyGraphProof (EQUIVALENT transformation)

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

(46) TRUE

(47) 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:
(0): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(2) -> (0), if ((i116[2] + 1 →* i116[0])∧(i121[2] + -1 →* i121[0])∧((i3[2] →* i3[0])∧(a1405data[2] →* a1405data[0])))



The set Q consists of the following terms:
Load1206(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(48) IDependencyGraphProof (EQUIVALENT transformation)

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

(49) TRUE