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 IDPNonInfProof (⇐)
↳10 AND
    ↳11 IDP
        ↳12 IDependencyGraphProof (⇔)
        ↳13 IDP
        ↳14 IDPNonInfProof (⇐)
        ↳15 IDP
        ↳16 IDependencyGraphProof (⇔)
        ↳17 IDP
        ↳18 IDPNonInfProof (⇐)
        ↳19 AND
            ↳20 IDP
                ↳21 IDependencyGraphProof (⇔)
                ↳22 TRUE
            ↳23 IDP
                ↳24 IDependencyGraphProof (⇔)
                ↳25 TRUE
    ↳26 IDP
        ↳27 IDependencyGraphProof (⇔)
        ↳28 IDP
        ↳29 IDPNonInfProof (⇐)
        ↳30 AND
            ↳31 IDP
                ↳32 IDependencyGraphProof (⇔)
                ↳33 TRUE
            ↳34 IDP
                ↳35 IDependencyGraphProof (⇔)
                ↳36 TRUE

(0) Obligation:

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

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

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

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

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
Load425(i60, i69) → Cond_Load425(i60 > 0 && i60 <= i69, i60, i69)
Cond_Load425(TRUE, i60, i69) → Load702(i60, i69)
Load702(i60, i99) → Cond_Load702(i99 > 0, i60, i99)
Cond_Load702(TRUE, i60, i99) → Load702(i60, i99 + -1)
Load702(i60, 0) → Load425(i60, 0)
Load719(0, i69) → Load425(0, i69)
Load425(i60, i69) → Cond_Load4251(i69 > 0 && i60 > i69, i60, i69)
Cond_Load4251(TRUE, i60, i69) → Load719(i60, i69)
Load719(i101, i69) → Cond_Load719(i101 > 0, i101, i69)
Cond_Load719(TRUE, i101, i69) → Load719(i101 + -1, i69)
The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(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:
Load425(i60, i69) → Cond_Load425(i60 > 0 && i60 <= i69, i60, i69)
Cond_Load425(TRUE, i60, i69) → Load702(i60, i69)
Load702(i60, i99) → Cond_Load702(i99 > 0, i60, i99)
Cond_Load702(TRUE, i60, i99) → Load702(i60, i99 + -1)
Load702(i60, 0) → Load425(i60, 0)
Load719(0, i69) → Load425(0, i69)
Load425(i60, i69) → Cond_Load4251(i69 > 0 && i60 > i69, i60, i69)
Cond_Load4251(TRUE, i60, i69) → Load719(i60, i69)
Load719(i101, i69) → Cond_Load719(i101 > 0, i101, i69)
Cond_Load719(TRUE, i101, i69) → Load719(i101 + -1, i69)

The integer pair graph contains the following rules and edges:
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])
(1): COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(4): LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
(5): LOAD719(0, i69[5]) → LOAD425(0, i69[5])
(6): LOAD425(i60[6], i69[6]) → COND_LOAD4251(i69[6] > 0 && i60[6] > i69[6], i60[6], i69[6])
(7): COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7])
(8): LOAD719(i101[8], i69[8]) → COND_LOAD719(i101[8] > 0, i101[8], i69[8])
(9): COND_LOAD719(TRUE, i101[9], i69[9]) → LOAD719(i101[9] + -1, i69[9])

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(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): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])
(1): COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(4): LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
(5): LOAD719(0, i69[5]) → LOAD425(0, i69[5])
(6): LOAD425(i60[6], i69[6]) → COND_LOAD4251(i69[6] > 0 && i60[6] > i69[6], i60[6], i69[6])
(7): COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7])
(8): LOAD719(i101[8], i69[8]) → COND_LOAD719(i101[8] > 0, i101[8], i69[8])
(9): COND_LOAD719(TRUE, i101[9], i69[9]) → LOAD719(i101[9] + -1, i69[9])

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(9) IDPNonInfProof (SOUND transformation)

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


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

    (1)    (i69[0]=i69[1]∧i60[0]=i60[1]∧&&(>(i60[0], 0), <=(i60[0], i69[0]))=TRUE ⇒ LOAD425(i60[0], i69[0])≥NonInfC∧LOAD425(i60[0], i69[0])≥COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])∧(UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥))



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

    (2)    (>(i60[0], 0)=TRUE∧<=(i60[0], i69[0])=TRUE ⇒ LOAD425(i60[0], i69[0])≥NonInfC∧LOAD425(i60[0], i69[0])≥COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])∧(UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (8)    (i69[1]=i99[2]∧i60[1]=i60[2] ⇒ COND_LOAD425(TRUE, i60[1], i69[1])≥NonInfC∧COND_LOAD425(TRUE, i60[1], i69[1])≥LOAD702(i60[1], i69[1])∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

    (9)    (COND_LOAD425(TRUE, i60[1], i69[1])≥NonInfC∧COND_LOAD425(TRUE, i60[1], i69[1])≥LOAD702(i60[1], i69[1])∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

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



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

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



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

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



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

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



  • We consider the chain COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1]), LOAD702(i60[4], 0) → LOAD425(i60[4], 0) which results in the following constraint:

    (14)    (i60[1]=i60[4]∧i69[1]=0 ⇒ COND_LOAD425(TRUE, i60[1], i69[1])≥NonInfC∧COND_LOAD425(TRUE, i60[1], i69[1])≥LOAD702(i60[1], i69[1])∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

    (15)    (COND_LOAD425(TRUE, i60[1], 0)≥NonInfC∧COND_LOAD425(TRUE, i60[1], 0)≥LOAD702(i60[1], 0)∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

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



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

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



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

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



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

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







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

    (20)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3] ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

    (21)    (>(i99[2], 0)=TRUE ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (27)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3]∧i60[3]=i60[2]1∧+(i99[3], -1)=i99[2]1 ⇒ COND_LOAD702(TRUE, i60[3], i99[3])≥NonInfC∧COND_LOAD702(TRUE, i60[3], i99[3])≥LOAD702(i60[3], +(i99[3], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

    (28)    (>(i99[2], 0)=TRUE ⇒ COND_LOAD702(TRUE, i60[2], i99[2])≥NonInfC∧COND_LOAD702(TRUE, i60[2], i99[2])≥LOAD702(i60[2], +(i99[2], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

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



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

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



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

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



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

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



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

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



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

    (34)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3]∧i60[3]=i60[4]∧+(i99[3], -1)=0 ⇒ COND_LOAD702(TRUE, i60[3], i99[3])≥NonInfC∧COND_LOAD702(TRUE, i60[3], i99[3])≥LOAD702(i60[3], +(i99[3], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

    (35)    (>(i99[2], 0)=TRUE∧+(i99[2], -1)=0 ⇒ COND_LOAD702(TRUE, i60[2], i99[2])≥NonInfC∧COND_LOAD702(TRUE, i60[2], i99[2])≥LOAD702(i60[2], +(i99[2], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (41)    (i60[4]=i60[0]∧0=i69[0] ⇒ LOAD702(i60[4], 0)≥NonInfC∧LOAD702(i60[4], 0)≥LOAD425(i60[4], 0)∧(UIncreasing(LOAD425(i60[4], 0)), ≥))



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

    (42)    (LOAD702(i60[4], 0)≥NonInfC∧LOAD702(i60[4], 0)≥LOAD425(i60[4], 0)∧(UIncreasing(LOAD425(i60[4], 0)), ≥))



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

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



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

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



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

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



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

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



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

    (47)    (0=i69[6]∧i60[4]=i60[6] ⇒ LOAD702(i60[4], 0)≥NonInfC∧LOAD702(i60[4], 0)≥LOAD425(i60[4], 0)∧(UIncreasing(LOAD425(i60[4], 0)), ≥))



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

    (48)    (LOAD702(i60[4], 0)≥NonInfC∧LOAD702(i60[4], 0)≥LOAD425(i60[4], 0)∧(UIncreasing(LOAD425(i60[4], 0)), ≥))



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

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



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

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



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

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



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

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







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

    (53)    (i69[5]=i69[0]∧0=i60[0] ⇒ LOAD719(0, i69[5])≥NonInfC∧LOAD719(0, i69[5])≥LOAD425(0, i69[5])∧(UIncreasing(LOAD425(0, i69[5])), ≥))



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

    (54)    (LOAD719(0, i69[5])≥NonInfC∧LOAD719(0, i69[5])≥LOAD425(0, i69[5])∧(UIncreasing(LOAD425(0, i69[5])), ≥))



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

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



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

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



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

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



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

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



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

    (59)    (i69[5]=i69[6]∧0=i60[6] ⇒ LOAD719(0, i69[5])≥NonInfC∧LOAD719(0, i69[5])≥LOAD425(0, i69[5])∧(UIncreasing(LOAD425(0, i69[5])), ≥))



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

    (60)    (LOAD719(0, i69[5])≥NonInfC∧LOAD719(0, i69[5])≥LOAD425(0, i69[5])∧(UIncreasing(LOAD425(0, i69[5])), ≥))



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

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



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

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



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

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



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

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







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

    (65)    (i60[6]=i60[7]∧i69[6]=i69[7]∧&&(>(i69[6], 0), >(i60[6], i69[6]))=TRUE ⇒ LOAD425(i60[6], i69[6])≥NonInfC∧LOAD425(i60[6], i69[6])≥COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])∧(UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥))



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

    (66)    (>(i69[6], 0)=TRUE∧>(i60[6], i69[6])=TRUE ⇒ LOAD425(i60[6], i69[6])≥NonInfC∧LOAD425(i60[6], i69[6])≥COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])∧(UIncreasing(COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (72)    (i69[7]=i69[5]∧i60[7]=0 ⇒ COND_LOAD4251(TRUE, i60[7], i69[7])≥NonInfC∧COND_LOAD4251(TRUE, i60[7], i69[7])≥LOAD719(i60[7], i69[7])∧(UIncreasing(LOAD719(i60[7], i69[7])), ≥))



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

    (73)    (COND_LOAD4251(TRUE, 0, i69[7])≥NonInfC∧COND_LOAD4251(TRUE, 0, i69[7])≥LOAD719(0, i69[7])∧(UIncreasing(LOAD719(i60[7], i69[7])), ≥))



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

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



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

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



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

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



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

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



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

    (78)    (i60[7]=i101[8]∧i69[7]=i69[8] ⇒ COND_LOAD4251(TRUE, i60[7], i69[7])≥NonInfC∧COND_LOAD4251(TRUE, i60[7], i69[7])≥LOAD719(i60[7], i69[7])∧(UIncreasing(LOAD719(i60[7], i69[7])), ≥))



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

    (79)    (COND_LOAD4251(TRUE, i60[7], i69[7])≥NonInfC∧COND_LOAD4251(TRUE, i60[7], i69[7])≥LOAD719(i60[7], i69[7])∧(UIncreasing(LOAD719(i60[7], i69[7])), ≥))



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

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



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

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



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

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



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

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







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

    (84)    (>(i101[8], 0)=TRUE∧i101[8]=i101[9]∧i69[8]=i69[9] ⇒ LOAD719(i101[8], i69[8])≥NonInfC∧LOAD719(i101[8], i69[8])≥COND_LOAD719(>(i101[8], 0), i101[8], i69[8])∧(UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥))



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

    (85)    (>(i101[8], 0)=TRUE ⇒ LOAD719(i101[8], i69[8])≥NonInfC∧LOAD719(i101[8], i69[8])≥COND_LOAD719(>(i101[8], 0), i101[8], i69[8])∧(UIncreasing(COND_LOAD719(>(i101[8], 0), i101[8], i69[8])), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (91)    (>(i101[8], 0)=TRUE∧i101[8]=i101[9]∧i69[8]=i69[9]∧i69[9]=i69[5]∧+(i101[9], -1)=0 ⇒ COND_LOAD719(TRUE, i101[9], i69[9])≥NonInfC∧COND_LOAD719(TRUE, i101[9], i69[9])≥LOAD719(+(i101[9], -1), i69[9])∧(UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥))



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

    (92)    (>(i101[8], 0)=TRUE∧+(i101[8], -1)=0 ⇒ COND_LOAD719(TRUE, i101[8], i69[8])≥NonInfC∧COND_LOAD719(TRUE, i101[8], i69[8])≥LOAD719(+(i101[8], -1), i69[8])∧(UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥))



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

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



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

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



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

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



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

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



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

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



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

    (98)    (>(i101[8], 0)=TRUE∧i101[8]=i101[9]∧i69[8]=i69[9]∧+(i101[9], -1)=i101[8]1∧i69[9]=i69[8]1 ⇒ COND_LOAD719(TRUE, i101[9], i69[9])≥NonInfC∧COND_LOAD719(TRUE, i101[9], i69[9])≥LOAD719(+(i101[9], -1), i69[9])∧(UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥))



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

    (99)    (>(i101[8], 0)=TRUE ⇒ COND_LOAD719(TRUE, i101[8], i69[8])≥NonInfC∧COND_LOAD719(TRUE, i101[8], i69[8])≥LOAD719(+(i101[8], -1), i69[8])∧(UIncreasing(LOAD719(+(i101[9], -1), i69[9])), ≥))



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

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



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

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



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

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



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

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



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

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







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

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

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

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

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

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

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

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

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

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




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD425(x1, x2)) = [-1] + [2]x1   
POL(COND_LOAD425(x1, x2, x3)) = [-1] + [2]x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(<=(x1, x2)) = [-1]   
POL(LOAD702(x1, x2)) = [-1] + [2]x1   
POL(COND_LOAD702(x1, x2, x3)) = [-1] + [2]x2   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(LOAD719(x1, x2)) = [-1] + x1   
POL(COND_LOAD4251(x1, x2, x3)) = [-1] + x2 + [-1]x1   
POL(COND_LOAD719(x1, x2, x3)) = [-1] + x2   

The following pairs are in P>:

LOAD425(i60[6], i69[6]) → COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])
COND_LOAD719(TRUE, i101[9], i69[9]) → LOAD719(+(i101[9], -1), i69[9])

The following pairs are in Pbound:

LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])
LOAD425(i60[6], i69[6]) → COND_LOAD4251(&&(>(i69[6], 0), >(i60[6], i69[6])), i60[6], i69[6])
LOAD719(i101[8], i69[8]) → COND_LOAD719(>(i101[8], 0), i101[8], i69[8])
COND_LOAD719(TRUE, i101[9], i69[9]) → LOAD719(+(i101[9], -1), i69[9])

The following pairs are in P≥:

LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])
COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])
LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2])
COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1))
LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
LOAD719(0, i69[5]) → LOAD425(0, i69[5])
COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7])
LOAD719(i101[8], i69[8]) → COND_LOAD719(>(i101[8], 0), i101[8], i69[8])

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

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

(10) Complex Obligation (AND)

(11) Obligation:

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


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])
(1): COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(4): LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
(5): LOAD719(0, i69[5]) → LOAD425(0, i69[5])
(7): COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7])
(8): LOAD719(i101[8], i69[8]) → COND_LOAD719(i101[8] > 0, i101[8], i69[8])

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


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


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


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


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


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


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


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


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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(12) IDependencyGraphProof (EQUIVALENT transformation)

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

(13) Obligation:

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


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(4): LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(1): COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])
(0): LOAD425(i60[0], i69[0]) → COND_LOAD425(i60[0] > 0 && i60[0] <= i69[0], i60[0], i69[0])

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


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


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


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


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


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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(14) IDPNonInfProof (SOUND transformation)

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


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

    (1)    (i60[4]=i60[0]∧0=i69[0] ⇒ LOAD702(i60[4], 0)≥NonInfC∧LOAD702(i60[4], 0)≥LOAD425(i60[4], 0)∧(UIncreasing(LOAD425(i60[4], 0)), ≥))



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

    (2)    (LOAD702(i60[4], 0)≥NonInfC∧LOAD702(i60[4], 0)≥LOAD425(i60[4], 0)∧(UIncreasing(LOAD425(i60[4], 0)), ≥))



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

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



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

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



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

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



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

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







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

    (7)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3]∧i60[3]=i60[2]1∧+(i99[3], -1)=i99[2]1 ⇒ COND_LOAD702(TRUE, i60[3], i99[3])≥NonInfC∧COND_LOAD702(TRUE, i60[3], i99[3])≥LOAD702(i60[3], +(i99[3], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

    (8)    (>(i99[2], 0)=TRUE ⇒ COND_LOAD702(TRUE, i60[2], i99[2])≥NonInfC∧COND_LOAD702(TRUE, i60[2], i99[2])≥LOAD702(i60[2], +(i99[2], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

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



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

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



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

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



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

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



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

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



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

    (14)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3]∧i60[3]=i60[4]∧+(i99[3], -1)=0 ⇒ COND_LOAD702(TRUE, i60[3], i99[3])≥NonInfC∧COND_LOAD702(TRUE, i60[3], i99[3])≥LOAD702(i60[3], +(i99[3], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

    (15)    (>(i99[2], 0)=TRUE∧+(i99[2], -1)=0 ⇒ COND_LOAD702(TRUE, i60[2], i99[2])≥NonInfC∧COND_LOAD702(TRUE, i60[2], i99[2])≥LOAD702(i60[2], +(i99[2], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (21)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3] ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

    (22)    (>(i99[2], 0)=TRUE ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (28)    (i69[1]=i99[2]∧i60[1]=i60[2] ⇒ COND_LOAD425(TRUE, i60[1], i69[1])≥NonInfC∧COND_LOAD425(TRUE, i60[1], i69[1])≥LOAD702(i60[1], i69[1])∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

    (29)    (COND_LOAD425(TRUE, i60[1], i69[1])≥NonInfC∧COND_LOAD425(TRUE, i60[1], i69[1])≥LOAD702(i60[1], i69[1])∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

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



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

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



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

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



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

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



  • We consider the chain COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1]), LOAD702(i60[4], 0) → LOAD425(i60[4], 0) which results in the following constraint:

    (34)    (i60[1]=i60[4]∧i69[1]=0 ⇒ COND_LOAD425(TRUE, i60[1], i69[1])≥NonInfC∧COND_LOAD425(TRUE, i60[1], i69[1])≥LOAD702(i60[1], i69[1])∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

    (35)    (COND_LOAD425(TRUE, i60[1], 0)≥NonInfC∧COND_LOAD425(TRUE, i60[1], 0)≥LOAD702(i60[1], 0)∧(UIncreasing(LOAD702(i60[1], i69[1])), ≥))



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

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



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

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



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

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



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

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







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

    (40)    (i69[0]=i69[1]∧i60[0]=i60[1]∧&&(>(i60[0], 0), <=(i60[0], i69[0]))=TRUE ⇒ LOAD425(i60[0], i69[0])≥NonInfC∧LOAD425(i60[0], i69[0])≥COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])∧(UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥))



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

    (41)    (>(i60[0], 0)=TRUE∧<=(i60[0], i69[0])=TRUE ⇒ LOAD425(i60[0], i69[0])≥NonInfC∧LOAD425(i60[0], i69[0])≥COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])∧(UIncreasing(COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])), ≥))



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

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



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

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



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

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



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

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



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

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







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

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

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

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

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




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

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

The following pairs are in P>:

LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])

The following pairs are in Pbound:

LOAD425(i60[0], i69[0]) → COND_LOAD425(&&(>(i60[0], 0), <=(i60[0], i69[0])), i60[0], i69[0])

The following pairs are in P≥:

LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1))
LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2])
COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])

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

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

(15) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(4): LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(1): COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])

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


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


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


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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(16) IDependencyGraphProof (EQUIVALENT transformation)

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

(17) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)

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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(18) IDPNonInfProof (SOUND transformation)

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


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

    (1)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3] ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

    (2)    (>(i99[2], 0)=TRUE ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (8)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3]∧i60[3]=i60[2]1∧+(i99[3], -1)=i99[2]1 ⇒ COND_LOAD702(TRUE, i60[3], i99[3])≥NonInfC∧COND_LOAD702(TRUE, i60[3], i99[3])≥LOAD702(i60[3], +(i99[3], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

    (9)    (>(i99[2], 0)=TRUE ⇒ COND_LOAD702(TRUE, i60[2], i99[2])≥NonInfC∧COND_LOAD702(TRUE, i60[2], i99[2])≥LOAD702(i60[2], +(i99[2], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

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



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

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



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

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



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

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



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

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







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

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




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD702(x1, x2)) = [-1] + x2   
POL(COND_LOAD702(x1, x2, x3)) = [-1] + x3   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   

The following pairs are in P>:

COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1))

The following pairs are in Pbound:

LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2])
COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1))

The following pairs are in P≥:

LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2])

There are no usable rules.

(19) Complex Obligation (AND)

(20) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])


The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(21) IDependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE

(23) Obligation:

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


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(24) IDependencyGraphProof (EQUIVALENT transformation)

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

(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:
(1): COND_LOAD425(TRUE, i60[1], i69[1]) → LOAD702(i60[1], i69[1])
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(4): LOAD702(i60[4], 0) → LOAD425(i60[4], 0)
(5): LOAD719(0, i69[5]) → LOAD425(0, i69[5])
(7): COND_LOAD4251(TRUE, i60[7], i69[7]) → LOAD719(i60[7], i69[7])

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


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


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


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


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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(28) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], i99[3] + -1)
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])

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


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



The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(29) IDPNonInfProof (SOUND transformation)

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


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

    (1)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3]∧i60[3]=i60[2]1∧+(i99[3], -1)=i99[2]1 ⇒ COND_LOAD702(TRUE, i60[3], i99[3])≥NonInfC∧COND_LOAD702(TRUE, i60[3], i99[3])≥LOAD702(i60[3], +(i99[3], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

    (2)    (>(i99[2], 0)=TRUE ⇒ COND_LOAD702(TRUE, i60[2], i99[2])≥NonInfC∧COND_LOAD702(TRUE, i60[2], i99[2])≥LOAD702(i60[2], +(i99[2], -1))∧(UIncreasing(LOAD702(i60[3], +(i99[3], -1))), ≥))



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

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



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

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



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

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



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

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



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

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







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

    (8)    (i99[2]=i99[3]∧>(i99[2], 0)=TRUE∧i60[2]=i60[3] ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

    (9)    (>(i99[2], 0)=TRUE ⇒ LOAD702(i60[2], i99[2])≥NonInfC∧LOAD702(i60[2], i99[2])≥COND_LOAD702(>(i99[2], 0), i60[2], i99[2])∧(UIncreasing(COND_LOAD702(>(i99[2], 0), i60[2], i99[2])), ≥))



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

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



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

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



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

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



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

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



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

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







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

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




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

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(COND_LOAD702(x1, x2, x3)) = [-1] + x3   
POL(LOAD702(x1, x2)) = [-1] + x2   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   

The following pairs are in P>:

COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1))

The following pairs are in Pbound:

COND_LOAD702(TRUE, i60[3], i99[3]) → LOAD702(i60[3], +(i99[3], -1))
LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2])

The following pairs are in P≥:

LOAD702(i60[2], i99[2]) → COND_LOAD702(>(i99[2], 0), i60[2], i99[2])

There are no usable rules.

(30) Complex Obligation (AND)

(31) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD702(i60[2], i99[2]) → COND_LOAD702(i99[2] > 0, i60[2], i99[2])


The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(32) IDependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

(34) Obligation:

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


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load425(x0, x1)
Cond_Load425(TRUE, x0, x1)
Load702(x0, x1)
Cond_Load702(TRUE, x0, x1)
Cond_Load4251(TRUE, x0, x1)
Load719(x0, x1)
Cond_Load719(TRUE, x0, x1)

(35) IDependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE