### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: DivMinus2
`public class DivMinus2 {  public static int div(int x, int y) {    int res = 0;    while (x >= y && y > 0) {      x = minus(x,y);      res = res + 1;    }    return res;  }  public static int minus(int x, int y) {    while (y != 0) {      if (y > 0)  {        y--;        x--;      } else  {        y++;        x++;      }    }    return x;  }  public static void main(String[] args) {    Random.args = args;    int x = Random.random();    int y = Random.random();    div(x, y);  }}public class Random {  static String[] args;  static int index = 0;  public static int random() {    String string = args[index];    index++;    return string.length();  }}`

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

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

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

### (4) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
Load1381(i669, i614, i669, i616) → Cond_Load1381(i669 > 0 && i614 >= i669, i669, i614, i669, i616)
Cond_Load1381(TRUE, i669, i614, i669, i616) → Load1471(i669, i669, i616, i669, i614, i669)
Load1471(i669, i669, i616, i669, i730, i743) → Cond_Load1471(i743 > 0, i669, i669, i616, i669, i730, i743)
Cond_Load1471(TRUE, i669, i669, i616, i669, i730, i743) → Load1471(i669, i669, i616, i669, i730 + -1, i743 + -1)
Load1471(i669, i669, i616, i669, i730, 0) → Load1381(i669, i730, i669, i616 + 1)
The set Q consists of the following terms:
Load1471(x0, x0, x1, x0, x2, x3)
Cond_Load1471(TRUE, x0, x0, x1, x0, x2, x3)

### (5) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

Cond_Load1471(x1, x2, x3, x4, x5, x6, x7) → Cond_Load1471(x1, x4, x5, x6, x7)

### (6) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
Load1381(i614, i669, i616) → Cond_Load1381(i669 > 0 && i614 >= i669, i614, i669, i616)
Load1471(i616, i669, i730, i743) → Cond_Load1471(i743 > 0, i616, i669, i730, i743)
Cond_Load1471(TRUE, i616, i669, i730, i743) → Load1471(i616, i669, i730 + -1, i743 + -1)
The set Q consists of the following terms:

### (8) 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:
Load1381(i614, i669, i616) → Cond_Load1381(i669 > 0 && i614 >= i669, i614, i669, i616)
Load1471(i616, i669, i730, i743) → Cond_Load1471(i743 > 0, i616, i669, i730, i743)
Cond_Load1471(TRUE, i616, i669, i730, i743) → Load1471(i616, i669, i730 + -1, i743 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(i669[0] > 0 && i614[0] >= i669[0], i614[0], i669[0], i616[0])
(2): LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(i743[2] > 0, i616[2], i669[2], i730[2], i743[2])
(3): COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], i730[3] + -1, i743[3] + -1)

(0) -> (1), if ((i669[0] > 0 && i614[0] >= i669[0]* TRUE)∧(i616[0]* i616[1])∧(i614[0]* i614[1])∧(i669[0]* i669[1]))

(1) -> (2), if ((i614[1]* i730[2])∧(i669[1]* i743[2])∧(i669[1]* i669[2])∧(i616[1]* i616[2]))

(1) -> (4), if ((i614[1]* i730[4])∧(i669[1]* i669[4])∧(i616[1]* i616[4])∧(i669[1]* 0))

(2) -> (3), if ((i669[2]* i669[3])∧(i743[2] > 0* TRUE)∧(i743[2]* i743[3])∧(i730[2]* i730[3])∧(i616[2]* i616[3]))

(3) -> (2), if ((i669[3]* i669[2])∧(i743[3] + -1* i743[2])∧(i616[3]* i616[2])∧(i730[3] + -1* i730[2]))

(3) -> (4), if ((i669[3]* i669[4])∧(i730[3] + -1* i730[4])∧(i616[3]* i616[4])∧(i743[3] + -1* 0))

(4) -> (0), if ((i669[4]* i669[0])∧(i616[4] + 1* i616[0])∧(i730[4]* i614[0]))

The set Q consists of the following terms:

### (9) 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.

### (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): LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(i669[0] > 0 && i614[0] >= i669[0], i614[0], i669[0], i616[0])
(2): LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(i743[2] > 0, i616[2], i669[2], i730[2], i743[2])
(3): COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], i730[3] + -1, i743[3] + -1)

(0) -> (1), if ((i669[0] > 0 && i614[0] >= i669[0]* TRUE)∧(i616[0]* i616[1])∧(i614[0]* i614[1])∧(i669[0]* i669[1]))

(1) -> (2), if ((i614[1]* i730[2])∧(i669[1]* i743[2])∧(i669[1]* i669[2])∧(i616[1]* i616[2]))

(1) -> (4), if ((i614[1]* i730[4])∧(i669[1]* i669[4])∧(i616[1]* i616[4])∧(i669[1]* 0))

(2) -> (3), if ((i669[2]* i669[3])∧(i743[2] > 0* TRUE)∧(i743[2]* i743[3])∧(i730[2]* i730[3])∧(i616[2]* i616[3]))

(3) -> (2), if ((i669[3]* i669[2])∧(i743[3] + -1* i743[2])∧(i616[3]* i616[2])∧(i730[3] + -1* i730[2]))

(3) -> (4), if ((i669[3]* i669[4])∧(i730[3] + -1* i730[4])∧(i616[3]* i616[4])∧(i743[3] + -1* 0))

(4) -> (0), if ((i669[4]* i669[0])∧(i616[4] + 1* i616[0])∧(i730[4]* i614[0]))

The set Q consists of the following terms:

### (11) 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 LOAD1381(i614, i669, i616) → COND_LOAD1381(&&(>(i669, 0), >=(i614, i669)), i614, i669, i616) the following chains were created:
• We consider the chain LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0]), COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]) which results in the following constraint:

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

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

(3)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]i669[0] + [bni_26]i614[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(4)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]i669[0] + [bni_26]i614[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(5)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]i669[0] + [bni_26]i614[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(6)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[(-1)Bound*bni_26] + [(-1)bni_26]i669[0] + [bni_26]i614[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

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

(7)    (i669[0] ≥ 0∧i614[0] + [-1] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[(-1)Bound*bni_26 + (-1)bni_26] + [(-1)bni_26]i669[0] + [bni_26]i614[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

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

(8)    (i669[0] ≥ 0∧i614[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[(-1)Bound*bni_26] + [bni_26]i614[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair COND_LOAD1381(TRUE, i614, i669, i616) → LOAD1471(i616, i669, i614, i669) the following chains were created:
• We consider the chain COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]), LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]) which results in the following constraint:

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

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

(11)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_29] ≥ 0)

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

(12)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_29] ≥ 0)

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

(13)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_29] ≥ 0)

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

(14)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

• We consider the chain COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]), LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)) which results in the following constraint:

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

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

(17)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_29] ≥ 0)

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

(18)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_29] ≥ 0)

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

(19)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_29] ≥ 0)

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

(20)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair LOAD1471(i616, i669, i730, i743) → COND_LOAD1471(>(i743, 0), i616, i669, i730, i743) the following chains were created:
• We consider the chain LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]), COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)) which results in the following constraint:

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

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

(23)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[(-1)Bound*bni_30] + [bni_30]i730[2] + [(-1)bni_30]i669[2] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

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

(24)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[(-1)Bound*bni_30] + [bni_30]i730[2] + [(-1)bni_30]i669[2] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

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

(25)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[(-1)Bound*bni_30] + [bni_30]i730[2] + [(-1)bni_30]i669[2] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

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

(26)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[bni_30] = 0∧[(-1)bni_30] = 0∧0 = 0∧[(-1)Bound*bni_30] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

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

(27)    (i743[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[bni_30] = 0∧[(-1)bni_30] = 0∧0 = 0∧[(-1)Bound*bni_30] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

For Pair COND_LOAD1471(TRUE, i616, i669, i730, i743) → LOAD1471(i616, i669, +(i730, -1), +(i743, -1)) the following chains were created:
• We consider the chain LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]), COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)), LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]) which results in the following constraint:

(28)    (i669[2]=i669[3]>(i743[2], 0)=TRUEi743[2]=i743[3]i730[2]=i730[3]i616[2]=i616[3]i669[3]=i669[2]1+(i743[3], -1)=i743[2]1i616[3]=i616[2]1+(i730[3], -1)=i730[2]1COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3])≥NonInfC∧COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3])≥LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))∧(UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥))

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

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

(30)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [bni_32]i730[2] + [(-1)bni_32]i669[2] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(31)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [bni_32]i730[2] + [(-1)bni_32]i669[2] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(32)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [bni_32]i730[2] + [(-1)bni_32]i669[2] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(33)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[bni_32] = 0∧[(-1)bni_32] = 0∧0 = 0∧[(-1)bni_32 + (-1)Bound*bni_32] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

(34)    (i743[2] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[bni_32] = 0∧[(-1)bni_32] = 0∧0 = 0∧[(-1)bni_32 + (-1)Bound*bni_32] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

• We consider the chain LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]), COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)), LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)) which results in the following constraint:

(35)    (i669[2]=i669[3]>(i743[2], 0)=TRUEi743[2]=i743[3]i730[2]=i730[3]i616[2]=i616[3]i669[3]=i669[4]+(i730[3], -1)=i730[4]i616[3]=i616[4]+(i743[3], -1)=0COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3])≥NonInfC∧COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3])≥LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))∧(UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥))

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

(36)    (>(i743[2], 0)=TRUE+(i743[2], -1)=0COND_LOAD1471(TRUE, i616[2], i669[2], i730[2], i743[2])≥NonInfC∧COND_LOAD1471(TRUE, i616[2], i669[2], i730[2], i743[2])≥LOAD1471(i616[2], i669[2], +(i730[2], -1), +(i743[2], -1))∧(UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥))

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

(37)    (i743[2] + [-1] ≥ 0∧i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [bni_32]i730[2] + [(-1)bni_32]i669[2] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(38)    (i743[2] + [-1] ≥ 0∧i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [bni_32]i730[2] + [(-1)bni_32]i669[2] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(39)    (i743[2] + [-1] ≥ 0∧i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [bni_32]i730[2] + [(-1)bni_32]i669[2] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(40)    (i743[2] + [-1] ≥ 0∧i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[bni_32] = 0∧[(-1)bni_32] = 0∧0 = 0∧[(-1)bni_32 + (-1)Bound*bni_32] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

(41)    (i743[2] ≥ 0∧i743[2] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[bni_32] = 0∧[(-1)bni_32] = 0∧0 = 0∧[(-1)bni_32 + (-1)Bound*bni_32] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair LOAD1471(i616, i669, i730, 0) → LOAD1381(i730, i669, +(i616, 1)) the following chains were created:
• We consider the chain COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]), LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)), LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0]) which results in the following constraint:

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

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

(44)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧[(-1)bso_35] ≥ 0)

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

(45)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧[(-1)bso_35] ≥ 0)

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

(46)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧[(-1)bso_35] ≥ 0)

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

(47)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

• We consider the chain COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)), LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)), LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0]) which results in the following constraint:

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

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

(50)    (i743[3] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 ≥ 0∧[(-1)bso_35] ≥ 0)

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

(51)    (i743[3] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 ≥ 0∧[(-1)bso_35] ≥ 0)

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

(52)    (i743[3] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 ≥ 0∧[(-1)bso_35] ≥ 0)

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

(53)    (i743[3] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1381(i614, i669, i616) → COND_LOAD1381(&&(>(i669, 0), >=(i614, i669)), i614, i669, i616)
• (i669[0] ≥ 0∧i614[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[(-1)Bound*bni_26] + [bni_26]i614[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

• ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
• ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

• LOAD1471(i616, i669, i730, i743) → COND_LOAD1471(>(i743, 0), i616, i669, i730, i743)
• (i743[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[bni_30] = 0∧[(-1)bni_30] = 0∧0 = 0∧[(-1)Bound*bni_30] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

• COND_LOAD1471(TRUE, i616, i669, i730, i743) → LOAD1471(i616, i669, +(i730, -1), +(i743, -1))
• (i743[2] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[bni_32] = 0∧[(-1)bni_32] = 0∧0 = 0∧[(-1)bni_32 + (-1)Bound*bni_32] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
• (i743[2] ≥ 0∧i743[2] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[bni_32] = 0∧[(-1)bni_32] = 0∧0 = 0∧[(-1)bni_32 + (-1)Bound*bni_32] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

• ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
• (i743[3] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 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(LOAD1381(x1, x2, x3)) = [-1]x2 + x1
POL(COND_LOAD1381(x1, x2, x3, x4)) = [-1]x3 + x2 + [-1]x1
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(>=(x1, x2)) = [-1]
POL(LOAD1471(x1, x2, x3, x4)) = x3 + [-1]x2
POL(COND_LOAD1471(x1, x2, x3, x4, x5)) = [-1] + x4 + [-1]x3
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(1) = [1]

The following pairs are in P>:

The following pairs are in Pbound:

The following pairs are in P:

COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))

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

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

### (13) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(i669[0] > 0 && i614[0] >= i669[0], i614[0], i669[0], i616[0])
(3): COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], i730[3] + -1, i743[3] + -1)

(4) -> (0), if ((i669[4]* i669[0])∧(i616[4] + 1* i616[0])∧(i730[4]* i614[0]))

(0) -> (1), if ((i669[0] > 0 && i614[0] >= i669[0]* TRUE)∧(i616[0]* i616[1])∧(i614[0]* i614[1])∧(i669[0]* i669[1]))

(1) -> (4), if ((i614[1]* i730[4])∧(i669[1]* i669[4])∧(i616[1]* i616[4])∧(i669[1]* 0))

(3) -> (4), if ((i669[3]* i669[4])∧(i730[3] + -1* i730[4])∧(i616[3]* i616[4])∧(i743[3] + -1* 0))

The set Q consists of the following terms:

### (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:
(0): LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(i669[0] > 0 && i614[0] >= i669[0], i614[0], i669[0], i616[0])

(4) -> (0), if ((i669[4]* i669[0])∧(i616[4] + 1* i616[0])∧(i730[4]* i614[0]))

(0) -> (1), if ((i669[0] > 0 && i614[0] >= i669[0]* TRUE)∧(i616[0]* i616[1])∧(i614[0]* i614[1])∧(i669[0]* i669[1]))

(1) -> (4), if ((i614[1]* i730[4])∧(i669[1]* i669[4])∧(i616[1]* i616[4])∧(i669[1]* 0))

The set Q consists of the following terms:

### (16) IDPNonInfProof (SOUND transformation)

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

For Pair LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)) the following chains were created:
• We consider the chain COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]), LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)), LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0]) which results in the following constraint:

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

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

(3)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧[1 + (-1)bso_21] ≥ 0)

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

(4)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧[1 + (-1)bso_21] ≥ 0)

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

(5)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧[1 + (-1)bso_21] ≥ 0)

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

(6)    ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)

For Pair COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]) the following chains were created:
• We consider the chain COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]), LOAD1471(i616[4], i669[4], i730[4], 0) → LOAD1381(i730[4], i669[4], +(i616[4], 1)) which results in the following constraint:

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

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

(9)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_23] ≥ 0)

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

(10)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_23] ≥ 0)

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

(11)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧[(-1)bso_23] ≥ 0)

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

(12)    ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

For Pair LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0]) the following chains were created:
• We consider the chain LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0]), COND_LOAD1381(TRUE, i614[1], i669[1], i616[1]) → LOAD1471(i616[1], i669[1], i614[1], i669[1]) which results in the following constraint:

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

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

(15)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧[-2 + (-1)bso_25] + [3]i669[0] ≥ 0)

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

(16)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧[-2 + (-1)bso_25] + [3]i669[0] ≥ 0)

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

(17)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧[-2 + (-1)bso_25] + [3]i669[0] ≥ 0)

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

(18)    (i669[0] + [-1] ≥ 0∧i614[0] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧0 = 0∧[-2 + (-1)bso_25] + [3]i669[0] ≥ 0)

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

(19)    (i669[0] ≥ 0∧i614[0] + [-1] + [-1]i669[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧0 = 0∧[1 + (-1)bso_25] + [3]i669[0] ≥ 0)

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

(20)    (i669[0] ≥ 0∧i614[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧0 = 0∧[1 + (-1)bso_25] + [3]i669[0] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• ((UIncreasing(LOAD1381(i730[4], i669[4], +(i616[4], 1))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)

• ((UIncreasing(LOAD1471(i616[1], i669[1], i614[1], i669[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• LOAD1381(i614[0], i669[0], i616[0]) → COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])
• (i669[0] ≥ 0∧i614[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1381(&&(>(i669[0], 0), >=(i614[0], i669[0])), i614[0], i669[0], i616[0])), ≥)∧0 = 0∧[bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i669[0] ≥ 0∧0 = 0∧[1 + (-1)bso_25] + [3]i669[0] ≥ 0)

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

POL(TRUE) = [1]
POL(FALSE) = [1]
POL(LOAD1471(x1, x2, x3, x4)) = [-1]x4 + [-1]x2
POL(0) = 0
POL(LOAD1381(x1, x2, x3)) = [-1] + [2]x2
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(COND_LOAD1381(x1, x2, x3, x4)) = [1] + [-1]x3 + [-1]x1
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]

The following pairs are in P>:

The following pairs are in Pbound:

The following pairs are in P:

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

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

### (18) Obligation:

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

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:

### (19) IDependencyGraphProof (EQUIVALENT transformation)

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

### (21) 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) -> (4), if ((i614[1]* i730[4])∧(i669[1]* i669[4])∧(i616[1]* i616[4])∧(i669[1]* 0))

The set Q consists of the following terms:

### (22) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(2): LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(i743[2] > 0, i616[2], i669[2], i730[2], i743[2])
(3): COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], i730[3] + -1, i743[3] + -1)

(1) -> (2), if ((i614[1]* i730[2])∧(i669[1]* i743[2])∧(i669[1]* i669[2])∧(i616[1]* i616[2]))

(3) -> (2), if ((i669[3]* i669[2])∧(i743[3] + -1* i743[2])∧(i616[3]* i616[2])∧(i730[3] + -1* i730[2]))

(2) -> (3), if ((i669[2]* i669[3])∧(i743[2] > 0* TRUE)∧(i743[2]* i743[3])∧(i730[2]* i730[3])∧(i616[2]* i616[3]))

(1) -> (4), if ((i614[1]* i730[4])∧(i669[1]* i669[4])∧(i616[1]* i616[4])∧(i669[1]* 0))

(3) -> (4), if ((i669[3]* i669[4])∧(i730[3] + -1* i730[4])∧(i616[3]* i616[4])∧(i743[3] + -1* 0))

The set Q consists of the following terms:

### (25) IDependencyGraphProof (EQUIVALENT transformation)

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

### (26) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], i730[3] + -1, i743[3] + -1)
(2): LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(i743[2] > 0, i616[2], i669[2], i730[2], i743[2])

(3) -> (2), if ((i669[3]* i669[2])∧(i743[3] + -1* i743[2])∧(i616[3]* i616[2])∧(i730[3] + -1* i730[2]))

(2) -> (3), if ((i669[2]* i669[3])∧(i743[2] > 0* TRUE)∧(i743[2]* i743[3])∧(i730[2]* i730[3])∧(i616[2]* i616[3]))

The set Q consists of the following terms:

### (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 COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)) the following chains were created:
• We consider the chain LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]), COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)), LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]) which results in the following constraint:

(1)    (i669[2]=i669[3]>(i743[2], 0)=TRUEi743[2]=i743[3]i730[2]=i730[3]i616[2]=i616[3]i669[3]=i669[2]1+(i743[3], -1)=i743[2]1i616[3]=i616[2]1+(i730[3], -1)=i730[2]1COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3])≥NonInfC∧COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3])≥LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))∧(UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥))

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

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

(3)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(2)bni_15 + (-1)Bound*bni_15] + [bni_15]i743[2] ≥ 0∧[1 + (-1)bso_16] ≥ 0)

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

(4)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(2)bni_15 + (-1)Bound*bni_15] + [bni_15]i743[2] ≥ 0∧[1 + (-1)bso_16] ≥ 0)

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

(5)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧[(2)bni_15 + (-1)Bound*bni_15] + [bni_15]i743[2] ≥ 0∧[1 + (-1)bso_16] ≥ 0)

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

(6)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_15 + (-1)Bound*bni_15] + [bni_15]i743[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

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

(7)    (i743[2] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_15 + (-1)Bound*bni_15] + [bni_15]i743[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

For Pair LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]) the following chains were created:
• We consider the chain LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2]), COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1)) which results in the following constraint:

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

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

(10)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i743[2] ≥ 0∧[(-1)bso_18] ≥ 0)

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

(11)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i743[2] ≥ 0∧[(-1)bso_18] ≥ 0)

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

(12)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i743[2] ≥ 0∧[(-1)bso_18] ≥ 0)

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

(13)    (i743[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i743[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_18] ≥ 0)

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

(14)    (i743[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_17 + (-1)Bound*bni_17] + [bni_17]i743[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_18] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))
• (i743[2] ≥ 0 ⇒ (UIncreasing(LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_15 + (-1)Bound*bni_15] + [bni_15]i743[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

• LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])
• (i743[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1471(>(i743[2], 0), i616[2], i669[2], i730[2], i743[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_17 + (-1)Bound*bni_17] + [bni_17]i743[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_18] ≥ 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) = [2]
POL(FALSE) = 0
POL(COND_LOAD1471(x1, x2, x3, x4, x5)) = [2] + x5
POL(LOAD1471(x1, x2, x3, x4)) = [2] + x4
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0

The following pairs are in P>:

COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))

The following pairs are in Pbound:

COND_LOAD1471(TRUE, i616[3], i669[3], i730[3], i743[3]) → LOAD1471(i616[3], i669[3], +(i730[3], -1), +(i743[3], -1))

The following pairs are in P:

There are no usable rules.

### (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:
(2): LOAD1471(i616[2], i669[2], i730[2], i743[2]) → COND_LOAD1471(i743[2] > 0, i616[2], i669[2], i730[2], i743[2])

The set Q consists of the following terms:

### (30) IDependencyGraphProof (EQUIVALENT transformation)

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

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

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms: