### (0) Obligation:

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

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

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 185 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:
Load425(i60, i69) → Cond_Load425(i60 > 0 && i60 <= i69, i60, i69)
Load425(i60, i69) → Cond_Load4251(i69 > 0 && i60 > i69, i60, i69)
The set Q consists of the following terms:

### (6) 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:
Load425(i60, i69) → Cond_Load425(i60 > 0 && i60 <= i69, i60, i69)
Load425(i60, i69) → Cond_Load4251(i69 > 0 && i60 > i69, i60, i69)

The integer pair graph contains the following rules and edges:
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])
(6): LOAD425(i60[6], i69[6]) → COND_LOAD4251(i69[6] > 0 && i60[6] > i69[6], i60[6], i69[6])

(0) -> (1), if ((i69[0]* i69[1])∧(i60[0]* i60[1])∧(i60[0] > 0 && i60[0] <= i69[0]* TRUE))

(1) -> (2), if ((i69[1]* i99[2])∧(i60[1]* i60[2]))

(1) -> (4), if ((i60[1]* i60[4])∧(i69[1]* 0))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(3) -> (4), if ((i60[3]* i60[4])∧(i99[3] + -1* 0))

(4) -> (0), if ((i60[4]* i60[0])∧(0* i69[0]))

(4) -> (6), if ((0* i69[6])∧(i60[4]* i60[6]))

(5) -> (0), if ((i69[5]* i69[0])∧(0* i60[0]))

(5) -> (6), if ((i69[5]* i69[6])∧(0* i60[6]))

(6) -> (7), if ((i60[6]* i60[7])∧(i69[6]* i69[7])∧(i69[6] > 0 && i60[6] > i69[6]* TRUE))

(7) -> (5), if ((i69[7]* i69[5])∧(i60[7]* 0))

(7) -> (8), if ((i60[7]* i101[8])∧(i69[7]* i69[8]))

(8) -> (9), if ((i101[8] > 0* TRUE)∧(i101[8]* i101[9])∧(i69[8]* i69[9]))

(9) -> (5), if ((i69[9]* i69[5])∧(i101[9] + -1* 0))

(9) -> (8), if ((i101[9] + -1* i101[8])∧(i69[9]* i69[8]))

The set Q consists of the following terms:

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

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

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])
(6): LOAD425(i60[6], i69[6]) → COND_LOAD4251(i69[6] > 0 && i60[6] > i69[6], i60[6], i69[6])

(0) -> (1), if ((i69[0]* i69[1])∧(i60[0]* i60[1])∧(i60[0] > 0 && i60[0] <= i69[0]* TRUE))

(1) -> (2), if ((i69[1]* i99[2])∧(i60[1]* i60[2]))

(1) -> (4), if ((i60[1]* i60[4])∧(i69[1]* 0))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(3) -> (4), if ((i60[3]* i60[4])∧(i99[3] + -1* 0))

(4) -> (0), if ((i60[4]* i60[0])∧(0* i69[0]))

(4) -> (6), if ((0* i69[6])∧(i60[4]* i60[6]))

(5) -> (0), if ((i69[5]* i69[0])∧(0* i60[0]))

(5) -> (6), if ((i69[5]* i69[6])∧(0* i60[6]))

(6) -> (7), if ((i60[6]* i60[7])∧(i69[6]* i69[7])∧(i69[6] > 0 && i60[6] > i69[6]* TRUE))

(7) -> (5), if ((i69[7]* i69[5])∧(i60[7]* 0))

(7) -> (8), if ((i60[7]* i101[8])∧(i69[7]* i69[8]))

(8) -> (9), if ((i101[8] > 0* TRUE)∧(i101[8]* i101[9])∧(i69[8]* i69[9]))

(9) -> (5), if ((i69[9]* i69[5])∧(i101[9] + -1* 0))

(9) -> (8), if ((i101[9] + -1* i101[8])∧(i69[9]* i69[8]))

The set Q consists of the following terms:

### (9) 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 LOAD425(i60, i69) → COND_LOAD425(&&(>(i60, 0), <=(i60, i69)), i60, i69) the following chains were created:
• We consider the chain LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0]), COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[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)    (i60[0] + [-1] ≥ 0∧i69[0] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(2)bni_31]i60[0] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(4)    (i60[0] + [-1] ≥ 0∧i69[0] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(2)bni_31]i60[0] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(5)    (i60[0] + [-1] ≥ 0∧i69[0] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(2)bni_31]i60[0] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(6)    (i60[0] ≥ 0∧i69[0] + [-1] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(2)bni_31]i60[0] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(7)    (i60[0] ≥ 0∧i69[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(2)bni_31]i60[0] ≥ 0∧[(-1)bso_32] ≥ 0)

For Pair COND_LOAD425(TRUE, i60, i69) → LOAD702(i60, i69) the following chains were created:
• We consider the chain COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1]), LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]) 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)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_34] ≥ 0)

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

(11)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_34] ≥ 0)

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

(12)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_34] ≥ 0)

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

(13)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

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

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

(16)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_34] ≥ 0)

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

(17)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_34] ≥ 0)

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

(18)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_34] ≥ 0)

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

(19)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧[(-1)bso_34] ≥ 0)

For Pair LOAD702(i60, i99) → COND_LOAD702(>(i99, 0), i60, i99) the following chains were created:
• We consider the chain LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]), COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1)) which results in the following constraint:

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

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

(22)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(2)bni_35]i60[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(23)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(2)bni_35]i60[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(24)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(2)bni_35]i60[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(25)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(2)bni_35] = 0∧[(-1)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

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

(26)    (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(2)bni_35] = 0∧[(-1)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

For Pair COND_LOAD702(TRUE, i60, i99) → LOAD702(i60, +(i99, -1)) the following chains were created:

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

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

(29)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i60[2] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(30)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i60[2] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(31)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i60[2] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(32)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

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

(33)    (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

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

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

(36)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i60[2] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(37)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i60[2] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(38)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]i60[2] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(39)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

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

(40)    (i99[2] ≥ 0∧i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

For Pair LOAD702(i60, 0) → LOAD425(i60, 0) the following chains were created:
• We consider the chain LOAD702(i60[4], 0) → LOAD425(i60[4], 0), LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0]) which results in the following constraint:

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

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

(43)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_40] ≥ 0)

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

(44)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_40] ≥ 0)

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

(45)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_40] ≥ 0)

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

(46)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)

• We consider the chain LOAD702(i60[4], 0) → LOAD425(i60[4], 0), LOAD425(i60[6], i69[6]) → COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6]) which results in the following constraint:

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

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

(49)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_40] ≥ 0)

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

(50)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_40] ≥ 0)

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

(51)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_40] ≥ 0)

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

(52)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)

For Pair LOAD719(0, i69) → LOAD425(0, i69) the following chains were created:
• We consider the chain LOAD719(0, i69[5]) → LOAD425(0, i69[5]), LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0]) which results in the following constraint:

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

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

(55)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧[(-1)bso_42] ≥ 0)

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

(56)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧[(-1)bso_42] ≥ 0)

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

(57)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧[(-1)bso_42] ≥ 0)

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

(58)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)

• We consider the chain LOAD719(0, i69[5]) → LOAD425(0, i69[5]), LOAD425(i60[6], i69[6]) → COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6]) which results in the following constraint:

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

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

(61)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧[(-1)bso_42] ≥ 0)

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

(62)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧[(-1)bso_42] ≥ 0)

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

(63)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧[(-1)bso_42] ≥ 0)

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

(64)    ((UIncreasing(LOAD425(0, i69[5])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)

For Pair LOAD425(i60, i69) → COND_LOAD4251(&&(>(i69, 0), >(i60, i69)), i60, i69) the following chains were created:
• We consider the chain LOAD425(i60[6], i69[6]) → COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6]), COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7]) which results in the following constraint:

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

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

(67)    (i69[6] + [-1] ≥ 0∧i60[6] + [-1] + [-1]i69[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]i60[6] ≥ 0∧[-1 + (-1)bso_44] + i60[6] ≥ 0)

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

(68)    (i69[6] + [-1] ≥ 0∧i60[6] + [-1] + [-1]i69[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]i60[6] ≥ 0∧[-1 + (-1)bso_44] + i60[6] ≥ 0)

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

(69)    (i69[6] + [-1] ≥ 0∧i60[6] + [-1] + [-1]i69[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]i60[6] ≥ 0∧[-1 + (-1)bso_44] + i60[6] ≥ 0)

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

(70)    (i69[6] ≥ 0∧i60[6] + [-2] + [-1]i69[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]i60[6] ≥ 0∧[-1 + (-1)bso_44] + i60[6] ≥ 0)

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

(71)    (i69[6] ≥ 0∧i60[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥)∧[(3)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]i69[6] + [(2)bni_43]i60[6] ≥ 0∧[1 + (-1)bso_44] + i69[6] + i60[6] ≥ 0)

For Pair COND_LOAD4251(TRUE, i60, i69) → LOAD719(i60, i69) the following chains were created:

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

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

(74)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧[(-1)bso_46] ≥ 0)

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

(75)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧[(-1)bso_46] ≥ 0)

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

(76)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧[(-1)bso_46] ≥ 0)

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

(77)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)

• We consider the chain COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7]), LOAD719(i101[8], i69[8]) → COND_LOAD719(>(i101[8], 0), i101[8], i69[8]) which results in the following constraint:

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

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

(80)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧[(-1)bso_46] ≥ 0)

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

(81)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧[(-1)bso_46] ≥ 0)

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

(82)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧[(-1)bso_46] ≥ 0)

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

(83)    ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

For Pair LOAD719(i101, i69) → COND_LOAD719(>(i101, 0), i101, i69) the following chains were created:
• We consider the chain LOAD719(i101[8], i69[8]) → COND_LOAD719(>(i101[8], 0), i101[8], i69[8]), COND_LOAD719(TRUE, i101[9], i69[9]) → LOAD719(+(i101[9], -1), i69[9]) which results in the following constraint:

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

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

(86)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [bni_47]i101[8] ≥ 0∧[(-1)bso_48] ≥ 0)

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

(87)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [bni_47]i101[8] ≥ 0∧[(-1)bso_48] ≥ 0)

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

(88)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [bni_47]i101[8] ≥ 0∧[(-1)bso_48] ≥ 0)

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

(89)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥)∧0 = 0∧[(-1)bni_47 + (-1)Bound*bni_47] + [bni_47]i101[8] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

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

(90)    (i101[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥)∧0 = 0∧[(-1)Bound*bni_47] + [bni_47]i101[8] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

For Pair COND_LOAD719(TRUE, i101, i69) → LOAD719(+(i101, -1), i69) the following chains were created:

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

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

(93)    (i101[8] + [-1] ≥ 0∧i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧[1 + (-1)bso_50] ≥ 0)

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

(94)    (i101[8] + [-1] ≥ 0∧i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧[1 + (-1)bso_50] ≥ 0)

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

(95)    (i101[8] + [-1] ≥ 0∧i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧[1 + (-1)bso_50] ≥ 0)

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

(96)    (i101[8] + [-1] ≥ 0∧i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧0 = 0∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

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

(97)    (i101[8] ≥ 0∧i101[8] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧0 = 0∧[(-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

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

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

(100)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧[1 + (-1)bso_50] ≥ 0)

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

(101)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧[1 + (-1)bso_50] ≥ 0)

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

(102)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧[1 + (-1)bso_50] ≥ 0)

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

(103)    (i101[8] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧0 = 0∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

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

(104)    (i101[8] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧0 = 0∧[(-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i60[0] ≥ 0∧i69[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(2)bni_31]i60[0] ≥ 0∧[(-1)bso_32] ≥ 0)

• ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)
• ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧[(-1)bso_34] ≥ 0)

• (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(2)bni_35] = 0∧[(-1)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

• (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)
• (i99[2] ≥ 0∧i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(2)bni_37] = 0∧[(-1)bni_37 + (-1)Bound*bni_37] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

• ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)
• ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)

• ((UIncreasing(LOAD425(0, i69[5])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)
• ((UIncreasing(LOAD425(0, i69[5])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)

• (i69[6] ≥ 0∧i60[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥)∧[(3)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]i69[6] + [(2)bni_43]i60[6] ≥ 0∧[1 + (-1)bso_44] + i69[6] + i60[6] ≥ 0)

• ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)
• ((UIncreasing(LOAD719(i60[7], i69[7])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

• (i101[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥)∧0 = 0∧[(-1)Bound*bni_47] + [bni_47]i101[8] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

• (i101[8] ≥ 0∧i101[8] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧0 = 0∧[(-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧0 = 0∧[1 + (-1)bso_50] ≥ 0)
• (i101[8] ≥ 0 ⇒ (UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥)∧0 = 0∧[(-1)Bound*bni_49] + [bni_49]i101[8] ≥ 0∧0 = 0∧[1 + (-1)bso_50] ≥ 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(LOAD425(x1, x2)) = [-1] + [2]x1
POL(COND_LOAD425(x1, x2, x3)) = [-1] + [2]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<=(x1, x2)) = [-1]
POL(LOAD702(x1, x2)) = [-1] + [2]x1
POL(COND_LOAD702(x1, x2, x3)) = [-1] + [2]x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(LOAD719(x1, x2)) = [-1] + x1
POL(COND_LOAD4251(x1, x2, x3)) = [-1] + x2 + [-1]x1
POL(COND_LOAD719(x1, x2, x3)) = [-1] + x2

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

### (11) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])

(4) -> (0), if ((i60[4]* i60[0])∧(0* i69[0]))

(5) -> (0), if ((i69[5]* i69[0])∧(0* i60[0]))

(0) -> (1), if ((i69[0]* i69[1])∧(i60[0]* i60[1])∧(i60[0] > 0 && i60[0] <= i69[0]* TRUE))

(1) -> (2), if ((i69[1]* i99[2])∧(i60[1]* i60[2]))

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

(1) -> (4), if ((i60[1]* i60[4])∧(i69[1]* 0))

(3) -> (4), if ((i60[3]* i60[4])∧(i99[3] + -1* 0))

(7) -> (5), if ((i69[7]* i69[5])∧(i60[7]* 0))

(7) -> (8), if ((i60[7]* i101[8])∧(i69[7]* i69[8]))

The set Q consists of the following terms:

### (12) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])

(4) -> (0), if ((i60[4]* i60[0])∧(0* i69[0]))

(0) -> (1), if ((i69[0]* i69[1])∧(i60[0]* i60[1])∧(i60[0] > 0 && i60[0] <= i69[0]* TRUE))

(1) -> (2), if ((i69[1]* i99[2])∧(i60[1]* i60[2]))

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

(1) -> (4), if ((i60[1]* i60[4])∧(i69[1]* 0))

(3) -> (4), if ((i60[3]* i60[4])∧(i99[3] + -1* 0))

The set Q consists of the following terms:

### (14) 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 LOAD702(i60[4], 0) → LOAD425(i60[4], 0) the following chains were created:
• We consider the chain LOAD702(i60[4], 0) → LOAD425(i60[4], 0), LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0]) which results in the following constraint:

We simplified constraint (1) using rule (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(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_21] ≥ 0)

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

(4)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_21] ≥ 0)

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

(5)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧[(-1)bso_21] ≥ 0)

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

(6)    ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1)) the following chains were created:

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)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i60[2] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(10)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i60[2] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(11)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i60[2] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(12)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

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

(13)    (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

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

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

(16)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i60[2] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(17)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i60[2] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(18)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i60[2] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(19)    (i99[2] + [-1] ≥ 0∧i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

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

(20)    (i99[2] ≥ 0∧i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

For Pair LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]) the following chains were created:
• We consider the chain LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]), COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[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)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i60[2] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(24)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i60[2] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(25)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i60[2] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(26)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

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

(27)    (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1]) the following chains were created:
• We consider the chain COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1]), LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]) which results in the following constraint:

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

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

(30)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_27] ≥ 0)

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

(31)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_27] ≥ 0)

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

(32)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_27] ≥ 0)

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

(33)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

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

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

(36)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_27] ≥ 0)

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

(37)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_27] ≥ 0)

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

(38)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧[(-1)bso_27] ≥ 0)

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

(39)    ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0]) the following chains were created:
• We consider the chain LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0]), COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1]) which results in the following constraint:

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

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

(42)    (i60[0] + [-1] ≥ 0∧i69[0] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(2)bni_28]i69[0] + [(-1)bni_28]i60[0] ≥ 0∧[(-1)bso_29] + [2]i69[0] ≥ 0)

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

(43)    (i60[0] + [-1] ≥ 0∧i69[0] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(2)bni_28]i69[0] + [(-1)bni_28]i60[0] ≥ 0∧[(-1)bso_29] + [2]i69[0] ≥ 0)

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

(44)    (i60[0] + [-1] ≥ 0∧i69[0] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(2)bni_28]i69[0] + [(-1)bni_28]i60[0] ≥ 0∧[(-1)bso_29] + [2]i69[0] ≥ 0)

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

(45)    (i60[0] ≥ 0∧i69[0] + [-1] + [-1]i60[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-2)bni_28 + (-1)Bound*bni_28] + [(2)bni_28]i69[0] + [(-1)bni_28]i60[0] ≥ 0∧[(-1)bso_29] + [2]i69[0] ≥ 0)

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

(46)    (i60[0] ≥ 0∧i69[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i60[0] + [(2)bni_28]i69[0] ≥ 0∧[2 + (-1)bso_29] + [2]i60[0] + [2]i69[0] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• ((UIncreasing(LOAD425(i60[4], 0)), ≥)∧0 = 0∧[(-1)bso_21] ≥ 0)

• (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
• (i99[2] ≥ 0∧i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

• ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
• ((UIncreasing(LOAD702(i60[1], i69[1])), ≥)∧0 = 0∧[(-1)bso_27] ≥ 0)

• (i60[0] ≥ 0∧i69[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i60[0] + [(2)bni_28]i69[0] ≥ 0∧[2 + (-1)bso_29] + [2]i60[0] + [2]i69[0] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = [1]
POL(LOAD702(x1, x2)) = [-1] + [-1]x1
POL(0) = 0
POL(LOAD425(x1, x2)) = [-1] + [2]x2 + [-1]x1
POL(COND_LOAD702(x1, x2, x3)) = [-1] + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]
POL(COND_LOAD425(x1, x2, x3)) = [-1] + [-1]x2 + [-1]x1
POL(&&(x1, x2)) = 0
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:

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

### (15) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

(1) -> (2), if ((i69[1]* i99[2])∧(i60[1]* i60[2]))

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

(1) -> (4), if ((i60[1]* i60[4])∧(i69[1]* 0))

(3) -> (4), if ((i60[3]* i60[4])∧(i99[3] + -1* 0))

The set Q consists of the following terms:

### (16) IDependencyGraphProof (EQUIVALENT transformation)

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

### (17) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

The set Q consists of the following terms:

### (18) IDPNonInfProof (SOUND transformation)

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

For Pair LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]) the following chains were created:
• We consider the chain LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]), COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1)) which results in the following constraint:

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

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

(3)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧[(-1)bso_12] ≥ 0)

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

(4)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧[(-1)bso_12] ≥ 0)

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

(5)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧[(-1)bso_12] ≥ 0)

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

(6)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧0 = 0∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧0 = 0∧[(-1)bso_12] ≥ 0)

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

(7)    (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧0 = 0∧[(-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧0 = 0∧[(-1)bso_12] ≥ 0)

For Pair COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1)) the following chains were created:

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

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

(10)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

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

(11)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

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

(12)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

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

(13)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧0 = 0∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

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

(14)    (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧0 = 0∧[(-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧0 = 0∧[(-1)bso_12] ≥ 0)

• (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧0 = 0∧[1 + (-1)bso_14] ≥ 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(LOAD702(x1, x2)) = [-1] + x2
POL(COND_LOAD702(x1, x2, x3)) = [-1] + x3
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]

The following pairs are in P>:

The following pairs are in Pbound:

The following pairs are in P:

There are no usable rules.

### (20) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:

### (21) IDependencyGraphProof (EQUIVALENT transformation)

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

### (23) Obligation:

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

The following domains are used:
none

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:

### (24) IDependencyGraphProof (EQUIVALENT transformation)

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

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

(1) -> (2), if ((i69[1]* i99[2])∧(i60[1]* i60[2]))

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

(1) -> (4), if ((i60[1]* i60[4])∧(i69[1]* 0))

(3) -> (4), if ((i60[3]* i60[4])∧(i99[3] + -1* 0))

(7) -> (5), if ((i69[7]* i69[5])∧(i60[7]* 0))

The set Q consists of the following terms:

### (27) IDependencyGraphProof (EQUIVALENT transformation)

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

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

(3) -> (2), if ((i60[3]* i60[2])∧(i99[3] + -1* i99[2]))

(2) -> (3), if ((i99[2]* i99[3])∧(i99[2] > 0* TRUE)∧(i60[2]* i60[3]))

The set Q consists of the following terms:

### (29) 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_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1)) the following chains were created:

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)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

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

(4)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

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

(5)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧[1 + (-1)bso_12] ≥ 0)

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

(6)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧0 = 0∧[(-1)bni_11 + (-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧0 = 0∧[1 + (-1)bso_12] ≥ 0)

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

(7)    (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧0 = 0∧[1 + (-1)bso_12] ≥ 0)

For Pair LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]) the following chains were created:
• We consider the chain LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2]), COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[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)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧[(-1)bso_14] ≥ 0)

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

(11)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧[(-1)bso_14] ≥ 0)

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

(12)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧[(-1)bso_14] ≥ 0)

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

(13)    (i99[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧0 = 0∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

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

(14)    (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i99[2] ≥ 0 ⇒ (UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_11] + [bni_11]i99[2] ≥ 0∧0 = 0∧[1 + (-1)bso_12] ≥ 0)

• (i99[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥)∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]i99[2] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 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_LOAD702(x1, x2, x3)) = [-1] + x3
POL(LOAD702(x1, x2)) = [-1] + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0

The following pairs are in P>:

The following pairs are in Pbound:

The following pairs are in P:

There are no usable rules.

### (31) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:

### (32) IDependencyGraphProof (EQUIVALENT transformation)

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

### (34) Obligation:

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

The following domains are used:
none

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms: