0 JBC
↳1 JBCToGraph (⇒, 370 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIDPv1Proof (⇒, 170 ms)
↳6 IDP
↳7 IDPNonInfProof (⇒, 930 ms)
↳8 IDP
↳9 IDependencyGraphProof (⇔, 0 ms)
↳10 IDP
↳11 IDPNonInfProof (⇒, 430 ms)
↳12 IDP
↳13 IDependencyGraphProof (⇔, 0 ms)
↳14 IDP
↳15 IDPNonInfProof (⇒, 290 ms)
↳16 IDP
↳17 IDependencyGraphProof (⇔, 0 ms)
↳18 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();
}
}
Generated 30 rules for P and 0 rules for R.
P rules:
1155_0_main_Load(EOS(STATIC_1155), i110, i140, i86, i110) → 1157_0_main_GT(EOS(STATIC_1157), i110, i140, i86, i110, i86)
1157_0_main_GT(EOS(STATIC_1157), i110, i140, i86, i110, i86) → 1159_0_main_GT(EOS(STATIC_1159), i110, i140, i86, i110, i86)
1157_0_main_GT(EOS(STATIC_1157), i110, i140, i86, i110, i86) → 1161_0_main_GT(EOS(STATIC_1161), i110, i140, i86, i110, i86)
1159_0_main_GT(EOS(STATIC_1159), i110, i140, i86, i110, i86) → 1162_0_main_Load(EOS(STATIC_1162), i110, i140, i86) | >(i110, i86)
1162_0_main_Load(EOS(STATIC_1162), i110, i140, i86) → 1186_0_main_Load(EOS(STATIC_1186), i110, i140, i86)
1186_0_main_Load(EOS(STATIC_1186), i110, i140, i86) → 1190_0_main_Load(EOS(STATIC_1190), i110, i140, i86, i110)
1190_0_main_Load(EOS(STATIC_1190), i110, i140, i86, i110) → 1191_0_main_LE(EOS(STATIC_1191), i110, i140, i86, i110, i86)
1191_0_main_LE(EOS(STATIC_1191), i110, i140, i86, i110, i86) → 1193_0_main_LE(EOS(STATIC_1193), i110, i140, i86, i110, i86)
1191_0_main_LE(EOS(STATIC_1191), i110, i140, i86, i110, i86) → 1194_0_main_LE(EOS(STATIC_1194), i110, i140, i86, i110, i86)
1193_0_main_LE(EOS(STATIC_1193), i110, i140, i86, i110, i86) → 1196_0_main_Load(EOS(STATIC_1196), i110, i140, i86) | <=(i110, i86)
1196_0_main_Load(EOS(STATIC_1196), i110, i140, i86) → 1200_0_main_Load(EOS(STATIC_1200), i110, i140, i86, i140)
1200_0_main_Load(EOS(STATIC_1200), i110, i140, i86, i140) → 1203_0_main_LE(EOS(STATIC_1203), i110, i140, i86, i140, i86)
1203_0_main_LE(EOS(STATIC_1203), i110, i140, i86, i140, i86) → 1208_0_main_LE(EOS(STATIC_1208), i110, i140, i86, i140, i86)
1203_0_main_LE(EOS(STATIC_1203), i110, i140, i86, i140, i86) → 1210_0_main_LE(EOS(STATIC_1210), i110, i140, i86, i140, i86)
1208_0_main_LE(EOS(STATIC_1208), i110, i140, i86, i140, i86) → 1213_0_main_Load(EOS(STATIC_1213), i110, i140, i86) | <=(i140, i86)
1213_0_main_Load(EOS(STATIC_1213), i110, i140, i86) → 1153_0_main_Load(EOS(STATIC_1153), i110, i140, i86)
1153_0_main_Load(EOS(STATIC_1153), i110, i140, i86) → 1155_0_main_Load(EOS(STATIC_1155), i110, i140, i86, i110)
1210_0_main_LE(EOS(STATIC_1210), i110, i140, i86, i140, i86) → 1215_0_main_Inc(EOS(STATIC_1215), i110, i140, i86) | >(i140, i86)
1215_0_main_Inc(EOS(STATIC_1215), i110, i140, i86) → 1216_0_main_JMP(EOS(STATIC_1216), i110, +(i140, -1), i86)
1216_0_main_JMP(EOS(STATIC_1216), i110, i144, i86) → 1219_0_main_Load(EOS(STATIC_1219), i110, i144, i86)
1219_0_main_Load(EOS(STATIC_1219), i110, i144, i86) → 1153_0_main_Load(EOS(STATIC_1153), i110, i144, i86)
1194_0_main_LE(EOS(STATIC_1194), i110, i140, i86, i110, i86) → 1198_0_main_Inc(EOS(STATIC_1198), i110, i140, i86) | >(i110, i86)
1198_0_main_Inc(EOS(STATIC_1198), i110, i140, i86) → 1201_0_main_JMP(EOS(STATIC_1201), +(i110, -1), i140, i86)
1201_0_main_JMP(EOS(STATIC_1201), i142, i140, i86) → 1207_0_main_Load(EOS(STATIC_1207), i142, i140, i86)
1207_0_main_Load(EOS(STATIC_1207), i142, i140, i86) → 1153_0_main_Load(EOS(STATIC_1153), i142, i140, i86)
1161_0_main_GT(EOS(STATIC_1161), i110, i140, i86, i110, i86) → 1164_0_main_Load(EOS(STATIC_1164), i110, i140, i86) | <=(i110, i86)
1164_0_main_Load(EOS(STATIC_1164), i110, i140, i86) → 1167_0_main_Load(EOS(STATIC_1167), i110, i140, i86, i140)
1167_0_main_Load(EOS(STATIC_1167), i110, i140, i86, i140) → 1171_0_main_LE(EOS(STATIC_1171), i110, i140, i86, i140, i86)
1171_0_main_LE(EOS(STATIC_1171), i110, i140, i86, i140, i86) → 1177_0_main_LE(EOS(STATIC_1177), i110, i140, i86, i140, i86)
1177_0_main_LE(EOS(STATIC_1177), i110, i140, i86, i140, i86) → 1186_0_main_Load(EOS(STATIC_1186), i110, i140, i86) | >(i140, i86)
R rules:
Combined rules. Obtained 5 conditional rules for P and 0 conditional rules for R.
P rules:
1155_0_main_Load(EOS(STATIC_1155), x0, x1, x2, x0) → 1191_0_main_LE(EOS(STATIC_1191), x0, x1, x2, x0, x2) | <(x2, x0)
1191_0_main_LE(EOS(STATIC_1191), x0, x1, x2, x0, x2) → 1155_0_main_Load(EOS(STATIC_1155), x0, x1, x2, x0) | &&(>=(x2, x1), >=(x2, x0))
1191_0_main_LE(EOS(STATIC_1191), x0, x1, x2, x0, x2) → 1155_0_main_Load(EOS(STATIC_1155), x0, +(x1, -1), x2, x0) | &&(>=(x2, x0), <(x2, x1))
1191_0_main_LE(EOS(STATIC_1191), x0, x1, x2, x0, x2) → 1155_0_main_Load(EOS(STATIC_1155), +(x0, -1), x1, x2, +(x0, -1)) | <(x2, x0)
1155_0_main_Load(EOS(STATIC_1155), x0, x1, x2, x0) → 1191_0_main_LE(EOS(STATIC_1191), x0, x1, x2, x0, x2) | &&(>=(x2, x0), <(x2, x1))
R rules:
Filtered ground terms:
1191_0_main_LE(x1, x2, x3, x4, x5, x6) → 1191_0_main_LE(x2, x3, x4, x5, x6)
Cond_1155_0_main_Load1(x1, x2, x3, x4, x5, x6) → Cond_1155_0_main_Load1(x1, x3, x4, x5, x6)
1155_0_main_Load(x1, x2, x3, x4, x5) → 1155_0_main_Load(x2, x3, x4, x5)
Cond_1191_0_main_LE2(x1, x2, x3, x4, x5, x6, x7) → Cond_1191_0_main_LE2(x1, x3, x4, x5, x6, x7)
Cond_1191_0_main_LE1(x1, x2, x3, x4, x5, x6, x7) → Cond_1191_0_main_LE1(x1, x3, x4, x5, x6, x7)
Cond_1191_0_main_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_1191_0_main_LE(x1, x3, x4, x5, x6, x7)
Cond_1155_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_1155_0_main_Load(x1, x3, x4, x5, x6)
Filtered duplicate args:
1155_0_main_Load(x1, x2, x3, x4) → 1155_0_main_Load(x2, x3, x4)
Cond_1155_0_main_Load(x1, x2, x3, x4, x5) → Cond_1155_0_main_Load(x1, x3, x4, x5)
1191_0_main_LE(x1, x2, x3, x4, x5) → 1191_0_main_LE(x2, x4, x5)
Cond_1191_0_main_LE(x1, x2, x3, x4, x5, x6) → Cond_1191_0_main_LE(x1, x3, x5, x6)
Cond_1191_0_main_LE1(x1, x2, x3, x4, x5, x6) → Cond_1191_0_main_LE1(x1, x3, x5, x6)
Cond_1191_0_main_LE2(x1, x2, x3, x4, x5, x6) → Cond_1191_0_main_LE2(x1, x3, x5, x6)
Cond_1155_0_main_Load1(x1, x2, x3, x4, x5) → Cond_1155_0_main_Load1(x1, x3, x4, x5)
Combined rules. Obtained 5 conditional rules for P and 0 conditional rules for R.
P rules:
1155_0_main_Load(x1, x2, x0) → 1191_0_main_LE(x1, x0, x2) | <(x2, x0)
1191_0_main_LE(x1, x0, x2) → 1155_0_main_Load(x1, x2, x0) | &&(>=(x2, x1), >=(x2, x0))
1191_0_main_LE(x1, x0, x2) → 1155_0_main_Load(+(x1, -1), x2, x0) | &&(>=(x2, x0), <(x2, x1))
1191_0_main_LE(x1, x0, x2) → 1155_0_main_Load(x1, x2, +(x0, -1)) | <(x2, x0)
1155_0_main_Load(x1, x2, x0) → 1191_0_main_LE(x1, x0, x2) | &&(>=(x2, x0), <(x2, x1))
R rules:
Finished conversion. Obtained 10 rules for P and 0 rules for R. System has predefined symbols.
P rules:
1155_0_MAIN_LOAD(x1, x2, x0) → COND_1155_0_MAIN_LOAD(<(x2, x0), x1, x2, x0)
COND_1155_0_MAIN_LOAD(TRUE, x1, x2, x0) → 1191_0_MAIN_LE(x1, x0, x2)
1191_0_MAIN_LE(x1, x0, x2) → COND_1191_0_MAIN_LE(&&(>=(x2, x1), >=(x2, x0)), x1, x0, x2)
COND_1191_0_MAIN_LE(TRUE, x1, x0, x2) → 1155_0_MAIN_LOAD(x1, x2, x0)
1191_0_MAIN_LE(x1, x0, x2) → COND_1191_0_MAIN_LE1(&&(>=(x2, x0), <(x2, x1)), x1, x0, x2)
COND_1191_0_MAIN_LE1(TRUE, x1, x0, x2) → 1155_0_MAIN_LOAD(+(x1, -1), x2, x0)
1191_0_MAIN_LE(x1, x0, x2) → COND_1191_0_MAIN_LE2(<(x2, x0), x1, x0, x2)
COND_1191_0_MAIN_LE2(TRUE, x1, x0, x2) → 1155_0_MAIN_LOAD(x1, x2, +(x0, -1))
1155_0_MAIN_LOAD(x1, x2, x0) → COND_1155_0_MAIN_LOAD1(&&(>=(x2, x0), <(x2, x1)), x1, x2, x0)
COND_1155_0_MAIN_LOAD1(TRUE, x1, x2, x0) → 1191_0_MAIN_LE(x1, x0, x2)
R rules:
!= | ~ | 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
(0) -> (1), if (x2[0] < x0[0] ∧x1[0] →* x1[1]∧x2[0] →* x2[1]∧x0[0] →* x0[1])
(1) -> (2), if (x1[1] →* x1[2]∧x0[1] →* x0[2]∧x2[1] →* x2[2])
(1) -> (4), if (x1[1] →* x1[4]∧x0[1] →* x0[4]∧x2[1] →* x2[4])
(1) -> (6), if (x1[1] →* x1[6]∧x0[1] →* x0[6]∧x2[1] →* x2[6])
(2) -> (3), if (x2[2] >= x1[2] && x2[2] >= x0[2] ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(3) -> (0), if (x1[3] →* x1[0]∧x2[3] →* x2[0]∧x0[3] →* x0[0])
(3) -> (8), if (x1[3] →* x1[8]∧x2[3] →* x2[8]∧x0[3] →* x0[8])
(4) -> (5), if (x2[4] >= x0[4] && x2[4] < x1[4] ∧x1[4] →* x1[5]∧x0[4] →* x0[5]∧x2[4] →* x2[5])
(5) -> (0), if (x1[5] + -1 →* x1[0]∧x2[5] →* x2[0]∧x0[5] →* x0[0])
(5) -> (8), if (x1[5] + -1 →* x1[8]∧x2[5] →* x2[8]∧x0[5] →* x0[8])
(6) -> (7), if (x2[6] < x0[6] ∧x1[6] →* x1[7]∧x0[6] →* x0[7]∧x2[6] →* x2[7])
(7) -> (0), if (x1[7] →* x1[0]∧x2[7] →* x2[0]∧x0[7] + -1 →* x0[0])
(7) -> (8), if (x1[7] →* x1[8]∧x2[7] →* x2[8]∧x0[7] + -1 →* x0[8])
(8) -> (9), if (x2[8] >= x0[8] && x2[8] < x1[8] ∧x1[8] →* x1[9]∧x2[8] →* x2[9]∧x0[8] →* x0[9])
(9) -> (2), if (x1[9] →* x1[2]∧x0[9] →* x0[2]∧x2[9] →* x2[2])
(9) -> (4), if (x1[9] →* x1[4]∧x0[9] →* x0[4]∧x2[9] →* x2[4])
(9) -> (6), if (x1[9] →* x1[6]∧x0[9] →* x0[6]∧x2[9] →* x2[6])
(1) (<(x2[0], x0[0])=TRUE∧x1[0]=x1[1]∧x2[0]=x2[1]∧x0[0]=x0[1] ⇒ 1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥NonInfC∧1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])∧(UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥))
(2) (<(x2[0], x0[0])=TRUE ⇒ 1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥NonInfC∧1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])∧(UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥))
(3) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]x2[0] + [bni_39]x1[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(4) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]x2[0] + [bni_39]x1[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(5) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]x2[0] + [bni_39]x1[0] ≥ 0∧[(-1)bso_40] ≥ 0)
(6) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]x2[0] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)
(7) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]x2[0] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)
(8) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] + [bni_39]x2[0] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)
(9) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]x2[0] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)
(10) (x1[1]=x1[2]∧x0[1]=x0[2]∧x2[1]=x2[2] ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(11) (COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(12) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(13) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(14) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(15) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)
(16) (x1[1]=x1[4]∧x0[1]=x0[4]∧x2[1]=x2[4] ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(17) (COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(18) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(19) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(20) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(21) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)
(22) (x1[1]=x1[6]∧x0[1]=x0[6]∧x2[1]=x2[6] ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(23) (COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(24) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(25) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(26) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)
(27) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)
(28) (&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3] ⇒ 1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(29) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ 1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(30) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] + [bni_43]x1[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(31) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] + [bni_43]x1[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(32) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] + [bni_43]x1[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(33) (x2[2] ≥ 0∧x1[2] + x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(34) (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(35) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(36) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x2[2] ≥ 0∧[(-1)bso_44] ≥ 0)
(37) (x1[3]=x1[0]∧x2[3]=x2[0]∧x0[3]=x0[0] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(38) (COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(39) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)
(40) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)
(41) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)
(42) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)
(43) (x1[3]=x1[8]∧x2[3]=x2[8]∧x0[3]=x0[8] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(44) (COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(45) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)
(46) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)
(47) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)
(48) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_45] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)
(49) (&&(>=(x2[4], x0[4]), <(x2[4], x1[4]))=TRUE∧x1[4]=x1[5]∧x0[4]=x0[5]∧x2[4]=x2[5] ⇒ 1191_0_MAIN_LE(x1[4], x0[4], x2[4])≥NonInfC∧1191_0_MAIN_LE(x1[4], x0[4], x2[4])≥COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])∧(UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥))
(50) (>=(x2[4], x0[4])=TRUE∧<(x2[4], x1[4])=TRUE ⇒ 1191_0_MAIN_LE(x1[4], x0[4], x2[4])≥NonInfC∧1191_0_MAIN_LE(x1[4], x0[4], x2[4])≥COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])∧(UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥))
(51) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x2[4] + [bni_47]x1[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(52) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x2[4] + [bni_47]x1[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(53) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x2[4] + [bni_47]x1[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(54) (x2[4] ≥ 0∧x1[4] + [-1] + [-1]x0[4] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x0[4] + [(-1)bni_47]x2[4] + [bni_47]x1[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(55) (x2[4] ≥ 0∧x0[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)Bound*bni_47] + [bni_47]x0[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(56) (x2[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)Bound*bni_47] + [bni_47]x0[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(57) (x2[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])), ≥)∧[(-1)Bound*bni_47] + [bni_47]x0[4] ≥ 0∧[(-1)bso_48] ≥ 0)
(58) (&&(>=(x2[4], x0[4]), <(x2[4], x1[4]))=TRUE∧x1[4]=x1[5]∧x0[4]=x0[5]∧x2[4]=x2[5]∧+(x1[5], -1)=x1[0]∧x2[5]=x2[0]∧x0[5]=x0[0] ⇒ COND_1191_0_MAIN_LE1(TRUE, x1[5], x0[5], x2[5])≥NonInfC∧COND_1191_0_MAIN_LE1(TRUE, x1[5], x0[5], x2[5])≥1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])∧(UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥))
(59) (>=(x2[4], x0[4])=TRUE∧<(x2[4], x1[4])=TRUE ⇒ COND_1191_0_MAIN_LE1(TRUE, x1[4], x0[4], x2[4])≥NonInfC∧COND_1191_0_MAIN_LE1(TRUE, x1[4], x0[4], x2[4])≥1155_0_MAIN_LOAD(+(x1[4], -1), x2[4], x0[4])∧(UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥))
(60) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(61) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(62) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(63) (x2[4] ≥ 0∧x1[4] + [-1] + [-1]x0[4] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x0[4] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(64) (x2[4] ≥ 0∧x0[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)Bound*bni_49] + [bni_49]x0[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(65) (x2[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)Bound*bni_49] + [bni_49]x0[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(66) (x2[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)Bound*bni_49] + [bni_49]x0[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(67) (&&(>=(x2[4], x0[4]), <(x2[4], x1[4]))=TRUE∧x1[4]=x1[5]∧x0[4]=x0[5]∧x2[4]=x2[5]∧+(x1[5], -1)=x1[8]∧x2[5]=x2[8]∧x0[5]=x0[8] ⇒ COND_1191_0_MAIN_LE1(TRUE, x1[5], x0[5], x2[5])≥NonInfC∧COND_1191_0_MAIN_LE1(TRUE, x1[5], x0[5], x2[5])≥1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])∧(UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥))
(68) (>=(x2[4], x0[4])=TRUE∧<(x2[4], x1[4])=TRUE ⇒ COND_1191_0_MAIN_LE1(TRUE, x1[4], x0[4], x2[4])≥NonInfC∧COND_1191_0_MAIN_LE1(TRUE, x1[4], x0[4], x2[4])≥1155_0_MAIN_LOAD(+(x1[4], -1), x2[4], x0[4])∧(UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥))
(69) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(70) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(71) (x2[4] + [-1]x0[4] ≥ 0∧x1[4] + [-1] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(72) (x2[4] ≥ 0∧x1[4] + [-1] + [-1]x0[4] + [-1]x2[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x0[4] + [(-1)bni_49]x2[4] + [bni_49]x1[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(73) (x2[4] ≥ 0∧x0[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)Bound*bni_49] + [bni_49]x0[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(74) (x2[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)Bound*bni_49] + [bni_49]x0[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(75) (x2[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])), ≥)∧[(-1)Bound*bni_49] + [bni_49]x0[4] ≥ 0∧[1 + (-1)bso_50] ≥ 0)
(76) (<(x2[6], x0[6])=TRUE∧x1[6]=x1[7]∧x0[6]=x0[7]∧x2[6]=x2[7] ⇒ 1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥NonInfC∧1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])∧(UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥))
(77) (<(x2[6], x0[6])=TRUE ⇒ 1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥NonInfC∧1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])∧(UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥))
(78) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x2[6] + [bni_51]x1[6] ≥ 0∧[(-1)bso_52] ≥ 0)
(79) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x2[6] + [bni_51]x1[6] ≥ 0∧[(-1)bso_52] ≥ 0)
(80) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x2[6] + [bni_51]x1[6] ≥ 0∧[(-1)bso_52] ≥ 0)
(81) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x2[6] ≥ 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(82) (x0[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x2[6] ≥ 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(83) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]x2[6] ≥ 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(84) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x2[6] ≥ 0∧0 = 0∧[(-1)bso_52] ≥ 0)
(85) (<(x2[6], x0[6])=TRUE∧x1[6]=x1[7]∧x0[6]=x0[7]∧x2[6]=x2[7]∧x1[7]=x1[0]∧x2[7]=x2[0]∧+(x0[7], -1)=x0[0] ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(86) (<(x2[6], x0[6])=TRUE ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥1155_0_MAIN_LOAD(x1[6], x2[6], +(x0[6], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(87) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] + [bni_53]x1[6] ≥ 0∧[(-1)bso_54] ≥ 0)
(88) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] + [bni_53]x1[6] ≥ 0∧[(-1)bso_54] ≥ 0)
(89) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] + [bni_53]x1[6] ≥ 0∧[(-1)bso_54] ≥ 0)
(90) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(91) (x0[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(92) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(93) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(94) (<(x2[6], x0[6])=TRUE∧x1[6]=x1[7]∧x0[6]=x0[7]∧x2[6]=x2[7]∧x1[7]=x1[8]∧x2[7]=x2[8]∧+(x0[7], -1)=x0[8] ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(95) (<(x2[6], x0[6])=TRUE ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥1155_0_MAIN_LOAD(x1[6], x2[6], +(x0[6], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(96) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] + [bni_53]x1[6] ≥ 0∧[(-1)bso_54] ≥ 0)
(97) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] + [bni_53]x1[6] ≥ 0∧[(-1)bso_54] ≥ 0)
(98) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] + [bni_53]x1[6] ≥ 0∧[(-1)bso_54] ≥ 0)
(99) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(100) (x0[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(101) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(102) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[bni_53] = 0∧[(-1)bni_53 + (-1)Bound*bni_53] + [bni_53]x2[6] ≥ 0∧0 = 0∧[(-1)bso_54] ≥ 0)
(103) (&&(>=(x2[8], x0[8]), <(x2[8], x1[8]))=TRUE∧x1[8]=x1[9]∧x2[8]=x2[9]∧x0[8]=x0[9] ⇒ 1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥NonInfC∧1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])∧(UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥))
(104) (>=(x2[8], x0[8])=TRUE∧<(x2[8], x1[8])=TRUE ⇒ 1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥NonInfC∧1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])∧(UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥))
(105) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(-1)bni_55]x2[8] + [bni_55]x1[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(106) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(-1)bni_55]x2[8] + [bni_55]x1[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(107) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(-1)bni_55]x2[8] + [bni_55]x1[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(108) (x2[8] ≥ 0∧x1[8] + [-1] + [-1]x0[8] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(-1)bni_55]x0[8] + [(-1)bni_55]x2[8] + [bni_55]x1[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(109) (x2[8] ≥ 0∧x0[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)Bound*bni_55] + [bni_55]x0[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(110) (x2[8] ≥ 0∧x0[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)Bound*bni_55] + [bni_55]x0[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(111) (x2[8] ≥ 0∧x0[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)Bound*bni_55] + [bni_55]x0[8] ≥ 0∧[(-1)bso_56] ≥ 0)
(112) (x1[9]=x1[2]∧x0[9]=x0[2]∧x2[9]=x2[2] ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(113) (COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(114) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(115) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(116) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(117) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
(118) (x1[9]=x1[4]∧x0[9]=x0[4]∧x2[9]=x2[4] ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(119) (COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(120) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(121) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(122) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(123) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
(124) (x1[9]=x1[6]∧x0[9]=x0[6]∧x2[9]=x2[6] ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(125) (COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(126) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(127) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(128) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(129) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_57] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1155_0_MAIN_LOAD(x1, x2, x3)) = [-1] + [-1]x2 + x1
POL(COND_1155_0_MAIN_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2
POL(<(x1, x2)) = [-1]
POL(1191_0_MAIN_LE(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(COND_1191_0_MAIN_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(COND_1191_0_MAIN_LE1(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_1191_0_MAIN_LE2(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(COND_1155_0_MAIN_LOAD1(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2
COND_1191_0_MAIN_LE1(TRUE, x1[5], x0[5], x2[5]) → 1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])
1191_0_MAIN_LE(x1[4], x0[4], x2[4]) → COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])
COND_1191_0_MAIN_LE1(TRUE, x1[5], x0[5], x2[5]) → 1155_0_MAIN_LOAD(+(x1[5], -1), x2[5], x0[5])
1155_0_MAIN_LOAD(x1[8], x2[8], x0[8]) → COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])
1155_0_MAIN_LOAD(x1[0], x2[0], x0[0]) → COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])
COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1]) → 1191_0_MAIN_LE(x1[1], x0[1], x2[1])
1191_0_MAIN_LE(x1[2], x0[2], x2[2]) → COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])
COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3]) → 1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])
1191_0_MAIN_LE(x1[4], x0[4], x2[4]) → COND_1191_0_MAIN_LE1(&&(>=(x2[4], x0[4]), <(x2[4], x1[4])), x1[4], x0[4], x2[4])
1191_0_MAIN_LE(x1[6], x0[6], x2[6]) → COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])
COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7]) → 1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))
1155_0_MAIN_LOAD(x1[8], x2[8], x0[8]) → COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])
COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9]) → 1191_0_MAIN_LE(x1[9], x0[9], x2[9])
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 |
Integer, Boolean
(3) -> (0), if (x1[3] →* x1[0]∧x2[3] →* x2[0]∧x0[3] →* x0[0])
(7) -> (0), if (x1[7] →* x1[0]∧x2[7] →* x2[0]∧x0[7] + -1 →* x0[0])
(0) -> (1), if (x2[0] < x0[0] ∧x1[0] →* x1[1]∧x2[0] →* x2[1]∧x0[0] →* x0[1])
(1) -> (2), if (x1[1] →* x1[2]∧x0[1] →* x0[2]∧x2[1] →* x2[2])
(9) -> (2), if (x1[9] →* x1[2]∧x0[9] →* x0[2]∧x2[9] →* x2[2])
(2) -> (3), if (x2[2] >= x1[2] && x2[2] >= x0[2] ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(1) -> (4), if (x1[1] →* x1[4]∧x0[1] →* x0[4]∧x2[1] →* x2[4])
(9) -> (4), if (x1[9] →* x1[4]∧x0[9] →* x0[4]∧x2[9] →* x2[4])
(1) -> (6), if (x1[1] →* x1[6]∧x0[1] →* x0[6]∧x2[1] →* x2[6])
(9) -> (6), if (x1[9] →* x1[6]∧x0[9] →* x0[6]∧x2[9] →* x2[6])
(6) -> (7), if (x2[6] < x0[6] ∧x1[6] →* x1[7]∧x0[6] →* x0[7]∧x2[6] →* x2[7])
(3) -> (8), if (x1[3] →* x1[8]∧x2[3] →* x2[8]∧x0[3] →* x0[8])
(7) -> (8), if (x1[7] →* x1[8]∧x2[7] →* x2[8]∧x0[7] + -1 →* x0[8])
(8) -> (9), if (x2[8] >= x0[8] && x2[8] < x1[8] ∧x1[8] →* x1[9]∧x2[8] →* x2[9]∧x0[8] →* x0[9])
!= | ~ | 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 (x1[3] →* x1[0]∧x2[3] →* x2[0]∧x0[3] →* x0[0])
(7) -> (0), if (x1[7] →* x1[0]∧x2[7] →* x2[0]∧x0[7] + -1 →* x0[0])
(0) -> (1), if (x2[0] < x0[0] ∧x1[0] →* x1[1]∧x2[0] →* x2[1]∧x0[0] →* x0[1])
(1) -> (2), if (x1[1] →* x1[2]∧x0[1] →* x0[2]∧x2[1] →* x2[2])
(9) -> (2), if (x1[9] →* x1[2]∧x0[9] →* x0[2]∧x2[9] →* x2[2])
(2) -> (3), if (x2[2] >= x1[2] && x2[2] >= x0[2] ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(1) -> (6), if (x1[1] →* x1[6]∧x0[1] →* x0[6]∧x2[1] →* x2[6])
(9) -> (6), if (x1[9] →* x1[6]∧x0[9] →* x0[6]∧x2[9] →* x2[6])
(6) -> (7), if (x2[6] < x0[6] ∧x1[6] →* x1[7]∧x0[6] →* x0[7]∧x2[6] →* x2[7])
(3) -> (8), if (x1[3] →* x1[8]∧x2[3] →* x2[8]∧x0[3] →* x0[8])
(7) -> (8), if (x1[7] →* x1[8]∧x2[7] →* x2[8]∧x0[7] + -1 →* x0[8])
(8) -> (9), if (x2[8] >= x0[8] && x2[8] < x1[8] ∧x1[8] →* x1[9]∧x2[8] →* x2[9]∧x0[8] →* x0[9])
(1) (<(x2[6], x0[6])=TRUE∧x1[6]=x1[7]∧x0[6]=x0[7]∧x2[6]=x2[7]∧x1[7]=x1[0]∧x2[7]=x2[0]∧+(x0[7], -1)=x0[0] ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(2) (<(x2[6], x0[6])=TRUE ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥1155_0_MAIN_LOAD(x1[6], x2[6], +(x0[6], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(3) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(4) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(5) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(6) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(7) (x0[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(8) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(9) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(10) (<(x2[6], x0[6])=TRUE∧x1[6]=x1[7]∧x0[6]=x0[7]∧x2[6]=x2[7]∧x1[7]=x1[8]∧x2[7]=x2[8]∧+(x0[7], -1)=x0[8] ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7])≥1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(11) (<(x2[6], x0[6])=TRUE ⇒ COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥NonInfC∧COND_1191_0_MAIN_LE2(TRUE, x1[6], x0[6], x2[6])≥1155_0_MAIN_LOAD(x1[6], x2[6], +(x0[6], -1))∧(UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥))
(12) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(13) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(14) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(15) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x2[6] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(16) (x0[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(17) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(18) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_34] + [bni_34]x0[6] ≥ 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(19) (<(x2[6], x0[6])=TRUE∧x1[6]=x1[7]∧x0[6]=x0[7]∧x2[6]=x2[7] ⇒ 1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥NonInfC∧1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])∧(UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥))
(20) (<(x2[6], x0[6])=TRUE ⇒ 1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥NonInfC∧1191_0_MAIN_LE(x1[6], x0[6], x2[6])≥COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])∧(UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥))
(21) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x2[6] + [bni_36]x0[6] ≥ 0∧[(-1)bso_37] ≥ 0)
(22) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x2[6] + [bni_36]x0[6] ≥ 0∧[(-1)bso_37] ≥ 0)
(23) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x2[6] + [bni_36]x0[6] ≥ 0∧[(-1)bso_37] ≥ 0)
(24) (x0[6] + [-1] + [-1]x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧0 = 0∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x2[6] + [bni_36]x0[6] ≥ 0∧0 = 0∧[(-1)bso_37] ≥ 0)
(25) (x0[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧0 = 0∧[(-1)Bound*bni_36] + [bni_36]x0[6] ≥ 0∧0 = 0∧[(-1)bso_37] ≥ 0)
(26) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧0 = 0∧[(-1)Bound*bni_36] + [bni_36]x0[6] ≥ 0∧0 = 0∧[(-1)bso_37] ≥ 0)
(27) (x0[6] ≥ 0∧x2[6] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])), ≥)∧0 = 0∧[(-1)Bound*bni_36] + [bni_36]x0[6] ≥ 0∧0 = 0∧[(-1)bso_37] ≥ 0)
(28) (x1[9]=x1[2]∧x0[9]=x0[2]∧x2[9]=x2[2] ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(29) (COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(30) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)
(31) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)
(32) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)
(33) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
(34) (x1[9]=x1[6]∧x0[9]=x0[6]∧x2[9]=x2[6] ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(35) (COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(36) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)
(37) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)
(38) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)
(39) ((UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[bni_38] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
(40) (&&(>=(x2[8], x0[8]), <(x2[8], x1[8]))=TRUE∧x1[8]=x1[9]∧x2[8]=x2[9]∧x0[8]=x0[9] ⇒ 1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥NonInfC∧1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])∧(UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥))
(41) (>=(x2[8], x0[8])=TRUE∧<(x2[8], x1[8])=TRUE ⇒ 1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥NonInfC∧1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])∧(UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥))
(42) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x0[8] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(43) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x0[8] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(44) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x0[8] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(45) (x2[8] ≥ 0∧x1[8] + [-1] + [-1]x0[8] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(46) (x2[8] ≥ 0∧x0[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(47) (x2[8] ≥ 0∧x0[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(48) (x2[8] ≥ 0∧x0[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x2[8] ≥ 0∧[(-1)bso_41] ≥ 0)
(49) (x1[3]=x1[0]∧x2[3]=x2[0]∧x0[3]=x0[0] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(50) (COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(51) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧[(-1)bso_43] ≥ 0)
(52) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧[(-1)bso_43] ≥ 0)
(53) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧[(-1)bso_43] ≥ 0)
(54) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)
(55) (x1[3]=x1[8]∧x2[3]=x2[8]∧x0[3]=x0[8] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(56) (COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(57) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧[(-1)bso_43] ≥ 0)
(58) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧[(-1)bso_43] ≥ 0)
(59) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧[(-1)bso_43] ≥ 0)
(60) ((UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_42] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)
(61) (&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3] ⇒ 1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(62) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ 1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(63) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x2[2] + [bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(64) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x2[2] + [bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(65) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x2[2] + [bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(66) (x2[2] ≥ 0∧x1[2] + x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x1[2] + [(-1)bni_44]x2[2] + [bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(67) (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(68) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(69) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]x0[2] ≥ 0∧[(-1)bso_45] ≥ 0)
(70) (x1[1]=x1[2]∧x0[1]=x0[2]∧x2[1]=x2[2] ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(71) (COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(72) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧[(-1)bso_47] ≥ 0)
(73) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧[(-1)bso_47] ≥ 0)
(74) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧[(-1)bso_47] ≥ 0)
(75) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
(76) (x1[1]=x1[6]∧x0[1]=x0[6]∧x2[1]=x2[6] ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(77) (COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(78) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧[(-1)bso_47] ≥ 0)
(79) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧[(-1)bso_47] ≥ 0)
(80) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧[(-1)bso_47] ≥ 0)
(81) ((UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[bni_46] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
(82) (<(x2[0], x0[0])=TRUE∧x1[0]=x1[1]∧x2[0]=x2[1]∧x0[0]=x0[1] ⇒ 1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥NonInfC∧1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])∧(UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥))
(83) (<(x2[0], x0[0])=TRUE ⇒ 1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥NonInfC∧1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])∧(UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥))
(84) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]x0[0] + [(-1)bni_48]x2[0] ≥ 0∧[(-1)bso_49] ≥ 0)
(85) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]x0[0] + [(-1)bni_48]x2[0] ≥ 0∧[(-1)bso_49] ≥ 0)
(86) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]x0[0] + [(-1)bni_48]x2[0] ≥ 0∧[(-1)bso_49] ≥ 0)
(87) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧0 = 0∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]x0[0] + [(-1)bni_48]x2[0] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)
(88) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧0 = 0∧[(-1)Bound*bni_48] + [bni_48]x0[0] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)
(89) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧0 = 0∧[(-1)Bound*bni_48] + [bni_48]x0[0] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)
(90) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧0 = 0∧[(-1)Bound*bni_48] + [bni_48]x0[0] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [1]
POL(COND_1191_0_MAIN_LE2(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(1155_0_MAIN_LOAD(x1, x2, x3)) = [-1] + x3 + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(1191_0_MAIN_LE(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(<(x1, x2)) = [-1]
POL(COND_1155_0_MAIN_LOAD1(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(COND_1191_0_MAIN_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(COND_1155_0_MAIN_LOAD(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3
COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7]) → 1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))
COND_1191_0_MAIN_LE2(TRUE, x1[7], x0[7], x2[7]) → 1155_0_MAIN_LOAD(x1[7], x2[7], +(x0[7], -1))
1191_0_MAIN_LE(x1[6], x0[6], x2[6]) → COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])
1155_0_MAIN_LOAD(x1[0], x2[0], x0[0]) → COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])
1191_0_MAIN_LE(x1[6], x0[6], x2[6]) → COND_1191_0_MAIN_LE2(<(x2[6], x0[6]), x1[6], x0[6], x2[6])
COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9]) → 1191_0_MAIN_LE(x1[9], x0[9], x2[9])
1155_0_MAIN_LOAD(x1[8], x2[8], x0[8]) → COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])
COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3]) → 1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])
1191_0_MAIN_LE(x1[2], x0[2], x2[2]) → COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])
COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1]) → 1191_0_MAIN_LE(x1[1], x0[1], x2[1])
1155_0_MAIN_LOAD(x1[0], x2[0], x0[0]) → COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])
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 |
Integer, Boolean
(3) -> (0), if (x1[3] →* x1[0]∧x2[3] →* x2[0]∧x0[3] →* x0[0])
(0) -> (1), if (x2[0] < x0[0] ∧x1[0] →* x1[1]∧x2[0] →* x2[1]∧x0[0] →* x0[1])
(1) -> (2), if (x1[1] →* x1[2]∧x0[1] →* x0[2]∧x2[1] →* x2[2])
(9) -> (2), if (x1[9] →* x1[2]∧x0[9] →* x0[2]∧x2[9] →* x2[2])
(2) -> (3), if (x2[2] >= x1[2] && x2[2] >= x0[2] ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(1) -> (6), if (x1[1] →* x1[6]∧x0[1] →* x0[6]∧x2[1] →* x2[6])
(9) -> (6), if (x1[9] →* x1[6]∧x0[9] →* x0[6]∧x2[9] →* x2[6])
(3) -> (8), if (x1[3] →* x1[8]∧x2[3] →* x2[8]∧x0[3] →* x0[8])
(8) -> (9), if (x2[8] >= x0[8] && x2[8] < x1[8] ∧x1[8] →* x1[9]∧x2[8] →* x2[9]∧x0[8] →* x0[9])
!= | ~ | 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 (x1[3] →* x1[0]∧x2[3] →* x2[0]∧x0[3] →* x0[0])
(0) -> (1), if (x2[0] < x0[0] ∧x1[0] →* x1[1]∧x2[0] →* x2[1]∧x0[0] →* x0[1])
(1) -> (2), if (x1[1] →* x1[2]∧x0[1] →* x0[2]∧x2[1] →* x2[2])
(9) -> (2), if (x1[9] →* x1[2]∧x0[9] →* x0[2]∧x2[9] →* x2[2])
(2) -> (3), if (x2[2] >= x1[2] && x2[2] >= x0[2] ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(3) -> (8), if (x1[3] →* x1[8]∧x2[3] →* x2[8]∧x0[3] →* x0[8])
(8) -> (9), if (x2[8] >= x0[8] && x2[8] < x1[8] ∧x1[8] →* x1[9]∧x2[8] →* x2[9]∧x0[8] →* x0[9])
(1) (&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧x1[3]=x1[8]∧x2[3]=x2[8]∧x0[3]=x0[8]∧&&(>=(x2[8], x0[8]), <(x2[8], x1[8]))=TRUE∧x1[8]=x1[9]∧x2[8]=x2[9]∧x0[8]=x0[9] ⇒ 1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥NonInfC∧1155_0_MAIN_LOAD(x1[8], x2[8], x0[8])≥COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])∧(UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥))
(2) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE∧<(x2[2], x1[2])=TRUE ⇒ 1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])≥NonInfC∧1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])≥COND_1155_0_MAIN_LOAD1(&&(>=(x2[2], x0[2]), <(x2[2], x1[2])), x1[2], x2[2], x0[2])∧(UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥))
(3) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x2[2] + [(-1)bni_14]x0[2] ≥ 0∧[-1 + (-1)bso_15] ≥ 0)
(4) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x2[2] + [(-1)bni_14]x0[2] ≥ 0∧[-1 + (-1)bso_15] ≥ 0)
(5) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0∧x1[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x2[2] + [(-1)bni_14]x0[2] ≥ 0∧[-1 + (-1)bso_15] ≥ 0)
(6) (x1[3]=x1[0]∧x2[3]=x2[0]∧x0[3]=x0[0]∧<(x2[0], x0[0])=TRUE∧x1[0]=x1[1]∧x2[0]=x2[1]∧x0[0]=x0[1]∧x1[1]=x1[2]∧x0[1]=x0[2]∧x2[1]=x2[2] ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1])≥1191_0_MAIN_LE(x1[1], x0[1], x2[1])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(7) (<(x2[0], x0[0])=TRUE ⇒ COND_1155_0_MAIN_LOAD(TRUE, x1[3], x2[0], x0[0])≥NonInfC∧COND_1155_0_MAIN_LOAD(TRUE, x1[3], x2[0], x0[0])≥1191_0_MAIN_LE(x1[3], x0[0], x2[0])∧(UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥))
(8) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]x2[0] + [(-1)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
(9) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]x2[0] + [(-1)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
(10) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]x2[0] + [(-1)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
(11) (x0[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧0 = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]x2[0] + [(-1)bni_16]x0[0] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(12) (x0[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧0 = 0∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x0[0] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(13) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧0 = 0∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x0[0] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(14) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[1], x0[1], x2[1])), ≥)∧0 = 0∧[(-2)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x0[0] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(15) (&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧x1[3]=x1[0]∧x2[3]=x2[0]∧x0[3]=x0[0]∧<(x2[0], x0[0])=TRUE∧x1[0]=x1[1]∧x2[0]=x2[1]∧x0[0]=x0[1] ⇒ 1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥NonInfC∧1155_0_MAIN_LOAD(x1[0], x2[0], x0[0])≥COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])∧(UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥))
(16) (<(x2[2], x0[2])=TRUE∧>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ 1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])≥NonInfC∧1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])≥COND_1155_0_MAIN_LOAD(<(x2[2], x0[2]), x1[2], x2[2], x0[2])∧(UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥))
(17) (x0[2] + [-1] + [-1]x2[2] ≥ 0∧x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x2[2] + [(-1)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(18) (x0[2] + [-1] + [-1]x2[2] ≥ 0∧x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x2[2] + [(-1)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(19) (x0[2] + [-1] + [-1]x2[2] ≥ 0∧x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x2[2] + [(-1)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(20) (x1[1]=x1[2]∧x0[1]=x0[2]∧x2[1]=x2[2]∧&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧x1[3]=x1[0]∧x2[3]=x2[0]∧x0[3]=x0[0] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(21) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(22) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(23) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(24) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(25) (x2[2] ≥ 0∧x1[2] + x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[2] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(26) (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(27) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(28) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(29) (x1[1]=x1[2]∧x0[1]=x0[2]∧x2[1]=x2[2]∧&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧x1[3]=x1[8]∧x2[3]=x2[8]∧x0[3]=x0[8] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(30) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(31) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(32) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(33) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(34) (x2[2] ≥ 0∧x1[2] + x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[2] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(35) (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(36) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(37) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(38) (x1[9]=x1[2]∧x0[9]=x0[2]∧x2[9]=x2[2]∧&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧x1[3]=x1[0]∧x2[3]=x2[0]∧x0[3]=x0[0] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(39) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(40) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(41) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(42) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(43) (x2[2] ≥ 0∧x1[2] + x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[2] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(44) (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(45) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(46) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(47) (x1[9]=x1[2]∧x0[9]=x0[2]∧x2[9]=x2[2]∧&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧x1[3]=x1[8]∧x2[3]=x2[8]∧x0[3]=x0[8] ⇒ COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3])≥1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(48) (>=(x2[2], x1[2])=TRUE∧>=(x2[2], x0[2])=TRUE ⇒ COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_1191_0_MAIN_LE(TRUE, x1[2], x0[2], x2[2])≥1155_0_MAIN_LOAD(x1[2], x2[2], x0[2])∧(UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥))
(49) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(50) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(51) (x2[2] + [-1]x1[2] ≥ 0∧x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(52) (x2[2] ≥ 0∧x1[2] + x2[2] + [-1]x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[2] + [bni_20]x2[2] + [(-1)bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(53) (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(54) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(55) (x2[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[2 + (-1)bso_21] ≥ 0)
(56) (<(x2[0], x0[0])=TRUE∧x1[0]=x1[1]∧x2[0]=x2[1]∧x0[0]=x0[1]∧x1[1]=x1[2]∧x0[1]=x0[2]∧x2[1]=x2[2]∧&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3] ⇒ 1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(57) (<(x2[0], x0[0])=TRUE∧>=(x2[0], x1[2])=TRUE∧>=(x2[0], x0[0])=TRUE ⇒ 1191_0_MAIN_LE(x1[2], x0[0], x2[0])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[0], x2[0])≥COND_1191_0_MAIN_LE(&&(>=(x2[0], x1[2]), >=(x2[0], x0[0])), x1[2], x0[0], x2[0])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(58) (x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] + [-1]x1[2] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[0] + [(-1)bni_22]x0[0] ≥ 0∧[-2 + (-1)bso_23] ≥ 0)
(59) (x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] + [-1]x1[2] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[0] + [(-1)bni_22]x0[0] ≥ 0∧[-2 + (-1)bso_23] ≥ 0)
(60) (x0[0] + [-1] + [-1]x2[0] ≥ 0∧x2[0] + [-1]x1[2] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[0] + [(-1)bni_22]x0[0] ≥ 0∧[-2 + (-1)bso_23] ≥ 0)
(61) (&&(>=(x2[8], x0[8]), <(x2[8], x1[8]))=TRUE∧x1[8]=x1[9]∧x2[8]=x2[9]∧x0[8]=x0[9]∧x1[9]=x1[2]∧x0[9]=x0[2]∧x2[9]=x2[2]∧&&(>=(x2[2], x1[2]), >=(x2[2], x0[2]))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3] ⇒ 1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥NonInfC∧1191_0_MAIN_LE(x1[2], x0[2], x2[2])≥COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(62) (>=(x2[8], x0[8])=TRUE∧<(x2[8], x1[8])=TRUE∧>=(x2[8], x1[8])=TRUE ⇒ 1191_0_MAIN_LE(x1[8], x0[8], x2[8])≥NonInfC∧1191_0_MAIN_LE(x1[8], x0[8], x2[8])≥COND_1191_0_MAIN_LE(&&(>=(x2[8], x1[8]), >=(x2[8], x0[8])), x1[8], x0[8], x2[8])∧(UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥))
(63) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0∧x2[8] + [-1]x1[8] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[8] + [(-1)bni_22]x0[8] ≥ 0∧[-2 + (-1)bso_23] ≥ 0)
(64) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0∧x2[8] + [-1]x1[8] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[8] + [(-1)bni_22]x0[8] ≥ 0∧[-2 + (-1)bso_23] ≥ 0)
(65) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0∧x2[8] + [-1]x1[8] ≥ 0 ⇒ (UIncreasing(COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[8] + [(-1)bni_22]x0[8] ≥ 0∧[-2 + (-1)bso_23] ≥ 0)
(66) (x1[3]=x1[8]∧x2[3]=x2[8]∧x0[3]=x0[8]∧&&(>=(x2[8], x0[8]), <(x2[8], x1[8]))=TRUE∧x1[8]=x1[9]∧x2[8]=x2[9]∧x0[8]=x0[9]∧x1[9]=x1[2]∧x0[9]=x0[2]∧x2[9]=x2[2] ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9])≥1191_0_MAIN_LE(x1[9], x0[9], x2[9])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(67) (>=(x2[8], x0[8])=TRUE∧<(x2[8], x1[8])=TRUE ⇒ COND_1155_0_MAIN_LOAD1(TRUE, x1[8], x2[8], x0[8])≥NonInfC∧COND_1155_0_MAIN_LOAD1(TRUE, x1[8], x2[8], x0[8])≥1191_0_MAIN_LE(x1[8], x0[8], x2[8])∧(UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥))
(68) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] + [(-1)bni_24]x0[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(69) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] + [(-1)bni_24]x0[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(70) (x2[8] + [-1]x0[8] ≥ 0∧x1[8] + [-1] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] + [(-1)bni_24]x0[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(71) (x2[8] ≥ 0∧x1[8] + [-1] + [-1]x0[8] + [-1]x2[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(72) (x2[8] ≥ 0∧x0[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(73) (x2[8] ≥ 0∧x0[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(74) (x2[8] ≥ 0∧x0[8] ≥ 0∧x1[8] ≥ 0 ⇒ (UIncreasing(1191_0_MAIN_LE(x1[9], x0[9], x2[9])), ≥)∧[(-1)Bound*bni_24] + [bni_24]x2[8] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1155_0_MAIN_LOAD(x1, x2, x3)) = [-1] + x2 + [-1]x3
POL(COND_1155_0_MAIN_LOAD1(x1, x2, x3, x4)) = x3 + [-1]x4
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(<(x1, x2)) = [-1]
POL(COND_1155_0_MAIN_LOAD(x1, x2, x3, x4)) = [-1] + x3 + [-1]x4
POL(1191_0_MAIN_LE(x1, x2, x3)) = [-1] + x3 + [-1]x2
POL(COND_1191_0_MAIN_LE(x1, x2, x3, x4)) = [1] + x4 + [-1]x3
1155_0_MAIN_LOAD(x1[8], x2[8], x0[8]) → COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])
1155_0_MAIN_LOAD(x1[0], x2[0], x0[0]) → COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])
COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3]) → 1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])
1191_0_MAIN_LE(x1[2], x0[2], x2[2]) → COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])
COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9]) → 1191_0_MAIN_LE(x1[9], x0[9], x2[9])
1155_0_MAIN_LOAD(x1[8], x2[8], x0[8]) → COND_1155_0_MAIN_LOAD1(&&(>=(x2[8], x0[8]), <(x2[8], x1[8])), x1[8], x2[8], x0[8])
1155_0_MAIN_LOAD(x1[0], x2[0], x0[0]) → COND_1155_0_MAIN_LOAD(<(x2[0], x0[0]), x1[0], x2[0], x0[0])
COND_1191_0_MAIN_LE(TRUE, x1[3], x0[3], x2[3]) → 1155_0_MAIN_LOAD(x1[3], x2[3], x0[3])
1191_0_MAIN_LE(x1[2], x0[2], x2[2]) → COND_1191_0_MAIN_LE(&&(>=(x2[2], x1[2]), >=(x2[2], x0[2])), x1[2], x0[2], x2[2])
COND_1155_0_MAIN_LOAD1(TRUE, x1[9], x2[9], x0[9]) → 1191_0_MAIN_LE(x1[9], x0[9], x2[9])
COND_1155_0_MAIN_LOAD(TRUE, x1[1], x2[1], x0[1]) → 1191_0_MAIN_LE(x1[1], x0[1], x2[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 |