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 AND
↳16 IDP
↳17 IDependencyGraphProof (⇔)
↳18 IDP
↳19 IDPNonInfProof (⇐)
↳20 AND
↳21 IDP
↳22 IDependencyGraphProof (⇔)
↳23 TRUE
↳24 IDP
↳25 IDependencyGraphProof (⇔)
↳26 TRUE
↳27 IDP
↳28 IDependencyGraphProof (⇔)
↳29 TRUE
↳30 IDP
↳31 IDependencyGraphProof (⇔)
↳32 IDP
↳33 IDPNonInfProof (⇐)
↳34 AND
↳35 IDP
↳36 IDependencyGraphProof (⇔)
↳37 IDP
↳38 IDPNonInfProof (⇐)
↳39 AND
↳40 IDP
↳41 IDependencyGraphProof (⇔)
↳42 TRUE
↳43 IDP
↳44 IDependencyGraphProof (⇔)
↳45 TRUE
↳46 IDP
↳47 IDependencyGraphProof (⇔)
↳48 TRUE
/**
* Example taken from "A Term Rewriting Approach to the Automated Termination
* Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
* and converted to Java.
*/
public class PastaB13 {
public static void main(String[] args) {
Random.args = args;
int x = Random.random();
int y = Random.random();
int z = Random.random();
while (x > z || y > z) {
if (x > z) {
x--;
} else if (y > z) {
y--;
} else {
continue;
}
}
}
}
public class Random {
static String[] args;
static int index = 0;
public static int random() {
String string = args[index];
index++;
return string.length();
}
}
!= | ~ | 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 |
!= | ~ | 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 |
Boolean, Integer
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
(1) -> (10), if ((i29[1] →* i29[10])∧(i14[1] →* i14[10])∧(i59[1] →* i59[10]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(3) -> (4), if ((i14[3] →* i14[4])∧(i29[3] →* i29[4])∧(i59[3] →* i59[4]))
(3) -> (8), if ((i14[3] →* i14[8])∧(i29[3] →* i29[8])∧(i59[3] →* i59[8]))
(3) -> (12), if ((i29[3] →* i29[12])∧(i14[3] →* i14[12])∧(i59[3] →* i59[12]))
(4) -> (5), if ((i29[4] →* i29[5])∧(i29[4] <= i59[4] && i14[4] <= i59[4] && i14[4] > i59[4] →* TRUE)∧(i59[4] →* i59[5])∧(i14[4] →* i14[5]))
(5) -> (0), if ((i59[5] →* i59[0])∧(i14[5] →* i14[0])∧(i29[5] →* i29[0]))
(5) -> (4), if ((i29[5] →* i29[4])∧(i14[5] →* i14[4])∧(i59[5] →* i59[4]))
(5) -> (8), if ((i14[5] →* i14[8])∧(i29[5] →* i29[8])∧(i59[5] →* i59[8]))
(5) -> (12), if ((i29[5] →* i29[12])∧(i59[5] →* i59[12])∧(i14[5] →* i14[12]))
(6) -> (7), if ((i59[6] →* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6] →* TRUE)∧(i29[6] →* i29[7])∧(i14[6] →* i14[7]))
(7) -> (0), if ((i59[7] →* i59[0])∧(i29[7] + -1 →* i29[0])∧(i14[7] →* i14[0]))
(7) -> (4), if ((i59[7] →* i59[4])∧(i29[7] + -1 →* i29[4])∧(i14[7] →* i14[4]))
(7) -> (8), if ((i14[7] →* i14[8])∧(i59[7] →* i59[8])∧(i29[7] + -1 →* i29[8]))
(7) -> (12), if ((i29[7] + -1 →* i29[12])∧(i14[7] →* i14[12])∧(i59[7] →* i59[12]))
(8) -> (9), if ((i29[8] →* i29[9])∧(i14[8] →* i14[9])∧(i29[8] > i59[8] && i14[8] <= i59[8] && i14[8] > i59[8] →* TRUE)∧(i59[8] →* i59[9]))
(9) -> (0), if ((i59[9] →* i59[0])∧(i29[9] + -1 →* i29[0])∧(i14[9] →* i14[0]))
(9) -> (4), if ((i14[9] →* i14[4])∧(i29[9] + -1 →* i29[4])∧(i59[9] →* i59[4]))
(9) -> (8), if ((i29[9] + -1 →* i29[8])∧(i14[9] →* i14[8])∧(i59[9] →* i59[8]))
(9) -> (12), if ((i59[9] →* i59[12])∧(i14[9] →* i14[12])∧(i29[9] + -1 →* i29[12]))
(10) -> (11), if ((i14[10] →* i14[11])∧(i14[10] > i59[10] →* TRUE)∧(i59[10] →* i59[11])∧(i29[10] →* i29[11]))
(11) -> (0), if ((i29[11] →* i29[0])∧(i14[11] + -1 →* i14[0])∧(i59[11] →* i59[0]))
(11) -> (4), if ((i59[11] →* i59[4])∧(i29[11] →* i29[4])∧(i14[11] + -1 →* i14[4]))
(11) -> (8), if ((i29[11] →* i29[8])∧(i14[11] + -1 →* i14[8])∧(i59[11] →* i59[8]))
(11) -> (12), if ((i59[11] →* i59[12])∧(i14[11] + -1 →* i14[12])∧(i29[11] →* i29[12]))
(12) -> (13), if ((i14[12] > i59[12] →* TRUE)∧(i59[12] →* i59[13])∧(i29[12] →* i29[13])∧(i14[12] →* i14[13]))
(13) -> (0), if ((i59[13] →* i59[0])∧(i29[13] →* i29[0])∧(i14[13] + -1 →* i14[0]))
(13) -> (4), if ((i29[13] →* i29[4])∧(i59[13] →* i59[4])∧(i14[13] + -1 →* i14[4]))
(13) -> (8), if ((i14[13] + -1 →* i14[8])∧(i29[13] →* i29[8])∧(i59[13] →* i59[8]))
(13) -> (12), if ((i59[13] →* i59[12])∧(i14[13] + -1 →* i14[12])∧(i29[13] →* i29[12]))
!= | ~ | 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 |
Boolean, Integer
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
(1) -> (10), if ((i29[1] →* i29[10])∧(i14[1] →* i14[10])∧(i59[1] →* i59[10]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(3) -> (4), if ((i14[3] →* i14[4])∧(i29[3] →* i29[4])∧(i59[3] →* i59[4]))
(3) -> (8), if ((i14[3] →* i14[8])∧(i29[3] →* i29[8])∧(i59[3] →* i59[8]))
(3) -> (12), if ((i29[3] →* i29[12])∧(i14[3] →* i14[12])∧(i59[3] →* i59[12]))
(4) -> (5), if ((i29[4] →* i29[5])∧(i29[4] <= i59[4] && i14[4] <= i59[4] && i14[4] > i59[4] →* TRUE)∧(i59[4] →* i59[5])∧(i14[4] →* i14[5]))
(5) -> (0), if ((i59[5] →* i59[0])∧(i14[5] →* i14[0])∧(i29[5] →* i29[0]))
(5) -> (4), if ((i29[5] →* i29[4])∧(i14[5] →* i14[4])∧(i59[5] →* i59[4]))
(5) -> (8), if ((i14[5] →* i14[8])∧(i29[5] →* i29[8])∧(i59[5] →* i59[8]))
(5) -> (12), if ((i29[5] →* i29[12])∧(i59[5] →* i59[12])∧(i14[5] →* i14[12]))
(6) -> (7), if ((i59[6] →* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6] →* TRUE)∧(i29[6] →* i29[7])∧(i14[6] →* i14[7]))
(7) -> (0), if ((i59[7] →* i59[0])∧(i29[7] + -1 →* i29[0])∧(i14[7] →* i14[0]))
(7) -> (4), if ((i59[7] →* i59[4])∧(i29[7] + -1 →* i29[4])∧(i14[7] →* i14[4]))
(7) -> (8), if ((i14[7] →* i14[8])∧(i59[7] →* i59[8])∧(i29[7] + -1 →* i29[8]))
(7) -> (12), if ((i29[7] + -1 →* i29[12])∧(i14[7] →* i14[12])∧(i59[7] →* i59[12]))
(8) -> (9), if ((i29[8] →* i29[9])∧(i14[8] →* i14[9])∧(i29[8] > i59[8] && i14[8] <= i59[8] && i14[8] > i59[8] →* TRUE)∧(i59[8] →* i59[9]))
(9) -> (0), if ((i59[9] →* i59[0])∧(i29[9] + -1 →* i29[0])∧(i14[9] →* i14[0]))
(9) -> (4), if ((i14[9] →* i14[4])∧(i29[9] + -1 →* i29[4])∧(i59[9] →* i59[4]))
(9) -> (8), if ((i29[9] + -1 →* i29[8])∧(i14[9] →* i14[8])∧(i59[9] →* i59[8]))
(9) -> (12), if ((i59[9] →* i59[12])∧(i14[9] →* i14[12])∧(i29[9] + -1 →* i29[12]))
(10) -> (11), if ((i14[10] →* i14[11])∧(i14[10] > i59[10] →* TRUE)∧(i59[10] →* i59[11])∧(i29[10] →* i29[11]))
(11) -> (0), if ((i29[11] →* i29[0])∧(i14[11] + -1 →* i14[0])∧(i59[11] →* i59[0]))
(11) -> (4), if ((i59[11] →* i59[4])∧(i29[11] →* i29[4])∧(i14[11] + -1 →* i14[4]))
(11) -> (8), if ((i29[11] →* i29[8])∧(i14[11] + -1 →* i14[8])∧(i59[11] →* i59[8]))
(11) -> (12), if ((i59[11] →* i59[12])∧(i14[11] + -1 →* i14[12])∧(i29[11] →* i29[12]))
(12) -> (13), if ((i14[12] > i59[12] →* TRUE)∧(i59[12] →* i59[13])∧(i29[12] →* i29[13])∧(i14[12] →* i14[13]))
(13) -> (0), if ((i59[13] →* i59[0])∧(i29[13] →* i29[0])∧(i14[13] + -1 →* i14[0]))
(13) -> (4), if ((i29[13] →* i29[4])∧(i59[13] →* i59[4])∧(i14[13] + -1 →* i14[4]))
(13) -> (8), if ((i14[13] + -1 →* i14[8])∧(i29[13] →* i29[8])∧(i59[13] →* i59[8]))
(13) -> (12), if ((i59[13] →* i59[12])∧(i14[13] + -1 →* i14[12])∧(i29[13] →* i29[12]))
(1) (i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1] ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(2) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(3) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(4) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(5) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(6) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(7) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(8) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(9) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(10) (i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(11) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(12) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(13) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(14) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(15) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(16) (i14[1]=i14[6]∧i59[1]=i59[6]∧i29[1]=i29[6] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(17) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(18) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(19) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(20) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(21) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(22) (i29[1]=i29[10]∧i14[1]=i14[10]∧i59[1]=i59[10] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(23) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(24) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(25) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(26) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)
(27) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(28) (i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3] ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(29) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(30) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(31) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(32) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(33) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i29[2] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(34) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(35) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(36) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(37) (i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(38) (COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(39) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(40) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(41) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(42) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
(43) (i14[3]=i14[4]∧i29[3]=i29[4]∧i59[3]=i59[4] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(44) (COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(45) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(46) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(47) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(48) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
(49) (i14[3]=i14[8]∧i29[3]=i29[8]∧i59[3]=i59[8] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(50) (COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(51) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(52) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(53) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(54) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
(55) (i29[3]=i29[12]∧i14[3]=i14[12]∧i59[3]=i59[12] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(56) (COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(57) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(58) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(59) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)
(60) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
(61) (i29[4]=i29[5]∧&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4]))=TRUE∧i59[4]=i59[5]∧i14[4]=i14[5] ⇒ LOAD1328(i14[4], i29[4], i59[4])≥NonInfC∧LOAD1328(i14[4], i29[4], i59[4])≥COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])∧(UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥))
(62) (>(i14[4], i59[4])=TRUE∧<=(i29[4], i59[4])=TRUE∧<=(i14[4], i59[4])=TRUE ⇒ LOAD1328(i14[4], i29[4], i59[4])≥NonInfC∧LOAD1328(i14[4], i29[4], i59[4])≥COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])∧(UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥))
(63) (i14[4] + [-1] + [-1]i59[4] ≥ 0∧i59[4] + [-1]i29[4] ≥ 0∧i59[4] + [-1]i14[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]i59[4] + [bni_57]i14[4] ≥ 0∧[-3 + (-1)bso_58] ≥ 0)
(64) (i14[4] + [-1] + [-1]i59[4] ≥ 0∧i59[4] + [-1]i29[4] ≥ 0∧i59[4] + [-1]i14[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]i59[4] + [bni_57]i14[4] ≥ 0∧[-3 + (-1)bso_58] ≥ 0)
(65) (i14[4] + [-1] + [-1]i59[4] ≥ 0∧i59[4] + [-1]i29[4] ≥ 0∧i59[4] + [-1]i14[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]i59[4] + [bni_57]i14[4] ≥ 0∧[-3 + (-1)bso_58] ≥ 0)
(66) (i59[5]=i59[0]∧i14[5]=i14[0]∧i29[5]=i29[0] ⇒ COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(67) (COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(68) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(69) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(70) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(71) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
(72) (i29[5]=i29[4]∧i14[5]=i14[4]∧i59[5]=i59[4] ⇒ COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(73) (COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(74) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(75) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(76) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(77) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
(78) (i14[5]=i14[8]∧i29[5]=i29[8]∧i59[5]=i59[8] ⇒ COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(79) (COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(80) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(81) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(82) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(83) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
(84) (i29[5]=i29[12]∧i59[5]=i59[12]∧i14[5]=i14[12] ⇒ COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(85) (COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥NonInfC∧COND_LOAD13281(TRUE, i14[5], i29[5], i59[5])≥LOAD1328(i14[5], i29[5], i59[5])∧(UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥))
(86) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(87) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(88) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)
(89) ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
(90) (i59[6]=i59[7]∧&&(>(i29[6], i59[6]), <=(i14[6], i59[6]))=TRUE∧i29[6]=i29[7]∧i14[6]=i14[7] ⇒ LOAD1411(i14[6], i29[6], i59[6])≥NonInfC∧LOAD1411(i14[6], i29[6], i59[6])≥COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])∧(UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥))
(91) (>(i29[6], i59[6])=TRUE∧<=(i14[6], i59[6])=TRUE ⇒ LOAD1411(i14[6], i29[6], i59[6])≥NonInfC∧LOAD1411(i14[6], i29[6], i59[6])≥COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])∧(UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥))
(92) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(93) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(94) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(95) (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(96) (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(97) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(98) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)
(99) (i59[6]=i59[7]∧&&(>(i29[6], i59[6]), <=(i14[6], i59[6]))=TRUE∧i29[6]=i29[7]∧i14[6]=i14[7] ⇒ COND_LOAD14111(TRUE, i14[7], i29[7], i59[7])≥NonInfC∧COND_LOAD14111(TRUE, i14[7], i29[7], i59[7])≥LOAD1328(i14[7], +(i29[7], -1), i59[7])∧(UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥))
(100) (>(i29[6], i59[6])=TRUE∧<=(i14[6], i59[6])=TRUE ⇒ COND_LOAD14111(TRUE, i14[6], i29[6], i59[6])≥NonInfC∧COND_LOAD14111(TRUE, i14[6], i29[6], i59[6])≥LOAD1328(i14[6], +(i29[6], -1), i59[6])∧(UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥))
(101) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(102) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(103) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(104) (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(105) (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(106) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(107) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(108) (i29[8]=i29[9]∧i14[8]=i14[9]∧&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8]))=TRUE∧i59[8]=i59[9] ⇒ LOAD1328(i14[8], i29[8], i59[8])≥NonInfC∧LOAD1328(i14[8], i29[8], i59[8])≥COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])∧(UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥))
(109) (>(i14[8], i59[8])=TRUE∧>(i29[8], i59[8])=TRUE∧<=(i14[8], i59[8])=TRUE ⇒ LOAD1328(i14[8], i29[8], i59[8])≥NonInfC∧LOAD1328(i14[8], i29[8], i59[8])≥COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])∧(UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥))
(110) (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]i59[8] + [bni_65]i14[8] ≥ 0∧[-1 + (-1)bso_66] + i29[8] + [2]i14[8] ≥ 0)
(111) (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]i59[8] + [bni_65]i14[8] ≥ 0∧[-1 + (-1)bso_66] + i29[8] + [2]i14[8] ≥ 0)
(112) (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]i59[8] + [bni_65]i14[8] ≥ 0∧[-1 + (-1)bso_66] + i29[8] + [2]i14[8] ≥ 0)
(113) (i29[8]=i29[9]∧i14[8]=i14[9]∧&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8]))=TRUE∧i59[8]=i59[9] ⇒ COND_LOAD13282(TRUE, i14[9], i29[9], i59[9])≥NonInfC∧COND_LOAD13282(TRUE, i14[9], i29[9], i59[9])≥LOAD1328(i14[9], +(i29[9], -1), i59[9])∧(UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥))
(114) (>(i14[8], i59[8])=TRUE∧>(i29[8], i59[8])=TRUE∧<=(i14[8], i59[8])=TRUE ⇒ COND_LOAD13282(TRUE, i14[8], i29[8], i59[8])≥NonInfC∧COND_LOAD13282(TRUE, i14[8], i29[8], i59[8])≥LOAD1328(i14[8], +(i29[8], -1), i59[8])∧(UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥))
(115) (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]i59[8] + [(-1)bni_67]i29[8] + [(-1)bni_67]i14[8] ≥ 0∧[(-1)bso_68] + [-1]i29[8] + [-2]i14[8] ≥ 0)
(116) (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]i59[8] + [(-1)bni_67]i29[8] + [(-1)bni_67]i14[8] ≥ 0∧[(-1)bso_68] + [-1]i29[8] + [-2]i14[8] ≥ 0)
(117) (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]i59[8] + [(-1)bni_67]i29[8] + [(-1)bni_67]i14[8] ≥ 0∧[(-1)bso_68] + [-1]i29[8] + [-2]i14[8] ≥ 0)
(118) (i14[10]=i14[11]∧>(i14[10], i59[10])=TRUE∧i59[10]=i59[11]∧i29[10]=i29[11] ⇒ LOAD1411(i14[10], i29[10], i59[10])≥NonInfC∧LOAD1411(i14[10], i29[10], i59[10])≥COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])∧(UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥))
(119) (>(i14[10], i59[10])=TRUE ⇒ LOAD1411(i14[10], i29[10], i59[10])≥NonInfC∧LOAD1411(i14[10], i29[10], i59[10])≥COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])∧(UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥))
(120) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧[(-1)bso_70] ≥ 0)
(121) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧[(-1)bso_70] ≥ 0)
(122) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧[(-1)bso_70] ≥ 0)
(123) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)
(124) (i14[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)
(125) (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)
(126) (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)
(127) (i14[10]=i14[11]∧>(i14[10], i59[10])=TRUE∧i59[10]=i59[11]∧i29[10]=i29[11] ⇒ COND_LOAD14112(TRUE, i14[11], i29[11], i59[11])≥NonInfC∧COND_LOAD14112(TRUE, i14[11], i29[11], i59[11])≥LOAD1328(+(i14[11], -1), i29[11], i59[11])∧(UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥))
(128) (>(i14[10], i59[10])=TRUE ⇒ COND_LOAD14112(TRUE, i14[10], i29[10], i59[10])≥NonInfC∧COND_LOAD14112(TRUE, i14[10], i29[10], i59[10])≥LOAD1328(+(i14[10], -1), i29[10], i59[10])∧(UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥))
(129) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)
(130) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)
(131) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)
(132) (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)
(133) (i14[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)
(134) (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)
(135) (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)
(136) (>(i14[12], i59[12])=TRUE∧i59[12]=i59[13]∧i29[12]=i29[13]∧i14[12]=i14[13] ⇒ LOAD1328(i14[12], i29[12], i59[12])≥NonInfC∧LOAD1328(i14[12], i29[12], i59[12])≥COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])∧(UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥))
(137) (>(i14[12], i59[12])=TRUE ⇒ LOAD1328(i14[12], i29[12], i59[12])≥NonInfC∧LOAD1328(i14[12], i29[12], i59[12])≥COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])∧(UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥))
(138) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧[(-1)bso_74] ≥ 0)
(139) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧[(-1)bso_74] ≥ 0)
(140) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧[(-1)bso_74] ≥ 0)
(141) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)
(142) (i14[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)
(143) (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)
(144) (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)
(145) (>(i14[12], i59[12])=TRUE∧i59[12]=i59[13]∧i29[12]=i29[13]∧i14[12]=i14[13] ⇒ COND_LOAD13283(TRUE, i14[13], i29[13], i59[13])≥NonInfC∧COND_LOAD13283(TRUE, i14[13], i29[13], i59[13])≥LOAD1328(+(i14[13], -1), i29[13], i59[13])∧(UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥))
(146) (>(i14[12], i59[12])=TRUE ⇒ COND_LOAD13283(TRUE, i14[12], i29[12], i59[12])≥NonInfC∧COND_LOAD13283(TRUE, i14[12], i29[12], i59[12])≥LOAD1328(+(i14[12], -1), i29[12], i59[12])∧(UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥))
(147) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)
(148) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)
(149) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)
(150) (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)
(151) (i14[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)
(152) (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)
(153) (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [3]
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(LOAD1411(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(COND_LOAD13281(x1, x2, x3, x4)) = [1] + [-1]x4 + x2 + [-1]x1
POL(COND_LOAD14111(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_LOAD13282(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2 + [-1]x1
POL(COND_LOAD14112(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(COND_LOAD13283(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])
COND_LOAD13281(TRUE, i14[5], i29[5], i59[5]) → LOAD1328(i14[5], i29[5], i59[5])
LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])
COND_LOAD13282(TRUE, i14[9], i29[9], i59[9]) → LOAD1328(i14[9], +(i29[9], -1), i59[9])
COND_LOAD14112(TRUE, i14[11], i29[11], i59[11]) → LOAD1328(+(i14[11], -1), i29[11], i59[11])
COND_LOAD13283(TRUE, i14[13], i29[13], i59[13]) → LOAD1328(+(i14[13], -1), i29[13], i59[13])
LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])
LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])
COND_LOAD13282(TRUE, i14[9], i29[9], i59[9]) → LOAD1328(i14[9], +(i29[9], -1), i59[9])
LOAD1411(i14[10], i29[10], i59[10]) → COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])
COND_LOAD14112(TRUE, i14[11], i29[11], i59[11]) → LOAD1328(+(i14[11], -1), i29[11], i59[11])
LOAD1328(i14[12], i29[12], i59[12]) → COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])
COND_LOAD13283(TRUE, i14[13], i29[13], i59[13]) → LOAD1328(+(i14[13], -1), i29[13], i59[13])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3])
LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7])
LOAD1411(i14[10], i29[10], i59[10]) → COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])
LOAD1328(i14[12], i29[12], i59[12]) → COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(7) -> (0), if ((i59[7] →* i59[0])∧(i29[7] + -1 →* i29[0])∧(i14[7] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
(6) -> (7), if ((i59[6] →* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6] →* TRUE)∧(i29[6] →* i29[7])∧(i14[6] →* i14[7]))
(1) -> (10), if ((i29[1] →* i29[10])∧(i14[1] →* i14[10])∧(i59[1] →* i59[10]))
(3) -> (12), if ((i29[3] →* i29[12])∧(i14[3] →* i14[12])∧(i59[3] →* i59[12]))
(7) -> (12), if ((i29[7] + -1 →* i29[12])∧(i14[7] →* i14[12])∧(i59[7] →* i59[12]))
!= | ~ | 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 |
Integer, Boolean
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(7) -> (0), if ((i59[7] →* i59[0])∧(i29[7] + -1 →* i29[0])∧(i14[7] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
(6) -> (7), if ((i59[6] →* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6] →* TRUE)∧(i29[6] →* i29[7])∧(i14[6] →* i14[7]))
(1) (i59[6]=i59[7]∧&&(>(i29[6], i59[6]), <=(i14[6], i59[6]))=TRUE∧i29[6]=i29[7]∧i14[6]=i14[7]∧i59[7]=i59[0]∧+(i29[7], -1)=i29[0]∧i14[7]=i14[0] ⇒ COND_LOAD14111(TRUE, i14[7], i29[7], i59[7])≥NonInfC∧COND_LOAD14111(TRUE, i14[7], i29[7], i59[7])≥LOAD1328(i14[7], +(i29[7], -1), i59[7])∧(UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥))
(2) (>(i29[6], i59[6])=TRUE∧<=(i14[6], i59[6])=TRUE ⇒ COND_LOAD14111(TRUE, i14[6], i29[6], i59[6])≥NonInfC∧COND_LOAD14111(TRUE, i14[6], i29[6], i59[6])≥LOAD1328(i14[6], +(i29[6], -1), i59[6])∧(UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥))
(3) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(4) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(5) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(6) (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(7) (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(8) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(9) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(10) (i59[6]=i59[7]∧&&(>(i29[6], i59[6]), <=(i14[6], i59[6]))=TRUE∧i29[6]=i29[7]∧i14[6]=i14[7] ⇒ LOAD1411(i14[6], i29[6], i59[6])≥NonInfC∧LOAD1411(i14[6], i29[6], i59[6])≥COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])∧(UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥))
(11) (>(i29[6], i59[6])=TRUE∧<=(i14[6], i59[6])=TRUE ⇒ LOAD1411(i14[6], i29[6], i59[6])≥NonInfC∧LOAD1411(i14[6], i29[6], i59[6])≥COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])∧(UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥))
(12) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(13) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(14) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(15) (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(16) (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(17) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(18) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(19) (i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(20) (COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(21) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)
(22) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)
(23) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)
(24) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)
(25) (i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3] ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(26) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(27) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(28) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(29) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(30) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(31) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(32) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(33) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(34) (i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(35) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(36) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(37) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(38) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(39) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
(40) (i14[1]=i14[6]∧i59[1]=i59[6]∧i29[1]=i29[6] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(41) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(42) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(43) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(44) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(45) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
(46) (i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1] ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(47) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(48) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(49) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(50) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(51) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(52) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(53) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(54) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [1]
POL(COND_LOAD14111(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(LOAD1411(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7])
COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7])
LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) (i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2]∧i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3] ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(2) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(3) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)
(4) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)
(5) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)
(6) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i29[2] + [(2)bni_24]i59[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(7) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(8) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(9) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(10) (i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1]∧i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(11) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ COND_LOAD1328(TRUE, i14[0], i29[0], i59[0])≥NonInfC∧COND_LOAD1328(TRUE, i14[0], i29[0], i59[0])≥LOAD1411(i14[0], i29[0], i59[0])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(12) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(13) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(14) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(15) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(16) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(17) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(18) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
(19) (i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0]∧i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1] ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(20) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(21) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-3 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)
(22) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-3 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)
(23) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-3 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)
(24) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)
(25) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)
(26) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)
(27) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)
(28) (i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3]∧i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(29) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ COND_LOAD1411(TRUE, i14[2], i29[2], i59[2])≥NonInfC∧COND_LOAD1411(TRUE, i14[2], i29[2], i59[2])≥LOAD1328(i14[2], i29[2], i59[2])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(30) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)
(31) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)
(32) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)
(33) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
(34) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
(35) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
(36) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [1]
POL(LOAD1411(x1, x2, x3)) = [2]x3 + [-1]x2 + [-1]x1
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + x3 + [-1]x2 + [-1]x1
POL(&&(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1328(x1, x2, x3, x4)) = [2] + [2]x4 + [-1]x3 + [-1]x2
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + [-1]x1
POL(>(x1, x2)) = [-1]
COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3])
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
!= | ~ | 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 |
!= | ~ | 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 |
Boolean, Integer
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(5) -> (0), if ((i59[5] →* i59[0])∧(i14[5] →* i14[0])∧(i29[5] →* i29[0]))
(7) -> (0), if ((i59[7] →* i59[0])∧(i29[7] + -1 →* i29[0])∧(i14[7] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
(6) -> (7), if ((i59[6] →* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6] →* TRUE)∧(i29[6] →* i29[7])∧(i14[6] →* i14[7]))
!= | ~ | 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 |
Integer, Boolean
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(7) -> (0), if ((i59[7] →* i59[0])∧(i29[7] + -1 →* i29[0])∧(i14[7] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
(6) -> (7), if ((i59[6] →* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6] →* TRUE)∧(i29[6] →* i29[7])∧(i14[6] →* i14[7]))
(1) (i59[6]=i59[7]∧&&(>(i29[6], i59[6]), <=(i14[6], i59[6]))=TRUE∧i29[6]=i29[7]∧i14[6]=i14[7]∧i59[7]=i59[0]∧+(i29[7], -1)=i29[0]∧i14[7]=i14[0] ⇒ COND_LOAD14111(TRUE, i14[7], i29[7], i59[7])≥NonInfC∧COND_LOAD14111(TRUE, i14[7], i29[7], i59[7])≥LOAD1328(i14[7], +(i29[7], -1), i59[7])∧(UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥))
(2) (>(i29[6], i59[6])=TRUE∧<=(i14[6], i59[6])=TRUE ⇒ COND_LOAD14111(TRUE, i14[6], i29[6], i59[6])≥NonInfC∧COND_LOAD14111(TRUE, i14[6], i29[6], i59[6])≥LOAD1328(i14[6], +(i29[6], -1), i59[6])∧(UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥))
(3) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(4) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(5) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(6) (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(7) (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(8) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(9) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
(10) (i59[6]=i59[7]∧&&(>(i29[6], i59[6]), <=(i14[6], i59[6]))=TRUE∧i29[6]=i29[7]∧i14[6]=i14[7] ⇒ LOAD1411(i14[6], i29[6], i59[6])≥NonInfC∧LOAD1411(i14[6], i29[6], i59[6])≥COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])∧(UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥))
(11) (>(i29[6], i59[6])=TRUE∧<=(i14[6], i59[6])=TRUE ⇒ LOAD1411(i14[6], i29[6], i59[6])≥NonInfC∧LOAD1411(i14[6], i29[6], i59[6])≥COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])∧(UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥))
(12) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(13) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(14) (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(15) (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(16) (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(17) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(18) (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
(19) (i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(20) (COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(21) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)
(22) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)
(23) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)
(24) ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)
(25) (i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3] ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(26) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(27) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(28) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(29) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(30) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(31) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(32) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(33) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
(34) (i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(35) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(36) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(37) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(38) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(39) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
(40) (i14[1]=i14[6]∧i59[1]=i59[6]∧i29[1]=i29[6] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(41) (COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(42) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(43) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(44) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)
(45) ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
(46) (i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1] ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(47) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(48) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(49) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(50) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(51) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(52) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(53) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(54) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_LOAD14111(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(LOAD1411(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7])
COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7])
LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) -> (6), if ((i14[1] →* i14[6])∧(i59[1] →* i59[6])∧(i29[1] →* i29[6]))
!= | ~ | 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 |
Boolean, Integer
(3) -> (0), if ((i59[3] →* i59[0])∧(i29[3] →* i29[0])∧(i14[3] →* i14[0]))
(0) -> (1), if ((i29[0] →* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0] →* TRUE)∧(i59[0] →* i59[1])∧(i14[0] →* i14[1]))
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
(1) (i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2]∧i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3] ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(2) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ LOAD1411(i14[2], i29[2], i59[2])≥NonInfC∧LOAD1411(i14[2], i29[2], i59[2])≥COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])∧(UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥))
(3) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)
(4) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)
(5) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)
(6) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i29[2] + [(2)bni_24]i59[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(7) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(8) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(9) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
(10) (i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1]∧i59[1]=i59[2]∧i14[1]=i14[2]∧i29[1]=i29[2] ⇒ COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥NonInfC∧COND_LOAD1328(TRUE, i14[1], i29[1], i59[1])≥LOAD1411(i14[1], i29[1], i59[1])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(11) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ COND_LOAD1328(TRUE, i14[0], i29[0], i59[0])≥NonInfC∧COND_LOAD1328(TRUE, i14[0], i29[0], i59[0])≥LOAD1411(i14[0], i29[0], i59[0])∧(UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥))
(12) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(13) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(14) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(15) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(16) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(17) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(18) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(19) (i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0]∧i29[0]=i29[1]∧&&(>(i29[0], i59[0]), <=(i14[0], i59[0]))=TRUE∧i59[0]=i59[1]∧i14[0]=i14[1] ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(20) (>(i29[0], i59[0])=TRUE∧<=(i14[0], i59[0])=TRUE ⇒ LOAD1328(i14[0], i29[0], i59[0])≥NonInfC∧LOAD1328(i14[0], i29[0], i59[0])≥COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])∧(UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥))
(21) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-1 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)
(22) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-1 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)
(23) (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-1 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)
(24) (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)
(25) (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)
(26) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)
(27) (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)
(28) (i14[2]=i14[3]∧i59[2]=i59[3]∧&&(<=(i29[2], i59[2]), <=(i14[2], i59[2]))=TRUE∧i29[2]=i29[3]∧i59[3]=i59[0]∧i29[3]=i29[0]∧i14[3]=i14[0] ⇒ COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥NonInfC∧COND_LOAD1411(TRUE, i14[3], i29[3], i59[3])≥LOAD1328(i14[3], i29[3], i59[3])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(29) (<=(i29[2], i59[2])=TRUE∧<=(i14[2], i59[2])=TRUE ⇒ COND_LOAD1411(TRUE, i14[2], i29[2], i59[2])≥NonInfC∧COND_LOAD1411(TRUE, i14[2], i29[2], i59[2])≥LOAD1328(i14[2], i29[2], i59[2])∧(UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥))
(30) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)
(31) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)
(32) (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)
(33) (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
(34) (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
(35) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
(36) (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD1411(x1, x2, x3)) = [-1] + [2]x3 + [-1]x2 + [-1]x1
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + x3 + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2 + [-1]x1
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + [-1]x1
POL(>(x1, x2)) = [-1]
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1])
COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3])
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | 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 |
Boolean, Integer
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))
!= | ~ | 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 |
!= | ~ | 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 |
Boolean, Integer
(1) -> (2), if ((i59[1] →* i59[2])∧(i14[1] →* i14[2])∧(i29[1] →* i29[2]))
(2) -> (3), if ((i14[2] →* i14[3])∧(i59[2] →* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2] →* TRUE)∧(i29[2] →* i29[3]))