Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 DuplicateArgsRemoverProof (⇔)
↳6 ITRS
↳7 ITRStoIDPProof (⇔)
↳8 IDP
↳9 UsableRulesProof (⇔)
↳10 IDP
↳11 IDPNonInfProof (⇐)
↳12 AND
    ↳13 IDP
        ↳14 IDependencyGraphProof (⇔)
        ↳15 IDP
        ↳16 IDPNonInfProof (⇐)
        ↳17 AND
            ↳18 IDP
                ↳19 IDependencyGraphProof (⇔)
                ↳20 TRUE
            ↳21 IDP
                ↳22 IDependencyGraphProof (⇔)
                ↳23 TRUE
    ↳24 IDP
        ↳25 IDependencyGraphProof (⇔)
        ↳26 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: GCD3

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 199 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:
Load839(i76, i72) → Cond_Load839(i76 > 0 && i72 > 0, i76, i72)
Cond_Load839(TRUE, i76, i72) → Load959(i76, i72, i72, i76, i72, i76, i72)
Load959(i76, i72, i72, i76, i72, i82, i72) → Cond_Load959(i72 > 0 && i82 >= i72, i76, i72, i72, i76, i72, i82, i72)
Cond_Load959(TRUE, i76, i72, i72, i76, i72, i82, i72) → Load959(i76, i72, i72, i76, i72, i82 - i72, i72)
Load959(i76, i72, i72, i76, i72, i82, i72) → Cond_Load9591(i82 < i72, i76, i72, i72, i76, i72, i82, i72)
Cond_Load9591(TRUE, i76, i72, i72, i76, i72, i82, i72) → Load839(i72, i82)
The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x1, x0, x1, x2, x1)
Cond_Load959(TRUE, x0, x1, x1, x0, x1, x2, x1)
Cond_Load9591(TRUE, x0, x1, x1, x0, x1, x2, x1)

(5) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Cond_Load9591(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load9591(x1, x5, x7, x8)
Load959(x1, x2, x3, x4, x5, x6, x7) → Load959(x4, x6, x7)
Cond_Load959(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load959(x1, x5, x7, x8)

(6) 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:
Load839(i76, i72) → Cond_Load839(i76 > 0 && i72 > 0, i76, i72)
Cond_Load839(TRUE, i76, i72) → Load959(i76, i76, i72)
Load959(i76, i82, i72) → Cond_Load959(i72 > 0 && i82 >= i72, i76, i82, i72)
Cond_Load959(TRUE, i76, i82, i72) → Load959(i76, i82 - i72, i72)
Load959(i76, i82, i72) → Cond_Load9591(i82 < i72, i76, i82, i72)
Cond_Load9591(TRUE, i76, i82, i72) → Load839(i72, i82)
The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(7) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(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


The ITRS R consists of the following rules:
Load839(i76, i72) → Cond_Load839(i76 > 0 && i72 > 0, i76, i72)
Cond_Load839(TRUE, i76, i72) → Load959(i76, i76, i72)
Load959(i76, i82, i72) → Cond_Load959(i72 > 0 && i82 >= i72, i76, i82, i72)
Cond_Load959(TRUE, i76, i82, i72) → Load959(i76, i82 - i72, i72)
Load959(i76, i82, i72) → Cond_Load9591(i82 < i72, i76, i82, i72)
Cond_Load9591(TRUE, i76, i82, i72) → Load839(i72, i82)

The integer pair graph contains the following rules and edges:
(0): LOAD839(i76[0], i72[0]) → COND_LOAD839(i76[0] > 0 && i72[0] > 0, i76[0], i72[0])
(1): COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1])
(2): LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(i72[2] > 0 && i82[2] >= i72[2], i76[2], i82[2], i72[2])
(3): COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], i82[3] - i72[3], i72[3])
(4): LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(i82[4] < i72[4], i76[4], i82[4], i72[4])
(5): COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5])

(0) -> (1), if ((i76[0] > 0 && i72[0] > 0 →* TRUE)∧(i72[0] →* i72[1])∧(i76[0] →* i76[1]))


(1) -> (2), if ((i72[1] →* i72[2])∧(i76[1] →* i82[2])∧(i76[1] →* i76[2]))


(1) -> (4), if ((i76[1] →* i82[4])∧(i76[1] →* i76[4])∧(i72[1] →* i72[4]))


(2) -> (3), if ((i72[2] →* i72[3])∧(i72[2] > 0 && i82[2] >= i72[2] →* TRUE)∧(i82[2] →* i82[3])∧(i76[2] →* i76[3]))


(3) -> (2), if ((i72[3] →* i72[2])∧(i82[3] - i72[3] →* i82[2])∧(i76[3] →* i76[2]))


(3) -> (4), if ((i76[3] →* i76[4])∧(i72[3] →* i72[4])∧(i82[3] - i72[3] →* i82[4]))


(4) -> (5), if ((i76[4] →* i76[5])∧(i72[4] →* i72[5])∧(i82[4] < i72[4] →* TRUE)∧(i82[4] →* i82[5]))


(5) -> (0), if ((i72[5] →* i76[0])∧(i82[5] →* i72[0]))



The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

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

(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): LOAD839(i76[0], i72[0]) → COND_LOAD839(i76[0] > 0 && i72[0] > 0, i76[0], i72[0])
(1): COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1])
(2): LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(i72[2] > 0 && i82[2] >= i72[2], i76[2], i82[2], i72[2])
(3): COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], i82[3] - i72[3], i72[3])
(4): LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(i82[4] < i72[4], i76[4], i82[4], i72[4])
(5): COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5])

(0) -> (1), if ((i76[0] > 0 && i72[0] > 0 →* TRUE)∧(i72[0] →* i72[1])∧(i76[0] →* i76[1]))


(1) -> (2), if ((i72[1] →* i72[2])∧(i76[1] →* i82[2])∧(i76[1] →* i76[2]))


(1) -> (4), if ((i76[1] →* i82[4])∧(i76[1] →* i76[4])∧(i72[1] →* i72[4]))


(2) -> (3), if ((i72[2] →* i72[3])∧(i72[2] > 0 && i82[2] >= i72[2] →* TRUE)∧(i82[2] →* i82[3])∧(i76[2] →* i76[3]))


(3) -> (2), if ((i72[3] →* i72[2])∧(i82[3] - i72[3] →* i82[2])∧(i76[3] →* i76[2]))


(3) -> (4), if ((i76[3] →* i76[4])∧(i72[3] →* i72[4])∧(i82[3] - i72[3] →* i82[4]))


(4) -> (5), if ((i76[4] →* i76[5])∧(i72[4] →* i72[5])∧(i82[4] < i72[4] →* TRUE)∧(i82[4] →* i82[5]))


(5) -> (0), if ((i72[5] →* i76[0])∧(i82[5] →* i72[0]))



The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(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 LOAD839(i76, i72) → COND_LOAD839(&&(>(i76, 0), >(i72, 0)), i76, i72) the following chains were created:
  • We consider the chain LOAD839(i76[0], i72[0]) → COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0]), COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1]) which results in the following constraint:

    (1)    (&&(>(i76[0], 0), >(i72[0], 0))=TRUE∧i72[0]=i72[1]∧i76[0]=i76[1] ⇒ LOAD839(i76[0], i72[0])≥NonInfC∧LOAD839(i76[0], i72[0])≥COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])∧(UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥))



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

    (2)    (>(i76[0], 0)=TRUE∧>(i72[0], 0)=TRUE ⇒ LOAD839(i76[0], i72[0])≥NonInfC∧LOAD839(i76[0], i72[0])≥COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])∧(UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥))



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

    (3)    (i76[0] + [-1] ≥ 0∧i72[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i72[0] ≥ 0∧[(-1)bso_29] ≥ 0)



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

    (4)    (i76[0] + [-1] ≥ 0∧i72[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i72[0] ≥ 0∧[(-1)bso_29] ≥ 0)



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

    (5)    (i76[0] + [-1] ≥ 0∧i72[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i72[0] ≥ 0∧[(-1)bso_29] ≥ 0)



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

    (6)    (i76[0] ≥ 0∧i72[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i72[0] ≥ 0∧[(-1)bso_29] ≥ 0)



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

    (7)    (i76[0] ≥ 0∧i72[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥)∧[(-1)Bound*bni_28 + bni_28] + [bni_28]i72[0] ≥ 0∧[(-1)bso_29] ≥ 0)







For Pair COND_LOAD839(TRUE, i76, i72) → LOAD959(i76, i76, i72) the following chains were created:
  • We consider the chain COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1]), LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]) which results in the following constraint:

    (8)    (i72[1]=i72[2]∧i76[1]=i82[2]∧i76[1]=i76[2] ⇒ COND_LOAD839(TRUE, i76[1], i72[1])≥NonInfC∧COND_LOAD839(TRUE, i76[1], i72[1])≥LOAD959(i76[1], i76[1], i72[1])∧(UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥))



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

    (9)    (COND_LOAD839(TRUE, i76[1], i72[1])≥NonInfC∧COND_LOAD839(TRUE, i76[1], i72[1])≥LOAD959(i76[1], i76[1], i72[1])∧(UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥))



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

    (10)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧[(-1)bso_31] ≥ 0)



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

    (11)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧[(-1)bso_31] ≥ 0)



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

    (12)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧[(-1)bso_31] ≥ 0)



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

    (13)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)



  • We consider the chain COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1]), LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4]) which results in the following constraint:

    (14)    (i76[1]=i82[4]∧i76[1]=i76[4]∧i72[1]=i72[4] ⇒ COND_LOAD839(TRUE, i76[1], i72[1])≥NonInfC∧COND_LOAD839(TRUE, i76[1], i72[1])≥LOAD959(i76[1], i76[1], i72[1])∧(UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥))



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

    (15)    (COND_LOAD839(TRUE, i76[1], i72[1])≥NonInfC∧COND_LOAD839(TRUE, i76[1], i72[1])≥LOAD959(i76[1], i76[1], i72[1])∧(UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥))



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

    (16)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧[(-1)bso_31] ≥ 0)



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

    (17)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧[(-1)bso_31] ≥ 0)



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

    (18)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧[(-1)bso_31] ≥ 0)



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

    (19)    ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)







For Pair LOAD959(i76, i82, i72) → COND_LOAD959(&&(>(i72, 0), >=(i82, i72)), i76, i82, i72) the following chains were created:
  • We consider the chain LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]), COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3]) which results in the following constraint:

    (20)    (i72[2]=i72[3]∧&&(>(i72[2], 0), >=(i82[2], i72[2]))=TRUE∧i82[2]=i82[3]∧i76[2]=i76[3] ⇒ LOAD959(i76[2], i82[2], i72[2])≥NonInfC∧LOAD959(i76[2], i82[2], i72[2])≥COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])∧(UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥))



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

    (21)    (>(i72[2], 0)=TRUE∧>=(i82[2], i72[2])=TRUE ⇒ LOAD959(i76[2], i82[2], i72[2])≥NonInfC∧LOAD959(i76[2], i82[2], i72[2])≥COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])∧(UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥))



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

    (22)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧[(-1)Bound*bni_32] + [bni_32]i72[2] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (23)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧[(-1)Bound*bni_32] + [bni_32]i72[2] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (24)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧[(-1)Bound*bni_32] + [bni_32]i72[2] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (25)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)Bound*bni_32] + [bni_32]i72[2] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)



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

    (26)    (i72[2] ≥ 0∧i82[2] + [-1] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + bni_32] + [bni_32]i72[2] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)



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

    (27)    (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + bni_32] + [bni_32]i72[2] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)







For Pair COND_LOAD959(TRUE, i76, i82, i72) → LOAD959(i76, -(i82, i72), i72) the following chains were created:
  • We consider the chain LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]), COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3]), LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]) which results in the following constraint:

    (28)    (i72[2]=i72[3]∧&&(>(i72[2], 0), >=(i82[2], i72[2]))=TRUE∧i82[2]=i82[3]∧i76[2]=i76[3]∧i72[3]=i72[2]1∧-(i82[3], i72[3])=i82[2]1∧i76[3]=i76[2]1 ⇒ COND_LOAD959(TRUE, i76[3], i82[3], i72[3])≥NonInfC∧COND_LOAD959(TRUE, i76[3], i82[3], i72[3])≥LOAD959(i76[3], -(i82[3], i72[3]), i72[3])∧(UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥))



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

    (29)    (>(i72[2], 0)=TRUE∧>=(i82[2], i72[2])=TRUE ⇒ COND_LOAD959(TRUE, i76[2], i82[2], i72[2])≥NonInfC∧COND_LOAD959(TRUE, i76[2], i82[2], i72[2])≥LOAD959(i76[2], -(i82[2], i72[2]), i72[2])∧(UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥))



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

    (30)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (31)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (32)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (33)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)



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

    (34)    (i72[2] ≥ 0∧i82[2] + [-1] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34 + bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)



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

    (35)    (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34 + bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)



  • We consider the chain LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]), COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3]), LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4]) which results in the following constraint:

    (36)    (i72[2]=i72[3]∧&&(>(i72[2], 0), >=(i82[2], i72[2]))=TRUE∧i82[2]=i82[3]∧i76[2]=i76[3]∧i76[3]=i76[4]∧i72[3]=i72[4]∧-(i82[3], i72[3])=i82[4] ⇒ COND_LOAD959(TRUE, i76[3], i82[3], i72[3])≥NonInfC∧COND_LOAD959(TRUE, i76[3], i82[3], i72[3])≥LOAD959(i76[3], -(i82[3], i72[3]), i72[3])∧(UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥))



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

    (37)    (>(i72[2], 0)=TRUE∧>=(i82[2], i72[2])=TRUE ⇒ COND_LOAD959(TRUE, i76[2], i82[2], i72[2])≥NonInfC∧COND_LOAD959(TRUE, i76[2], i82[2], i72[2])≥LOAD959(i76[2], -(i82[2], i72[2]), i72[2])∧(UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥))



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

    (38)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (39)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (40)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (41)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)



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

    (42)    (i72[2] ≥ 0∧i82[2] + [-1] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34 + bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)



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

    (43)    (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34 + bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)







For Pair LOAD959(i76, i82, i72) → COND_LOAD9591(<(i82, i72), i76, i82, i72) the following chains were created:
  • We consider the chain LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4]), COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5]) which results in the following constraint:

    (44)    (i76[4]=i76[5]∧i72[4]=i72[5]∧<(i82[4], i72[4])=TRUE∧i82[4]=i82[5] ⇒ LOAD959(i76[4], i82[4], i72[4])≥NonInfC∧LOAD959(i76[4], i82[4], i72[4])≥COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])∧(UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥))



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

    (45)    (<(i82[4], i72[4])=TRUE ⇒ LOAD959(i76[4], i82[4], i72[4])≥NonInfC∧LOAD959(i76[4], i82[4], i72[4])≥COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])∧(UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥))



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

    (46)    (i72[4] + [-1] + [-1]i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]i72[4] ≥ 0∧[(-1)bso_37] + i72[4] + [-1]i82[4] ≥ 0)



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

    (47)    (i72[4] + [-1] + [-1]i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]i72[4] ≥ 0∧[(-1)bso_37] + i72[4] + [-1]i82[4] ≥ 0)



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

    (48)    (i72[4] + [-1] + [-1]i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]i72[4] ≥ 0∧[(-1)bso_37] + i72[4] + [-1]i82[4] ≥ 0)



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

    (49)    (i72[4] + [-1] + [-1]i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧0 = 0∧[(-1)Bound*bni_36] + [bni_36]i72[4] ≥ 0∧0 = 0∧[(-1)bso_37] + i72[4] + [-1]i82[4] ≥ 0)



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

    (50)    (i72[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧0 = 0∧[(-1)Bound*bni_36 + bni_36] + [bni_36]i82[4] + [bni_36]i72[4] ≥ 0∧0 = 0∧[1 + (-1)bso_37] + i72[4] ≥ 0)



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

    (51)    (i72[4] ≥ 0∧i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧0 = 0∧[(-1)Bound*bni_36 + bni_36] + [(-1)bni_36]i82[4] + [bni_36]i72[4] ≥ 0∧0 = 0∧[1 + (-1)bso_37] + i72[4] ≥ 0)


    (52)    (i72[4] ≥ 0∧i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧0 = 0∧[(-1)Bound*bni_36 + bni_36] + [bni_36]i82[4] + [bni_36]i72[4] ≥ 0∧0 = 0∧[1 + (-1)bso_37] + i72[4] ≥ 0)







For Pair COND_LOAD9591(TRUE, i76, i82, i72) → LOAD839(i72, i82) the following chains were created:
  • We consider the chain COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5]), LOAD839(i76[0], i72[0]) → COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0]) which results in the following constraint:

    (53)    (i72[5]=i76[0]∧i82[5]=i72[0] ⇒ COND_LOAD9591(TRUE, i76[5], i82[5], i72[5])≥NonInfC∧COND_LOAD9591(TRUE, i76[5], i82[5], i72[5])≥LOAD839(i72[5], i82[5])∧(UIncreasing(LOAD839(i72[5], i82[5])), ≥))



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

    (54)    (COND_LOAD9591(TRUE, i76[5], i82[5], i72[5])≥NonInfC∧COND_LOAD9591(TRUE, i76[5], i82[5], i72[5])≥LOAD839(i72[5], i82[5])∧(UIncreasing(LOAD839(i72[5], i82[5])), ≥))



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

    (55)    ((UIncreasing(LOAD839(i72[5], i82[5])), ≥)∧[(-1)bso_39] ≥ 0)



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

    (56)    ((UIncreasing(LOAD839(i72[5], i82[5])), ≥)∧[(-1)bso_39] ≥ 0)



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

    (57)    ((UIncreasing(LOAD839(i72[5], i82[5])), ≥)∧[(-1)bso_39] ≥ 0)



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

    (58)    ((UIncreasing(LOAD839(i72[5], i82[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD839(i76, i72) → COND_LOAD839(&&(>(i76, 0), >(i72, 0)), i76, i72)
    • (i76[0] ≥ 0∧i72[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])), ≥)∧[(-1)Bound*bni_28 + bni_28] + [bni_28]i72[0] ≥ 0∧[(-1)bso_29] ≥ 0)

  • COND_LOAD839(TRUE, i76, i72) → LOAD959(i76, i76, i72)
    • ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    • ((UIncreasing(LOAD959(i76[1], i76[1], i72[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  • LOAD959(i76, i82, i72) → COND_LOAD959(&&(>(i72, 0), >=(i82, i72)), i76, i82, i72)
    • (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + bni_32] + [bni_32]i72[2] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)

  • COND_LOAD959(TRUE, i76, i82, i72) → LOAD959(i76, -(i82, i72), i72)
    • (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34 + bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    • (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)Bound*bni_34 + bni_34] + [bni_34]i72[2] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  • LOAD959(i76, i82, i72) → COND_LOAD9591(<(i82, i72), i76, i82, i72)
    • (i72[4] ≥ 0∧i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧0 = 0∧[(-1)Bound*bni_36 + bni_36] + [(-1)bni_36]i82[4] + [bni_36]i72[4] ≥ 0∧0 = 0∧[1 + (-1)bso_37] + i72[4] ≥ 0)
    • (i72[4] ≥ 0∧i82[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])), ≥)∧0 = 0∧[(-1)Bound*bni_36 + bni_36] + [bni_36]i82[4] + [bni_36]i72[4] ≥ 0∧0 = 0∧[1 + (-1)bso_37] + i72[4] ≥ 0)

  • COND_LOAD9591(TRUE, i76, i82, i72) → LOAD839(i72, i82)
    • ((UIncreasing(LOAD839(i72[5], i82[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 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) = [1]   
POL(FALSE) = [3]   
POL(LOAD839(x1, x2)) = x2   
POL(COND_LOAD839(x1, x2, x3)) = [1] + x3 + [-1]x1   
POL(&&(x1, x2)) = [1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(LOAD959(x1, x2, x3)) = x3   
POL(COND_LOAD959(x1, x2, x3, x4)) = x4   
POL(>=(x1, x2)) = [-1]   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(COND_LOAD9591(x1, x2, x3, x4)) = x3   
POL(<(x1, x2)) = [-1]   

The following pairs are in P>:

LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(<(i82[4], i72[4]), i76[4], i82[4], i72[4])

The following pairs are in Pbound:

LOAD839(i76[0], i72[0]) → COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])
LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])
COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3])

The following pairs are in P≥:

LOAD839(i76[0], i72[0]) → COND_LOAD839(&&(>(i76[0], 0), >(i72[0], 0)), i76[0], i72[0])
COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1])
LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])
COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3])
COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5])

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

(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): LOAD839(i76[0], i72[0]) → COND_LOAD839(i76[0] > 0 && i72[0] > 0, i76[0], i72[0])
(1): COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1])
(2): LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(i72[2] > 0 && i82[2] >= i72[2], i76[2], i82[2], i72[2])
(3): COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], i82[3] - i72[3], i72[3])
(5): COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5])

(5) -> (0), if ((i72[5] →* i76[0])∧(i82[5] →* i72[0]))


(0) -> (1), if ((i76[0] > 0 && i72[0] > 0 →* TRUE)∧(i72[0] →* i72[1])∧(i76[0] →* i76[1]))


(1) -> (2), if ((i72[1] →* i72[2])∧(i76[1] →* i82[2])∧(i76[1] →* i76[2]))


(3) -> (2), if ((i72[3] →* i72[2])∧(i82[3] - i72[3] →* i82[2])∧(i76[3] →* i76[2]))


(2) -> (3), if ((i72[2] →* i72[3])∧(i72[2] > 0 && i82[2] >= i72[2] →* TRUE)∧(i82[2] →* i82[3])∧(i76[2] →* i76[3]))



The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 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:
(3): COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], i82[3] - i72[3], i72[3])
(2): LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(i72[2] > 0 && i82[2] >= i72[2], i76[2], i82[2], i72[2])

(3) -> (2), if ((i72[3] →* i72[2])∧(i82[3] - i72[3] →* i82[2])∧(i76[3] →* i76[2]))


(2) -> (3), if ((i72[2] →* i72[3])∧(i72[2] > 0 && i82[2] >= i72[2] →* TRUE)∧(i82[2] →* i82[3])∧(i76[2] →* i76[3]))



The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(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_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3]) the following chains were created:
  • We consider the chain LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]), COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3]), LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]) which results in the following constraint:

    (1)    (i72[2]=i72[3]∧&&(>(i72[2], 0), >=(i82[2], i72[2]))=TRUE∧i82[2]=i82[3]∧i76[2]=i76[3]∧i72[3]=i72[2]1∧-(i82[3], i72[3])=i82[2]1∧i76[3]=i76[2]1 ⇒ COND_LOAD959(TRUE, i76[3], i82[3], i72[3])≥NonInfC∧COND_LOAD959(TRUE, i76[3], i82[3], i72[3])≥LOAD959(i76[3], -(i82[3], i72[3]), i72[3])∧(UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥))



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

    (2)    (>(i72[2], 0)=TRUE∧>=(i82[2], i72[2])=TRUE ⇒ COND_LOAD959(TRUE, i76[2], i82[2], i72[2])≥NonInfC∧COND_LOAD959(TRUE, i76[2], i82[2], i72[2])≥LOAD959(i76[2], -(i82[2], i72[2]), i72[2])∧(UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥))



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

    (3)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]i72[2] + [bni_15]i82[2] ≥ 0∧[(-1)bso_16] + i72[2] ≥ 0)



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

    (4)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]i72[2] + [bni_15]i82[2] ≥ 0∧[(-1)bso_16] + i72[2] ≥ 0)



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

    (5)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]i72[2] + [bni_15]i82[2] ≥ 0∧[(-1)bso_16] + i72[2] ≥ 0)



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

    (6)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]i72[2] + [bni_15]i82[2] ≥ 0∧0 = 0∧[(-1)bso_16] + i72[2] ≥ 0)



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

    (7)    (i72[2] ≥ 0∧i82[2] + [-1] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-2)bni_15 + (-1)Bound*bni_15] + [(-1)bni_15]i72[2] + [bni_15]i82[2] ≥ 0∧0 = 0∧[1 + (-1)bso_16] + i72[2] ≥ 0)



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

    (8)    (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]i82[2] ≥ 0∧0 = 0∧[1 + (-1)bso_16] + i72[2] ≥ 0)







For Pair LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]) the following chains were created:
  • We consider the chain LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2]), COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3]) which results in the following constraint:

    (9)    (i72[2]=i72[3]∧&&(>(i72[2], 0), >=(i82[2], i72[2]))=TRUE∧i82[2]=i82[3]∧i76[2]=i76[3] ⇒ LOAD959(i76[2], i82[2], i72[2])≥NonInfC∧LOAD959(i76[2], i82[2], i72[2])≥COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])∧(UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥))



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

    (10)    (>(i72[2], 0)=TRUE∧>=(i82[2], i72[2])=TRUE ⇒ LOAD959(i76[2], i82[2], i72[2])≥NonInfC∧LOAD959(i76[2], i82[2], i72[2])≥COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])∧(UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥))



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

    (11)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]i72[2] + [bni_17]i82[2] ≥ 0∧[(-1)bso_18] ≥ 0)



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

    (12)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]i72[2] + [bni_17]i82[2] ≥ 0∧[(-1)bso_18] ≥ 0)



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

    (13)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]i72[2] + [bni_17]i82[2] ≥ 0∧[(-1)bso_18] ≥ 0)



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

    (14)    (i72[2] + [-1] ≥ 0∧i82[2] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]i72[2] + [bni_17]i82[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)



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

    (15)    (i72[2] ≥ 0∧i82[2] + [-1] + [-1]i72[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-2)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]i72[2] + [bni_17]i82[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)



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

    (16)    (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]i82[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3])
    • (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(LOAD959(i76[3], -(i82[3], i72[3]), i72[3])), ≥)∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]i82[2] ≥ 0∧0 = 0∧[1 + (-1)bso_16] + i72[2] ≥ 0)

  • LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])
    • (i72[2] ≥ 0∧i82[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])), ≥)∧0 = 0∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]i82[2] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 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_LOAD959(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [-1]x1   
POL(LOAD959(x1, x2, x3)) = [-1] + [-1]x3 + x2   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(&&(x1, x2)) = 0   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(>=(x1, x2)) = [-1]   

The following pairs are in P>:

COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3])

The following pairs are in Pbound:

COND_LOAD959(TRUE, i76[3], i82[3], i72[3]) → LOAD959(i76[3], -(i82[3], i72[3]), i72[3])
LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])

The following pairs are in P≥:

LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(&&(>(i72[2], 0), >=(i82[2], i72[2])), i76[2], i82[2], i72[2])

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

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

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

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD959(i76[2], i82[2], i72[2]) → COND_LOAD959(i72[2] > 0 && i82[2] >= i72[2], i76[2], i82[2], i72[2])


The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(19) IDependencyGraphProof (EQUIVALENT transformation)

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

(20) TRUE

(21) 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:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(22) IDependencyGraphProof (EQUIVALENT transformation)

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

(23) TRUE

(24) Obligation:

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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LOAD839(TRUE, i76[1], i72[1]) → LOAD959(i76[1], i76[1], i72[1])
(4): LOAD959(i76[4], i82[4], i72[4]) → COND_LOAD9591(i82[4] < i72[4], i76[4], i82[4], i72[4])
(5): COND_LOAD9591(TRUE, i76[5], i82[5], i72[5]) → LOAD839(i72[5], i82[5])

(1) -> (4), if ((i76[1] →* i82[4])∧(i76[1] →* i76[4])∧(i72[1] →* i72[4]))


(4) -> (5), if ((i76[4] →* i76[5])∧(i72[4] →* i72[5])∧(i82[4] < i72[4] →* TRUE)∧(i82[4] →* i82[5]))



The set Q consists of the following terms:
Load839(x0, x1)
Cond_Load839(TRUE, x0, x1)
Load959(x0, x1, x2)
Cond_Load959(TRUE, x0, x1, x2)
Cond_Load9591(TRUE, x0, x1, x2)

(25) IDependencyGraphProof (EQUIVALENT transformation)

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

(26) TRUE