### (0) Obligation:

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

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 222 nodes with 2 SCCs.

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

### (5) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
JMP981(i59, i59, i59, i148, i162) → Cond_JMP981(i162 > 0, i59, i59, i59, i148, i162)
Cond_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981(i59, i59, i59, i148 + -1, i162 + -1)
JMP873(i59, i71, i59) → Cond_JMP873(i59 > 0 && i71 >= i59, i59, i71, i59)
Cond_JMP873(TRUE, i59, i71, i59) → JMP981(i59, i59, i59, i71 + -1 + -1, i59 + -1 + -1)
JMP981(i59, i59, i59, i148, 0) → JMP873(i59, i148, i59)
JMP873(1, i71, 1) → Cond_JMP8731(1 > 0 && i71 >= 1, 1, i71, 1)
Cond_JMP8731(TRUE, 1, i71, 1) → JMP873(1, i71 + -1, 1)
The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (7) Obligation:

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

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
JMP981(i59, i59, i59, i148, i162) → Cond_JMP981(i162 > 0, i59, i59, i59, i148, i162)
Cond_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981(i59, i59, i59, i148 + -1, i162 + -1)
JMP873(i59, i71, i59) → Cond_JMP873(i59 > 0 && i71 >= i59, i59, i71, i59)
Cond_JMP873(TRUE, i59, i71, i59) → JMP981(i59, i59, i59, i71 + -1 + -1, i59 + -1 + -1)
JMP981(i59, i59, i59, i148, 0) → JMP873(i59, i148, i59)
JMP873(1, i71, 1) → Cond_JMP8731(1 > 0 && i71 >= 1, 1, i71, 1)
Cond_JMP8731(TRUE, 1, i71, 1) → JMP873(1, i71 + -1, 1)

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(2): JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(i59[2] > 0 && i71[2] >= i59[2], i59[2], i71[2], i59[2])
(3): COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], i71[3] + -1 + -1, i59[3] + -1 + -1)
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(5): JMP873'(1, i71[5], 1) → COND_JMP8731(1 > 0 && i71[5] >= 1, 1, i71[5], 1)
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(0) -> (1), if ((i162[0] > 0* TRUE)∧(i162[0]* i162[1])∧(i148[0]* i148[1])∧(i59[0]* i59[1]))

(1) -> (0), if ((i162[1] + -1* i162[0])∧(i59[1]* i59[0])∧(i148[1] + -1* i148[0]))

(1) -> (4), if ((i59[1]* i59[4])∧(i162[1] + -1* 0)∧(i148[1] + -1* i148[4]))

(2) -> (3), if ((i59[2]* i59[3])∧(i59[2] > 0 && i71[2] >= i59[2]* TRUE)∧(i71[2]* i71[3]))

(3) -> (0), if ((i59[3]* i59[0])∧(i59[3] + -1 + -1* i162[0])∧(i71[3] + -1 + -1* i148[0]))

(3) -> (4), if ((i59[3] + -1 + -1* 0)∧(i59[3]* i59[4])∧(i71[3] + -1 + -1* i148[4]))

(4) -> (2), if ((i59[4]* i59[2])∧(i148[4]* i71[2]))

(4) -> (5), if ((i59[4]* 1)∧(i148[4]* i71[5]))

(5) -> (6), if ((i71[5]* i71[6])∧(1 > 0 && i71[5] >= 1* TRUE))

(6) -> (2), if ((i71[6] + -1* i71[2])∧(1* i59[2]))

(6) -> (5), if (i71[6] + -1* i71[5])

The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

### (9) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(2): JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(i59[2] > 0 && i71[2] >= i59[2], i59[2], i71[2], i59[2])
(3): COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], i71[3] + -1 + -1, i59[3] + -1 + -1)
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(5): JMP873'(1, i71[5], 1) → COND_JMP8731(1 > 0 && i71[5] >= 1, 1, i71[5], 1)
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(0) -> (1), if ((i162[0] > 0* TRUE)∧(i162[0]* i162[1])∧(i148[0]* i148[1])∧(i59[0]* i59[1]))

(1) -> (0), if ((i162[1] + -1* i162[0])∧(i59[1]* i59[0])∧(i148[1] + -1* i148[0]))

(1) -> (4), if ((i59[1]* i59[4])∧(i162[1] + -1* 0)∧(i148[1] + -1* i148[4]))

(2) -> (3), if ((i59[2]* i59[3])∧(i59[2] > 0 && i71[2] >= i59[2]* TRUE)∧(i71[2]* i71[3]))

(3) -> (0), if ((i59[3]* i59[0])∧(i59[3] + -1 + -1* i162[0])∧(i71[3] + -1 + -1* i148[0]))

(3) -> (4), if ((i59[3] + -1 + -1* 0)∧(i59[3]* i59[4])∧(i71[3] + -1 + -1* i148[4]))

(4) -> (2), if ((i59[4]* i59[2])∧(i148[4]* i71[2]))

(4) -> (5), if ((i59[4]* 1)∧(i148[4]* i71[5]))

(5) -> (6), if ((i71[5]* i71[6])∧(1 > 0 && i71[5] >= 1* TRUE))

(6) -> (2), if ((i71[6] + -1* i71[2])∧(1* i59[2]))

(6) -> (5), if (i71[6] + -1* i71[5])

The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (10) IDPNonInfProof (SOUND transformation)

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

For Pair JMP981'(i59, i59, i59, i148, i162) → COND_JMP981(>(i162, 0), i59, i59, i59, i148, i162) the following chains were created:
• We consider the chain JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0]), COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

(1)    (>(i162[0], 0)=TRUEi162[0]=i162[1]i148[0]=i148[1]i59[0]=i59[1]JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))

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

(2)    (>(i162[0], 0)=TRUEJMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))

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

(3)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]i148[0] + [(2)bni_21]i59[0] ≥ 0∧[(-1)bso_22] ≥ 0)

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

(4)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]i148[0] + [(2)bni_21]i59[0] ≥ 0∧[(-1)bso_22] ≥ 0)

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

(5)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]i148[0] + [(2)bni_21]i59[0] ≥ 0∧[(-1)bso_22] ≥ 0)

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

(6)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[bni_21] = 0∧[(2)bni_21] = 0∧[(-1)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

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

(7)    (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[bni_21] = 0∧[(2)bni_21] = 0∧[(-1)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

For Pair COND_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981'(i59, i59, i59, +(i148, -1), +(i162, -1)) the following chains were created:
• We consider the chain COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

(8)    (COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥NonInfC∧COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))∧(UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥))

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

(9)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[1 + (-1)bso_24] ≥ 0)

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

(10)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[1 + (-1)bso_24] ≥ 0)

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

(11)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[1 + (-1)bso_24] ≥ 0)

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

(12)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)

For Pair JMP873'(i59, i71, i59) → COND_JMP873(&&(>(i59, 0), >=(i71, i59)), i59, i71, i59) the following chains were created:
• We consider the chain JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2]), COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1)) which results in the following constraint:

(13)    (i59[2]=i59[3]&&(>(i59[2], 0), >=(i71[2], i59[2]))=TRUEi71[2]=i71[3]JMP873'(i59[2], i71[2], i59[2])≥NonInfC∧JMP873'(i59[2], i71[2], i59[2])≥COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])∧(UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥))

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

(14)    (>(i59[2], 0)=TRUE>=(i71[2], i59[2])=TRUEJMP873'(i59[2], i71[2], i59[2])≥NonInfC∧JMP873'(i59[2], i71[2], i59[2])≥COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])∧(UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥))

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

(15)    (i59[2] + [-1] ≥ 0∧i71[2] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

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

(16)    (i59[2] + [-1] ≥ 0∧i71[2] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

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

(17)    (i59[2] + [-1] ≥ 0∧i71[2] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

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

(18)    (i59[2] ≥ 0∧i71[2] + [-1] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

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

(19)    (i59[2] ≥ 0∧i71[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(2)bni_25 + (-1)Bound*bni_25] + [(3)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

For Pair COND_JMP873(TRUE, i59, i71, i59) → JMP981'(i59, i59, i59, +(+(i71, -1), -1), +(+(i59, -1), -1)) the following chains were created:
• We consider the chain COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1)) which results in the following constraint:

(20)    (COND_JMP873(TRUE, i59[3], i71[3], i59[3])≥NonInfC∧COND_JMP873(TRUE, i59[3], i71[3], i59[3])≥JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))∧(UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥))

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

(21)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧[2 + (-1)bso_28] ≥ 0)

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

(22)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧[2 + (-1)bso_28] ≥ 0)

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

(23)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧[2 + (-1)bso_28] ≥ 0)

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

(24)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_28] ≥ 0)

For Pair JMP981'(i59, i59, i59, i148, 0) → JMP873'(i59, i148, i59) the following chains were created:
• We consider the chain JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4]), JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2]) which results in the following constraint:

(25)    (i59[4]=i59[2]i148[4]=i71[2]JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥NonInfC∧JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥JMP873'(i59[4], i148[4], i59[4])∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))

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

(26)    (JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥NonInfC∧JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥JMP873'(i59[4], i148[4], i59[4])∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))

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

(27)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)

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

(28)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)

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

(29)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)

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

(30)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)

• We consider the chain JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4]), JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1) which results in the following constraint:

(31)    (i59[4]=1i148[4]=i71[5]JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥NonInfC∧JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥JMP873'(i59[4], i148[4], i59[4])∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))

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

(32)    (JMP981'(1, 1, 1, i148[4], 0)≥NonInfC∧JMP981'(1, 1, 1, i148[4], 0)≥JMP873'(1, i148[4], 1)∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))

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

(33)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)

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

(34)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)

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

(35)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)

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

(36)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧[(-1)bso_30] ≥ 0)

For Pair JMP873'(1, i71, 1) → COND_JMP8731(&&(>(1, 0), >=(i71, 1)), 1, i71, 1) the following chains were created:
• We consider the chain JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1), COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, +(i71[6], -1), 1) which results in the following constraint:

(37)    (i71[5]=i71[6]&&(>(1, 0), >=(i71[5], 1))=TRUEJMP873'(1, i71[5], 1)≥NonInfC∧JMP873'(1, i71[5], 1)≥COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)∧(UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥))

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

(38)    (>=(i71[5], 1)=TRUEJMP873'(1, i71[5], 1)≥NonInfC∧JMP873'(1, i71[5], 1)≥COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)∧(UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥))

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

(39)    (i71[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)

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

(40)    (i71[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)

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

(41)    (i71[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)

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

(42)    (i71[5] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)

For Pair COND_JMP8731(TRUE, 1, i71, 1) → JMP873'(1, +(i71, -1), 1) the following chains were created:
• We consider the chain COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, +(i71[6], -1), 1) which results in the following constraint:

(43)    (COND_JMP8731(TRUE, 1, i71[6], 1)≥NonInfC∧COND_JMP8731(TRUE, 1, i71[6], 1)≥JMP873'(1, +(i71[6], -1), 1)∧(UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥))

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

(44)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧[(-1)bso_34] ≥ 0)

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

(45)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧[(-1)bso_34] ≥ 0)

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

(46)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧[(-1)bso_34] ≥ 0)

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

(47)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧0 = 0∧[(-1)bso_34] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• JMP981'(i59, i59, i59, i148, i162) → COND_JMP981(>(i162, 0), i59, i59, i59, i148, i162)
• (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[bni_21] = 0∧[(2)bni_21] = 0∧[(-1)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

• COND_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981'(i59, i59, i59, +(i148, -1), +(i162, -1))
• ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)

• JMP873'(i59, i71, i59) → COND_JMP873(&&(>(i59, 0), >=(i71, i59)), i59, i71, i59)
• (i59[2] ≥ 0∧i71[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(2)bni_25 + (-1)Bound*bni_25] + [(3)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

• COND_JMP873(TRUE, i59, i71, i59) → JMP981'(i59, i59, i59, +(+(i71, -1), -1), +(+(i59, -1), -1))
• ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_28] ≥ 0)

• JMP981'(i59, i59, i59, i148, 0) → JMP873'(i59, i148, i59)
• ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)
• ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧[(-1)bso_30] ≥ 0)

• JMP873'(1, i71, 1) → COND_JMP8731(&&(>(1, 0), >=(i71, 1)), 1, i71, 1)
• (i71[5] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)

• COND_JMP8731(TRUE, 1, i71, 1) → JMP873'(1, +(i71, -1), 1)
• ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧0 = 0∧[(-1)bso_34] ≥ 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(JMP981'(x1, x2, x3, x4, x5)) = [-1] + x4 + [-1]x3 + x2 + [2]x1
POL(COND_JMP981(x1, x2, x3, x4, x5, x6)) = [-1] + [2]x4 + x3 + x5 + [-1]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(JMP873'(x1, x2, x3)) = [-1] + x1 + x3 + x2
POL(COND_JMP873(x1, x2, x3, x4)) = [-1] + x4 + x2 + x3
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(1) = [1]
POL(COND_JMP8731(x1, x2, x3, x4)) = x3

The following pairs are in P>:

COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))
COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))
JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)

The following pairs are in Pbound:

JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])
JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)

The following pairs are in P:

JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])
JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])
JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, +(i71[6], -1), 1)

There are no usable rules.

### (12) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(2): JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(i59[2] > 0 && i71[2] >= i59[2], i59[2], i71[2], i59[2])
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(4) -> (2), if ((i59[4]* i59[2])∧(i148[4]* i71[2]))

(6) -> (2), if ((i71[6] + -1* i71[2])∧(1* i59[2]))

The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (13) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 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

R is empty.

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(3): COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], i71[3] + -1 + -1, i59[3] + -1 + -1)
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(1) -> (0), if ((i162[1] + -1* i162[0])∧(i59[1]* i59[0])∧(i148[1] + -1* i148[0]))

(3) -> (0), if ((i59[3]* i59[0])∧(i59[3] + -1 + -1* i162[0])∧(i71[3] + -1 + -1* i148[0]))

(0) -> (1), if ((i162[0] > 0* TRUE)∧(i162[0]* i162[1])∧(i148[0]* i148[1])∧(i59[0]* i59[1]))

(1) -> (4), if ((i59[1]* i59[4])∧(i162[1] + -1* 0)∧(i148[1] + -1* i148[4]))

(3) -> (4), if ((i59[3] + -1 + -1* 0)∧(i59[3]* i59[4])∧(i71[3] + -1 + -1* i148[4]))

The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (16) IDependencyGraphProof (EQUIVALENT transformation)

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

### (17) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])

(1) -> (0), if ((i162[1] + -1* i162[0])∧(i59[1]* i59[0])∧(i148[1] + -1* i148[0]))

(0) -> (1), if ((i162[0] > 0* TRUE)∧(i162[0]* i162[1])∧(i148[0]* i148[1])∧(i59[0]* i59[1]))

The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (18) IDPNonInfProof (SOUND transformation)

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

For Pair COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) the following chains were created:
• We consider the chain COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

(1)    (COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥NonInfC∧COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))∧(UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥))

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

(2)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[(-1)bso_7] ≥ 0)

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

(3)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[(-1)bso_7] ≥ 0)

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

(4)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[(-1)bso_7] ≥ 0)

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

(5)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_7] ≥ 0)

For Pair JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0]) the following chains were created:
• We consider the chain JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0]), COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

(6)    (>(i162[0], 0)=TRUEi162[0]=i162[1]i148[0]=i148[1]i59[0]=i59[1]JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))

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

(7)    (>(i162[0], 0)=TRUEJMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))

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

(8)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧[2 + (-1)bso_9] ≥ 0)

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

(9)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧[2 + (-1)bso_9] ≥ 0)

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

(10)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧[2 + (-1)bso_9] ≥ 0)

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

(11)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧0 = 0∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

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

(12)    (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧0 = 0∧[(4)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))
• ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_7] ≥ 0)

• JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])
• (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧0 = 0∧[(4)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 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_JMP981(x1, x2, x3, x4, x5, x6)) = [2]x6
POL(JMP981'(x1, x2, x3, x4, x5)) = [2] + [2]x5
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = 0
POL(0) = 0

The following pairs are in P>:

JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])

The following pairs are in Pbound:

JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])

The following pairs are in P:

COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))

There are no usable rules.

### (19) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)

The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

### (20) IDependencyGraphProof (EQUIVALENT transformation)

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

### (22) 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:
JMP839(i71, i74) → Cond_JMP839(i74 > 0, i71, i74)
Cond_JMP839(TRUE, i71, i74) → JMP839(i71 + -1, i74 + -1)
The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

### (24) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
JMP839(i71, i74) → Cond_JMP839(i74 > 0, i71, i74)
Cond_JMP839(TRUE, i71, i74) → JMP839(i71 + -1, i74 + -1)

The integer pair graph contains the following rules and edges:
(0): JMP839'(i71[0], i74[0]) → COND_JMP839(i74[0] > 0, i71[0], i74[0])
(1): COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(i71[1] + -1, i74[1] + -1)

(0) -> (1), if ((i74[0]* i74[1])∧(i74[0] > 0* TRUE)∧(i71[0]* i71[1]))

(1) -> (0), if ((i71[1] + -1* i71[0])∧(i74[1] + -1* i74[0]))

The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

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

### (26) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): JMP839'(i71[0], i74[0]) → COND_JMP839(i74[0] > 0, i71[0], i74[0])
(1): COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(i71[1] + -1, i74[1] + -1)

(0) -> (1), if ((i74[0]* i74[1])∧(i74[0] > 0* TRUE)∧(i71[0]* i71[1]))

(1) -> (0), if ((i71[1] + -1* i71[0])∧(i74[1] + -1* i74[0]))

The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

### (27) IDPNonInfProof (SOUND transformation)

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

For Pair JMP839'(i71, i74) → COND_JMP839(>(i74, 0), i71, i74) the following chains were created:
• We consider the chain JMP839'(i71[0], i74[0]) → COND_JMP839(>(i74[0], 0), i71[0], i74[0]), COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(+(i71[1], -1), +(i74[1], -1)) which results in the following constraint:

(1)    (i74[0]=i74[1]>(i74[0], 0)=TRUEi71[0]=i71[1]JMP839'(i71[0], i74[0])≥NonInfC∧JMP839'(i71[0], i74[0])≥COND_JMP839(>(i74[0], 0), i71[0], i74[0])∧(UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥))

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

(2)    (>(i74[0], 0)=TRUEJMP839'(i71[0], i74[0])≥NonInfC∧JMP839'(i71[0], i74[0])≥COND_JMP839(>(i74[0], 0), i71[0], i74[0])∧(UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥))

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

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

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

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

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

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

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

(6)    (i74[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥)∧0 = 0∧[bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i74[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

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

(7)    (i74[0] ≥ 0 ⇒ (UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥)∧0 = 0∧[(3)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i74[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

For Pair COND_JMP839(TRUE, i71, i74) → JMP839'(+(i71, -1), +(i74, -1)) the following chains were created:
• We consider the chain COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(+(i71[1], -1), +(i74[1], -1)) which results in the following constraint:

(8)    (COND_JMP839(TRUE, i71[1], i74[1])≥NonInfC∧COND_JMP839(TRUE, i71[1], i74[1])≥JMP839'(+(i71[1], -1), +(i74[1], -1))∧(UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥))

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

(9)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧[(-1)bso_11] ≥ 0)

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

(10)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧[(-1)bso_11] ≥ 0)

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

(11)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧[(-1)bso_11] ≥ 0)

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

(12)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• JMP839'(i71, i74) → COND_JMP839(>(i74, 0), i71, i74)
• (i74[0] ≥ 0 ⇒ (UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥)∧0 = 0∧[(3)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i74[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

• COND_JMP839(TRUE, i71, i74) → JMP839'(+(i71, -1), +(i74, -1))
• ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(JMP839'(x1, x2)) = [1] + [2]x2
POL(COND_JMP839(x1, x2, x3)) = [-1] + [2]x3
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]

The following pairs are in P>:

JMP839'(i71[0], i74[0]) → COND_JMP839(>(i74[0], 0), i71[0], i74[0])

The following pairs are in Pbound:

JMP839'(i71[0], i74[0]) → COND_JMP839(>(i74[0], 0), i71[0], i74[0])

The following pairs are in P:

COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(+(i71[1], -1), +(i74[1], -1))

There are no usable rules.

### (28) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(i71[1] + -1, i74[1] + -1)

The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

### (29) IDependencyGraphProof (EQUIVALENT transformation)

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