Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 ITRStoIDPProof (⇔)
↳6 IDP
↳7 UsableRulesProof (⇔)
↳8 IDP
↳9 ItpfGraphProof (⇔)
↳10 IDP
↳11 IDPNonInfProof (⇐)
↳12 AND
    ↳13 IDP
        ↳14 IDependencyGraphProof (⇔)
        ↳15 IDP
        ↳16 IDPNonInfProof (⇐)
        ↳17 AND
            ↳18 IDP
                ↳19 IDependencyGraphProof (⇔)
                ↳20 IDP
                ↳21 IDPNonInfProof (⇐)
                ↳22 AND
                    ↳23 IDP
                        ↳24 IDependencyGraphProof (⇔)
                        ↳25 TRUE
                    ↳26 IDP
                        ↳27 IDependencyGraphProof (⇔)
                        ↳28 TRUE
            ↳29 IDP
                ↳30 IDependencyGraphProof (⇔)
                ↳31 TRUE
    ↳32 IDP
        ↳33 IDependencyGraphProof (⇔)
        ↳34 IDP
        ↳35 IDPNonInfProof (⇐)
        ↳36 AND
            ↳37 IDP
                ↳38 IDependencyGraphProof (⇔)
                ↳39 TRUE
            ↳40 IDP
                ↳41 IDependencyGraphProof (⇔)
                ↳42 TRUE

(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)
Cond_Load8271(TRUE, i80, 1) → Load827(i80, 0)
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)
Cond_Load8272(TRUE, 1, i88) → Load827(0, 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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(5) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(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)
Cond_Load8271(TRUE, i80, 1) → Load827(i80, 0)
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)
Cond_Load8272(TRUE, 1, i88) → Load827(0, 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)
(7): COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 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])
(10): LOAD827(1, i88[10]) → COND_LOAD8272(i88[10] > 0 && 1 > i88[10], 1, i88[10])
(11): COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11])
(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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)
(7): COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 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])
(10): LOAD827(1, i88[10]) → COND_LOAD8272(i88[10] > 0 && 1 > i88[10], 1, i88[10])
(11): COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11])
(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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)
(7): COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 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])
(10): LOAD827(1, i88[10]) → COND_LOAD8272(i88[10] > 0 && 1 > i88[10], 1, i88[10])
(11): COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11])
(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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))=TRUE∧i80[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)=TRUE ⇒ 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 (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))=TRUE ⇒ LOAD827(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])=TRUE ⇒ LOAD827(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)=TRUE∧i80[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:

    (32)    (COND_LE10111(TRUE, i80[5], 1, 1)≥NonInfC∧COND_LE10111(TRUE, i80[5], 1, 1)≥LOAD827(i80[5], 0)∧(UIncreasing(LOAD827(i80[5], 0)), ≥))



    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:

    (37)    (&&(>(i80[6], 0), <=(i80[6], 1))=TRUE∧i80[6]=i80[7] ⇒ LOAD827(i80[6], 1)≥NonInfC∧LOAD827(i80[6], 1)≥COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)∧(UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥))



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

    (38)    (>(i80[6], 0)=TRUE∧<=(i80[6], 1)=TRUE ⇒ LOAD827(i80[6], 1)≥NonInfC∧LOAD827(i80[6], 1)≥COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)∧(UIncreasing(COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)), ≥))



    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:

    (44)    (COND_LOAD8271(TRUE, i80[7], 1)≥NonInfC∧COND_LOAD8271(TRUE, i80[7], 1)≥LOAD827(i80[7], 0)∧(UIncreasing(LOAD827(i80[7], 0)), ≥))



    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)=TRUE ⇒ 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 (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:

    (55)    (COND_LE1012(TRUE, 1, i88[9], 1)≥NonInfC∧COND_LE1012(TRUE, 1, i88[9], 1)≥LOAD827(0, i88[9])∧(UIncreasing(LOAD827(0, i88[9])), ≥))



    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:

    (60)    (&&(>(i88[10], 0), >(1, i88[10]))=TRUE∧i88[10]=i88[11] ⇒ LOAD827(1, i88[10])≥NonInfC∧LOAD827(1, i88[10])≥COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])∧(UIncreasing(COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])), ≥))



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

    (61)    (>(i88[10], 0)=TRUE∧>(1, i88[10])=TRUE ⇒ LOAD827(1, i88[10])≥NonInfC∧LOAD827(1, i88[10])≥COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])∧(UIncreasing(COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])), ≥))



    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:

    (65)    (COND_LOAD8272(TRUE, 1, i88[11])≥NonInfC∧COND_LOAD8272(TRUE, 1, i88[11])≥LOAD827(0, i88[11])∧(UIncreasing(LOAD827(0, i88[11])), ≥))



    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))=TRUE ⇒ LE1012'(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)=TRUE ⇒ LE1012'(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:

    (83)    (&&(>(i88[14], 0), >(i80[14], i88[14]))=TRUE∧i80[14]=i80[15]∧i88[14]=i88[15] ⇒ LOAD827(i80[14], i88[14])≥NonInfC∧LOAD827(i80[14], i88[14])≥COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])∧(UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥))



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

    (84)    (>(i88[14], 0)=TRUE∧>(i80[14], i88[14])=TRUE ⇒ LOAD827(i80[14], i88[14])≥NonInfC∧LOAD827(i80[14], i88[14])≥COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])∧(UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥))



    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)

  • LOAD827(i80, 1) → COND_LOAD8271(&&(>(i80, 0), <=(i80, 1)), i80, 1)
    • (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)

  • COND_LOAD8271(TRUE, i80, 1) → LOAD827(i80, 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)

  • LOAD827(1, i88) → COND_LOAD8272(&&(>(i88, 0), >(1, i88)), 1, i88)

  • COND_LOAD8272(TRUE, 1, i88) → LOAD827(0, i88)
    • ((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)

  • LOAD827(i80, i88) → COND_LOAD8273(&&(>(i88, 0), >(i80, i88)), i80, i88)
    • (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(COND_LOAD8271(x1, x2, x3)) = [-1]   
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)
LOAD827(i80[6], 1) → COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)
LOAD827(1, i88[10]) → COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])

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])
LOAD827(i80[6], 1) → COND_LOAD8271(&&(>(i80[6], 0), <=(i80[6], 1)), i80[6], 1)
LOAD827(1, i88[10]) → COND_LOAD8272(&&(>(i88[10], 0), >(1, i88[10])), 1, i88[10])
LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])

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)
COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 0)
LE1012'(1, i88[8], 1) → COND_LE1012(>(1, 0), 1, i88[8], 1)
COND_LE1012(TRUE, 1, i88[9], 1) → LOAD827(0, i88[9])
COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11])
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))
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))

There are no usable rules.

(12) Complex Obligation (AND)

(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)
(7): COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 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])
(11): COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11])
(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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))=TRUE ⇒ LE1012'(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)=TRUE ⇒ LE1012'(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:

    (14)    (COND_LE1012(TRUE, 1, i88[9], 1)≥NonInfC∧COND_LE1012(TRUE, 1, i88[9], 1)≥LOAD827(0, i88[9])∧(UIncreasing(LOAD827(0, i88[9])), ≥))



    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)=TRUE ⇒ 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 (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:

    (30)    (&&(>(i88[14], 0), >(i80[14], i88[14]))=TRUE∧i80[14]=i80[15]∧i88[14]=i88[15] ⇒ LOAD827(i80[14], i88[14])≥NonInfC∧LOAD827(i80[14], i88[14])≥COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])∧(UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥))



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

    (31)    (>(i88[14], 0)=TRUE∧>(i80[14], i88[14])=TRUE ⇒ LOAD827(i80[14], i88[14])≥NonInfC∧LOAD827(i80[14], i88[14])≥COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])∧(UIncreasing(COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])), ≥))



    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)

  • LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])
    • (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   
POL(COND_LOAD8273(x1, x2, x3)) = [1]   

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])
LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])

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)
LOAD827(i80[14], i88[14]) → COND_LOAD8273(&&(>(i88[14], 0), >(i80[14], i88[14])), i80[14], i88[14])

There are no usable rules.

(17) Complex Obligation (AND)

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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))=TRUE ⇒ LE1012'(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)=TRUE ⇒ LE1012'(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.

(22) Complex Obligation (AND)

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(24) IDependencyGraphProof (EQUIVALENT transformation)

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

(25) TRUE

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(28) TRUE

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(30) IDependencyGraphProof (EQUIVALENT transformation)

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

(31) TRUE

(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)
(7): COND_LOAD8271(TRUE, i80[7], 1) → LOAD827(i80[7], 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])
(11): COND_LOAD8272(TRUE, 1, i88[11]) → LOAD827(0, i88[11])
(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(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))=TRUE ⇒ LE1012'(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)=TRUE ⇒ LE1012'(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.

(36) Complex Obligation (AND)

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(38) IDependencyGraphProof (EQUIVALENT transformation)

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

(39) TRUE

(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)
Load827(x0, x1)
Cond_Load827(TRUE, x0, x1)
Cond_LE10111(TRUE, x0, 1, 1)
Cond_Load8271(TRUE, x0, 1)
Cond_LE1012(TRUE, 1, x0, 1)
Cond_Load8272(TRUE, 1, x0)
LE1012(x0, x1, x0)
Cond_LE10121(TRUE, x0, x1, x0)
Cond_Load8273(TRUE, x0, x1)

(41) IDependencyGraphProof (EQUIVALENT transformation)

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

(42) TRUE