(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 0.98 MAINCLASS: Max
public class Max {
public static void main(String[] args) {
int[] a = new int[args.length];
for (int i = 0; i < args.length; i++) {
a[i] = args[i].length();
}
max(a);
}

public static int max(int[] a) {
int x = 0;
int y = a.length-1;

while (x != y) {
if (a[x] <= a[y]) x++;
else y--;
}
return x;
}


}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Max.main([Ljava/lang/String;)V: Graph of 240 nodes with 2 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Max.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 23 rules for P and 0 rules for R.


P rules:
542_0_max_Load(EOS(STATIC_542), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i174) → 543_0_max_EQ(EOS(STATIC_543), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i174, i175)
543_0_max_EQ(EOS(STATIC_543), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i174, i175) → 545_0_max_EQ(EOS(STATIC_545), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i174, i175)
545_0_max_EQ(EOS(STATIC_545), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i174, i175) → 547_0_max_Load(EOS(STATIC_547), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175) | !(=(i174, i175))
547_0_max_Load(EOS(STATIC_547), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175) → 549_0_max_Load(EOS(STATIC_549), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, java.lang.Object(ARRAY(i97)))
549_0_max_Load(EOS(STATIC_549), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, java.lang.Object(ARRAY(i97))) → 551_0_max_ArrayAccess(EOS(STATIC_551), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, java.lang.Object(ARRAY(i97)), i174)
551_0_max_ArrayAccess(EOS(STATIC_551), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, java.lang.Object(ARRAY(i97)), i174) → 553_0_max_ArrayAccess(EOS(STATIC_553), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, java.lang.Object(ARRAY(i97)), i174)
553_0_max_ArrayAccess(EOS(STATIC_553), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, java.lang.Object(ARRAY(i97)), i174) → 556_0_max_Load(EOS(STATIC_556), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i178) | <(i174, i97)
556_0_max_Load(EOS(STATIC_556), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i178) → 558_0_max_Load(EOS(STATIC_558), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i178, java.lang.Object(ARRAY(i97)))
558_0_max_Load(EOS(STATIC_558), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i178, java.lang.Object(ARRAY(i97))) → 559_0_max_ArrayAccess(EOS(STATIC_559), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i178, java.lang.Object(ARRAY(i97)), i175)
559_0_max_ArrayAccess(EOS(STATIC_559), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, java.lang.Object(ARRAY(i97)), i184) → 562_0_max_ArrayAccess(EOS(STATIC_562), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, java.lang.Object(ARRAY(i97)), i184)
562_0_max_ArrayAccess(EOS(STATIC_562), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, java.lang.Object(ARRAY(i97)), i184) → 565_0_max_ArrayAccess(EOS(STATIC_565), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, java.lang.Object(ARRAY(i97)), i184)
565_0_max_ArrayAccess(EOS(STATIC_565), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, java.lang.Object(ARRAY(i97)), i184) → 567_0_max_GT(EOS(STATIC_567), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185) | <(i184, i97)
567_0_max_GT(EOS(STATIC_567), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185) → 571_0_max_GT(EOS(STATIC_571), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185)
567_0_max_GT(EOS(STATIC_567), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185) → 572_0_max_GT(EOS(STATIC_572), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185)
571_0_max_GT(EOS(STATIC_571), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185) → 575_0_max_Inc(EOS(STATIC_575), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184) | >(i178, i185)
575_0_max_Inc(EOS(STATIC_575), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184) → 578_0_max_JMP(EOS(STATIC_578), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, +(i184, -1)) | >=(i184, 0)
578_0_max_JMP(EOS(STATIC_578), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i192) → 583_0_max_Load(EOS(STATIC_583), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i192)
583_0_max_Load(EOS(STATIC_583), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i192) → 541_0_max_Load(EOS(STATIC_541), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i192)
541_0_max_Load(EOS(STATIC_541), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175) → 542_0_max_Load(EOS(STATIC_542), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i175, i174)
572_0_max_GT(EOS(STATIC_572), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184, i178, i185) → 576_0_max_Inc(EOS(STATIC_576), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184) | <=(i178, i185)
576_0_max_Inc(EOS(STATIC_576), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i174, i184) → 579_0_max_JMP(EOS(STATIC_579), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), +(i174, 1), i184) | >=(i174, 0)
579_0_max_JMP(EOS(STATIC_579), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i193, i184) → 584_0_max_Load(EOS(STATIC_584), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i193, i184)
584_0_max_Load(EOS(STATIC_584), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i193, i184) → 541_0_max_Load(EOS(STATIC_541), java.lang.Object(ARRAY(i97)), java.lang.Object(ARRAY(i97)), i193, i184)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.


P rules:
542_0_max_Load(EOS(STATIC_542), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x1) → 542_0_max_Load(EOS(STATIC_542), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, -1), x1) | &&(&&(&&(>(+(x2, 1), 0), <(x2, x0)), <(x1, x0)), !(=(x1, x2)))
542_0_max_Load(EOS(STATIC_542), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x1) → 542_0_max_Load(EOS(STATIC_542), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), x2, +(x1, 1)) | &&(&&(&&(<(x2, x0), >(+(x1, 1), 0)), <(x1, x0)), !(=(x1, x2)))
R rules:

Filtered ground terms:



542_0_max_Load(x1, x2, x3, x4, x5, x6) → 542_0_max_Load(x2, x3, x4, x5, x6)
EOS(x1) → EOS
Cond_542_0_max_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_542_0_max_Load1(x1, x3, x4, x5, x6, x7)
Cond_542_0_max_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_542_0_max_Load(x1, x3, x4, x5, x6, x7)

Filtered duplicate args:



542_0_max_Load(x1, x2, x3, x4, x5) → 542_0_max_Load(x2, x4, x5)
Cond_542_0_max_Load(x1, x2, x3, x4, x5, x6) → Cond_542_0_max_Load(x1, x3, x5, x6)
Cond_542_0_max_Load1(x1, x2, x3, x4, x5, x6) → Cond_542_0_max_Load1(x1, x3, x5, x6)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.


P rules:
542_0_max_Load(java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_max_Load(java.lang.Object(ARRAY(x0)), +(x2, -1), x1) | &&(&&(&&(>(x2, -1), <(x2, x0)), <(x1, x0)), !(=(x1, x2)))
542_0_max_Load(java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_max_Load(java.lang.Object(ARRAY(x0)), x2, +(x1, 1)) | &&(&&(&&(<(x2, x0), >(x1, -1)), <(x1, x0)), !(=(x1, x2)))
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.


P rules:
542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, x1) → COND_542_0_MAX_LOAD(&&(&&(&&(>(x2, -1), <(x2, x0)), <(x1, x0)), !(=(x1, x2))), java.lang.Object(ARRAY(x0)), x2, x1)
COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), +(x2, -1), x1)
542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, x1) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2, x0), >(x1, -1)), <(x1, x0)), !(=(x1, x2))), java.lang.Object(ARRAY(x0)), x2, x1)
COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, +(x1, 1))
R rules:

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

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0]) → COND_542_0_MAX_LOAD(x2[0] > -1 && x2[0] < x0[0] && x1[0] < x0[0] && !(x1[0] = x2[0]), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])
(1): COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), x2[1] + -1, x1[1])
(2): 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])
(3): COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], x1[3] + 1)

(0) -> (1), if (x2[0] > -1 && x2[0] < x0[0] && x1[0] < x0[0] && !(x1[0] = x2[0]) ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧x2[0]* x2[1]x1[0]* x1[1])


(1) -> (0), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[0]))∧x2[1] + -1* x2[0]x1[1]* x1[0])


(1) -> (2), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[2]))∧x2[1] + -1* x2[2]x1[1]* x1[2])


(2) -> (3), if (x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]) ∧java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[3]))∧x2[2]* x2[3]x1[2]* x1[3])


(3) -> (0), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[0]))∧x2[3]* x2[0]x1[3] + 1* x1[0])


(3) -> (2), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[2]))∧x2[3]* x2[2]x1[3] + 1* x1[2])



The set Q is empty.

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@391a3a26 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

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 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, x1) → COND_542_0_MAX_LOAD(&&(&&(&&(>(x2, -1), <(x2, x0)), <(x1, x0)), !(=(x1, x2))), java.lang.Object(ARRAY(x0)), x2, x1) the following chains were created:
  • We consider the chain 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0]) → COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0]), COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1]) which results in the following constraint:

    (1)    (&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0])))=TRUEjava.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x2[0]=x2[1]x1[0]=x1[1]542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])≥COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥))



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

    (2)    (<(x1[0], x0[0])=TRUE>(x2[0], -1)=TRUE<(x2[0], x0[0])=TRUE<(x1[0], x2[0])=TRUE542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])≥COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥))


    (3)    (<(x1[0], x0[0])=TRUE>(x2[0], -1)=TRUE<(x2[0], x0[0])=TRUE>(x1[0], x2[0])=TRUE542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])≥COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥))



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

    (4)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (5)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (6)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (7)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (8)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (9)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧x0[0] + [-1] + [-1]x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (10)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + x0[0] + [-1]x2[0] ≥ 0∧x2[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (11)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + x0[0] + [-1]x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (12)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + x0[0] + [-1]x2[0] ≥ 0∧x2[0] + [-1] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)


    (13)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[-1]x1[0] + x0[0] + [-1]x2[0] ≥ 0∧x2[0] + [-1] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (14)    (x0[0] ≥ 0∧[1] + x1[0] + x2[0] ≥ 0∧[-1] + x0[0] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)Bound*bni_14 + (2)bni_14] + [(2)bni_14]x1[0] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (15)    (x1[0] + x2[0] + x0[0] ≥ 0∧x2[0] ≥ 0∧x0[0] ≥ 0∧x2[0] + [-1] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]x1[0] + [(3)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (16)    ([1] + x2[0] + x0[0] ≥ 0∧[1] + x1[0] + x2[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)Bound*bni_14 + (4)bni_14] + [(2)bni_14]x1[0] + [(3)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)



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

    (17)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]x2[0] + [bni_14]x1[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)







For Pair COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), +(x2, -1), x1) the following chains were created:
  • We consider the chain COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1]) which results in the following constraint:

    (18)    (COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1])≥NonInfC∧COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1])≥542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])∧(UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])), ≥))



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

    (19)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)



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

    (20)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)



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

    (21)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)



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

    (22)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)







For Pair 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, x1) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2, x0), >(x1, -1)), <(x1, x0)), !(=(x1, x2))), java.lang.Object(ARRAY(x0)), x2, x1) the following chains were created:
  • We consider the chain 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]), COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1)) which results in the following constraint:

    (23)    (&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2])))=TRUEjava.lang.Object(ARRAY(x0[2]))=java.lang.Object(ARRAY(x0[3]))∧x2[2]=x2[3]x1[2]=x1[3]542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])∧(UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥))



    We simplified constraint (23) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraints:

    (24)    (<(x1[2], x0[2])=TRUE<(x2[2], x0[2])=TRUE>(x1[2], -1)=TRUE<(x1[2], x2[2])=TRUE542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])∧(UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥))


    (25)    (<(x1[2], x0[2])=TRUE<(x2[2], x0[2])=TRUE>(x1[2], -1)=TRUE>(x1[2], x2[2])=TRUE542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])∧(UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥))



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

    (26)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (27)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (28)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (29)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (30)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (31)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (32)    (x0[2] ≥ 0∧x1[2] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (33)    (x0[2] ≥ 0∧x1[2] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (34)    (x0[2] ≥ 0∧[-1] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_18 + (2)bni_18] + [(2)bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (35)    ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_18 + (4)bni_18] + [(2)bni_18]x1[2] + [(3)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (36)    (x0[2] ≥ 0∧x1[2] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x1[2] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)


    (37)    (x0[2] ≥ 0∧x1[2] + x0[2] + x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x1[2] + [(-1)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)



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

    (38)    (x0[2] ≥ 0∧[1] + x1[2] + x0[2] ≥ 0∧[1] + x2[2] + x1[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [(2)bni_18]x2[2] + [bni_18]x1[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)







For Pair COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, +(x1, 1)) the following chains were created:
  • We consider the chain COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1)) which results in the following constraint:

    (39)    (COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3])≥NonInfC∧COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3])≥542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))∧(UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥))



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

    (40)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_20] = 0∧[1 + (-1)bso_21] ≥ 0)



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

    (41)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_20] = 0∧[1 + (-1)bso_21] ≥ 0)



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

    (42)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_20] = 0∧[1 + (-1)bso_21] ≥ 0)



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

    (43)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_20] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, x1) → COND_542_0_MAX_LOAD(&&(&&(&&(>(x2, -1), <(x2, x0)), <(x1, x0)), !(=(x1, x2))), java.lang.Object(ARRAY(x0)), x2, x1)
    • ([1] + x2[0] + x0[0] ≥ 0∧[1] + x1[0] + x2[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(-1)Bound*bni_14 + (4)bni_14] + [(2)bni_14]x1[0] + [(3)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
    • (x1[0] + x2[0] + x0[0] ≥ 0∧x2[0] ≥ 0∧x0[0] ≥ 0∧x2[0] + [-1] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]x1[0] + [(3)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
    • (x0[0] ≥ 0∧x2[0] ≥ 0∧[1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]x2[0] + [bni_14]x1[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)

  • COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), +(x2, -1), x1)
    • ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)

  • 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, x1) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2, x0), >(x1, -1)), <(x1, x0)), !(=(x1, x2))), java.lang.Object(ARRAY(x0)), x2, x1)
    • ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_18 + (4)bni_18] + [(2)bni_18]x1[2] + [(3)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
    • (x0[2] ≥ 0∧x1[2] + x0[2] + x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x1[2] + [(-1)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
    • (x0[2] ≥ 0∧[1] + x1[2] + x0[2] ≥ 0∧[1] + x2[2] + x1[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [(2)bni_18]x2[2] + [bni_18]x1[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)

  • COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0)), x2, x1) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0)), x2, +(x1, 1))
    • ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_20] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-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(542_0_MAX_LOAD(x1, x2, x3)) = [-1] + [-1]x3 + x2 + [2]x1   
POL(java.lang.Object(x1)) = x1   
POL(ARRAY(x1)) = x1   
POL(COND_542_0_MAX_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [2]x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(-1) = [-1]   
POL(<(x1, x2)) = [-1]   
POL(!(x1)) = [-1]   
POL(=(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(COND_542_0_MAX_LOAD1(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [2]x2   
POL(1) = [1]   

The following pairs are in P>:

COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), +(x2[1], -1), x1[1])
COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))

The following pairs are in Pbound:

542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0]) → COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])

The following pairs are in P:

542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0]) → COND_542_0_MAX_LOAD(&&(&&(&&(>(x2[0], -1), <(x2[0], x0[0])), <(x1[0], x0[0])), !(=(x1[0], x2[0]))), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])
542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])

There are no usable rules.

(9) Complex Obligation (AND)

(10) Obligation:

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


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[0])), x2[0], x1[0]) → COND_542_0_MAX_LOAD(x2[0] > -1 && x2[0] < x0[0] && x1[0] < x0[0] && !(x1[0] = x2[0]), java.lang.Object(ARRAY(x0[0])), x2[0], x1[0])
(2): 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])


The set Q is empty.

(11) IDependencyGraphProof (EQUIVALENT transformation)

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

(12) TRUE

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

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_542_0_MAX_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x1[1]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[1])), x2[1] + -1, x1[1])
(2): 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])
(3): COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], x1[3] + 1)

(1) -> (2), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[2]))∧x2[1] + -1* x2[2]x1[1]* x1[2])


(3) -> (2), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[2]))∧x2[3]* x2[2]x1[3] + 1* x1[2])


(2) -> (3), if (x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]) ∧java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[3]))∧x2[2]* x2[3]x1[2]* x1[3])



The set Q is empty.

(14) IDependencyGraphProof (EQUIVALENT transformation)

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

(15) Obligation:

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


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], x1[3] + 1)
(2): 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])

(3) -> (2), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[2]))∧x2[3]* x2[2]x1[3] + 1* x1[2])


(2) -> (3), if (x2[2] < x0[2] && x1[2] > -1 && x1[2] < x0[2] && !(x1[2] = x2[2]) ∧java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[3]))∧x2[2]* x2[3]x1[2]* x1[3])



The set Q is empty.

(16) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@391a3a26 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

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_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1)) the following chains were created:
  • We consider the chain COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1)) which results in the following constraint:

    (1)    (COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3])≥NonInfC∧COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3])≥542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))∧(UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥))



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

    (2)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_12] = 0∧[(-1)bso_13] ≥ 0)



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

    (3)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_12] = 0∧[(-1)bso_13] ≥ 0)



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

    (4)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_12] = 0∧[(-1)bso_13] ≥ 0)



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

    (5)    ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_13] ≥ 0)







For Pair 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) the following chains were created:
  • We consider the chain 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]), COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1)) which results in the following constraint:

    (6)    (&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2])))=TRUEjava.lang.Object(ARRAY(x0[2]))=java.lang.Object(ARRAY(x0[3]))∧x2[2]=x2[3]x1[2]=x1[3]542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])∧(UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥))



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

    (7)    (<(x1[2], x0[2])=TRUE<(x2[2], x0[2])=TRUE>(x1[2], -1)=TRUE<(x1[2], x2[2])=TRUE542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])∧(UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥))


    (8)    (<(x1[2], x0[2])=TRUE<(x2[2], x0[2])=TRUE>(x1[2], -1)=TRUE>(x1[2], x2[2])=TRUE542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥NonInfC∧542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])≥COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])∧(UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥))



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

    (9)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (10)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (11)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (12)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (13)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (14)    (x0[2] + [-1] + [-1]x1[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (15)    (x0[2] ≥ 0∧x1[2] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] + [-1] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (2)bni_14] + [bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (16)    (x0[2] ≥ 0∧x1[2] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (2)bni_14] + [bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (17)    (x0[2] ≥ 0∧[-1] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + bni_14] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (18)    ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (3)bni_14] + [bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (19)    (x0[2] ≥ 0∧x1[2] + x0[2] + [-1]x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (2)bni_14] + [bni_14]x1[2] + [(-1)bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)


    (20)    (x0[2] ≥ 0∧x1[2] + x0[2] + x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (2)bni_14] + [bni_14]x1[2] + [bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)



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

    (21)    (x0[2] ≥ 0∧[1] + x1[2] + x0[2] ≥ 0∧[1] + x2[2] + x1[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (3)bni_14] + [bni_14]x1[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))
    • ((UIncreasing(542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_13] ≥ 0)

  • 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])
    • ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (3)bni_14] + [bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)
    • (x0[2] ≥ 0∧x1[2] + x0[2] + x2[2] ≥ 0∧x1[2] ≥ 0∧x1[2] + [-1] + x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (2)bni_14] + [bni_14]x1[2] + [bni_14]x2[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)
    • (x0[2] ≥ 0∧[1] + x1[2] + x0[2] ≥ 0∧[1] + x2[2] + x1[2] ≥ 0∧x1[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])), ≥)∧[(-1)Bound*bni_14 + (3)bni_14] + [bni_14]x1[2] + [(2)bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_542_0_MAX_LOAD1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [2]x2 + [-1]x4   
POL(java.lang.Object(x1)) = x1   
POL(ARRAY(x1)) = x1   
POL(542_0_MAX_LOAD(x1, x2, x3)) = [-1]x3 + [-1]x2 + [2]x1   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(&&(x1, x2)) = [-1]   
POL(<(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(-1) = [-1]   
POL(!(x1)) = [-1]   
POL(=(x1, x2)) = [-1]   

The following pairs are in P>:

542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])

The following pairs are in Pbound:

542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[2])), x2[2], x1[2]) → COND_542_0_MAX_LOAD1(&&(&&(&&(<(x2[2], x0[2]), >(x1[2], -1)), <(x1[2], x0[2])), !(=(x1[2], x2[2]))), java.lang.Object(ARRAY(x0[2])), x2[2], x1[2])

The following pairs are in P:

COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], +(x1[3], 1))

There are no usable rules.

(17) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_542_0_MAX_LOAD1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x1[3]) → 542_0_MAX_LOAD(java.lang.Object(ARRAY(x0[3])), x2[3], x1[3] + 1)


The set Q is empty.

(18) IDependencyGraphProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Max.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(21) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 22 rules for P and 0 rules for R.


P rules:
263_0_main_Load(EOS(STATIC_263), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71) → 264_0_main_ArrayLength(EOS(STATIC_264), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71, java.lang.Object(ARRAY(i14)))
264_0_main_ArrayLength(EOS(STATIC_264), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71, java.lang.Object(ARRAY(i14))) → 265_0_main_GE(EOS(STATIC_265), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71, i14) | >=(i14, 0)
265_0_main_GE(EOS(STATIC_265), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71, i14) → 267_0_main_GE(EOS(STATIC_267), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71, i14)
267_0_main_GE(EOS(STATIC_267), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71, i14) → 269_0_main_Load(EOS(STATIC_269), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71) | <(i71, i14)
269_0_main_Load(EOS(STATIC_269), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71) → 271_0_main_Load(EOS(STATIC_271), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)))
271_0_main_Load(EOS(STATIC_271), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14))) → 273_0_main_Load(EOS(STATIC_273), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71)
273_0_main_Load(EOS(STATIC_273), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71) → 274_0_main_Load(EOS(STATIC_274), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)))
274_0_main_Load(EOS(STATIC_274), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14))) → 276_0_main_ArrayAccess(EOS(STATIC_276), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71)
276_0_main_ArrayAccess(EOS(STATIC_276), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71) → 278_0_main_ArrayAccess(EOS(STATIC_278), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71)
278_0_main_ArrayAccess(EOS(STATIC_278), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71) → 281_0_main_InvokeMethod(EOS(STATIC_281), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, o51) | <(i71, i14)
281_0_main_InvokeMethod(EOS(STATIC_281), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(o54sub)) → 284_0_main_InvokeMethod(EOS(STATIC_284), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(o54sub))
284_0_main_InvokeMethod(EOS(STATIC_284), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(o54sub)) → 287_0_length_Load(EOS(STATIC_287), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(o54sub), java.lang.Object(o54sub))
287_0_length_Load(EOS(STATIC_287), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(o54sub), java.lang.Object(o54sub)) → 294_0_length_FieldAccess(EOS(STATIC_294), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(o54sub), java.lang.Object(o54sub))
294_0_length_FieldAccess(EOS(STATIC_294), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(java.lang.String(o58sub, i82)), java.lang.Object(java.lang.String(o58sub, i82))) → 296_0_length_FieldAccess(EOS(STATIC_296), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(java.lang.String(o58sub, i82)), java.lang.Object(java.lang.String(o58sub, i82))) | &&(>=(i82, 0), >=(i83, 0))
296_0_length_FieldAccess(EOS(STATIC_296), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(java.lang.String(o58sub, i82)), java.lang.Object(java.lang.String(o58sub, i82))) → 300_0_length_Return(EOS(STATIC_300), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(java.lang.String(o58sub, i82)))
300_0_length_Return(EOS(STATIC_300), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71, java.lang.Object(java.lang.String(o58sub, i82))) → 305_0_main_ArrayAccess(EOS(STATIC_305), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71)
305_0_main_ArrayAccess(EOS(STATIC_305), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71) → 308_0_main_ArrayAccess(EOS(STATIC_308), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71)
308_0_main_ArrayAccess(EOS(STATIC_308), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, java.lang.Object(ARRAY(i14)), i71) → 314_0_main_Inc(EOS(STATIC_314), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71) | <(i71, i14)
314_0_main_Inc(EOS(STATIC_314), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71) → 320_0_main_JMP(EOS(STATIC_320), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), +(i71, 1)) | >=(i71, 0)
320_0_main_JMP(EOS(STATIC_320), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i87) → 324_0_main_Load(EOS(STATIC_324), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i87)
324_0_main_Load(EOS(STATIC_324), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i87) → 262_0_main_Load(EOS(STATIC_262), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i87)
262_0_main_Load(EOS(STATIC_262), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71) → 263_0_main_Load(EOS(STATIC_263), java.lang.Object(ARRAY(i14)), java.lang.Object(ARRAY(i14)), i71, i71)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.


P rules:
263_0_main_Load(EOS(STATIC_263), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → 263_0_main_Load(EOS(STATIC_263), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), <(x1, x0)), >(+(x0, 1), 0))
R rules:

Filtered ground terms:



263_0_main_Load(x1, x2, x3, x4, x5) → 263_0_main_Load(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_263_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_263_0_main_Load(x1, x3, x4, x5, x6)

Filtered duplicate args:



263_0_main_Load(x1, x2, x3, x4) → 263_0_main_Load(x2, x4)
Cond_263_0_main_Load(x1, x2, x3, x4, x5) → Cond_263_0_main_Load(x1, x3, x5)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.


P rules:
263_0_main_Load(java.lang.Object(ARRAY(x0)), x1) → 263_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1)) | &&(&&(>(x1, -1), <(x1, x0)), >(x0, -1))
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.


P rules:
263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_263_0_MAIN_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1)
COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1))
R rules:

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

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_263_0_MAIN_LOAD(x1[0] > -1 && x1[0] < x0[0] && x0[0] > -1, java.lang.Object(ARRAY(x0[0])), x1[0])
(1): COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), x1[1] + 1)

(0) -> (1), if (x1[0] > -1 && x1[0] < x0[0] && x0[0] > -1java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧x1[0]* x1[1])


(1) -> (0), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[0]))∧x1[1] + 1* x1[0])



The set Q is empty.

(23) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@391a3a26 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

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 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_263_0_MAIN_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1) the following chains were created:
  • We consider the chain 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0]), COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1)) which results in the following constraint:

    (1)    (&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1))=TRUEjava.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x1[0]=x1[1]263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥NonInfC∧263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])∧(UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥))



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

    (2)    (>(x0[0], -1)=TRUE>(x1[0], -1)=TRUE<(x1[0], x0[0])=TRUE263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥NonInfC∧263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0])≥COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])∧(UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥))



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

    (3)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)



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

    (4)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)



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

    (5)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] + [-1] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(-1)bni_10]x1[0] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)



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

    (6)    ([1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)







For Pair COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1)) the following chains were created:
  • We consider the chain COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1)) which results in the following constraint:

    (7)    (COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1])≥NonInfC∧COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1])≥263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))∧(UIncreasing(263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥))



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

    (8)    ((UIncreasing(263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)



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

    (9)    ((UIncreasing(263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)



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

    (10)    ((UIncreasing(263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)



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

    (11)    ((UIncreasing(263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), x1) → COND_263_0_MAIN_LOAD(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x1)
    • ([1] + x1[0] + x0[0] ≥ 0∧x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

  • COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0)), x1) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), +(x1, 1))
    • ((UIncreasing(263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 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(263_0_MAIN_LOAD(x1, x2)) = [-1] + [-1]x2 + x1   
POL(java.lang.Object(x1)) = x1   
POL(ARRAY(x1)) = x1   
POL(COND_263_0_MAIN_LOAD(x1, x2, x3)) = [-1] + [-1]x3 + x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(-1) = [-1]   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   

The following pairs are in P>:

COND_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), +(x1[1], 1))

The following pairs are in Pbound:

263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])

The following pairs are in P:

263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_263_0_MAIN_LOAD(&&(&&(>(x1[0], -1), <(x1[0], x0[0])), >(x0[0], -1)), java.lang.Object(ARRAY(x0[0])), x1[0])

There are no usable rules.

(24) Complex Obligation (AND)

(25) 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): 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), x1[0]) → COND_263_0_MAIN_LOAD(x1[0] > -1 && x1[0] < x0[0] && x0[0] > -1, java.lang.Object(ARRAY(x0[0])), x1[0])


The set Q is empty.

(26) IDependencyGraphProof (EQUIVALENT transformation)

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

(27) TRUE

(28) 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_263_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), x1[1]) → 263_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), x1[1] + 1)


The set Q is empty.

(29) IDependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE