### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaB18
/**
* Example taken from "A Term Rewriting Approach to the Automated Termination
* Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
* and converted to Java.
*/

public class PastaB18 {
public static void main(String[] args) {
Random.args = args;
int x = Random.random();
int y = Random.random();

while (x > 0 && y > 0) {
if (x > y) {
while (x > 0) {
x--;
}
} else {
while (y > 0) {
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 208 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:
LE1011(i80, i88, i88) → Cond_LE1011(i88 > 0 && i88 + -1 > 0, i80, i88, i88)
Cond_LE1011(TRUE, i80, i88, i88) → LE1011(i80, i88 + -1, i88 + -1)
Load827(i80, i88) → Cond_Load827(i80 > 0 && i80 <= i88 && i88 + -1 > 0, i80, i88)
Cond_Load827(TRUE, i80, i88) → LE1011(i80, i88 + -1, i88 + -1)
LE1011(i80, 1, 1) → Cond_LE10111(1 > 0, i80, 1, 1)
Cond_LE10111(TRUE, i80, 1, 1) → Load827(i80, 0)
Load827(i80, 1) → Cond_Load8271(i80 > 0 && i80 <= 1, i80, 1)
LE1012(1, i88, 1) → Cond_LE1012(1 > 0, 1, i88, 1)
Cond_LE1012(TRUE, 1, i88, 1) → Load827(0, i88)
Load827(1, i88) → Cond_Load8272(i88 > 0 && 1 > i88, 1, i88)
LE1012(i80, i88, i80) → Cond_LE10121(i80 > 0 && i80 + -1 > 0, i80, i88, i80)
Cond_LE10121(TRUE, i80, i88, i80) → LE1012(i80 + -1, i88, i80 + -1)
Load827(i80, i88) → Cond_Load8273(i88 > 0 && i80 > i88, i80, i88)
Cond_Load8273(TRUE, i80, i88) → LE1012(i80 + -1, i88, i80 + -1)
The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (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:
LE1011(i80, i88, i88) → Cond_LE1011(i88 > 0 && i88 + -1 > 0, i80, i88, i88)
Cond_LE1011(TRUE, i80, i88, i88) → LE1011(i80, i88 + -1, i88 + -1)
Load827(i80, i88) → Cond_Load827(i80 > 0 && i80 <= i88 && i88 + -1 > 0, i80, i88)
Cond_Load827(TRUE, i80, i88) → LE1011(i80, i88 + -1, i88 + -1)
LE1011(i80, 1, 1) → Cond_LE10111(1 > 0, i80, 1, 1)
Cond_LE10111(TRUE, i80, 1, 1) → Load827(i80, 0)
Load827(i80, 1) → Cond_Load8271(i80 > 0 && i80 <= 1, i80, 1)
LE1012(1, i88, 1) → Cond_LE1012(1 > 0, 1, i88, 1)
Cond_LE1012(TRUE, 1, i88, 1) → Load827(0, i88)
Load827(1, i88) → Cond_Load8272(i88 > 0 && 1 > i88, 1, i88)
LE1012(i80, i88, i80) → Cond_LE10121(i80 > 0 && i80 + -1 > 0, i80, i88, i80)
Cond_LE10121(TRUE, i80, i88, i80) → LE1012(i80 + -1, i88, i80 + -1)
Load827(i80, i88) → Cond_Load8273(i88 > 0 && i80 > i88, i80, i88)
Cond_Load8273(TRUE, i80, i88) → LE1012(i80 + -1, i88, i80 + -1)

The integer pair graph contains the following rules and edges:
(0): LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(i88[0] > 0 && i88[0] + -1 > 0, i80[0], i88[0], i88[0])
(1): COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], i88[1] + -1, i88[1] + -1)
(2): LOAD827(i80[2], i88[2]) → COND_LOAD827(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0, i80[2], i88[2])
(3): COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], i88[3] + -1, i88[3] + -1)
(4): LE1011'(i80[4], 1, 1) → COND_LE10111(1 > 0, i80[4], 1, 1)
(5): COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0)
(6): LOAD827(i80[6], 1) → COND_LOAD8271(i80[6] > 0 && i80[6] <= 1, i80[6], 1)
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(10): LOAD827(1, i88[10]) → COND_LOAD8272(i88[10] > 0 && 1 > i88[10], 1, i88[10])
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(14): LOAD827(i80[14], i88[14]) → COND_LOAD8273(i88[14] > 0 && i80[14] > i88[14], i80[14], i88[14])
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)

(0) -> (1), if ((i88[0]* i88[1])∧(i88[0] > 0 && i88[0] + -1 > 0* TRUE)∧(i80[0]* i80[1]))

(1) -> (0), if ((i80[1]* i80[0])∧(i88[1] + -1* i88[0]))

(1) -> (4), if ((i88[1] + -1* 1)∧(i80[1]* i80[4]))

(2) -> (3), if ((i88[2]* i88[3])∧(i80[2]* i80[3])∧(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0* TRUE))

(3) -> (0), if ((i88[3] + -1* i88[0])∧(i80[3]* i80[0]))

(3) -> (4), if ((i80[3]* i80[4])∧(i88[3] + -1* 1))

(4) -> (5), if ((1 > 0* TRUE)∧(i80[4]* i80[5]))

(5) -> (2), if ((0* i88[2])∧(i80[5]* i80[2]))

(5) -> (6), if ((i80[5]* i80[6])∧(0* 1))

(5) -> (10), if ((i80[5]* 1)∧(0* i88[10]))

(5) -> (14), if ((0* i88[14])∧(i80[5]* i80[14]))

(6) -> (7), if ((i80[6] > 0 && i80[6] <= 1* TRUE)∧(i80[6]* i80[7]))

(7) -> (2), if ((i80[7]* i80[2])∧(0* i88[2]))

(7) -> (6), if ((i80[7]* i80[6])∧(0* 1))

(7) -> (10), if ((0* i88[10])∧(i80[7]* 1))

(7) -> (14), if ((i80[7]* i80[14])∧(0* i88[14]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(9) -> (2), if ((0* i80[2])∧(i88[9]* i88[2]))

(9) -> (6), if ((0* i80[6])∧(i88[9]* 1))

(9) -> (10), if ((0* 1)∧(i88[9]* i88[10]))

(9) -> (14), if ((0* i80[14])∧(i88[9]* i88[14]))

(10) -> (11), if ((i88[10] > 0 && 1 > i88[10]* TRUE)∧(i88[10]* i88[11]))

(11) -> (2), if ((i88[11]* i88[2])∧(0* i80[2]))

(11) -> (6), if ((0* i80[6])∧(i88[11]* 1))

(11) -> (10), if ((0* 1)∧(i88[11]* i88[10]))

(11) -> (14), if ((i88[11]* i88[14])∧(0* i80[14]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(14) -> (15), if ((i88[14] > 0 && i80[14] > i88[14]* TRUE)∧(i80[14]* i80[15])∧(i88[14]* i88[15]))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(15) -> (12), if ((i80[15] + -1* i80[12])∧(i88[15]* i88[12]))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (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): LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(i88[0] > 0 && i88[0] + -1 > 0, i80[0], i88[0], i88[0])
(1): COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], i88[1] + -1, i88[1] + -1)
(2): LOAD827(i80[2], i88[2]) → COND_LOAD827(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0, i80[2], i88[2])
(3): COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], i88[3] + -1, i88[3] + -1)
(4): LE1011'(i80[4], 1, 1) → COND_LE10111(1 > 0, i80[4], 1, 1)
(5): COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0)
(6): LOAD827(i80[6], 1) → COND_LOAD8271(i80[6] > 0 && i80[6] <= 1, i80[6], 1)
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(10): LOAD827(1, i88[10]) → COND_LOAD8272(i88[10] > 0 && 1 > i88[10], 1, i88[10])
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(14): LOAD827(i80[14], i88[14]) → COND_LOAD8273(i88[14] > 0 && i80[14] > i88[14], i80[14], i88[14])
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)

(0) -> (1), if ((i88[0]* i88[1])∧(i88[0] > 0 && i88[0] + -1 > 0* TRUE)∧(i80[0]* i80[1]))

(1) -> (0), if ((i80[1]* i80[0])∧(i88[1] + -1* i88[0]))

(1) -> (4), if ((i88[1] + -1* 1)∧(i80[1]* i80[4]))

(2) -> (3), if ((i88[2]* i88[3])∧(i80[2]* i80[3])∧(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0* TRUE))

(3) -> (0), if ((i88[3] + -1* i88[0])∧(i80[3]* i80[0]))

(3) -> (4), if ((i80[3]* i80[4])∧(i88[3] + -1* 1))

(4) -> (5), if ((1 > 0* TRUE)∧(i80[4]* i80[5]))

(5) -> (2), if ((0* i88[2])∧(i80[5]* i80[2]))

(5) -> (6), if ((i80[5]* i80[6])∧(0* 1))

(5) -> (10), if ((i80[5]* 1)∧(0* i88[10]))

(5) -> (14), if ((0* i88[14])∧(i80[5]* i80[14]))

(6) -> (7), if ((i80[6] > 0 && i80[6] <= 1* TRUE)∧(i80[6]* i80[7]))

(7) -> (2), if ((i80[7]* i80[2])∧(0* i88[2]))

(7) -> (6), if ((i80[7]* i80[6])∧(0* 1))

(7) -> (10), if ((0* i88[10])∧(i80[7]* 1))

(7) -> (14), if ((i80[7]* i80[14])∧(0* i88[14]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(9) -> (2), if ((0* i80[2])∧(i88[9]* i88[2]))

(9) -> (6), if ((0* i80[6])∧(i88[9]* 1))

(9) -> (10), if ((0* 1)∧(i88[9]* i88[10]))

(9) -> (14), if ((0* i80[14])∧(i88[9]* i88[14]))

(10) -> (11), if ((i88[10] > 0 && 1 > i88[10]* TRUE)∧(i88[10]* i88[11]))

(11) -> (2), if ((i88[11]* i88[2])∧(0* i80[2]))

(11) -> (6), if ((0* i80[6])∧(i88[11]* 1))

(11) -> (10), if ((0* 1)∧(i88[11]* i88[10]))

(11) -> (14), if ((i88[11]* i88[14])∧(0* i80[14]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(14) -> (15), if ((i88[14] > 0 && i80[14] > i88[14]* TRUE)∧(i80[14]* i80[15])∧(i88[14]* i88[15]))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(15) -> (12), if ((i80[15] + -1* i80[12])∧(i88[15]* i88[12]))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (9) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (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): LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(i88[0] > 0 && i88[0] + -1 > 0, i80[0], i88[0], i88[0])
(1): COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], i88[1] + -1, i88[1] + -1)
(2): LOAD827(i80[2], i88[2]) → COND_LOAD827(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0, i80[2], i88[2])
(3): COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], i88[3] + -1, i88[3] + -1)
(4): LE1011'(i80[4], 1, 1) → COND_LE10111(1 > 0, i80[4], 1, 1)
(5): COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0)
(6): LOAD827(i80[6], 1) → COND_LOAD8271(i80[6] > 0 && i80[6] <= 1, i80[6], 1)
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(10): LOAD827(1, i88[10]) → COND_LOAD8272(i88[10] > 0 && 1 > i88[10], 1, i88[10])
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(14): LOAD827(i80[14], i88[14]) → COND_LOAD8273(i88[14] > 0 && i80[14] > i88[14], i80[14], i88[14])
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)

(0) -> (1), if ((i88[0]* i88[1])∧(i88[0] > 0 && i88[0] + -1 > 0* TRUE)∧(i80[0]* i80[1]))

(1) -> (0), if ((i80[1]* i80[0])∧(i88[1] + -1* i88[0]))

(1) -> (4), if ((i88[1] + -1* 1)∧(i80[1]* i80[4]))

(2) -> (3), if ((i88[2]* i88[3])∧(i80[2]* i80[3])∧(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0* TRUE))

(3) -> (0), if ((i88[3] + -1* i88[0])∧(i80[3]* i80[0]))

(3) -> (4), if ((i80[3]* i80[4])∧(i88[3] + -1* 1))

(4) -> (5), if ((1 > 0* TRUE)∧(i80[4]* i80[5]))

(5) -> (2), if ((0* i88[2])∧(i80[5]* i80[2]))

(5) -> (10), if ((i80[5]* 1)∧(0* i88[10]))

(5) -> (14), if ((0* i88[14])∧(i80[5]* i80[14]))

(6) -> (7), if ((i80[6] > 0 && i80[6] <= 1* TRUE)∧(i80[6]* i80[7]))

(7) -> (2), if ((i80[7]* i80[2])∧(0* i88[2]))

(7) -> (10), if ((0* i88[10])∧(i80[7]* 1))

(7) -> (14), if ((i80[7]* i80[14])∧(0* i88[14]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(9) -> (2), if ((0* i80[2])∧(i88[9]* i88[2]))

(9) -> (6), if ((0* i80[6])∧(i88[9]* 1))

(9) -> (14), if ((0* i80[14])∧(i88[9]* i88[14]))

(10) -> (11), if ((i88[10] > 0 && 1 > i88[10]* TRUE)∧(i88[10]* i88[11]))

(11) -> (2), if ((i88[11]* i88[2])∧(0* i80[2]))

(11) -> (6), if ((0* i80[6])∧(i88[11]* 1))

(11) -> (14), if ((i88[11]* i88[14])∧(0* i80[14]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(14) -> (15), if ((i88[14] > 0 && i80[14] > i88[14]* TRUE)∧(i80[14]* i80[15])∧(i88[14]* i88[15]))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(15) -> (12), if ((i80[15] + -1* i80[12])∧(i88[15]* i88[12]))

(5) -> (6), if ((i80[5]* i80[6])∧false)

(7) -> (6), if ((i80[7]* i80[6])∧false)

(9) -> (10), if (false∧(i88[9]* i88[10]))

(11) -> (10), if (false∧(i88[11]* i88[10]))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (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 LE1011'(i80, i88, i88) → COND_LE1011(&&(>(i88, 0), >(+(i88, -1), 0)), i80, i88, i88) the following chains were created:
• We consider the chain LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0]), COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1)) which results in the following constraint:

(1)    (i88[0]=i88[1]&&(>(i88[0], 0), >(+(i88[0], -1), 0))=TRUEi80[0]=i80[1]LE1011'(i80[0], i88[0], i88[0])≥NonInfC∧LE1011'(i80[0], i88[0], i88[0])≥COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])∧(UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥))

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

(2)    (>(i88[0], 0)=TRUE>(+(i88[0], -1), 0)=TRUELE1011'(i80[0], i88[0], i88[0])≥NonInfC∧LE1011'(i80[0], i88[0], i88[0])≥COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])∧(UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥))

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

(3)    (i88[0] + [-1] ≥ 0∧i88[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧[(-1)bso_30] ≥ 0)

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

(4)    (i88[0] + [-1] ≥ 0∧i88[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧[(-1)bso_30] ≥ 0)

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

(5)    (i88[0] + [-1] ≥ 0∧i88[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧[(-1)bso_30] ≥ 0)

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

(6)    (i88[0] + [-1] ≥ 0∧i88[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧0 = 0∧[(-1)bni_29 + (-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

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

(7)    (i88[0] ≥ 0∧[-1] + i88[0] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧0 = 0∧[(-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

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

(8)    ([1] + i88[0] ≥ 0∧i88[0] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧0 = 0∧[bni_29 + (-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

For Pair COND_LE1011(TRUE, i80, i88, i88) → LE1011'(i80, +(i88, -1), +(i88, -1)) the following chains were created:
• We consider the chain COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1)) which results in the following constraint:

(9)    (COND_LE1011(TRUE, i80[1], i88[1], i88[1])≥NonInfC∧COND_LE1011(TRUE, i80[1], i88[1], i88[1])≥LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))∧(UIncreasing(LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))), ≥))

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

(10)    ((UIncreasing(LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))), ≥)∧[1 + (-1)bso_32] ≥ 0)

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

(11)    ((UIncreasing(LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))), ≥)∧[1 + (-1)bso_32] ≥ 0)

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

(12)    ((UIncreasing(LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))), ≥)∧[1 + (-1)bso_32] ≥ 0)

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

(13)    ((UIncreasing(LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_32] ≥ 0)

For Pair LOAD827(i80, i88) → COND_LOAD827(&&(&&(>(i80, 0), <=(i80, i88)), >(+(i88, -1), 0)), i80, i88) the following chains were created:
• We consider the chain LOAD827(i80[2], i88[2]) → COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2]), COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1)) which results in the following constraint:

(14)    (i88[2]=i88[3]i80[2]=i80[3]&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0))=TRUELOAD827(i80[2], i88[2])≥NonInfC∧LOAD827(i80[2], i88[2])≥COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])∧(UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥))

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

(15)    (>(+(i88[2], -1), 0)=TRUE>(i80[2], 0)=TRUE<=(i80[2], i88[2])=TRUELOAD827(i80[2], i88[2])≥NonInfC∧LOAD827(i80[2], i88[2])≥COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])∧(UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥))

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

(16)    (i88[2] + [-2] ≥ 0∧i80[2] + [-1] ≥ 0∧i88[2] + [-1]i80[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥)∧[(-1)bni_33 + (-1)Bound*bni_33] + [bni_33]i88[2] ≥ 0∧[(-1)bso_34] ≥ 0)

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

(17)    (i88[2] + [-2] ≥ 0∧i80[2] + [-1] ≥ 0∧i88[2] + [-1]i80[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥)∧[(-1)bni_33 + (-1)Bound*bni_33] + [bni_33]i88[2] ≥ 0∧[(-1)bso_34] ≥ 0)

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

(18)    (i88[2] + [-2] ≥ 0∧i80[2] + [-1] ≥ 0∧i88[2] + [-1]i80[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥)∧[(-1)bni_33 + (-1)Bound*bni_33] + [bni_33]i88[2] ≥ 0∧[(-1)bso_34] ≥ 0)

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

(19)    (i88[2] ≥ 0∧i80[2] + [-1] ≥ 0∧[2] + i88[2] + [-1]i80[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥)∧[bni_33 + (-1)Bound*bni_33] + [bni_33]i88[2] ≥ 0∧[(-1)bso_34] ≥ 0)

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

(20)    (i88[2] ≥ 0∧i80[2] ≥ 0∧[1] + i88[2] + [-1]i80[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥)∧[bni_33 + (-1)Bound*bni_33] + [bni_33]i88[2] ≥ 0∧[(-1)bso_34] ≥ 0)

For Pair COND_LOAD827(TRUE, i80, i88) → LE1011'(i80, +(i88, -1), +(i88, -1)) the following chains were created:
• We consider the chain COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1)) which results in the following constraint:

(21)    (COND_LOAD827(TRUE, i80[3], i88[3])≥NonInfC∧COND_LOAD827(TRUE, i80[3], i88[3])≥LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))∧(UIncreasing(LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))), ≥))

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

(22)    ((UIncreasing(LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))), ≥)∧[1 + (-1)bso_36] ≥ 0)

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

(23)    ((UIncreasing(LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))), ≥)∧[1 + (-1)bso_36] ≥ 0)

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

(24)    ((UIncreasing(LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))), ≥)∧[1 + (-1)bso_36] ≥ 0)

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

(25)    ((UIncreasing(LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)

For Pair LE1011'(i80, 1, 1) → COND_LE10111(>(1, 0), i80, 1, 1) the following chains were created:
• We consider the chain LE1011'(i80[4], 1, 1) → COND_LE10111(>(1, 0), i80[4], 1, 1), COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0) which results in the following constraint:

(26)    (>(1, 0)=TRUEi80[4]=i80[5]LE1011'(i80[4], 1, 1)≥NonInfC∧LE1011'(i80[4], 1, 1)≥COND_LE10111(>(1, 0), i80[4], 1, 1)∧(UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥))

We simplified constraint (26) using rules (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:

(27)    (LE1011'(i80[4], 1, 1)≥NonInfC∧LE1011'(i80[4], 1, 1)≥COND_LE10111(>(1, 0), i80[4], 1, 1)∧(UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥))

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

(28)    ((UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥)∧[(-1)bso_38] ≥ 0)

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

(29)    ((UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥)∧[(-1)bso_38] ≥ 0)

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

(30)    ((UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥)∧[(-1)bso_38] ≥ 0)

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

(31)    ((UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥)∧0 = 0∧[(-1)bso_38] ≥ 0)

For Pair COND_LE10111(TRUE, i80, 1, 1) → LOAD827(i80, 0) the following chains were created:
• We consider the chain COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0) which results in the following constraint:

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

(33)    ((UIncreasing(LOAD827(i80[5], 0)), ≥)∧[1 + (-1)bso_40] ≥ 0)

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

(34)    ((UIncreasing(LOAD827(i80[5], 0)), ≥)∧[1 + (-1)bso_40] ≥ 0)

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

(35)    ((UIncreasing(LOAD827(i80[5], 0)), ≥)∧[1 + (-1)bso_40] ≥ 0)

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

(36)    ((UIncreasing(LOAD827(i80[5], 0)), ≥)∧0 = 0∧[1 + (-1)bso_40] ≥ 0)

For Pair LOAD827(i80, 1) → COND_LOAD8271(&&(>(i80, 0), <=(i80, 1)), i80, 1) the following chains were created:
• We consider the chain LOAD827(i80[6], 1) → COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1), COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 0) which results in the following constraint:

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

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

(39)    (i80[6] + [-1] ≥ 0∧[1] + [-1]i80[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥)∧[(-1)Bound*bni_41] ≥ 0∧[1 + (-1)bso_42] ≥ 0)

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

(40)    (i80[6] + [-1] ≥ 0∧[1] + [-1]i80[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥)∧[(-1)Bound*bni_41] ≥ 0∧[1 + (-1)bso_42] ≥ 0)

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

(41)    (i80[6] + [-1] ≥ 0∧[1] + [-1]i80[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥)∧[(-1)Bound*bni_41] ≥ 0∧[1 + (-1)bso_42] ≥ 0)

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

(42)    (i80[6] ≥ 0∧[-1]i80[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥)∧[(-1)Bound*bni_41] ≥ 0∧[1 + (-1)bso_42] ≥ 0)

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

(43)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥)∧[(-1)Bound*bni_41] ≥ 0∧[1 + (-1)bso_42] ≥ 0)

For Pair COND_LOAD8271(TRUE, i80, 1) → LOAD827(i80, 0) the following chains were created:
• We consider the chain COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 0) which results in the following constraint:

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

(45)    ((UIncreasing(LOAD827(i80[7], 0)), ≥)∧[(-1)bso_44] ≥ 0)

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

(46)    ((UIncreasing(LOAD827(i80[7], 0)), ≥)∧[(-1)bso_44] ≥ 0)

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

(47)    ((UIncreasing(LOAD827(i80[7], 0)), ≥)∧[(-1)bso_44] ≥ 0)

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

(48)    ((UIncreasing(LOAD827(i80[7], 0)), ≥)∧0 = 0∧[(-1)bso_44] ≥ 0)

For Pair LE1012'(1, i88, 1) → COND_LE1012(>(1, 0), 1, i88, 1) the following chains were created:
• We consider the chain LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1), COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9]) which results in the following constraint:

(49)    (i88[8]=i88[9]>(1, 0)=TRUELE1012'(1, i88[8], 1)≥NonInfC∧LE1012'(1, i88[8], 1)≥COND_LE1012(>(1, 0), 1, i88[8], 1)∧(UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥))

We simplified constraint (49) using rules (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:

(50)    (LE1012'(1, i88[8], 1)≥NonInfC∧LE1012'(1, i88[8], 1)≥COND_LE1012(>(1, 0), 1, i88[8], 1)∧(UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥))

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

(51)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧[(-1)bso_46] ≥ 0)

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

(52)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧[(-1)bso_46] ≥ 0)

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

(53)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧[(-1)bso_46] ≥ 0)

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

(54)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)

For Pair COND_LE1012(TRUE, 1, i88, 1) → LOAD827(0, i88) the following chains were created:
• We consider the chain COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9]) which results in the following constraint:

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

(56)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧[(-1)bso_48] ≥ 0)

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

(57)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧[(-1)bso_48] ≥ 0)

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

(58)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧[(-1)bso_48] ≥ 0)

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

(59)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧0 = 0∧[(-1)bso_48] ≥ 0)

For Pair LOAD827(1, i88) → COND_LOAD8272(&&(>(i88, 0), >(1, i88)), 1, i88) the following chains were created:
• We consider the chain LOAD827(1, i88[10]) → COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10]), COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11]) which results in the following constraint:

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

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

(62)    (i88[10] + [-1] ≥ 0∧[-1]i88[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i88[10] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(63)    (i88[10] + [-1] ≥ 0∧[-1]i88[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i88[10] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(64)    (i88[10] + [-1] ≥ 0∧[-1]i88[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [bni_49]i88[10] ≥ 0∧[(-1)bso_50] ≥ 0)

We solved constraint (64) using rule (IDP_SMT_SPLIT).

For Pair COND_LOAD8272(TRUE, 1, i88) → LOAD827(0, i88) the following chains were created:
• We consider the chain COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11]) which results in the following constraint:

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

(66)    ((UIncreasing(LOAD827(0, i88[11])), ≥)∧[(-1)bso_52] ≥ 0)

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

(67)    ((UIncreasing(LOAD827(0, i88[11])), ≥)∧[(-1)bso_52] ≥ 0)

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

(68)    ((UIncreasing(LOAD827(0, i88[11])), ≥)∧[(-1)bso_52] ≥ 0)

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

(69)    ((UIncreasing(LOAD827(0, i88[11])), ≥)∧0 = 0∧[(-1)bso_52] ≥ 0)

For Pair LE1012'(i80, i88, i80) → COND_LE10121(&&(>(i80, 0), >(+(i80, -1), 0)), i80, i88, i80) the following chains were created:
• We consider the chain LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]), COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(70)    (i88[12]=i88[13]i80[12]=i80[13]&&(>(i80[12], 0), >(+(i80[12], -1), 0))=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(71)    (>(i80[12], 0)=TRUE>(+(i80[12], -1), 0)=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(72)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [bni_53]i88[12] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(73)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [bni_53]i88[12] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(74)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [bni_53]i88[12] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(75)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)

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

(76)    (i80[12] ≥ 0∧[-1] + i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)

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

(77)    ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)

For Pair COND_LE10121(TRUE, i80, i88, i80) → LE1012'(+(i80, -1), i88, +(i80, -1)) the following chains were created:
• We consider the chain COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(78)    (COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥NonInfC∧COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))∧(UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥))

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

(79)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[(-1)bso_56] ≥ 0)

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

(80)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[(-1)bso_56] ≥ 0)

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

(81)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[(-1)bso_56] ≥ 0)

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

(82)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

For Pair LOAD827(i80, i88) → COND_LOAD8273(&&(>(i88, 0), >(i80, i88)), i80, i88) the following chains were created:
• We consider the chain LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14]), COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1)) which results in the following constraint:

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

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

(85)    (i88[14] + [-1] ≥ 0∧i80[14] + [-1] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [bni_57]i88[14] ≥ 0∧[(-1)bso_58] ≥ 0)

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

(86)    (i88[14] + [-1] ≥ 0∧i80[14] + [-1] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [bni_57]i88[14] ≥ 0∧[(-1)bso_58] ≥ 0)

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

(87)    (i88[14] + [-1] ≥ 0∧i80[14] + [-1] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [bni_57]i88[14] ≥ 0∧[(-1)bso_58] ≥ 0)

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

(88)    (i88[14] ≥ 0∧i80[14] + [-2] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)Bound*bni_57] + [bni_57]i88[14] ≥ 0∧[(-1)bso_58] ≥ 0)

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

(89)    (i88[14] ≥ 0∧i80[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)Bound*bni_57] + [bni_57]i88[14] ≥ 0∧[(-1)bso_58] ≥ 0)

For Pair COND_LOAD8273(TRUE, i80, i88) → LE1012'(+(i80, -1), i88, +(i80, -1)) the following chains were created:
• We consider the chain COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1)) which results in the following constraint:

(90)    (COND_LOAD8273(TRUE, i80[15], i88[15])≥NonInfC∧COND_LOAD8273(TRUE, i80[15], i88[15])≥LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))∧(UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥))

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

(91)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧[(-1)bso_60] ≥ 0)

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

(92)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧[(-1)bso_60] ≥ 0)

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

(93)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧[(-1)bso_60] ≥ 0)

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

(94)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_60] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LE1011'(i80, i88, i88) → COND_LE1011(&&(>(i88, 0), >(+(i88, -1), 0)), i80, i88, i88)
• ([1] + i88[0] ≥ 0∧i88[0] ≥ 0 ⇒ (UIncreasing(COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])), ≥)∧0 = 0∧[bni_29 + (-1)Bound*bni_29] + [bni_29]i88[0] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

• COND_LE1011(TRUE, i80, i88, i88) → LE1011'(i80, +(i88, -1), +(i88, -1))
• ((UIncreasing(LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_32] ≥ 0)

• LOAD827(i80, i88) → COND_LOAD827(&&(&&(>(i80, 0), <=(i80, i88)), >(+(i88, -1), 0)), i80, i88)
• (i88[2] ≥ 0∧i80[2] ≥ 0∧[1] + i88[2] + [-1]i80[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])), ≥)∧[bni_33 + (-1)Bound*bni_33] + [bni_33]i88[2] ≥ 0∧[(-1)bso_34] ≥ 0)

• COND_LOAD827(TRUE, i80, i88) → LE1011'(i80, +(i88, -1), +(i88, -1))
• ((UIncreasing(LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)

• LE1011'(i80, 1, 1) → COND_LE10111(>(1, 0), i80, 1, 1)
• ((UIncreasing(COND_LE10111(>(1, 0), i80[4], 1, 1)), ≥)∧0 = 0∧[(-1)bso_38] ≥ 0)

• COND_LE10111(TRUE, i80, 1, 1) → LOAD827(i80, 0)
• ((UIncreasing(LOAD827(i80[5], 0)), ≥)∧0 = 0∧[1 + (-1)bso_40] ≥ 0)

• (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥)∧[(-1)Bound*bni_41] ≥ 0∧[1 + (-1)bso_42] ≥ 0)

• ((UIncreasing(LOAD827(i80[7], 0)), ≥)∧0 = 0∧[(-1)bso_44] ≥ 0)

• LE1012'(1, i88, 1) → COND_LE1012(>(1, 0), 1, i88, 1)
• ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)

• COND_LE1012(TRUE, 1, i88, 1) → LOAD827(0, i88)
• ((UIncreasing(LOAD827(0, i88[9])), ≥)∧0 = 0∧[(-1)bso_48] ≥ 0)

• ((UIncreasing(LOAD827(0, i88[11])), ≥)∧0 = 0∧[(-1)bso_52] ≥ 0)

• LE1012'(i80, i88, i80) → COND_LE10121(&&(>(i80, 0), >(+(i80, -1), 0)), i80, i88, i80)
• ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)

• COND_LE10121(TRUE, i80, i88, i80) → LE1012'(+(i80, -1), i88, +(i80, -1))
• ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

• (i88[14] ≥ 0∧i80[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)Bound*bni_57] + [bni_57]i88[14] ≥ 0∧[(-1)bso_58] ≥ 0)

• COND_LOAD8273(TRUE, i80, i88) → LE1012'(+(i80, -1), i88, +(i80, -1))
• ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_60] ≥ 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(LE1011'(x1, x2, x3)) = [-1] + [2]x3 + [-1]x2
POL(COND_LE1011(x1, x2, x3, x4)) = [-1] + [-1]x4 + [2]x3
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(LOAD827(x1, x2)) = [-1] + x2
POL(COND_LOAD827(x1, x2, x3)) = [-1] + x3
POL(<=(x1, x2)) = [-1]
POL(1) = [1]
POL(COND_LE10111(x1, x2, x3, x4)) = 0
POL(LE1012'(x1, x2, x3)) = [-1] + x2
POL(COND_LE1012(x1, x2, x3, x4)) = [-1] + x3
POL(COND_LOAD8272(x1, x2, x3)) = [-1] + x3
POL(COND_LE10121(x1, x2, x3, x4)) = [-1] + x3
POL(COND_LOAD8273(x1, x2, x3)) = [-1] + x3

The following pairs are in P>:

COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], +(i88[1], -1), +(i88[1], -1))
COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], +(i88[3], -1), +(i88[3], -1))
COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0)

The following pairs are in Pbound:

LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])
LOAD827(i80[2], i88[2]) → COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])

The following pairs are in P:

LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(&&(>(i88[0], 0), >(+(i88[0], -1), 0)), i80[0], i88[0], i88[0])
LOAD827(i80[2], i88[2]) → COND_LOAD827(&&(&&(>(i80[2], 0), <=(i80[2], i88[2])), >(+(i88[2], -1), 0)), i80[2], i88[2])
LE1011'(i80[4], 1, 1) → COND_LE10111(>(1, 0), i80[4], 1, 1)
LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1)
COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])
COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))
COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))

There are no usable rules.

### (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): LE1011'(i80[0], i88[0], i88[0]) → COND_LE1011(i88[0] > 0 && i88[0] + -1 > 0, i80[0], i88[0], i88[0])
(2): LOAD827(i80[2], i88[2]) → COND_LOAD827(i80[2] > 0 && i80[2] <= i88[2] && i88[2] + -1 > 0, i80[2], i88[2])
(4): LE1011'(i80[4], 1, 1) → COND_LE10111(1 > 0, i80[4], 1, 1)
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(14): LOAD827(i80[14], i88[14]) → COND_LOAD8273(i88[14] > 0 && i80[14] > i88[14], i80[14], i88[14])
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)

(7) -> (2), if ((i80[7]* i80[2])∧(0* i88[2]))

(9) -> (2), if ((0* i80[2])∧(i88[9]* i88[2]))

(11) -> (2), if ((i88[11]* i88[2])∧(0* i80[2]))

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(15) -> (12), if ((i80[15] + -1* i80[12])∧(i88[15]* i88[12]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

(7) -> (14), if ((i80[7]* i80[14])∧(0* i88[14]))

(9) -> (14), if ((0* i80[14])∧(i88[9]* i88[14]))

(11) -> (14), if ((i88[11]* i88[14])∧(0* i80[14]))

(14) -> (15), if ((i88[14] > 0 && i80[14] > i88[14]* TRUE)∧(i80[14]* i80[15])∧(i88[14]* i88[15]))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (14) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)
(14): LOAD827(i80[14], i88[14]) → COND_LOAD8273(i88[14] > 0 && i80[14] > i88[14], i80[14], i88[14])

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(15) -> (12), if ((i80[15] + -1* i80[12])∧(i88[15]* i88[12]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

(9) -> (14), if ((0* i80[14])∧(i88[9]* i88[14]))

(14) -> (15), if ((i88[14] > 0 && i80[14] > i88[14]* TRUE)∧(i80[14]* i80[15])∧(i88[14]* i88[15]))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (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 COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) the following chains were created:
• We consider the chain COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(1)    (COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥NonInfC∧COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))∧(UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥))

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

(2)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[(-1)bso_16] ≥ 0)

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

(3)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[(-1)bso_16] ≥ 0)

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

(4)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[(-1)bso_16] ≥ 0)

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

(5)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

For Pair LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]) the following chains were created:
• We consider the chain LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]), COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(6)    (i88[12]=i88[13]i80[12]=i80[13]&&(>(i80[12], 0), >(+(i80[12], -1), 0))=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(7)    (>(i80[12], 0)=TRUE>(+(i80[12], -1), 0)=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(8)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧[(-1)bso_18] ≥ 0)

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

(9)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧[(-1)bso_18] ≥ 0)

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

(10)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧[(-1)bso_18] ≥ 0)

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

(11)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

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

(12)    (i80[12] ≥ 0∧[-1] + i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

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

(13)    ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

For Pair COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9]) the following chains were created:
• We consider the chain COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9]) which results in the following constraint:

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

(15)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧[(-1)bso_20] ≥ 0)

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

(16)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧[(-1)bso_20] ≥ 0)

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

(17)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧[(-1)bso_20] ≥ 0)

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

(18)    ((UIncreasing(LOAD827(0, i88[9])), ≥)∧0 = 0∧[(-1)bso_20] ≥ 0)

For Pair LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1) the following chains were created:
• We consider the chain LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1), COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9]) which results in the following constraint:

(19)    (i88[8]=i88[9]>(1, 0)=TRUELE1012'(1, i88[8], 1)≥NonInfC∧LE1012'(1, i88[8], 1)≥COND_LE1012(>(1, 0), 1, i88[8], 1)∧(UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥))

We simplified constraint (19) using rules (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:

(20)    (LE1012'(1, i88[8], 1)≥NonInfC∧LE1012'(1, i88[8], 1)≥COND_LE1012(>(1, 0), 1, i88[8], 1)∧(UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥))

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

(21)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧[(-1)bso_22] ≥ 0)

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

(22)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧[(-1)bso_22] ≥ 0)

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

(23)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧[(-1)bso_22] ≥ 0)

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

(24)    ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧0 = 0∧[(-1)bso_22] ≥ 0)

For Pair COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1)) the following chains were created:
• We consider the chain COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1)) which results in the following constraint:

(25)    (COND_LOAD8273(TRUE, i80[15], i88[15])≥NonInfC∧COND_LOAD8273(TRUE, i80[15], i88[15])≥LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))∧(UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥))

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

(26)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧[2 + (-1)bso_24] ≥ 0)

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

(27)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧[2 + (-1)bso_24] ≥ 0)

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

(28)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧[2 + (-1)bso_24] ≥ 0)

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

(29)    ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_24] ≥ 0)

For Pair LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14]) the following chains were created:
• We consider the chain LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14]), COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1)) which results in the following constraint:

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

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

(32)    (i88[14] + [-1] ≥ 0∧i80[14] + [-1] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [bni_25]i80[14] ≥ 0∧[-2 + (-1)bso_26] + i80[14] ≥ 0)

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

(33)    (i88[14] + [-1] ≥ 0∧i80[14] + [-1] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [bni_25]i80[14] ≥ 0∧[-2 + (-1)bso_26] + i80[14] ≥ 0)

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

(34)    (i88[14] + [-1] ≥ 0∧i80[14] + [-1] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [bni_25]i80[14] ≥ 0∧[-2 + (-1)bso_26] + i80[14] ≥ 0)

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

(35)    (i88[14] ≥ 0∧i80[14] + [-2] + [-1]i88[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [bni_25]i80[14] ≥ 0∧[-2 + (-1)bso_26] + i80[14] ≥ 0)

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

(36)    (i88[14] ≥ 0∧i80[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [bni_25]i88[14] + [bni_25]i80[14] ≥ 0∧[(-1)bso_26] + i88[14] + i80[14] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))
• ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

• LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])
• ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

• COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
• ((UIncreasing(LOAD827(0, i88[9])), ≥)∧0 = 0∧[(-1)bso_20] ≥ 0)

• LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1)
• ((UIncreasing(COND_LE1012(>(1, 0), 1, i88[8], 1)), ≥)∧0 = 0∧[(-1)bso_22] ≥ 0)

• COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))
• ((UIncreasing(LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_24] ≥ 0)

• (i88[14] ≥ 0∧i80[14] ≥ 0 ⇒ (UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [bni_25]i88[14] + [bni_25]i80[14] ≥ 0∧[(-1)bso_26] + i88[14] + i80[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_LE10121(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(LE1012'(x1, x2, x3)) = [-1] + x3 + [-1]x1
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(COND_LE1012(x1, x2, x3, x4)) = [-1]
POL(1) = [1]
POL(LOAD827(x1, x2)) = [-1] + x1

The following pairs are in P>:

COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(+(i80[15], -1), i88[15], +(i80[15], -1))

The following pairs are in Pbound:

LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])

The following pairs are in P:

COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))
LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])
COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1)

There are no usable rules.

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

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(14): LOAD827(i80[14], i88[14]) → COND_LOAD8273(i88[14] > 0 && i80[14] > i88[14], i80[14], i88[14])

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

(9) -> (14), if ((0* i80[14])∧(i88[9]* i88[14]))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (19) IDependencyGraphProof (EQUIVALENT transformation)

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

### (20) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (21) IDPNonInfProof (SOUND transformation)

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

For Pair LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]) the following chains were created:
• We consider the chain LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]), COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(1)    (i88[12]=i88[13]i80[12]=i80[13]&&(>(i80[12], 0), >(+(i80[12], -1), 0))=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(2)    (>(i80[12], 0)=TRUE>(+(i80[12], -1), 0)=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(3)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_7 + (-1)Bound*bni_7] + [bni_7]i80[12] ≥ 0∧[(-1)bso_8] ≥ 0)

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

(4)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_7 + (-1)Bound*bni_7] + [bni_7]i80[12] ≥ 0∧[(-1)bso_8] ≥ 0)

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

(5)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_7 + (-1)Bound*bni_7] + [bni_7]i80[12] ≥ 0∧[(-1)bso_8] ≥ 0)

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

(6)    (i80[12] ≥ 0∧[-1] + i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(2)bni_7 + (-1)Bound*bni_7] + [bni_7]i80[12] ≥ 0∧[(-1)bso_8] ≥ 0)

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

(7)    ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(3)bni_7 + (-1)Bound*bni_7] + [bni_7]i80[12] ≥ 0∧[(-1)bso_8] ≥ 0)

For Pair COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) the following chains were created:
• We consider the chain COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(8)    (COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥NonInfC∧COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))∧(UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥))

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

(9)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[1 + (-1)bso_10] ≥ 0)

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

(10)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[1 + (-1)bso_10] ≥ 0)

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

(11)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[1 + (-1)bso_10] ≥ 0)

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

(12)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧[1 + (-1)bso_10] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])
• ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(3)bni_7 + (-1)Bound*bni_7] + [bni_7]i80[12] ≥ 0∧[(-1)bso_8] ≥ 0)

• COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))
• ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧[1 + (-1)bso_10] ≥ 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(LE1012'(x1, x2, x3)) = [1] + x3
POL(COND_LE10121(x1, x2, x3, x4)) = [1] + [2]x4 + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]

The following pairs are in P>:

COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))

The following pairs are in Pbound:

LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])

The following pairs are in P:

LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])

There are no usable rules.

### (23) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (24) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (27) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (30) IDependencyGraphProof (EQUIVALENT transformation)

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

### (32) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LE1011(TRUE, i80[1], i88[1], i88[1]) → LE1011'(i80[1], i88[1] + -1, i88[1] + -1)
(3): COND_LOAD827(TRUE, i80[3], i88[3]) → LE1011'(i80[3], i88[3] + -1, i88[3] + -1)
(4): LE1011'(i80[4], 1, 1) → COND_LE10111(1 > 0, i80[4], 1, 1)
(5): COND_LE10111(TRUE, i80[5], 1, 1) → LOAD827(i80[5], 0)
(8): LE1012'(1, i88[8], 1) → COND_LE1012(1 > 0, 1, i88[8], 1)
(9): COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(15): COND_LOAD8273(TRUE, i80[15], i88[15]) → LE1012'(i80[15] + -1, i88[15], i80[15] + -1)

(1) -> (4), if ((i88[1] + -1* 1)∧(i80[1]* i80[4]))

(3) -> (4), if ((i80[3]* i80[4])∧(i88[3] + -1* 1))

(4) -> (5), if ((1 > 0* TRUE)∧(i80[4]* i80[5]))

(13) -> (8), if ((i88[13]* i88[8])∧(i80[13] + -1* 1))

(15) -> (8), if ((i80[15] + -1* 1)∧(i88[15]* i88[8]))

(8) -> (9), if ((i88[8]* i88[9])∧(1 > 0* TRUE))

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(15) -> (12), if ((i80[15] + -1* i80[12])∧(i88[15]* i88[12]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (33) IDependencyGraphProof (EQUIVALENT transformation)

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

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

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])

(13) -> (12), if ((i88[13]* i88[12])∧(i80[13] + -1* i80[12]))

(12) -> (13), if ((i88[12]* i88[13])∧(i80[12]* i80[13])∧(i80[12] > 0 && i80[12] + -1 > 0* TRUE))

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (35) 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_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) the following chains were created:
• We consider the chain COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(1)    (COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥NonInfC∧COND_LE10121(TRUE, i80[13], i88[13], i80[13])≥LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))∧(UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥))

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

(2)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[2 + (-1)bso_8] ≥ 0)

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

(3)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[2 + (-1)bso_8] ≥ 0)

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

(4)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧[2 + (-1)bso_8] ≥ 0)

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

(5)    ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧[2 + (-1)bso_8] ≥ 0)

For Pair LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]) the following chains were created:
• We consider the chain LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12]), COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1)) which results in the following constraint:

(6)    (i88[12]=i88[13]i80[12]=i80[13]&&(>(i80[12], 0), >(+(i80[12], -1), 0))=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(7)    (>(i80[12], 0)=TRUE>(+(i80[12], -1), 0)=TRUELE1012'(i80[12], i88[12], i80[12])≥NonInfC∧LE1012'(i80[12], i88[12], i80[12])≥COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])∧(UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥))

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

(8)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_9 + (-1)Bound*bni_9] + [(2)bni_9]i80[12] ≥ 0∧[(-1)bso_10] ≥ 0)

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

(9)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_9 + (-1)Bound*bni_9] + [(2)bni_9]i80[12] ≥ 0∧[(-1)bso_10] ≥ 0)

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

(10)    (i80[12] + [-1] ≥ 0∧i80[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(-1)bni_9 + (-1)Bound*bni_9] + [(2)bni_9]i80[12] ≥ 0∧[(-1)bso_10] ≥ 0)

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

(11)    (i80[12] ≥ 0∧[-1] + i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[bni_9 + (-1)Bound*bni_9] + [(2)bni_9]i80[12] ≥ 0∧[(-1)bso_10] ≥ 0)

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

(12)    ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(3)bni_9 + (-1)Bound*bni_9] + [(2)bni_9]i80[12] ≥ 0∧[(-1)bso_10] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))
• ((UIncreasing(LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))), ≥)∧0 = 0∧[2 + (-1)bso_8] ≥ 0)

• LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])
• ([1] + i80[12] ≥ 0∧i80[12] ≥ 0 ⇒ (UIncreasing(COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])), ≥)∧[(3)bni_9 + (-1)Bound*bni_9] + [(2)bni_9]i80[12] ≥ 0∧[(-1)bso_10] ≥ 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_LE10121(x1, x2, x3, x4)) = [-1] + x4 + x2
POL(LE1012'(x1, x2, x3)) = [-1] + x3 + x1
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(&&(x1, x2)) = [1]
POL(>(x1, x2)) = [-1]
POL(0) = 0

The following pairs are in P>:

COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(+(i80[13], -1), i88[13], +(i80[13], -1))

The following pairs are in Pbound:

LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])

The following pairs are in P:

LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(&&(>(i80[12], 0), >(+(i80[12], -1), 0)), i80[12], i88[12], i80[12])

There are no usable rules.

### (37) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(12): LE1012'(i80[12], i88[12], i80[12]) → COND_LE10121(i80[12] > 0 && i80[12] + -1 > 0, i80[12], i88[12], i80[12])

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_LE1012(TRUE, 1, x0, 1)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)

### (38) IDependencyGraphProof (EQUIVALENT transformation)

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

### (40) 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:
(13): COND_LE10121(TRUE, i80[13], i88[13], i80[13]) → LE1012'(i80[13] + -1, i88[13], i80[13] + -1)

The set Q consists of the following terms:
LE1011(x0, x1, x1)
Cond_LE1011(TRUE, x0, x1, x1)