0 JBC
↳1 JBCToGraph (⇒, 2228 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 5 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 403 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 3519 ms)
↳9 IDP
↳10 IDependencyGraphProof (⇔, 0 ms)
↳11 TRUE
↳12 JBCTerminationSCC
↳13 SCCToIntTRSProof (⇒, 92 ms)
↳14 intTRS
↳15 PolynomialOrderProcessor (⇔, 3 ms)
↳16 YES
↳17 JBCTerminationSCC
↳18 SCCToIntTRSProof (⇒, 531 ms)
↳19 intTRS
↳20 PolynomialOrderProcessor (⇔, 0 ms)
↳21 YES
↳22 JBCTerminationSCC
↳23 SCCToIDPv1Proof (⇒, 1080 ms)
↳24 IDP
↳25 IDPNonInfProof (⇒, 689 ms)
↳26 AND
↳27 IDP
↳28 IDependencyGraphProof (⇔, 0 ms)
↳29 TRUE
↳30 IDP
↳31 IDependencyGraphProof (⇔, 0 ms)
↳32 TRUE
↳33 JBCTerminationSCC
↳34 SCCToIntTRSProof (⇒, 100 ms)
↳35 intTRS
↳36 PolynomialOrderProcessor (⇔, 0 ms)
↳37 YES
public class TriTas {
static int N;
static int[] a;
static int nTas = 0;
static void Ajouter(int v) {
int i,j;
nTas++;
i = nTas - 1;
while (i > 0 && a[(i - 1)/2] <= v){
a[i] = a[(i - 1)/2];
j = (i - 1)/2;
if (j >= i) break; else i = j;
}
a[i] = v;
}
static int Maximum() {
return a[0];
}
static void Supprimer() {
int i, j, v;
a[0] = a[nTas - 1];
nTas--;
i = 0; v = a[0];
while (2 * i + 1 < nTas)
{
j = 2*i + 1;
if (j + 1 < nTas)
if (a[j + 1] > a[j])
j++;
if (v >= a[j]) break;
a[i] = a[j];
i = j;
}
a[i] = v;
}
static void HeapSort(){
int i, v;
nTas = 0;
for (i = 0; i < N; i++)
Ajouter(a[i]);
for (i = N - 1; i >= 0; i--)
{
v = Maximum();
Supprimer();
a[i]=v;
}
}
public static void main(String[] args){
Random.args = args;
N = args.length;
a = new int[N];
for (int i = 0; i < N; i++)
a[i] = Random.random();
//for (int i = 0; i < N; i++)
// System.out.print(a[i]+" ");
//System.out.println();
HeapSort();
//for (int i = 0; i < N; i++)
// System.out.print(a[i]+" ");
//System.out.println();
}
}
public class Random {
static String[] args;
static int index = 0;
public static int random() {
if (index >= args.length)
return 0;
String string = args[index];
index++;
return string.length();
}
}
Generated 61 rules for P and 0 rules for R.
P rules:
f11075_0_Supprimer_Load(EOS(STATIC_11075(i1756)), i2440, i1245, matching1) → f11077_0_Supprimer_IntArithmetic(EOS(STATIC_11077(i1756)), i2440, i1245, 2, i2440) | =(matching1, 2)
f11077_0_Supprimer_IntArithmetic(EOS(STATIC_11077(i1756)), i2440, i1245, matching1, i2440) → f11078_0_Supprimer_ConstantStackPush(EOS(STATIC_11078(i1756)), i2440, i1245, *(2, i2440)) | =(matching1, 2)
f11078_0_Supprimer_ConstantStackPush(EOS(STATIC_11078(i1756)), i2440, i1245, i2442) → f11080_0_Supprimer_IntArithmetic(EOS(STATIC_11080(i1756)), i2440, i1245, i2442, 1)
f11080_0_Supprimer_IntArithmetic(EOS(STATIC_11080(i1756)), i2440, i1245, i2442, matching1) → f11082_0_Supprimer_FieldAccess(EOS(STATIC_11082(i1756)), i2440, i1245, +(i2442, 1)) | &&(>=(i2442, 0), =(matching1, 1))
f11082_0_Supprimer_FieldAccess(EOS(STATIC_11082(i1756)), i2440, i1245, i2444) → f11084_0_Supprimer_GE(EOS(STATIC_11084(i1756)), i2440, i1245, i2444, i1756)
f11084_0_Supprimer_GE(EOS(STATIC_11084(i1756)), i2440, i1245, i2444, i1756) → f11087_0_Supprimer_GE(EOS(STATIC_11087(i1756)), i2440, i1245, i2444, i1756)
f11087_0_Supprimer_GE(EOS(STATIC_11087(i1756)), i2440, i1245, i2444, i1756) → f11091_0_Supprimer_ConstantStackPush(EOS(STATIC_11091(i1756)), i2440, i1245) | <(i2444, i1756)
f11091_0_Supprimer_ConstantStackPush(EOS(STATIC_11091(i1756)), i2440, i1245) → f11094_0_Supprimer_Load(EOS(STATIC_11094(i1756)), i2440, i1245, 2)
f11094_0_Supprimer_Load(EOS(STATIC_11094(i1756)), i2440, i1245, matching1) → f11097_0_Supprimer_IntArithmetic(EOS(STATIC_11097(i1756)), i2440, i1245, 2, i2440) | =(matching1, 2)
f11097_0_Supprimer_IntArithmetic(EOS(STATIC_11097(i1756)), i2440, i1245, matching1, i2440) → f11101_0_Supprimer_ConstantStackPush(EOS(STATIC_11101(i1756)), i2440, i1245, *(2, i2440)) | =(matching1, 2)
f11101_0_Supprimer_ConstantStackPush(EOS(STATIC_11101(i1756)), i2440, i1245, i2445) → f11105_0_Supprimer_IntArithmetic(EOS(STATIC_11105(i1756)), i2440, i1245, i2445, 1)
f11105_0_Supprimer_IntArithmetic(EOS(STATIC_11105(i1756)), i2440, i1245, i2445, matching1) → f11111_0_Supprimer_Store(EOS(STATIC_11111(i1756)), i2440, i1245, +(i2445, 1)) | &&(>=(i2445, 0), =(matching1, 1))
f11111_0_Supprimer_Store(EOS(STATIC_11111(i1756)), i2440, i1245, i2446) → f11115_0_Supprimer_Load(EOS(STATIC_11115(i1756)), i2440, i2446, i1245)
f11115_0_Supprimer_Load(EOS(STATIC_11115(i1756)), i2440, i2446, i1245) → f11137_0_Supprimer_ConstantStackPush(EOS(STATIC_11137(i1756)), i2440, i2446, i1245, i2446)
f11137_0_Supprimer_ConstantStackPush(EOS(STATIC_11137(i1756)), i2440, i2446, i1245, i2446) → f11141_0_Supprimer_IntArithmetic(EOS(STATIC_11141(i1756)), i2440, i2446, i1245, i2446, 1)
f11141_0_Supprimer_IntArithmetic(EOS(STATIC_11141(i1756)), i2440, i2446, i1245, i2446, matching1) → f11143_0_Supprimer_FieldAccess(EOS(STATIC_11143(i1756)), i2440, i2446, i1245, +(i2446, 1)) | &&(>(i2446, 0), =(matching1, 1))
f11143_0_Supprimer_FieldAccess(EOS(STATIC_11143(i1756)), i2440, i2446, i1245, i2465) → f11156_0_Supprimer_GE(EOS(STATIC_11156(i1756)), i2440, i2446, i1245, i2465, i1756)
f11156_0_Supprimer_GE(EOS(STATIC_11156(i1756)), i2440, i2446, i1245, i2465, i1756) → f11161_0_Supprimer_GE(EOS(STATIC_11161(i1756)), i2440, i2446, i1245, i2465, i1756)
f11156_0_Supprimer_GE(EOS(STATIC_11156(i1756)), i2440, i2446, i1245, i2465, i1756) → f11162_0_Supprimer_GE(EOS(STATIC_11162(i1756)), i2440, i2446, i1245, i2465, i1756)
f11161_0_Supprimer_GE(EOS(STATIC_11161(i1756)), i2440, i2446, i1245, i2465, i1756) → f11165_0_Supprimer_Load(EOS(STATIC_11165(i1756)), i2440, i2446, i1245) | >=(i2465, i1756)
f11165_0_Supprimer_Load(EOS(STATIC_11165(i1756)), i2440, i2446, i1245) → f11326_0_Supprimer_Load(EOS(STATIC_11326(i1756)), i2440, i2446, i1245)
f11326_0_Supprimer_Load(EOS(STATIC_11326(i1756)), i2440, i2446, i1245) → f11345_0_Supprimer_FieldAccess(EOS(STATIC_11345(i1756)), i2440, i2446, i1245, i1245)
f11345_0_Supprimer_FieldAccess(EOS(STATIC_11345(i1756)), i2440, i2446, i1245, i1245) → f11354_0_Supprimer_Load(EOS(STATIC_11354(i1756)), i2440, i2446, i1245, i1245, java.lang.Object(ARRAY(i1755)))
f11354_0_Supprimer_Load(EOS(STATIC_11354(i1756)), i2440, i2446, i1245, i1245, java.lang.Object(ARRAY(i1755))) → f11383_0_Supprimer_ArrayAccess(EOS(STATIC_11383(i1756)), i2440, i2446, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2446)
f11383_0_Supprimer_ArrayAccess(EOS(STATIC_11383(i1756)), i2440, i2446, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2446) → f11397_0_Supprimer_ArrayAccess(EOS(STATIC_11397(i1756)), i2440, i2446, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2446)
f11397_0_Supprimer_ArrayAccess(EOS(STATIC_11397(i1756)), i2440, i2446, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2446) → f11407_0_Supprimer_LT(EOS(STATIC_11407(i1756)), i2440, i2446, i1245, i1245, i2546) | <(i2446, i1755)
f11407_0_Supprimer_LT(EOS(STATIC_11407(i1756)), i2440, i2446, i1245, i1245, i2546) → f11427_0_Supprimer_LT(EOS(STATIC_11427(i1756)), i2440, i2446, i1245, i1245, i2546)
f11427_0_Supprimer_LT(EOS(STATIC_11427(i1756)), i2440, i2446, i1245, i1245, i2546) → f11441_0_Supprimer_FieldAccess(EOS(STATIC_11441(i1756)), i2440, i2446, i1245) | <(i1245, i2546)
f11441_0_Supprimer_FieldAccess(EOS(STATIC_11441(i1756)), i2440, i2446, i1245) → f11458_0_Supprimer_Load(EOS(STATIC_11458(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)))
f11458_0_Supprimer_Load(EOS(STATIC_11458(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755))) → f11474_0_Supprimer_FieldAccess(EOS(STATIC_11474(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440)
f11474_0_Supprimer_FieldAccess(EOS(STATIC_11474(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440) → f11493_0_Supprimer_Load(EOS(STATIC_11493(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440, java.lang.Object(ARRAY(i1755)))
f11493_0_Supprimer_Load(EOS(STATIC_11493(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440, java.lang.Object(ARRAY(i1755))) → f11511_0_Supprimer_ArrayAccess(EOS(STATIC_11511(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440, java.lang.Object(ARRAY(i1755)), i2446)
f11511_0_Supprimer_ArrayAccess(EOS(STATIC_11511(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440, java.lang.Object(ARRAY(i1755)), i2446) → f11523_0_Supprimer_ArrayAccess(EOS(STATIC_11523(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440, java.lang.Object(ARRAY(i1755)), i2446)
f11523_0_Supprimer_ArrayAccess(EOS(STATIC_11523(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440, java.lang.Object(ARRAY(i1755)), i2446) → f11544_0_Supprimer_ArrayAccess(EOS(STATIC_11544(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440) | <(i2446, i1755)
f11544_0_Supprimer_ArrayAccess(EOS(STATIC_11544(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440) → f11584_0_Supprimer_ArrayAccess(EOS(STATIC_11584(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440)
f11584_0_Supprimer_ArrayAccess(EOS(STATIC_11584(i1756)), i2446, i1245, java.lang.Object(ARRAY(i1755)), i2440) → f11612_0_Supprimer_Load(EOS(STATIC_11612(i1756)), i2446, i1245) | <(i2440, i1755)
f11612_0_Supprimer_Load(EOS(STATIC_11612(i1756)), i2446, i1245) → f11681_0_Supprimer_Store(EOS(STATIC_11681(i1756)), i1245, i2446)
f11681_0_Supprimer_Store(EOS(STATIC_11681(i1756)), i1245, i2446) → f11726_0_Supprimer_JMP(EOS(STATIC_11726(i1756)), i2446, i1245)
f11726_0_Supprimer_JMP(EOS(STATIC_11726(i1756)), i2446, i1245) → f11770_0_Supprimer_ConstantStackPush(EOS(STATIC_11770(i1756)), i2446, i1245)
f11770_0_Supprimer_ConstantStackPush(EOS(STATIC_11770(i1756)), i2446, i1245) → f11063_0_Supprimer_ConstantStackPush(EOS(STATIC_11063(i1756)), i2446, i1245)
f11063_0_Supprimer_ConstantStackPush(EOS(STATIC_11063(i1756)), i2440, i1245) → f11075_0_Supprimer_Load(EOS(STATIC_11075(i1756)), i2440, i1245, 2)
f11162_0_Supprimer_GE(EOS(STATIC_11162(i1756)), i2440, i2446, i1245, i2465, i1756) → f11167_0_Supprimer_FieldAccess(EOS(STATIC_11167(i1756)), i2440, i2446, i1245) | <(i2465, i1756)
f11167_0_Supprimer_FieldAccess(EOS(STATIC_11167(i1756)), i2440, i2446, i1245) → f11183_0_Supprimer_Load(EOS(STATIC_11183(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)))
f11183_0_Supprimer_Load(EOS(STATIC_11183(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755))) → f11190_0_Supprimer_ConstantStackPush(EOS(STATIC_11190(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2446)
f11190_0_Supprimer_ConstantStackPush(EOS(STATIC_11190(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2446) → f11195_0_Supprimer_IntArithmetic(EOS(STATIC_11195(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2446, 1)
f11195_0_Supprimer_IntArithmetic(EOS(STATIC_11195(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2446, matching1) → f11210_0_Supprimer_ArrayAccess(EOS(STATIC_11210(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), +(i2446, 1)) | &&(>(i2446, 0), =(matching1, 1))
f11210_0_Supprimer_ArrayAccess(EOS(STATIC_11210(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2480) → f11220_0_Supprimer_ArrayAccess(EOS(STATIC_11220(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2480)
f11220_0_Supprimer_ArrayAccess(EOS(STATIC_11220(i1756)), i2440, i2446, i1245, java.lang.Object(ARRAY(i1755)), i2480) → f11227_0_Supprimer_FieldAccess(EOS(STATIC_11227(i1756)), i2440, i2446, i1245, i2482) | <(i2480, i1755)
f11227_0_Supprimer_FieldAccess(EOS(STATIC_11227(i1756)), i2440, i2446, i1245, i2482) → f11257_0_Supprimer_Load(EOS(STATIC_11257(i1756)), i2440, i2446, i1245, i2482, java.lang.Object(ARRAY(i1755)))
f11257_0_Supprimer_Load(EOS(STATIC_11257(i1756)), i2440, i2446, i1245, i2482, java.lang.Object(ARRAY(i1755))) → f11275_0_Supprimer_ArrayAccess(EOS(STATIC_11275(i1756)), i2440, i2446, i1245, i2482, java.lang.Object(ARRAY(i1755)), i2446)
f11275_0_Supprimer_ArrayAccess(EOS(STATIC_11275(i1756)), i2440, i2446, i1245, i2482, java.lang.Object(ARRAY(i1755)), i2446) → f11285_0_Supprimer_ArrayAccess(EOS(STATIC_11285(i1756)), i2440, i2446, i1245, i2482, java.lang.Object(ARRAY(i1755)), i2446)
f11285_0_Supprimer_ArrayAccess(EOS(STATIC_11285(i1756)), i2440, i2446, i1245, i2482, java.lang.Object(ARRAY(i1755)), i2446) → f11298_0_Supprimer_LE(EOS(STATIC_11298(i1756)), i2440, i2446, i1245, i2482, i2509) | <(i2446, i1755)
f11298_0_Supprimer_LE(EOS(STATIC_11298(i1756)), i2440, i2446, i1245, i2482, i2509) → f11308_0_Supprimer_LE(EOS(STATIC_11308(i1756)), i2440, i2446, i1245, i2482, i2509)
f11298_0_Supprimer_LE(EOS(STATIC_11298(i1756)), i2440, i2446, i1245, i2482, i2509) → f11309_0_Supprimer_LE(EOS(STATIC_11309(i1756)), i2440, i2446, i1245, i2482, i2509)
f11308_0_Supprimer_LE(EOS(STATIC_11308(i1756)), i2440, i2446, i1245, i2482, i2509) → f11326_0_Supprimer_Load(EOS(STATIC_11326(i1756)), i2440, i2446, i1245) | <=(i2482, i2509)
f11309_0_Supprimer_LE(EOS(STATIC_11309(i1756)), i2440, i2446, i1245, i2482, i2509) → f11329_0_Supprimer_Inc(EOS(STATIC_11329(i1756)), i2440, i2446, i1245) | >(i2482, i2509)
f11329_0_Supprimer_Inc(EOS(STATIC_11329(i1756)), i2440, i2446, i1245) → f11348_0_Supprimer_Load(EOS(STATIC_11348(i1756)), i2440, +(i2446, 1), i1245) | >(i2446, 0)
f11348_0_Supprimer_Load(EOS(STATIC_11348(i1756)), i2440, i2520, i1245) → f11357_0_Supprimer_FieldAccess(EOS(STATIC_11357(i1756)), i2440, i2520, i1245, i1245)
f11357_0_Supprimer_FieldAccess(EOS(STATIC_11357(i1756)), i2440, i2520, i1245, i1245) → f11386_0_Supprimer_Load(EOS(STATIC_11386(i1756)), i2440, i2520, i1245, i1245, java.lang.Object(ARRAY(i1755)))
f11386_0_Supprimer_Load(EOS(STATIC_11386(i1756)), i2440, i2520, i1245, i1245, java.lang.Object(ARRAY(i1755))) → f11403_0_Supprimer_ArrayAccess(EOS(STATIC_11403(i1756)), i2440, i2520, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2520)
f11403_0_Supprimer_ArrayAccess(EOS(STATIC_11403(i1756)), i2440, i2520, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2520) → f11383_0_Supprimer_ArrayAccess(EOS(STATIC_11383(i1756)), i2440, i2520, i1245, i1245, java.lang.Object(ARRAY(i1755)), i2520)
R rules:
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
f11075_0_Supprimer_Load(EOS(STATIC_11075(x0)), x1, x2, 2) → f11075_0_Supprimer_Load(EOS(STATIC_11075(x0)), +(*(2, x1), 1), x2, 2) | &&(&&(>(x0, +(*(2, x1), 1)), <=(x0, +(*(2, x1), 2))), >=(*(2, x1), 0))
f11075_0_Supprimer_Load(EOS(STATIC_11075(x0)), x1, x2, 2) → f11075_0_Supprimer_Load(EOS(STATIC_11075(x0)), +(*(2, x1), 1), x2, 2) | &&(&&(>(x0, +(*(2, x1), 2)), >(x0, +(*(2, x1), 1))), >=(*(2, x1), 0))
f11075_0_Supprimer_Load(EOS(STATIC_11075(x0)), x1, x2, 2) → f11075_0_Supprimer_Load(EOS(STATIC_11075(x0)), +(*(2, x1), 2), x2, 2) | &&(&&(>(x0, +(*(2, x1), 2)), >(x0, +(*(2, x1), 1))), >=(*(2, x1), 0))
R rules:
Filtered ground terms:
f11075_0_Supprimer_Load(x1, x2, x3, x4) → f11075_0_Supprimer_Load(x1, x2, x3)
Cond_f11075_0_Supprimer_Load(x1, x2, x3, x4, x5) → Cond_f11075_0_Supprimer_Load(x1, x2, x3, x4)
Cond_f11075_0_Supprimer_Load1(x1, x2, x3, x4, x5) → Cond_f11075_0_Supprimer_Load1(x1, x2, x3, x4)
Cond_f11075_0_Supprimer_Load2(x1, x2, x3, x4, x5) → Cond_f11075_0_Supprimer_Load2(x1, x2, x3, x4)
Filtered unneeded arguments:
Cond_f11075_0_Supprimer_Load(x1, x2, x3, x4) → Cond_f11075_0_Supprimer_Load(x1, x2, x3)
Cond_f11075_0_Supprimer_Load1(x1, x2, x3, x4) → Cond_f11075_0_Supprimer_Load1(x1, x2, x3)
Cond_f11075_0_Supprimer_Load2(x1, x2, x3, x4) → Cond_f11075_0_Supprimer_Load2(x1, x2, x3)
f11075_0_Supprimer_Load(x1, x2, x3) → f11075_0_Supprimer_Load(x1, x2)
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
F11075_0_SUPPRIMER_LOAD(EOS(STATIC_11075(x0)), x1) → F11075_0_SUPPRIMER_LOAD(EOS(STATIC_11075(x0)), +(*(2, x1), 1)) | &&(&&(>(x0, +(*(2, x1), 1)), >=(*(2, x1), 0)), <=(x0, +(*(2, x1), 2)))
F11075_0_SUPPRIMER_LOAD(EOS(STATIC_11075(x0)), x1) → F11075_0_SUPPRIMER_LOAD(EOS(STATIC_11075(x0)), +(*(2, x1), 1)) | &&(&&(>(x0, +(*(2, x1), 2)), >=(*(2, x1), 0)), >(x0, +(*(2, x1), 1)))
F11075_0_SUPPRIMER_LOAD(EOS(STATIC_11075(x0)), x1) → F11075_0_SUPPRIMER_LOAD(EOS(STATIC_11075(x0)), +(*(2, x1), 2)) | &&(&&(>(x0, +(*(2, x1), 2)), >=(*(2, x1), 0)), >(x0, +(*(2, x1), 1)))
R rules:
Finished conversion. Obtained 6 rules for P and 0 rules for R. System has predefined symbols.
P rules:
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0)), x1) → COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0, +(*(2, x1), 1)), >=(*(2, x1), 0)), <=(x0, +(*(2, x1), 2))), EOS(STATIC_11075(x0)), x1)
COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0)), x1) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0)), +(*(2, x1), 1))
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0)), x1) → COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0, +(*(2, x1), 2)), >=(*(2, x1), 0)), >(x0, +(*(2, x1), 1))), EOS(STATIC_11075(x0)), x1)
COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0)), x1) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0)), +(*(2, x1), 1))
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0)), x1) → COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0, +(*(2, x1), 2)), >=(*(2, x1), 0)), >(x0, +(*(2, x1), 1))), EOS(STATIC_11075(x0)), x1)
COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0)), x1) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0)), +(*(2, x1), 2))
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 |
Boolean, Integer
(0) -> (1), if (x0[0] > 2 * x1[0] + 1 && 2 * x1[0] >= 0 && x0[0] <= 2 * x1[0] + 2 ∧EOS(STATIC_11075(x0[0])) →* EOS(STATIC_11075(x0[1]))∧x1[0] →* x1[1])
(1) -> (0), if (EOS(STATIC_11075(x0[1])) →* EOS(STATIC_11075(x0[0]))∧2 * x1[1] + 1 →* x1[0])
(1) -> (2), if (EOS(STATIC_11075(x0[1])) →* EOS(STATIC_11075(x0[2]))∧2 * x1[1] + 1 →* x1[2])
(1) -> (4), if (EOS(STATIC_11075(x0[1])) →* EOS(STATIC_11075(x0[4]))∧2 * x1[1] + 1 →* x1[4])
(2) -> (3), if (x0[2] > 2 * x1[2] + 2 && 2 * x1[2] >= 0 && x0[2] > 2 * x1[2] + 1 ∧EOS(STATIC_11075(x0[2])) →* EOS(STATIC_11075(x0[3]))∧x1[2] →* x1[3])
(3) -> (0), if (EOS(STATIC_11075(x0[3])) →* EOS(STATIC_11075(x0[0]))∧2 * x1[3] + 1 →* x1[0])
(3) -> (2), if (EOS(STATIC_11075(x0[3])) →* EOS(STATIC_11075(x0[2]))∧2 * x1[3] + 1 →* x1[2])
(3) -> (4), if (EOS(STATIC_11075(x0[3])) →* EOS(STATIC_11075(x0[4]))∧2 * x1[3] + 1 →* x1[4])
(4) -> (5), if (x0[4] > 2 * x1[4] + 2 && 2 * x1[4] >= 0 && x0[4] > 2 * x1[4] + 1 ∧EOS(STATIC_11075(x0[4])) →* EOS(STATIC_11075(x0[5]))∧x1[4] →* x1[5])
(5) -> (0), if (EOS(STATIC_11075(x0[5])) →* EOS(STATIC_11075(x0[0]))∧2 * x1[5] + 2 →* x1[0])
(5) -> (2), if (EOS(STATIC_11075(x0[5])) →* EOS(STATIC_11075(x0[2]))∧2 * x1[5] + 2 →* x1[2])
(5) -> (4), if (EOS(STATIC_11075(x0[5])) →* EOS(STATIC_11075(x0[4]))∧2 * x1[5] + 2 →* x1[4])
(1) (&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2)))=TRUE∧EOS(STATIC_11075(x0[0]))=EOS(STATIC_11075(x0[1]))∧x1[0]=x1[1] ⇒ F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), x1[0])≥NonInfC∧F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), x1[0])≥COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])∧(UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥))
(2) (<=(x0[0], +(*(2, x1[0]), 2))=TRUE∧>(x0[0], +(*(2, x1[0]), 1))=TRUE∧>=(*(2, x1[0]), 0)=TRUE ⇒ F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), x1[0])≥NonInfC∧F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), x1[0])≥COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])∧(UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥))
(3) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(4) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(5) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(6) ([-1]x0[0] ≥ 0∧x0[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]x1[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(7) (0 ≥ 0∧0 ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]x1[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(8) (0 ≥ 0∧0 ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]x1[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(9) (&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2)))=TRUE∧EOS(STATIC_11075(x0[0]))=EOS(STATIC_11075(x0[1]))∧x1[0]=x1[1]∧EOS(STATIC_11075(x0[1]))=EOS(STATIC_11075(x0[0]1))∧+(*(2, x1[1]), 1)=x1[0]1 ⇒ COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥))
(10) (<=(x0[0], +(*(2, x1[0]), 2))=TRUE∧>(x0[0], +(*(2, x1[0]), 1))=TRUE∧>=(*(2, x1[0]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[0])), x1[0])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[0])), x1[0])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), +(*(2, x1[0]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥))
(11) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(12) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(13) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(14) ([-1]x0[0] ≥ 0∧x0[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(15) (0 ≥ 0∧0 ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(16) (0 ≥ 0∧0 ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(17) (&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2)))=TRUE∧EOS(STATIC_11075(x0[0]))=EOS(STATIC_11075(x0[1]))∧x1[0]=x1[1]∧EOS(STATIC_11075(x0[1]))=EOS(STATIC_11075(x0[2]))∧+(*(2, x1[1]), 1)=x1[2] ⇒ COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥))
(18) (<=(x0[0], +(*(2, x1[0]), 2))=TRUE∧>(x0[0], +(*(2, x1[0]), 1))=TRUE∧>=(*(2, x1[0]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[0])), x1[0])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[0])), x1[0])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), +(*(2, x1[0]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥))
(19) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(20) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(21) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(22) ([-1]x0[0] ≥ 0∧x0[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(23) (0 ≥ 0∧0 ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(24) (0 ≥ 0∧0 ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(25) (&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2)))=TRUE∧EOS(STATIC_11075(x0[0]))=EOS(STATIC_11075(x0[1]))∧x1[0]=x1[1]∧EOS(STATIC_11075(x0[1]))=EOS(STATIC_11075(x0[4]))∧+(*(2, x1[1]), 1)=x1[4] ⇒ COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥))
(26) (<=(x0[0], +(*(2, x1[0]), 2))=TRUE∧>(x0[0], +(*(2, x1[0]), 1))=TRUE∧>=(*(2, x1[0]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[0])), x1[0])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[0])), x1[0])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), +(*(2, x1[0]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥))
(27) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(28) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(29) ([2]x1[0] + [2] + [-1]x0[0] ≥ 0∧x0[0] + [-2] + [-2]x1[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(30) ([-1]x0[0] ≥ 0∧x0[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(31) (0 ≥ 0∧0 ≥ 0∧[2]x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(32) (0 ≥ 0∧0 ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))), ≥)∧[(3)bni_28 + (-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧[1 + (-1)bso_29] + x1[0] ≥ 0)
(33) (&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1)))=TRUE∧EOS(STATIC_11075(x0[2]))=EOS(STATIC_11075(x0[3]))∧x1[2]=x1[3] ⇒ F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), x1[2])≥NonInfC∧F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), x1[2])≥COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])∧(UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥))
(34) (>(x0[2], +(*(2, x1[2]), 1))=TRUE∧>(x0[2], +(*(2, x1[2]), 2))=TRUE∧>=(*(2, x1[2]), 0)=TRUE ⇒ F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), x1[2])≥NonInfC∧F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), x1[2])≥COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])∧(UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥))
(35) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[2] + [bni_30]x0[2] ≥ 0∧[(-1)bso_31] ≥ 0)
(36) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[2] + [bni_30]x0[2] ≥ 0∧[(-1)bso_31] ≥ 0)
(37) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[2] + [bni_30]x0[2] ≥ 0∧[(-1)bso_31] ≥ 0)
(38) (x0[2] ≥ 0∧[-1] + x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥)∧[(3)bni_30 + (-1)Bound*bni_30] + [bni_30]x1[2] + [bni_30]x0[2] ≥ 0∧[(-1)bso_31] ≥ 0)
(39) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥)∧[(4)bni_30 + (-1)Bound*bni_30] + [bni_30]x1[2] + [bni_30]x0[2] ≥ 0∧[(-1)bso_31] ≥ 0)
(40) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])), ≥)∧[(4)bni_30 + (-1)Bound*bni_30] + [bni_30]x1[2] + [bni_30]x0[2] ≥ 0∧[(-1)bso_31] ≥ 0)
(41) (&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1)))=TRUE∧EOS(STATIC_11075(x0[2]))=EOS(STATIC_11075(x0[3]))∧x1[2]=x1[3]∧EOS(STATIC_11075(x0[3]))=EOS(STATIC_11075(x0[0]))∧+(*(2, x1[3]), 1)=x1[0] ⇒ COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥))
(42) (>(x0[2], +(*(2, x1[2]), 1))=TRUE∧>(x0[2], +(*(2, x1[2]), 2))=TRUE∧>=(*(2, x1[2]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[2])), x1[2])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[2])), x1[2])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), +(*(2, x1[2]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥))
(43) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(44) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(45) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(46) (x0[2] ≥ 0∧[-1] + x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(3)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(47) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(4)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(48) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(4)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(49) (&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1)))=TRUE∧EOS(STATIC_11075(x0[2]))=EOS(STATIC_11075(x0[3]))∧x1[2]=x1[3]∧EOS(STATIC_11075(x0[3]))=EOS(STATIC_11075(x0[2]1))∧+(*(2, x1[3]), 1)=x1[2]1 ⇒ COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥))
(50) (>(x0[2], +(*(2, x1[2]), 1))=TRUE∧>(x0[2], +(*(2, x1[2]), 2))=TRUE∧>=(*(2, x1[2]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[2])), x1[2])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[2])), x1[2])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), +(*(2, x1[2]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥))
(51) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(52) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(53) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(54) (x0[2] ≥ 0∧[-1] + x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(3)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(55) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(4)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(56) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(4)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(57) (&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1)))=TRUE∧EOS(STATIC_11075(x0[2]))=EOS(STATIC_11075(x0[3]))∧x1[2]=x1[3]∧EOS(STATIC_11075(x0[3]))=EOS(STATIC_11075(x0[4]))∧+(*(2, x1[3]), 1)=x1[4] ⇒ COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥))
(58) (>(x0[2], +(*(2, x1[2]), 1))=TRUE∧>(x0[2], +(*(2, x1[2]), 2))=TRUE∧>=(*(2, x1[2]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[2])), x1[2])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[2])), x1[2])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), +(*(2, x1[2]), 1))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥))
(59) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(60) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(61) (x0[2] + [-2] + [-2]x1[2] ≥ 0∧x0[2] + [-3] + [-2]x1[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(62) (x0[2] ≥ 0∧[-1] + x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(3)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(63) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧[2]x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(4)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(64) ([1] + x0[2] ≥ 0∧x0[2] ≥ 0∧x1[2] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))), ≥)∧[(4)bni_32 + (-1)Bound*bni_32] + [bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[1 + (-1)bso_33] + x1[2] ≥ 0)
(65) (&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1)))=TRUE∧EOS(STATIC_11075(x0[4]))=EOS(STATIC_11075(x0[5]))∧x1[4]=x1[5] ⇒ F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), x1[4])≥NonInfC∧F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), x1[4])≥COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])∧(UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥))
(66) (>(x0[4], +(*(2, x1[4]), 1))=TRUE∧>(x0[4], +(*(2, x1[4]), 2))=TRUE∧>=(*(2, x1[4]), 0)=TRUE ⇒ F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), x1[4])≥NonInfC∧F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), x1[4])≥COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])∧(UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥))
(67) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥)∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[4] + [bni_34]x0[4] ≥ 0∧[(-1)bso_35] ≥ 0)
(68) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥)∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[4] + [bni_34]x0[4] ≥ 0∧[(-1)bso_35] ≥ 0)
(69) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥)∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[4] + [bni_34]x0[4] ≥ 0∧[(-1)bso_35] ≥ 0)
(70) (x0[4] ≥ 0∧[-1] + x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥)∧[(3)bni_34 + (-1)Bound*bni_34] + [bni_34]x1[4] + [bni_34]x0[4] ≥ 0∧[(-1)bso_35] ≥ 0)
(71) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥)∧[(4)bni_34 + (-1)Bound*bni_34] + [bni_34]x1[4] + [bni_34]x0[4] ≥ 0∧[(-1)bso_35] ≥ 0)
(72) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])), ≥)∧[(4)bni_34 + (-1)Bound*bni_34] + [bni_34]x1[4] + [bni_34]x0[4] ≥ 0∧[(-1)bso_35] ≥ 0)
(73) (&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1)))=TRUE∧EOS(STATIC_11075(x0[4]))=EOS(STATIC_11075(x0[5]))∧x1[4]=x1[5]∧EOS(STATIC_11075(x0[5]))=EOS(STATIC_11075(x0[0]))∧+(*(2, x1[5]), 2)=x1[0] ⇒ COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥))
(74) (>(x0[4], +(*(2, x1[4]), 1))=TRUE∧>(x0[4], +(*(2, x1[4]), 2))=TRUE∧>=(*(2, x1[4]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[4])), x1[4])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[4])), x1[4])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), +(*(2, x1[4]), 2))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥))
(75) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(76) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(77) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(78) (x0[4] ≥ 0∧[-1] + x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(3)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(79) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(80) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(81) (&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1)))=TRUE∧EOS(STATIC_11075(x0[4]))=EOS(STATIC_11075(x0[5]))∧x1[4]=x1[5]∧EOS(STATIC_11075(x0[5]))=EOS(STATIC_11075(x0[2]))∧+(*(2, x1[5]), 2)=x1[2] ⇒ COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥))
(82) (>(x0[4], +(*(2, x1[4]), 1))=TRUE∧>(x0[4], +(*(2, x1[4]), 2))=TRUE∧>=(*(2, x1[4]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[4])), x1[4])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[4])), x1[4])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), +(*(2, x1[4]), 2))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥))
(83) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(84) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(85) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(86) (x0[4] ≥ 0∧[-1] + x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(3)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(87) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(88) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(89) (&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1)))=TRUE∧EOS(STATIC_11075(x0[4]))=EOS(STATIC_11075(x0[5]))∧x1[4]=x1[5]∧EOS(STATIC_11075(x0[5]))=EOS(STATIC_11075(x0[4]1))∧+(*(2, x1[5]), 2)=x1[4]1 ⇒ COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥))
(90) (>(x0[4], +(*(2, x1[4]), 1))=TRUE∧>(x0[4], +(*(2, x1[4]), 2))=TRUE∧>=(*(2, x1[4]), 0)=TRUE ⇒ COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[4])), x1[4])≥NonInfC∧COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[4])), x1[4])≥F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), +(*(2, x1[4]), 2))∧(UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥))
(91) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(92) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(93) (x0[4] + [-2] + [-2]x1[4] ≥ 0∧x0[4] + [-3] + [-2]x1[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(94) (x0[4] ≥ 0∧[-1] + x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(3)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(95) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧[2]x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
(96) ([1] + x0[4] ≥ 0∧x0[4] ≥ 0∧x1[4] ≥ 0 ⇒ (UIncreasing(F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))), ≥)∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]x1[4] + [bni_36]x0[4] ≥ 0∧[2 + (-1)bso_37] + x1[4] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(F11075_0_SUPPRIMER_LOAD'(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(EOS(x1)) = [-1] + x1
POL(STATIC_11075(x1)) = [-1] + [-1]x1
POL(COND_F11075_0_SUPPRIMER_LOAD(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(*(x1, x2)) = x1·x2
POL(2) = [2]
POL(1) = [1]
POL(>=(x1, x2)) = [-1]
POL(0) = 0
POL(<=(x1, x2)) = [-1]
POL(COND_F11075_0_SUPPRIMER_LOAD1(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(COND_F11075_0_SUPPRIMER_LOAD2(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1]) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))
COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3]) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))
COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5]) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), x1[0]) → COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])
COND_F11075_0_SUPPRIMER_LOAD(TRUE, EOS(STATIC_11075(x0[1])), x1[1]) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[1])), +(*(2, x1[1]), 1))
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), x1[2]) → COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])
COND_F11075_0_SUPPRIMER_LOAD1(TRUE, EOS(STATIC_11075(x0[3])), x1[3]) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[3])), +(*(2, x1[3]), 1))
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), x1[4]) → COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])
COND_F11075_0_SUPPRIMER_LOAD2(TRUE, EOS(STATIC_11075(x0[5])), x1[5]) → F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[5])), +(*(2, x1[5]), 2))
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[0])), x1[0]) → COND_F11075_0_SUPPRIMER_LOAD(&&(&&(>(x0[0], +(*(2, x1[0]), 1)), >=(*(2, x1[0]), 0)), <=(x0[0], +(*(2, x1[0]), 2))), EOS(STATIC_11075(x0[0])), x1[0])
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[2])), x1[2]) → COND_F11075_0_SUPPRIMER_LOAD1(&&(&&(>(x0[2], +(*(2, x1[2]), 2)), >=(*(2, x1[2]), 0)), >(x0[2], +(*(2, x1[2]), 1))), EOS(STATIC_11075(x0[2])), x1[2])
F11075_0_SUPPRIMER_LOAD'(EOS(STATIC_11075(x0[4])), x1[4]) → COND_F11075_0_SUPPRIMER_LOAD2(&&(&&(>(x0[4], +(*(2, x1[4]), 2)), >=(*(2, x1[4]), 0)), >(x0[4], +(*(2, x1[4]), 1))), EOS(STATIC_11075(x0[4])), x1[4])
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
Generated rules. Obtained 40 IRules
P rules:
f4539_0_Ajouter_LE(EOS, i342, i342, i836, i836) → f4563_0_Ajouter_LE(EOS, i342, i342, i836, i836)
f4563_0_Ajouter_LE(EOS, i342, i342, i836, i836) → f4577_0_Ajouter_FieldAccess(EOS, i342, i342, i836) | >(i836, 0)
f4577_0_Ajouter_FieldAccess(EOS, i342, i342, i836) → f4587_0_Ajouter_Load(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)))
f4587_0_Ajouter_Load(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339))) → f4605_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f4605_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f4627_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, 1)
f4627_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, matching1) → f4735_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), -(i836, 1)) | &&(>(i836, 0), =(matching1, 1))
f4735_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i862) → f4788_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i862, 2)
f4788_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i862, matching1) → f4816_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), /(i862, 2)) | =(matching1, 2)
f4816_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f4846_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f4846_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f4882_0_Ajouter_Load(EOS, i342, i342, i836, i886) | <(i877, i339)
f4882_0_Ajouter_Load(EOS, i342, i342, i836, i886) → f4956_0_Ajouter_GT(EOS, i342, i342, i836, i886, i342)
f4956_0_Ajouter_GT(EOS, i342, i342, i836, i886, i342) → f5001_0_Ajouter_GT(EOS, i342, i342, i836, i886, i342)
f5001_0_Ajouter_GT(EOS, i342, i342, i836, i886, i342) → f5047_0_Ajouter_FieldAccess(EOS, i342, i342, i836) | <=(i886, i342)
f5047_0_Ajouter_FieldAccess(EOS, i342, i342, i836) → f5115_0_Ajouter_Load(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)))
f5115_0_Ajouter_Load(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339))) → f5167_0_Ajouter_FieldAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f5167_0_Ajouter_FieldAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f5230_0_Ajouter_Load(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)))
f5230_0_Ajouter_Load(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339))) → f5289_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836)
f5289_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836) → f5341_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836, 1)
f5341_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836, matching1) → f5465_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), -(i836, 1)) | &&(>(i836, 0), =(matching1, 1))
f5465_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1072) → f5803_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1072, 2)
f5803_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1072, matching1) → f5882_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), /(i1072, 2)) | =(matching1, 2)
f5882_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f5961_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f5961_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6069_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) | <(i1129, i339)
f6069_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6118_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6118_0_Ajouter_ArrayAccess(EOS, i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6195_0_Ajouter_Load(EOS, i342, i342, i836) | <(i836, i339)
f6195_0_Ajouter_Load(EOS, i342, i342, i836) → f6317_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, i836)
f6317_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, i836) → f6397_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, i836, 1)
f6397_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, i836, matching1) → f6501_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, -(i836, 1)) | &&(>(i836, 0), =(matching1, 1))
f6501_0_Ajouter_ConstantStackPush(EOS, i342, i342, i836, i1205) → f6634_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, i1205, 2)
f6634_0_Ajouter_IntArithmetic(EOS, i342, i342, i836, i1205, matching1) → f6739_0_Ajouter_Store(EOS, i342, i342, i836, /(i1205, 2)) | =(matching1, 2)
f6739_0_Ajouter_Store(EOS, i342, i342, i836, i1228) → f6838_0_Ajouter_Load(EOS, i342, i342, i836, i1228)
f6838_0_Ajouter_Load(EOS, i342, i342, i836, i1228) → f6895_0_Ajouter_Load(EOS, i342, i342, i836, i1228, i1228)
f6895_0_Ajouter_Load(EOS, i342, i342, i836, i1228, i1228) → f6942_0_Ajouter_LT(EOS, i342, i342, i836, i1228, i1228, i836)
f6942_0_Ajouter_LT(EOS, i342, i342, i836, i1228, i1228, i836) → f7004_0_Ajouter_LT(EOS, i342, i342, i836, i1228, i1228, i836)
f7004_0_Ajouter_LT(EOS, i342, i342, i836, i1228, i1228, i836) → f7105_0_Ajouter_Load(EOS, i342, i342, i1228) | <(i1228, i836)
f7105_0_Ajouter_Load(EOS, i342, i342, i1228) → f7260_0_Ajouter_Store(EOS, i342, i342, i1228)
f7260_0_Ajouter_Store(EOS, i342, i342, i1228) → f7362_0_Ajouter_JMP(EOS, i342, i342, i1228)
f7362_0_Ajouter_JMP(EOS, i342, i342, i1228) → f7408_0_Ajouter_Load(EOS, i342, i342, i1228)
f7408_0_Ajouter_Load(EOS, i342, i342, i1228) → f4477_0_Ajouter_Load(EOS, i342, i342, i1228)
f4477_0_Ajouter_Load(EOS, i342, i342, i804) → f4539_0_Ajouter_LE(EOS, i342, i342, i804, i804)
Combined rules. Obtained 1 IRules
P rules:
f4539_0_Ajouter_LE(EOS, x0, x0, x1, x1) → f4539_0_Ajouter_LE(EOS, x0, x0, /(-(x1, 1), 2), /(-(x1, 1), 2)) | &&(>(x1, 0), <(/(-(x1, 1), 2), x1))
Filtered ground terms:
f4539_0_Ajouter_LE(x1, x2, x3, x4, x5) → f4539_0_Ajouter_LE(x2, x3, x4, x5)
Cond_f4539_0_Ajouter_LE(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE(x1, x3, x4, x5, x6)
Filtered duplicate terms:
f4539_0_Ajouter_LE(x1, x2, x3, x4) → f4539_0_Ajouter_LE(x2, x4)
Cond_f4539_0_Ajouter_LE(x1, x2, x3, x4, x5) → Cond_f4539_0_Ajouter_LE(x1, x3, x5)
Filtered unneeded terms:
Cond_f4539_0_Ajouter_LE(x1, x2, x3) → Cond_f4539_0_Ajouter_LE(x1, x3)
f4539_0_Ajouter_LE(x1, x2) → f4539_0_Ajouter_LE(x2)
Prepared 1 rules for path length conversion:
P rules:
f4539_0_Ajouter_LE(x1) → f4539_0_Ajouter_LE(/(-(x1, 1), 2)) | &&(>(x1, 0), <(/(-(x1, 1), 2), x1))
Finished conversion. Obtained 2 rules.
P rules:
f4539_0_Ajouter_LE(x0) → f4539_0_Ajouter_LE'(x0) | &&(>(x0, 0), >(x0, div))
f4539_0_Ajouter_LE'(x0) → f4539_0_Ajouter_LE(arith) | &&(&&(&&(&&(&&(>(x0, div), >(x0, 0)), >=(-(-(x0, 1), *(2, div)), 0)), <(-(-(x0, 1), *(2, div)), 2)), <(-(-(x0, 1), *(2, arith)), 2)), >=(-(-(x0, 1), *(2, arith)), 0))
Found the following polynomial interpretation:
Therefore the following rule(s) have been dropped:
Generated rules. Obtained 24 IRules
P rules:
f7938_0_HeapSort_LT(EOS, i1488, i1488) → f7957_0_HeapSort_LT(EOS, i1488, i1488)
f7957_0_HeapSort_LT(EOS, i1488, i1488) → f8017_0_HeapSort_InvokeMethod(EOS, i1488) | >=(i1488, 0)
f8017_0_HeapSort_InvokeMethod(EOS, i1488) → f8040_0_Maximum_FieldAccess(EOS, i1488)
f8040_0_Maximum_FieldAccess(EOS, i1488) → f8115_0_Maximum_ConstantStackPush(EOS, i1488, java.lang.Object(ARRAY(i1467)))
f8115_0_Maximum_ConstantStackPush(EOS, i1488, java.lang.Object(ARRAY(i1467))) → f8141_0_Maximum_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1467)), 0)
f8141_0_Maximum_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1531)), matching1) → f8156_0_Maximum_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1531)), 0) | =(matching1, 0)
f8156_0_Maximum_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1531)), matching1) → f8212_0_Maximum_Return(EOS, i1488) | &&(<(0, i1531), =(matching1, 0))
f8212_0_Maximum_Return(EOS, i1488) → f8222_0_HeapSort_Store(EOS, i1488)
f8222_0_HeapSort_Store(EOS, i1488) → f8238_0_HeapSort_InvokeMethod(EOS, i1488)
f8238_0_HeapSort_InvokeMethod(EOS, i1488) → f8248_0_Supprimer_FieldAccess(EOS)
f8238_0_HeapSort_InvokeMethod(EOS, i1488) → f8248_1_Supprimer_FieldAccess(EOS, i1488)
f8248_0_Supprimer_FieldAccess(EOS) → f8321_0_Supprimer_FieldAccess(EOS)
f11660_0_Supprimer_Return(EOS, i1488) → f9261_0_Supprimer_Return(EOS, i1488)
f9261_0_Supprimer_Return(EOS, i1488) → f9272_0_HeapSort_FieldAccess(EOS, i1488)
f9272_0_HeapSort_FieldAccess(EOS, i1488) → f9306_0_HeapSort_Load(EOS, i1488, java.lang.Object(ARRAY(i1797)))
f9306_0_HeapSort_Load(EOS, i1488, java.lang.Object(ARRAY(i1797))) → f9328_0_HeapSort_Load(EOS, i1488, java.lang.Object(ARRAY(i1797)), i1488)
f9328_0_HeapSort_Load(EOS, i1488, java.lang.Object(ARRAY(i1797)), i1488) → f9335_0_HeapSort_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1797)), i1488)
f9335_0_HeapSort_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1797)), i1488) → f9341_0_HeapSort_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1797)), i1488)
f9341_0_HeapSort_ArrayAccess(EOS, i1488, java.lang.Object(ARRAY(i1797)), i1488) → f9344_0_HeapSort_Inc(EOS, i1488) | <(i1488, i1797)
f9344_0_HeapSort_Inc(EOS, i1488) → f9352_0_HeapSort_JMP(EOS, +(i1488, -1)) | >=(i1488, 0)
f9352_0_HeapSort_JMP(EOS, i1823) → f9368_0_HeapSort_Load(EOS, i1823)
f9368_0_HeapSort_Load(EOS, i1823) → f7895_0_HeapSort_Load(EOS, i1823)
f7895_0_HeapSort_Load(EOS, i1470) → f7938_0_HeapSort_LT(EOS, i1470, i1470)
f8248_1_Supprimer_FieldAccess(EOS, i1488) → f11660_0_Supprimer_Return(EOS, i1488)
Combined rules. Obtained 2 IRules
P rules:
f11660_0_Supprimer_Return(EOS, x0) → f8321_0_Supprimer_FieldAccess(EOS) | >(+(x0, 1), 1)
f11660_0_Supprimer_Return(EOS, x0) → f11660_0_Supprimer_Return(EOS, -(x0, 1)) | >(+(x0, 1), 1)
Filtered ground terms:
f11660_0_Supprimer_Return(x1, x2) → f11660_0_Supprimer_Return(x2)
Cond_f11660_0_Supprimer_Return(x1, x2, x3) → Cond_f11660_0_Supprimer_Return(x1, x3)
f8321_0_Supprimer_FieldAccess(x1) → f8321_0_Supprimer_FieldAccess
Cond_f11660_0_Supprimer_Return1(x1, x2, x3) → Cond_f11660_0_Supprimer_Return1(x1, x3)
Filtered unneeded terms:
Cond_f11660_0_Supprimer_Return(x1, x2) → Cond_f11660_0_Supprimer_Return(x1)
Prepared 2 rules for path length conversion:
P rules:
f11660_0_Supprimer_Return(x0) → f8321_0_Supprimer_FieldAccess | >(+(x0, 1), 1)
f11660_0_Supprimer_Return(x0) → f11660_0_Supprimer_Return(-(x0, 1)) | >(+(x0, 1), 1)
Finished conversion. Obtained 1 rules.
P rules:
f11660_0_Supprimer_Return(x1) → f11660_0_Supprimer_Return(-(x1, 1)) | >(x1, 0)
Found the following polynomial interpretation:
Therefore the following rule(s) have been dropped:
Generated 20 rules for P and 210 rules for R.
P rules:
f5116_0_HeapSort_FieldAccess(EOS(STATIC_5116(i950)), i953, i953) → f5122_0_HeapSort_GE(EOS(STATIC_5122(i950)), i953, i953, i950)
f5122_0_HeapSort_GE(EOS(STATIC_5122(i950)), i953, i953, i950) → f5131_0_HeapSort_GE(EOS(STATIC_5131(i950)), i953, i953, i950)
f5131_0_HeapSort_GE(EOS(STATIC_5131(i950)), i953, i953, i950) → f5163_0_HeapSort_FieldAccess(EOS(STATIC_5163(i950)), i953) | <(i953, i950)
f5163_0_HeapSort_FieldAccess(EOS(STATIC_5163(i950)), i953) → f5179_0_HeapSort_Load(EOS(STATIC_5179(i950)), i953, java.lang.Object(ARRAY(i950)))
f5179_0_HeapSort_Load(EOS(STATIC_5179(i950)), i953, java.lang.Object(ARRAY(i950))) → f5200_0_HeapSort_ArrayAccess(EOS(STATIC_5200(i950)), i953, java.lang.Object(ARRAY(i950)), i953)
f5200_0_HeapSort_ArrayAccess(EOS(STATIC_5200(i950)), i953, java.lang.Object(ARRAY(i950)), i953) → f5232_0_HeapSort_ArrayAccess(EOS(STATIC_5232(i950)), i953, java.lang.Object(ARRAY(i950)), i953)
f5232_0_HeapSort_ArrayAccess(EOS(STATIC_5232(i950)), i953, java.lang.Object(ARRAY(i950)), i953) → f5250_0_HeapSort_InvokeMethod(EOS(STATIC_5250(i950)), i953, i1001) | <(i953, i950)
f5250_0_HeapSort_InvokeMethod(EOS(STATIC_5250(i950)), i953, i1001) → f5290_1_HeapSort_InvokeMethod(f5290_0_Ajouter_FieldAccess(EOS(STATIC_5290(i950)), i1001, i1001), i953, i1001)
f5290_0_Ajouter_FieldAccess(EOS(STATIC_5290(i950)), i1001, i1001) → f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(i950)), i1001, i1001)
f5544_0_Ajouter_Return(EOS(STATIC_5544(i1055)), i953, i1053) → f5716_0_Ajouter_Return(EOS(STATIC_5716(i1055)), i953, i1053)
f5716_0_Ajouter_Return(EOS(STATIC_5716(i1100)), i953, i1103) → f5846_0_HeapSort_Inc(EOS(STATIC_5846(i1100)), i953)
f5846_0_HeapSort_Inc(EOS(STATIC_5846(i1100)), i953) → f5901_0_HeapSort_JMP(EOS(STATIC_5901(i1100)), +(i953, 1)) | >=(i953, 0)
f5901_0_HeapSort_JMP(EOS(STATIC_5901(i1100)), i1134) → f5950_0_HeapSort_Load(EOS(STATIC_5950(i1100)), i1134)
f5950_0_HeapSort_Load(EOS(STATIC_5950(i1100)), i1134) → f5069_0_HeapSort_Load(EOS(STATIC_5069(i1100)), i1134)
f5069_0_HeapSort_Load(EOS(STATIC_5069(i950)), i953) → f5116_0_HeapSort_FieldAccess(EOS(STATIC_5116(i950)), i953, i953)
f5715_0_Ajouter_Return(EOS(STATIC_5715(i1065)), i953, i1063) → f5716_0_Ajouter_Return(EOS(STATIC_5716(i1065)), i953, i1063)
f7858_0_Ajouter_Return(EOS(STATIC_7858(i1440)), i953, i1438) → f5716_0_Ajouter_Return(EOS(STATIC_5716(i1440)), i953, i1438)
f5290_1_HeapSort_InvokeMethod(f4806_0_Ajouter_Return(EOS(STATIC_4806(i1055)), i1053), i953, i1053) → f5544_0_Ajouter_Return(EOS(STATIC_5544(i1055)), i953, i1053)
f5290_1_HeapSort_InvokeMethod(f5320_0_Ajouter_Return(EOS(STATIC_5320(i1065)), i1063), i953, i1063) → f5715_0_Ajouter_Return(EOS(STATIC_5715(i1065)), i953, i1063)
f5290_1_HeapSort_InvokeMethod(f7598_0_Ajouter_Return(EOS(STATIC_7598(i1440)), i1438), i953, i1438) → f7858_0_Ajouter_Return(EOS(STATIC_7858(i1440)), i953, i1438)
R rules:
f5290_0_Ajouter_FieldAccess(EOS(STATIC_5290(i950)), i1001, i1001) → f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(i950)), i1001, i1001)
f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(i950)), i1001, i1001) → f2463_0_Ajouter_FieldAccess(EOS(STATIC_2463(i950)), i1001, i1001)
f2463_0_Ajouter_FieldAccess(EOS(STATIC_2463(i339)), i342, i342) → f2567_0_Ajouter_ConstantStackPush(EOS(STATIC_2567(i339)), i342, i342, i340)
f2567_0_Ajouter_ConstantStackPush(EOS(STATIC_2567(i339)), i342, i342, i340) → f2574_0_Ajouter_IntArithmetic(EOS(STATIC_2574(i339)), i342, i342, i340, 1)
f2574_0_Ajouter_IntArithmetic(EOS(STATIC_2574(i339)), i342, i342, i340, matching1) → f2578_0_Ajouter_FieldAccess(EOS(STATIC_2578(i339)), i342, i342, +(i340, 1)) | =(matching1, 1)
f2578_0_Ajouter_FieldAccess(EOS(STATIC_2578(i339)), i342, i342, i355) → f2583_0_Ajouter_FieldAccess(EOS(STATIC_2583(i339)), i342, i342)
f2583_0_Ajouter_FieldAccess(EOS(STATIC_2583(i339)), i342, i342) → f2591_0_Ajouter_ConstantStackPush(EOS(STATIC_2591(i339)), i342, i342, i355)
f2591_0_Ajouter_ConstantStackPush(EOS(STATIC_2591(i339)), i342, i342, i355) → f2596_0_Ajouter_IntArithmetic(EOS(STATIC_2596(i339)), i342, i342, i355, 1)
f2596_0_Ajouter_IntArithmetic(EOS(STATIC_2596(i339)), i342, i342, i355, matching1) → f2603_0_Ajouter_Store(EOS(STATIC_2603(i339)), i342, i342, -(i355, 1)) | =(matching1, 1)
f2603_0_Ajouter_Store(EOS(STATIC_2603(i339)), i342, i342, i357) → f2611_0_Ajouter_Load(EOS(STATIC_2611(i339)), i342, i342, i357)
f2611_0_Ajouter_Load(EOS(STATIC_2611(i339)), i342, i342, i357) → f4477_0_Ajouter_Load(EOS(STATIC_4477(i339)), i342, i342, i357)
f4477_0_Ajouter_Load(EOS(STATIC_4477(i339)), i342, i342, i804) → f4539_0_Ajouter_LE(EOS(STATIC_4539(i339)), i342, i342, i804, i804)
f4539_0_Ajouter_LE(EOS(STATIC_4539(i339)), i342, i342, i835, i835) → f4562_0_Ajouter_LE(EOS(STATIC_4562(i339)), i342, i342, i835, i835)
f4539_0_Ajouter_LE(EOS(STATIC_4539(i339)), i342, i342, i836, i836) → f4563_0_Ajouter_LE(EOS(STATIC_4563(i339)), i342, i342, i836, i836)
f4562_0_Ajouter_LE(EOS(STATIC_4562(i339)), i342, i342, i835, i835) → f4570_0_Ajouter_FieldAccess(EOS(STATIC_4570(i339)), i342, i342, i835) | <=(i835, 0)
f4563_0_Ajouter_LE(EOS(STATIC_4563(i339)), i342, i342, i836, i836) → f4577_0_Ajouter_FieldAccess(EOS(STATIC_4577(i339)), i342, i342, i836) | >(i836, 0)
f4570_0_Ajouter_FieldAccess(EOS(STATIC_4570(i339)), i342, i342, i835) → f4581_0_Ajouter_Load(EOS(STATIC_4581(i339)), i342, i342, i835, java.lang.Object(ARRAY(i339)))
f4577_0_Ajouter_FieldAccess(EOS(STATIC_4577(i339)), i342, i342, i836) → f4587_0_Ajouter_Load(EOS(STATIC_4587(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)))
f4581_0_Ajouter_Load(EOS(STATIC_4581(i339)), i342, i342, i835, java.lang.Object(ARRAY(i339))) → f4593_0_Ajouter_Load(EOS(STATIC_4593(i339)), i342, i342, java.lang.Object(ARRAY(i339)), i835)
f4587_0_Ajouter_Load(EOS(STATIC_4587(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339))) → f4605_0_Ajouter_ConstantStackPush(EOS(STATIC_4605(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f4593_0_Ajouter_Load(EOS(STATIC_4593(i339)), i342, i342, java.lang.Object(ARRAY(i339)), i835) → f4613_0_Ajouter_ArrayAccess(EOS(STATIC_4613(i339)), i342, java.lang.Object(ARRAY(i339)), i835, i342)
f4605_0_Ajouter_ConstantStackPush(EOS(STATIC_4605(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f4627_0_Ajouter_IntArithmetic(EOS(STATIC_4627(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, 1)
f4613_0_Ajouter_ArrayAccess(EOS(STATIC_4613(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f4648_0_Ajouter_ArrayAccess(EOS(STATIC_4648(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f4613_0_Ajouter_ArrayAccess(EOS(STATIC_4613(i339)), i342, java.lang.Object(ARRAY(i339)), matching1, i342) → f4649_0_Ajouter_ArrayAccess(EOS(STATIC_4649(i339)), i342, java.lang.Object(ARRAY(i339)), 0, i342) | =(matching1, 0)
f4627_0_Ajouter_IntArithmetic(EOS(STATIC_4627(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, matching1) → f4735_0_Ajouter_ConstantStackPush(EOS(STATIC_4735(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), -(i836, 1)) | &&(>(i836, 0), =(matching1, 1))
f4648_0_Ajouter_ArrayAccess(EOS(STATIC_4648(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f4755_0__init__Load(EOS(STATIC_4755(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) | <=(i854, -1)
f4649_0_Ajouter_ArrayAccess(EOS(STATIC_4649(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f4778_0_Ajouter_ArrayAccess(EOS(STATIC_4778(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f4649_0_Ajouter_ArrayAccess(EOS(STATIC_4649(i871)), i342, java.lang.Object(ARRAY(i871)), matching1, i342) → f4779_0_Ajouter_ArrayAccess(EOS(STATIC_4779(i871)), i342, java.lang.Object(ARRAY(i871)), 0, i342) | =(matching1, 0)
f4735_0_Ajouter_ConstantStackPush(EOS(STATIC_4735(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i862) → f4788_0_Ajouter_IntArithmetic(EOS(STATIC_4788(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i862, 2)
f4755_0__init__Load(EOS(STATIC_4755(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f4824_0__init__InvokeMethod(EOS(STATIC_4824(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f4778_0_Ajouter_ArrayAccess(EOS(STATIC_4778(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f4802_0__init__Load(EOS(STATIC_4802(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | &&(&&(>=(0, 0), <=(i870, 0)), =(matching1, 0))
f4779_0_Ajouter_ArrayAccess(EOS(STATIC_4779(i871)), i342, java.lang.Object(ARRAY(i871)), matching1, i342) → f4806_0_Ajouter_Return(EOS(STATIC_4806(i871)), i342) | &&(<(0, i871), =(matching1, 0))
f4788_0_Ajouter_IntArithmetic(EOS(STATIC_4788(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i862, matching1) → f4816_0_Ajouter_ArrayAccess(EOS(STATIC_4816(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), /(i862, 2)) | =(matching1, 2)
f4802_0__init__Load(EOS(STATIC_4802(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f4869_0__init__InvokeMethod(EOS(STATIC_4869(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f4806_0_Ajouter_Return(EOS(STATIC_4806(i871)), i342) → f5320_0_Ajouter_Return(EOS(STATIC_5320(i871)), i342)
f4816_0_Ajouter_ArrayAccess(EOS(STATIC_4816(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f4846_0_Ajouter_ArrayAccess(EOS(STATIC_4846(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f4816_0_Ajouter_ArrayAccess(EOS(STATIC_4816(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f4847_0_Ajouter_ArrayAccess(EOS(STATIC_4847(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f4824_0__init__InvokeMethod(EOS(STATIC_4824(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f4863_0__init__Load(EOS(STATIC_4863(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f4846_0_Ajouter_ArrayAccess(EOS(STATIC_4846(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f4882_0_Ajouter_Load(EOS(STATIC_4882(i339)), i342, i342, i836, i886) | <(i877, i339)
f4847_0_Ajouter_ArrayAccess(EOS(STATIC_4847(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f4903_0__init__Load(EOS(STATIC_4903(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) | >=(i877, i339)
f4863_0__init__Load(EOS(STATIC_4863(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f4983_0__init__InvokeMethod(EOS(STATIC_4983(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f4869_0__init__InvokeMethod(EOS(STATIC_4869(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f4931_0__init__Load(EOS(STATIC_4931(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f4882_0_Ajouter_Load(EOS(STATIC_4882(i339)), i342, i342, i836, i886) → f4956_0_Ajouter_GT(EOS(STATIC_4956(i339)), i342, i342, i836, i886, i342)
f4903_0__init__Load(EOS(STATIC_4903(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5013_0__init__InvokeMethod(EOS(STATIC_5013(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f4931_0__init__Load(EOS(STATIC_4931(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5028_0__init__InvokeMethod(EOS(STATIC_5028(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f4956_0_Ajouter_GT(EOS(STATIC_4956(i339)), i342, i342, i836, i886, i342) → f5000_0_Ajouter_GT(EOS(STATIC_5000(i339)), i342, i342, i836, i886, i342)
f4956_0_Ajouter_GT(EOS(STATIC_4956(i339)), i342, i342, i836, i886, i342) → f5001_0_Ajouter_GT(EOS(STATIC_5001(i339)), i342, i342, i836, i886, i342)
f4983_0__init__InvokeMethod(EOS(STATIC_4983(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5020_0__init__Load(EOS(STATIC_5020(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5000_0_Ajouter_GT(EOS(STATIC_5000(i339)), i342, i342, i836, i886, i342) → f5042_0_Ajouter_FieldAccess(EOS(STATIC_5042(i339)), i342, i342, i836) | >(i886, i342)
f5001_0_Ajouter_GT(EOS(STATIC_5001(i339)), i342, i342, i836, i886, i342) → f5047_0_Ajouter_FieldAccess(EOS(STATIC_5047(i339)), i342, i342, i836) | <=(i886, i342)
f5013_0__init__InvokeMethod(EOS(STATIC_5013(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5057_0__init__Load(EOS(STATIC_5057(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5020_0__init__Load(EOS(STATIC_5020(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5128_0__init__InvokeMethod(EOS(STATIC_5128(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5028_0__init__InvokeMethod(EOS(STATIC_5028(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5093_0__init__Load(EOS(STATIC_5093(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5042_0_Ajouter_FieldAccess(EOS(STATIC_5042(i339)), i342, i342, i836) → f7272_0_Ajouter_FieldAccess(EOS(STATIC_7272(i339)), i342, i342, i836)
f5047_0_Ajouter_FieldAccess(EOS(STATIC_5047(i339)), i342, i342, i836) → f5115_0_Ajouter_Load(EOS(STATIC_5115(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)))
f5057_0__init__Load(EOS(STATIC_5057(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5177_0__init__InvokeMethod(EOS(STATIC_5177(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5093_0__init__Load(EOS(STATIC_5093(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5198_0__init__InvokeMethod(EOS(STATIC_5198(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5115_0_Ajouter_Load(EOS(STATIC_5115(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339))) → f5167_0_Ajouter_FieldAccess(EOS(STATIC_5167(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f5128_0__init__InvokeMethod(EOS(STATIC_5128(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5181_0__init__Load(EOS(STATIC_5181(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5167_0_Ajouter_FieldAccess(EOS(STATIC_5167(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f5230_0_Ajouter_Load(EOS(STATIC_5230(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)))
f5177_0__init__InvokeMethod(EOS(STATIC_5177(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5241_0__init__Load(EOS(STATIC_5241(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5181_0__init__Load(EOS(STATIC_5181(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5306_0__init__InvokeMethod(EOS(STATIC_5306(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5198_0__init__InvokeMethod(EOS(STATIC_5198(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5255_0__init__Load(EOS(STATIC_5255(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5230_0_Ajouter_Load(EOS(STATIC_5230(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339))) → f5289_0_Ajouter_ConstantStackPush(EOS(STATIC_5289(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836)
f5241_0__init__Load(EOS(STATIC_5241(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5361_0__init__InvokeMethod(EOS(STATIC_5361(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5255_0__init__Load(EOS(STATIC_5255(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5387_0__init__InvokeMethod(EOS(STATIC_5387(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5289_0_Ajouter_ConstantStackPush(EOS(STATIC_5289(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836) → f5341_0_Ajouter_IntArithmetic(EOS(STATIC_5341(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836, 1)
f5306_0__init__InvokeMethod(EOS(STATIC_5306(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5377_0__init__Load(EOS(STATIC_5377(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5320_0_Ajouter_Return(EOS(STATIC_5320(i339)), i342) → f7598_0_Ajouter_Return(EOS(STATIC_7598(i339)), i342)
f5341_0_Ajouter_IntArithmetic(EOS(STATIC_5341(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i836, matching1) → f5465_0_Ajouter_ConstantStackPush(EOS(STATIC_5465(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), -(i836, 1)) | &&(>(i836, 0), =(matching1, 1))
f5361_0__init__InvokeMethod(EOS(STATIC_5361(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5469_0__init__Load(EOS(STATIC_5469(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5377_0__init__Load(EOS(STATIC_5377(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5816_0__init__InvokeMethod(EOS(STATIC_5816(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5387_0__init__InvokeMethod(EOS(STATIC_5387(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5542_0__init__Load(EOS(STATIC_5542(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5465_0_Ajouter_ConstantStackPush(EOS(STATIC_5465(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1072) → f5803_0_Ajouter_IntArithmetic(EOS(STATIC_5803(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1072, 2)
f5469_0__init__Load(EOS(STATIC_5469(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5898_0__init__InvokeMethod(EOS(STATIC_5898(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5542_0__init__Load(EOS(STATIC_5542(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f5934_0__init__InvokeMethod(EOS(STATIC_5934(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5803_0_Ajouter_IntArithmetic(EOS(STATIC_5803(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1072, matching1) → f5882_0_Ajouter_ArrayAccess(EOS(STATIC_5882(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), /(i1072, 2)) | =(matching1, 2)
f5816_0__init__InvokeMethod(EOS(STATIC_5816(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f5929_0__init__Load(EOS(STATIC_5929(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5882_0_Ajouter_ArrayAccess(EOS(STATIC_5882(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f5961_0_Ajouter_ArrayAccess(EOS(STATIC_5961(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f5882_0_Ajouter_ArrayAccess(EOS(STATIC_5882(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f5963_0_Ajouter_ArrayAccess(EOS(STATIC_5963(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f5898_0__init__InvokeMethod(EOS(STATIC_5898(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f5994_0__init__Load(EOS(STATIC_5994(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f5929_0__init__Load(EOS(STATIC_5929(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6008_0__init__Load(EOS(STATIC_6008(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f5934_0__init__InvokeMethod(EOS(STATIC_5934(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6045_0__init__Load(EOS(STATIC_6045(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f5961_0_Ajouter_ArrayAccess(EOS(STATIC_5961(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6069_0_Ajouter_ArrayAccess(EOS(STATIC_6069(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) | <(i1129, i339)
f5963_0_Ajouter_ArrayAccess(EOS(STATIC_5963(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6076_0__init__Load(EOS(STATIC_6076(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) | >=(i1129, i339)
f5994_0__init__Load(EOS(STATIC_5994(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6153_0__init__InvokeMethod(EOS(STATIC_6153(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6008_0__init__Load(EOS(STATIC_6008(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6087_0__init__FieldAccess(EOS(STATIC_6087(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6045_0__init__Load(EOS(STATIC_6045(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6098_0__init__Load(EOS(STATIC_6098(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6069_0_Ajouter_ArrayAccess(EOS(STATIC_6069(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6118_0_Ajouter_ArrayAccess(EOS(STATIC_6118(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6069_0_Ajouter_ArrayAccess(EOS(STATIC_6069(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6119_0_Ajouter_ArrayAccess(EOS(STATIC_6119(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6076_0__init__Load(EOS(STATIC_6076(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6235_0__init__InvokeMethod(EOS(STATIC_6235(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6087_0__init__FieldAccess(EOS(STATIC_6087(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6164_0__init__Load(EOS(STATIC_6164(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6098_0__init__Load(EOS(STATIC_6098(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6177_0__init__FieldAccess(EOS(STATIC_6177(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6118_0_Ajouter_ArrayAccess(EOS(STATIC_6118(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6195_0_Ajouter_Load(EOS(STATIC_6195(i339)), i342, i342, i836) | <(i836, i339)
f6119_0_Ajouter_ArrayAccess(EOS(STATIC_6119(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6204_0__init__Load(EOS(STATIC_6204(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) | >=(i836, i339)
f6153_0__init__InvokeMethod(EOS(STATIC_6153(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6254_0__init__Load(EOS(STATIC_6254(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6164_0__init__Load(EOS(STATIC_6164(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6276_0__init__InvokeMethod(EOS(STATIC_6276(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6177_0__init__FieldAccess(EOS(STATIC_6177(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6292_0__init__Load(EOS(STATIC_6292(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6195_0_Ajouter_Load(EOS(STATIC_6195(i339)), i342, i342, i836) → f6317_0_Ajouter_ConstantStackPush(EOS(STATIC_6317(i339)), i342, i342, i836, i836)
f6204_0__init__Load(EOS(STATIC_6204(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6430_0__init__InvokeMethod(EOS(STATIC_6430(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6235_0__init__InvokeMethod(EOS(STATIC_6235(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6333_0__init__Load(EOS(STATIC_6333(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6254_0__init__Load(EOS(STATIC_6254(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6347_0__init__Load(EOS(STATIC_6347(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6276_0__init__InvokeMethod(EOS(STATIC_6276(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6362_0__init__StackPop(EOS(STATIC_6362(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6292_0__init__Load(EOS(STATIC_6292(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6378_0__init__InvokeMethod(EOS(STATIC_6378(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6317_0_Ajouter_ConstantStackPush(EOS(STATIC_6317(i339)), i342, i342, i836, i836) → f6397_0_Ajouter_IntArithmetic(EOS(STATIC_6397(i339)), i342, i342, i836, i836, 1)
f6333_0__init__Load(EOS(STATIC_6333(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6535_0__init__InvokeMethod(EOS(STATIC_6535(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6347_0__init__Load(EOS(STATIC_6347(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6457_0__init__FieldAccess(EOS(STATIC_6457(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6362_0__init__StackPop(EOS(STATIC_6362(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6467_0__init__Return(EOS(STATIC_6467(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6378_0__init__InvokeMethod(EOS(STATIC_6378(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6479_0__init__StackPop(EOS(STATIC_6479(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6397_0_Ajouter_IntArithmetic(EOS(STATIC_6397(i339)), i342, i342, i836, i836, matching1) → f6501_0_Ajouter_ConstantStackPush(EOS(STATIC_6501(i339)), i342, i342, i836, -(i836, 1)) | &&(>(i836, 0), =(matching1, 1))
f6430_0__init__InvokeMethod(EOS(STATIC_6430(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6515_0__init__Load(EOS(STATIC_6515(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6457_0__init__FieldAccess(EOS(STATIC_6457(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6563_0__init__Load(EOS(STATIC_6563(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6467_0__init__Return(EOS(STATIC_6467(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6577_0__init__Return(EOS(STATIC_6577(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6479_0__init__StackPop(EOS(STATIC_6479(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6590_0__init__Return(EOS(STATIC_6590(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6501_0_Ajouter_ConstantStackPush(EOS(STATIC_6501(i339)), i342, i342, i836, i1205) → f6634_0_Ajouter_IntArithmetic(EOS(STATIC_6634(i339)), i342, i342, i836, i1205, 2)
f6515_0__init__Load(EOS(STATIC_6515(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6763_0__init__InvokeMethod(EOS(STATIC_6763(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6535_0__init__InvokeMethod(EOS(STATIC_6535(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6654_0__init__Load(EOS(STATIC_6654(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6563_0__init__Load(EOS(STATIC_6563(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6690_0__init__InvokeMethod(EOS(STATIC_6690(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6577_0__init__Return(EOS(STATIC_6577(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6705_0__init__Return(EOS(STATIC_6705(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6590_0__init__Return(EOS(STATIC_6590(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6720_0__init__Return(EOS(STATIC_6720(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6634_0_Ajouter_IntArithmetic(EOS(STATIC_6634(i339)), i342, i342, i836, i1205, matching1) → f6739_0_Ajouter_Store(EOS(STATIC_6739(i339)), i342, i342, i836, /(i1205, 2)) | =(matching1, 2)
f6654_0__init__Load(EOS(STATIC_6654(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6861_0__init__InvokeMethod(EOS(STATIC_6861(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6690_0__init__InvokeMethod(EOS(STATIC_6690(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6784_0__init__StackPop(EOS(STATIC_6784(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6705_0__init__Return(EOS(STATIC_6705(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6791_0__init__Return(EOS(STATIC_6791(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6720_0__init__Return(EOS(STATIC_6720(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6798_0__init__Return(EOS(STATIC_6798(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6739_0_Ajouter_Store(EOS(STATIC_6739(i339)), i342, i342, i836, i1228) → f6838_0_Ajouter_Load(EOS(STATIC_6838(i339)), i342, i342, i836, i1228)
f6763_0__init__InvokeMethod(EOS(STATIC_6763(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6844_0__init__Load(EOS(STATIC_6844(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6784_0__init__StackPop(EOS(STATIC_6784(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6869_0__init__Return(EOS(STATIC_6869(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6791_0__init__Return(EOS(STATIC_6791(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6874_0__init__Return(EOS(STATIC_6874(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6798_0__init__Return(EOS(STATIC_6798(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6877_0__init__Return(EOS(STATIC_6877(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6838_0_Ajouter_Load(EOS(STATIC_6838(i339)), i342, i342, i836, i1228) → f6895_0_Ajouter_Load(EOS(STATIC_6895(i339)), i342, i342, i836, i1228, i1228)
f6844_0__init__Load(EOS(STATIC_6844(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f6963_0__init__InvokeMethod(EOS(STATIC_6963(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6861_0__init__InvokeMethod(EOS(STATIC_6861(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f6900_0__init__Load(EOS(STATIC_6900(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6869_0__init__Return(EOS(STATIC_6869(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6909_0__init__Return(EOS(STATIC_6909(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6874_0__init__Return(EOS(STATIC_6874(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342) → f6913_0_Ajouter_ArrayAccess(EOS(STATIC_6913(i339)), i342, java.lang.Object(ARRAY(i339)), i854, i342)
f6877_0__init__Return(EOS(STATIC_6877(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6919_0__init__Return(EOS(STATIC_6919(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6895_0_Ajouter_Load(EOS(STATIC_6895(i339)), i342, i342, i836, i1228, i1228) → f6942_0_Ajouter_LT(EOS(STATIC_6942(i339)), i342, i342, i836, i1228, i1228, i836)
f6900_0__init__Load(EOS(STATIC_6900(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7027_0__init__InvokeMethod(EOS(STATIC_7027(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f6909_0__init__Return(EOS(STATIC_6909(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f6977_0__init__Return(EOS(STATIC_6977(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f6919_0__init__Return(EOS(STATIC_6919(i870)), i342, java.lang.Object(ARRAY(i870)), matching1, i342) → f6985_0_Ajouter_ArrayAccess(EOS(STATIC_6985(i870)), i342, java.lang.Object(ARRAY(i870)), 0, i342) | =(matching1, 0)
f6942_0_Ajouter_LT(EOS(STATIC_6942(i339)), i342, i342, i836, i1228, i1228, i836) → f7004_0_Ajouter_LT(EOS(STATIC_7004(i339)), i342, i342, i836, i1228, i1228, i836)
f6942_0_Ajouter_LT(EOS(STATIC_6942(i339)), i342, i342, i836, i1228, i1228, i836) → f7005_0_Ajouter_LT(EOS(STATIC_7005(i339)), i342, i342, i836, i1228, i1228, i836)
f6963_0__init__InvokeMethod(EOS(STATIC_6963(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7008_0__init__Load(EOS(STATIC_7008(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f6977_0__init__Return(EOS(STATIC_6977(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f7048_0__init__Return(EOS(STATIC_7048(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f7004_0_Ajouter_LT(EOS(STATIC_7004(i339)), i342, i342, i836, i1228, i1228, i836) → f7105_0_Ajouter_Load(EOS(STATIC_7105(i339)), i342, i342, i1228) | <(i1228, i836)
f7005_0_Ajouter_LT(EOS(STATIC_7005(i339)), i342, i342, i836, i1228, i1228, i836) → f7120_0_Ajouter_JMP(EOS(STATIC_7120(i339)), i342, i342, i836) | >=(i1228, i836)
f7008_0__init__Load(EOS(STATIC_7008(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7305_0__init__InvokeMethod(EOS(STATIC_7305(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7027_0__init__InvokeMethod(EOS(STATIC_7027(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7150_0__init__Load(EOS(STATIC_7150(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7048_0__init__Return(EOS(STATIC_7048(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f7174_0__init__Return(EOS(STATIC_7174(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f7105_0_Ajouter_Load(EOS(STATIC_7105(i339)), i342, i342, i1228) → f7260_0_Ajouter_Store(EOS(STATIC_7260(i339)), i342, i342, i1228)
f7120_0_Ajouter_JMP(EOS(STATIC_7120(i339)), i342, i342, i836) → f7272_0_Ajouter_FieldAccess(EOS(STATIC_7272(i339)), i342, i342, i836)
f7150_0__init__Load(EOS(STATIC_7150(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7392_0__init__InvokeMethod(EOS(STATIC_7392(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7174_0__init__Return(EOS(STATIC_7174(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877) → f7354_0_Ajouter_ArrayAccess(EOS(STATIC_7354(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i877)
f7260_0_Ajouter_Store(EOS(STATIC_7260(i339)), i342, i342, i1228) → f7362_0_Ajouter_JMP(EOS(STATIC_7362(i339)), i342, i342, i1228)
f7272_0_Ajouter_FieldAccess(EOS(STATIC_7272(i339)), i342, i342, i836) → f7368_0_Ajouter_Load(EOS(STATIC_7368(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)))
f7305_0__init__InvokeMethod(EOS(STATIC_7305(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7371_0__init__Load(EOS(STATIC_7371(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7362_0_Ajouter_JMP(EOS(STATIC_7362(i339)), i342, i342, i1228) → f7408_0_Ajouter_Load(EOS(STATIC_7408(i339)), i342, i342, i1228)
f7368_0_Ajouter_Load(EOS(STATIC_7368(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339))) → f7412_0_Ajouter_Load(EOS(STATIC_7412(i339)), i342, i342, java.lang.Object(ARRAY(i339)), i836)
f7371_0__init__Load(EOS(STATIC_7371(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7482_0__init__InvokeMethod(EOS(STATIC_7482(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7392_0__init__InvokeMethod(EOS(STATIC_7392(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7435_0__init__Load(EOS(STATIC_7435(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7408_0_Ajouter_Load(EOS(STATIC_7408(i339)), i342, i342, i1228) → f4477_0_Ajouter_Load(EOS(STATIC_4477(i339)), i342, i342, i1228)
f7412_0_Ajouter_Load(EOS(STATIC_7412(i339)), i342, i342, java.lang.Object(ARRAY(i339)), i836) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f7435_0__init__Load(EOS(STATIC_7435(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7507_0__init__Load(EOS(STATIC_7507(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7514_0_Ajouter_ArrayAccess(EOS(STATIC_7514(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7515_0_Ajouter_ArrayAccess(EOS(STATIC_7515(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f7482_0__init__InvokeMethod(EOS(STATIC_7482(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7562_0__init__Load(EOS(STATIC_7562(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7507_0__init__Load(EOS(STATIC_7507(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7587_0__init__FieldAccess(EOS(STATIC_7587(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7514_0_Ajouter_ArrayAccess(EOS(STATIC_7514(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7598_0_Ajouter_Return(EOS(STATIC_7598(i339)), i342) | <(i836, i339)
f7515_0_Ajouter_ArrayAccess(EOS(STATIC_7515(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7604_0__init__Load(EOS(STATIC_7604(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) | >=(i836, i339)
f7562_0__init__Load(EOS(STATIC_7562(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7624_0__init__Load(EOS(STATIC_7624(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7587_0__init__FieldAccess(EOS(STATIC_7587(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7647_0__init__Load(EOS(STATIC_7647(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7604_0__init__Load(EOS(STATIC_7604(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7773_0__init__InvokeMethod(EOS(STATIC_7773(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f7624_0__init__Load(EOS(STATIC_7624(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7693_0__init__FieldAccess(EOS(STATIC_7693(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7647_0__init__Load(EOS(STATIC_7647(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7709_0__init__InvokeMethod(EOS(STATIC_7709(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7693_0__init__FieldAccess(EOS(STATIC_7693(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7801_0__init__Load(EOS(STATIC_7801(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7709_0__init__InvokeMethod(EOS(STATIC_7709(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7843_0__init__StackPop(EOS(STATIC_7843(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7773_0__init__InvokeMethod(EOS(STATIC_7773(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7848_0__init__Load(EOS(STATIC_7848(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f7801_0__init__Load(EOS(STATIC_7801(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7877_0__init__InvokeMethod(EOS(STATIC_7877(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7843_0__init__StackPop(EOS(STATIC_7843(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7912_0__init__Return(EOS(STATIC_7912(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7848_0__init__Load(EOS(STATIC_7848(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f7986_0__init__InvokeMethod(EOS(STATIC_7986(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f7877_0__init__InvokeMethod(EOS(STATIC_7877(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f7932_0__init__StackPop(EOS(STATIC_7932(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7912_0__init__Return(EOS(STATIC_7912(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f7951_0__init__Return(EOS(STATIC_7951(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7932_0__init__StackPop(EOS(STATIC_7932(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f8011_0__init__Return(EOS(STATIC_8011(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f7951_0__init__Return(EOS(STATIC_7951(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f8028_0__init__Return(EOS(STATIC_8028(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f7986_0__init__InvokeMethod(EOS(STATIC_7986(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8035_0__init__Load(EOS(STATIC_8035(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8011_0__init__Return(EOS(STATIC_8011(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f8054_0__init__Return(EOS(STATIC_8054(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f8028_0__init__Return(EOS(STATIC_8028(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f8090_0__init__Return(EOS(STATIC_8090(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f8035_0__init__Load(EOS(STATIC_8035(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8188_0__init__InvokeMethod(EOS(STATIC_8188(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8054_0__init__Return(EOS(STATIC_8054(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f8135_0__init__Return(EOS(STATIC_8135(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f8090_0__init__Return(EOS(STATIC_8090(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f8150_0__init__Return(EOS(STATIC_8150(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f8135_0__init__Return(EOS(STATIC_8135(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f8207_0__init__Return(EOS(STATIC_8207(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f8150_0__init__Return(EOS(STATIC_8150(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129) → f8215_0_Ajouter_ArrayAccess(EOS(STATIC_8215(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836, java.lang.Object(ARRAY(i339)), i1129)
f8188_0__init__InvokeMethod(EOS(STATIC_8188(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8220_0__init__Load(EOS(STATIC_8220(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8207_0__init__Return(EOS(STATIC_8207(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f8229_0__init__Return(EOS(STATIC_8229(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f8220_0__init__Load(EOS(STATIC_8220(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8317_0__init__InvokeMethod(EOS(STATIC_8317(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8229_0__init__Return(EOS(STATIC_8229(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836) → f8243_0_Ajouter_ArrayAccess(EOS(STATIC_8243(i339)), i342, i342, i836, java.lang.Object(ARRAY(i339)), i836)
f8317_0__init__InvokeMethod(EOS(STATIC_8317(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8327_0__init__Load(EOS(STATIC_8327(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8327_0__init__Load(EOS(STATIC_8327(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8400_0__init__InvokeMethod(EOS(STATIC_8400(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8400_0__init__InvokeMethod(EOS(STATIC_8400(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8424_0__init__Load(EOS(STATIC_8424(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8424_0__init__Load(EOS(STATIC_8424(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8445_0__init__Load(EOS(STATIC_8445(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8445_0__init__Load(EOS(STATIC_8445(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8556_0__init__FieldAccess(EOS(STATIC_8556(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8556_0__init__FieldAccess(EOS(STATIC_8556(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8585_0__init__Load(EOS(STATIC_8585(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8585_0__init__Load(EOS(STATIC_8585(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8607_0__init__InvokeMethod(EOS(STATIC_8607(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8607_0__init__InvokeMethod(EOS(STATIC_8607(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8642_0__init__StackPop(EOS(STATIC_8642(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8642_0__init__StackPop(EOS(STATIC_8642(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8664_0__init__Return(EOS(STATIC_8664(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8664_0__init__Return(EOS(STATIC_8664(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8694_0__init__Return(EOS(STATIC_8694(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8694_0__init__Return(EOS(STATIC_8694(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8735_0__init__Return(EOS(STATIC_8735(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8735_0__init__Return(EOS(STATIC_8735(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8771_0__init__Return(EOS(STATIC_8771(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8771_0__init__Return(EOS(STATIC_8771(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8796_0__init__Return(EOS(STATIC_8796(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
f8796_0__init__Return(EOS(STATIC_8796(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342) → f8814_0_Ajouter_ArrayAccess(EOS(STATIC_8814(i339)), i342, java.lang.Object(ARRAY(i339)), i836, i342)
Combined rules. Obtained 3 conditional rules for P and 11 conditional rules for R.
P rules:
f5290_1_HeapSort_InvokeMethod(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0)), x1), x2, x1) → f5290_1_HeapSort_InvokeMethod(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0)), x3, x3), +(x2, 1), x3) | &&(>(+(x2, 1), 0), <(+(x2, 1), x0))
f5290_1_HeapSort_InvokeMethod(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0)), x1), x2, x1) → f5290_1_HeapSort_InvokeMethod(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0)), x3, x3), +(x2, 1), x3) | &&(>(+(x2, 1), 0), <(+(x2, 1), x0))
f5290_1_HeapSort_InvokeMethod(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)), x1), x2, x1) → f5290_1_HeapSort_InvokeMethod(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0)), x3, x3), +(x2, 1), x3) | &&(>(+(x2, 1), 0), <(+(x2, 1), x0))
R rules:
f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0)), x1, x1) → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, -(x2, 1), -(x2, 1))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, 0, 0) → f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)), x1) | >(x0, 0)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, x2, x2) → f6913_0_Ajouter_ArrayAccess(EOS(STATIC_6913(x0)), x1, java.lang.Object(ARRAY(x0)), x2, x1) | &&(<=(x2, -1), <=(x2, 0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, 0, 0) → f6985_0_Ajouter_ArrayAccess(EOS(STATIC_6985(x0)), x1, java.lang.Object(ARRAY(x0)), 0, x1) | <=(x0, 0)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, x2, x2) → f7354_0_Ajouter_ArrayAccess(EOS(STATIC_7354(x0)), x1, x1, x2, java.lang.Object(ARRAY(x0)), /(-(x2, 1), 2)) | &&(>(x2, 0), >=(/(-(x2, 1), 2), x0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, x2, x2) → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, /(-(x2, 1), 2), /(-(x2, 1), 2)) | &&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x2)), <(/(-(x2, 1), 2), x0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, x2, x2) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), x1, java.lang.Object(ARRAY(x0)), x2, x1) | &&(>(x2, 0), <(/(-(x2, 1), 2), x0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, x2, x2) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), x1, java.lang.Object(ARRAY(x0)), x2, x1) | &&(&&(&&(>(x2, 0), <(x2, x0)), >=(/(-(x2, 1), 2), x2)), <(/(-(x2, 1), 2), x0))
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), x1, java.lang.Object(ARRAY(x0)), x2, x1) → f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)), x1) | <(x2, x0)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x1, x1, x2, x2) → f8243_0_Ajouter_ArrayAccess(EOS(STATIC_8243(x0)), x1, x1, x2, java.lang.Object(ARRAY(x0)), x2) | &&(&&(>=(x2, x0), >(x2, 0)), <(/(-(x2, 1), 2), x0))
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), x1, java.lang.Object(ARRAY(x0)), x2, x1) → f8814_0_Ajouter_ArrayAccess(EOS(STATIC_8814(x0)), x1, java.lang.Object(ARRAY(x0)), x2, x1) | >=(x2, x0)
Filtered ground terms:
Cond_f4539_0_Ajouter_LE(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE(x1, x2, x3, x4)
Cond_f4539_0_Ajouter_LE2(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE2(x1, x2, x3, x4)
f6985_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5) → f6985_0_Ajouter_ArrayAccess(x1, x2, x3, x5)
Filtered unneeded arguments:
f5290_1_HeapSort_InvokeMethod(x1, x2, x3) → f5290_1_HeapSort_InvokeMethod(x1, x2)
Cond_f5290_1_HeapSort_InvokeMethod(x1, x2, x3, x4, x5) → Cond_f5290_1_HeapSort_InvokeMethod(x1, x2, x3, x5)
Cond_f5290_1_HeapSort_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_f5290_1_HeapSort_InvokeMethod1(x1, x2, x3, x5)
Cond_f5290_1_HeapSort_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_f5290_1_HeapSort_InvokeMethod2(x1, x2, x3, x5)
Cond_f4539_0_Ajouter_LE1(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE1(x1, x3, x4, x5, x6)
Cond_f4539_0_Ajouter_LE2(x1, x2, x3, x4) → Cond_f4539_0_Ajouter_LE2(x1, x3, x4)
Cond_f4539_0_Ajouter_LE3(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE3(x1, x3, x4, x5, x6)
Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5, x6) → Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x6)
Cond_f4539_0_Ajouter_LE7(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE7(x1, x3, x4, x5, x6)
Cond_f7463_0_Ajouter_ArrayAccess1(x1, x2, x3, x4, x5, x6) → Cond_f7463_0_Ajouter_ArrayAccess1(x1, x3, x6)
f4806_0_Ajouter_Return(x1, x2) → f4806_0_Ajouter_Return(x1)
f5320_0_Ajouter_Return(x1, x2) → f5320_0_Ajouter_Return(x1)
f7598_0_Ajouter_Return(x1, x2) → f7598_0_Ajouter_Return(x1)
Filtered duplicate args:
f5311_0_Ajouter_FieldAccess(x1, x2, x3) → f5311_0_Ajouter_FieldAccess(x1, x3)
f4539_0_Ajouter_LE(x1, x2, x3, x4, x5) → f4539_0_Ajouter_LE(x1, x3, x5)
Cond_f4539_0_Ajouter_LE(x1, x2, x3, x4) → Cond_f4539_0_Ajouter_LE(x1, x2, x4)
Cond_f4539_0_Ajouter_LE1(x1, x2, x3, x4, x5) → Cond_f4539_0_Ajouter_LE1(x1, x3, x5)
f6913_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5) → f6913_0_Ajouter_ArrayAccess(x1, x3, x4, x5)
Cond_f4539_0_Ajouter_LE2(x1, x2, x3) → Cond_f4539_0_Ajouter_LE2(x1, x3)
f6985_0_Ajouter_ArrayAccess(x1, x2, x3, x4) → f6985_0_Ajouter_ArrayAccess(x1, x3, x4)
Cond_f4539_0_Ajouter_LE3(x1, x2, x3, x4, x5) → Cond_f4539_0_Ajouter_LE3(x1, x3, x5)
f7354_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5, x6) → f7354_0_Ajouter_ArrayAccess(x1, x3, x5, x6)
Cond_f4539_0_Ajouter_LE4(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE4(x1, x2, x4, x6)
Cond_f4539_0_Ajouter_LE5(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE5(x1, x2, x4, x6)
f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5) → f7463_0_Ajouter_ArrayAccess(x1, x3, x4, x5)
Cond_f4539_0_Ajouter_LE6(x1, x2, x3, x4, x5, x6) → Cond_f4539_0_Ajouter_LE6(x1, x2, x4, x6)
Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5) → Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x4, x5)
Cond_f4539_0_Ajouter_LE7(x1, x2, x3, x4, x5) → Cond_f4539_0_Ajouter_LE7(x1, x3, x5)
f8243_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5, x6) → f8243_0_Ajouter_ArrayAccess(x1, x3, x5, x6)
Cond_f7463_0_Ajouter_ArrayAccess1(x1, x2, x3) → Cond_f7463_0_Ajouter_ArrayAccess1(x1, x3)
f8814_0_Ajouter_ArrayAccess(x1, x2, x3, x4, x5) → f8814_0_Ajouter_ArrayAccess(x1, x3, x4, x5)
Filtered unneeded arguments:
Cond_f5290_1_HeapSort_InvokeMethod(x1, x2, x3, x4) → Cond_f5290_1_HeapSort_InvokeMethod(x1, x2, x3)
Cond_f5290_1_HeapSort_InvokeMethod1(x1, x2, x3, x4) → Cond_f5290_1_HeapSort_InvokeMethod1(x1, x2, x3)
Cond_f5290_1_HeapSort_InvokeMethod2(x1, x2, x3, x4) → Cond_f5290_1_HeapSort_InvokeMethod2(x1, x2, x3)
f4539_0_Ajouter_LE(x1, x2, x3) → f4539_0_Ajouter_LE(x1, x3)
Cond_f4539_0_Ajouter_LE(x1, x2, x3) → Cond_f4539_0_Ajouter_LE(x1, x2)
Cond_f4539_0_Ajouter_LE1(x1, x2, x3) → Cond_f4539_0_Ajouter_LE1(x1)
Cond_f4539_0_Ajouter_LE2(x1, x2) → Cond_f4539_0_Ajouter_LE2(x1)
Cond_f4539_0_Ajouter_LE3(x1, x2, x3) → Cond_f4539_0_Ajouter_LE3(x1)
Cond_f4539_0_Ajouter_LE4(x1, x2, x3, x4) → Cond_f4539_0_Ajouter_LE4(x1, x2, x4)
Cond_f4539_0_Ajouter_LE5(x1, x2, x3, x4) → Cond_f4539_0_Ajouter_LE5(x1, x2, x4)
Cond_f4539_0_Ajouter_LE6(x1, x2, x3, x4) → Cond_f4539_0_Ajouter_LE6(x1, x2, x4)
Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4) → Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x3)
Cond_f4539_0_Ajouter_LE7(x1, x2, x3) → Cond_f4539_0_Ajouter_LE7(x1)
Cond_f7463_0_Ajouter_ArrayAccess1(x1, x2) → Cond_f7463_0_Ajouter_ArrayAccess1(x1)
f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4) → f7463_0_Ajouter_ArrayAccess(x1, x2, x3)
f5311_0_Ajouter_FieldAccess(x1, x2) → f5311_0_Ajouter_FieldAccess(x1)
Combined rules. Obtained 3 conditional rules for P and 11 conditional rules for R.
P rules:
F5290_1_HEAPSORT_INVOKEMETHOD(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0))), x2) → F5290_1_HEAPSORT_INVOKEMETHOD(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))), +(x2, 1)) | &&(<(+(x2, 1), x0), >(x2, -1))
F5290_1_HEAPSORT_INVOKEMETHOD(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0))), x2) → F5290_1_HEAPSORT_INVOKEMETHOD(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))), +(x2, 1)) | &&(<(+(x2, 1), x0), >(x2, -1))
F5290_1_HEAPSORT_INVOKEMETHOD(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0))), x2) → F5290_1_HEAPSORT_INVOKEMETHOD(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))), +(x2, 1)) | &&(<(+(x2, 1), x0), >(x2, -1))
R rules:
f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))) → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), -(x2, 1))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), 0) → f7598_0_Ajouter_Return(EOS(STATIC_7598(x0))) | >(x0, 0)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → f6913_0_Ajouter_ArrayAccess(EOS(STATIC_6913(x0)), java.lang.Object(ARRAY(x0)), x2, x1) | &&(<=(x2, -1), <=(x2, 0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), 0) → f6985_0_Ajouter_ArrayAccess(EOS(STATIC_6985(x0)), java.lang.Object(ARRAY(x0)), x1) | <=(x0, 0)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → f7354_0_Ajouter_ArrayAccess(EOS(STATIC_7354(x0)), x1, java.lang.Object(ARRAY(x0)), /(-(x2, 1), 2)) | &&(>=(/(-(x2, 1), 2), x0), >(x2, 0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), /(-(x2, 1), 2)) | &&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x0)), <(/(-(x2, 1), 2), x2))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) | &&(<(/(-(x2, 1), 2), x0), >(x2, 0))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) | &&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x0)), >=(/(-(x2, 1), 2), x2))
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) → f7598_0_Ajouter_Return(EOS(STATIC_7598(x0))) | <(x2, x0)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → f8243_0_Ajouter_ArrayAccess(EOS(STATIC_8243(x0)), x1, java.lang.Object(ARRAY(x0)), x2) | &&(&&(>=(x2, x0), <(/(-(x2, 1), 2), x0)), >(x2, 0))
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) → f8814_0_Ajouter_ArrayAccess(EOS(STATIC_8814(x0)), java.lang.Object(ARRAY(x0)), x2, x1) | >=(x2, x0)
Finished conversion. Obtained 6 rules for P and 21 rules for R. System has predefined symbols.
P rules:
F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0))), x2) → COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2, 1), x0), >(x2, -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0))), x2)
COND_F5290_1_HEAPSORT_INVOKEMETHOD(TRUE, f4806_0_Ajouter_Return(EOS(STATIC_4806(x0))), x2) → F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))), +(x2, 1))
F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0))), x2) → COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2, 1), x0), >(x2, -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0))), x2)
COND_F5290_1_HEAPSORT_INVOKEMETHOD1(TRUE, f5320_0_Ajouter_Return(EOS(STATIC_5320(x0))), x2) → F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))), +(x2, 1))
F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0))), x2) → COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2, 1), x0), >(x2, -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0))), x2)
COND_F5290_1_HEAPSORT_INVOKEMETHOD2(TRUE, f7598_0_Ajouter_Return(EOS(STATIC_7598(x0))), x2) → F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))), +(x2, 1))
R rules:
f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0))) → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), -(x2, 1))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), 0) → Cond_f4539_0_Ajouter_LE(>(x0, 0), EOS(STATIC_4539(x0)), 0)
Cond_f4539_0_Ajouter_LE(TRUE, EOS(STATIC_4539(x0)), 0) → f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → Cond_f4539_0_Ajouter_LE1(&&(<=(x2, -1), <=(x2, 0)), EOS(STATIC_4539(x0)), x2, x1)
Cond_f4539_0_Ajouter_LE1(TRUE, EOS(STATIC_4539(x0)), x2, x1) → f6913_0_Ajouter_ArrayAccess(EOS(STATIC_6913(x0)), java.lang.Object(ARRAY(x0)), x2, x1)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), 0) → Cond_f4539_0_Ajouter_LE2(<=(x0, 0), EOS(STATIC_4539(x0)), 0, x1)
Cond_f4539_0_Ajouter_LE2(TRUE, EOS(STATIC_4539(x0)), 0, x1) → f6985_0_Ajouter_ArrayAccess(EOS(STATIC_6985(x0)), java.lang.Object(ARRAY(x0)), x1)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → Cond_f4539_0_Ajouter_LE3(&&(>=(/(-(x2, 1), 2), x0), >(x2, 0)), EOS(STATIC_4539(x0)), x2, x1)
Cond_f4539_0_Ajouter_LE3(TRUE, EOS(STATIC_4539(x0)), x2, x1) → f7354_0_Ajouter_ArrayAccess(EOS(STATIC_7354(x0)), x1, java.lang.Object(ARRAY(x0)), /(-(x2, 1), 2))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → Cond_f4539_0_Ajouter_LE4(&&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x0)), <(/(-(x2, 1), 2), x2)), EOS(STATIC_4539(x0)), x2)
Cond_f4539_0_Ajouter_LE4(TRUE, EOS(STATIC_4539(x0)), x2) → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), /(-(x2, 1), 2))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → Cond_f4539_0_Ajouter_LE5(&&(<(/(-(x2, 1), 2), x0), >(x2, 0)), EOS(STATIC_4539(x0)), x2)
Cond_f4539_0_Ajouter_LE5(TRUE, EOS(STATIC_4539(x0)), x2) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → Cond_f4539_0_Ajouter_LE6(&&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x0)), >=(/(-(x2, 1), 2), x2)), EOS(STATIC_4539(x0)), x2)
Cond_f4539_0_Ajouter_LE6(TRUE, EOS(STATIC_4539(x0)), x2) → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) → Cond_f7463_0_Ajouter_ArrayAccess(<(x2, x0), EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)
Cond_f7463_0_Ajouter_ArrayAccess(TRUE, EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) → f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)))
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2) → Cond_f4539_0_Ajouter_LE7(&&(&&(>=(x2, x0), <(/(-(x2, 1), 2), x0)), >(x2, 0)), EOS(STATIC_4539(x0)), x2, x1)
Cond_f4539_0_Ajouter_LE7(TRUE, EOS(STATIC_4539(x0)), x2, x1) → f8243_0_Ajouter_ArrayAccess(EOS(STATIC_8243(x0)), x1, java.lang.Object(ARRAY(x0)), x2)
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2) → Cond_f7463_0_Ajouter_ArrayAccess1(>=(x2, x0), EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2, x1)
Cond_f7463_0_Ajouter_ArrayAccess1(TRUE, EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2, x1) → f8814_0_Ajouter_ArrayAccess(EOS(STATIC_8814(x0)), java.lang.Object(ARRAY(x0)), x2, x1)
!= | ~ | 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] + 1 < x0[0] && x2[0] > -1 ∧f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))) →* f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[1])))∧x2[0] →* x2[1])
(1) -> (0), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))) →* f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0])))∧x2[1] + 1 →* x2[0])
(1) -> (2), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))) →* f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2])))∧x2[1] + 1 →* x2[2])
(1) -> (4), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))) →* f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4])))∧x2[1] + 1 →* x2[4])
(2) -> (3), if (x2[2] + 1 < x0[2] && x2[2] > -1 ∧f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))) →* f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[3])))∧x2[2] →* x2[3])
(3) -> (0), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))) →* f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0])))∧x2[3] + 1 →* x2[0])
(3) -> (2), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))) →* f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2])))∧x2[3] + 1 →* x2[2])
(3) -> (4), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))) →* f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4])))∧x2[3] + 1 →* x2[4])
(4) -> (5), if (x2[4] + 1 < x0[4] && x2[4] > -1 ∧f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))) →* f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[5])))∧x2[4] →* x2[5])
(5) -> (0), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))) →* f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0])))∧x2[5] + 1 →* x2[0])
(5) -> (2), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))) →* f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2])))∧x2[5] + 1 →* x2[2])
(5) -> (4), if (f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))) →* f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4])))∧x2[5] + 1 →* x2[4])
(1) (&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1))=TRUE∧f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0])))=f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[1])))∧x2[0]=x2[1] ⇒ F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])≥NonInfC∧F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])≥COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])∧(UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])), ≥))
(2) (<(+(x2[0], 1), x0[0])=TRUE∧>(x2[0], -1)=TRUE ⇒ F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])≥NonInfC∧F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])≥COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])∧(UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])), ≥))
(3) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[0] + [bni_49]x0[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(4) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[0] + [bni_49]x0[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(5) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]x2[0] + [bni_49]x0[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(6) (x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])), ≥)∧[bni_49 + (-1)Bound*bni_49] + [bni_49]x0[0] ≥ 0∧[(-1)bso_50] ≥ 0)
(7) (COND_F5290_1_HEAPSORT_INVOKEMETHOD(TRUE, f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[1]))), x2[1])≥NonInfC∧COND_F5290_1_HEAPSORT_INVOKEMETHOD(TRUE, f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[1]))), x2[1])≥F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))∧(UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))), ≥))
(8) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))), ≥)∧[bni_51] = 0∧[1 + (-1)bso_52] ≥ 0)
(9) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))), ≥)∧[bni_51] = 0∧[1 + (-1)bso_52] ≥ 0)
(10) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))), ≥)∧[bni_51] = 0∧[1 + (-1)bso_52] ≥ 0)
(11) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))), ≥)∧[bni_51] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_52] ≥ 0)
(12) (&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1))=TRUE∧f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2])))=f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[3])))∧x2[2]=x2[3] ⇒ F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])≥NonInfC∧F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])≥COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])∧(UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])), ≥))
(13) (<(+(x2[2], 1), x0[2])=TRUE∧>(x2[2], -1)=TRUE ⇒ F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])≥NonInfC∧F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])≥COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])∧(UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])), ≥))
(14) (x0[2] + [-2] + [-1]x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[2] + [bni_53]x0[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(15) (x0[2] + [-2] + [-1]x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[2] + [bni_53]x0[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(16) (x0[2] + [-2] + [-1]x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]x2[2] + [bni_53]x0[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(17) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])), ≥)∧[bni_53 + (-1)Bound*bni_53] + [bni_53]x0[2] ≥ 0∧[(-1)bso_54] ≥ 0)
(18) (COND_F5290_1_HEAPSORT_INVOKEMETHOD1(TRUE, f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[3]))), x2[3])≥NonInfC∧COND_F5290_1_HEAPSORT_INVOKEMETHOD1(TRUE, f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[3]))), x2[3])≥F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))∧(UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))), ≥))
(19) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))), ≥)∧[bni_55] = 0∧[1 + (-1)bso_56] ≥ 0)
(20) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))), ≥)∧[bni_55] = 0∧[1 + (-1)bso_56] ≥ 0)
(21) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))), ≥)∧[bni_55] = 0∧[1 + (-1)bso_56] ≥ 0)
(22) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))), ≥)∧[bni_55] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_56] ≥ 0)
(23) (&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1))=TRUE∧f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4])))=f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[5])))∧x2[4]=x2[5] ⇒ F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])≥NonInfC∧F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])≥COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])∧(UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])), ≥))
(24) (<(+(x2[4], 1), x0[4])=TRUE∧>(x2[4], -1)=TRUE ⇒ F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])≥NonInfC∧F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])≥COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])∧(UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])), ≥))
(25) (x0[4] + [-2] + [-1]x2[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]x2[4] + [bni_57]x0[4] ≥ 0∧[(-1)bso_58] ≥ 0)
(26) (x0[4] + [-2] + [-1]x2[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]x2[4] + [bni_57]x0[4] ≥ 0∧[(-1)bso_58] ≥ 0)
(27) (x0[4] + [-2] + [-1]x2[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]x2[4] + [bni_57]x0[4] ≥ 0∧[(-1)bso_58] ≥ 0)
(28) (x0[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])), ≥)∧[bni_57 + (-1)Bound*bni_57] + [bni_57]x0[4] ≥ 0∧[(-1)bso_58] ≥ 0)
(29) (COND_F5290_1_HEAPSORT_INVOKEMETHOD2(TRUE, f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[5]))), x2[5])≥NonInfC∧COND_F5290_1_HEAPSORT_INVOKEMETHOD2(TRUE, f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[5]))), x2[5])≥F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))∧(UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))), ≥))
(30) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))), ≥)∧[bni_59] = 0∧[1 + (-1)bso_60] ≥ 0)
(31) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))), ≥)∧[bni_59] = 0∧[1 + (-1)bso_60] ≥ 0)
(32) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))), ≥)∧[bni_59] = 0∧[1 + (-1)bso_60] ≥ 0)
(33) ((UIncreasing(F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))), ≥)∧[bni_59] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_60] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(f5311_0_Ajouter_FieldAccess(x1)) = x1
POL(EOS(x1)) = x1
POL(STATIC_5311(x1)) = x1
POL(f4539_0_Ajouter_LE(x1, x2)) = x1
POL(STATIC_4539(x1)) = x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(1) = [1]
POL(0) = 0
POL(Cond_f4539_0_Ajouter_LE(x1, x2, x3)) = x2
POL(>(x1, x2)) = [-1]
POL(f7598_0_Ajouter_Return(x1)) = x1
POL(STATIC_7598(x1)) = x1
POL(Cond_f4539_0_Ajouter_LE1(x1, x2, x3, x4)) = [-1] + x2
POL(&&(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(-1) = [-1]
POL(f6913_0_Ajouter_ArrayAccess(x1, x2, x3, x4)) = [-1] + [2]x2 + [-1]x1
POL(STATIC_6913(x1)) = x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1)) = x1
POL(Cond_f4539_0_Ajouter_LE2(x1, x2, x3, x4)) = [-1] + x2
POL(f6985_0_Ajouter_ArrayAccess(x1, x2, x3)) = [-1] + [2]x2 + [-1]x1
POL(STATIC_6985(x1)) = x1
POL(Cond_f4539_0_Ajouter_LE3(x1, x2, x3, x4)) = x2
POL(>=(x1, x2)) = [-1]
POL(2) = [2]
POL(f7354_0_Ajouter_ArrayAccess(x1, x2, x3, x4)) = [-1] + x3
POL(STATIC_7354(x1)) = x1
POL(Cond_f4539_0_Ajouter_LE4(x1, x2, x3)) = x2
POL(<(x1, x2)) = [-1]
POL(Cond_f4539_0_Ajouter_LE5(x1, x2, x3)) = x2
POL(f7463_0_Ajouter_ArrayAccess(x1, x2, x3)) = x2
POL(STATIC_7463(x1)) = x1
POL(Cond_f4539_0_Ajouter_LE6(x1, x2, x3)) = x2
POL(Cond_f7463_0_Ajouter_ArrayAccess(x1, x2, x3, x4)) = x3
POL(Cond_f4539_0_Ajouter_LE7(x1, x2, x3, x4)) = [-1] + x2
POL(f8243_0_Ajouter_ArrayAccess(x1, x2, x3, x4)) = [-1] + [2]x3 + [-1]x1
POL(STATIC_8243(x1)) = x1
POL(Cond_f7463_0_Ajouter_ArrayAccess1(x1, x2, x3, x4, x5)) = [-1] + x3
POL(f8814_0_Ajouter_ArrayAccess(x1, x2, x3, x4)) = [-1] + x2
POL(STATIC_8814(x1)) = x1
POL(F5290_1_HEAPSORT_INVOKEMETHOD'(x1, x2)) = [-1] + [-1]x2 + x1
POL(f4806_0_Ajouter_Return(x1)) = x1
POL(STATIC_4806(x1)) = x1
POL(COND_F5290_1_HEAPSORT_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(+(x1, x2)) = x1 + x2
POL(f5320_0_Ajouter_Return(x1)) = x1
POL(STATIC_5320(x1)) = x1
POL(COND_F5290_1_HEAPSORT_INVOKEMETHOD1(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(COND_F5290_1_HEAPSORT_INVOKEMETHOD2(x1, x2, x3)) = [-1] + [-1]x3 + x2
Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(TermCSAR-Mode @ Context)
POL(/(x1, 2)1 @ {f4539_0_Ajouter_LE_2/1}) = max{x1, [-1]x1} + [-1]
POL(/(x1, 2)1 @ {f7354_0_Ajouter_ArrayAccess_4/3}) = [-1]max{x1, [-1]x1} + [1]
COND_F5290_1_HEAPSORT_INVOKEMETHOD(TRUE, f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[1]))), x2[1]) → F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[1]))), +(x2[1], 1))
COND_F5290_1_HEAPSORT_INVOKEMETHOD1(TRUE, f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[3]))), x2[3]) → F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[3]))), +(x2[3], 1))
COND_F5290_1_HEAPSORT_INVOKEMETHOD2(TRUE, f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[5]))), x2[5]) → F5290_1_HEAPSORT_INVOKEMETHOD'(f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0[5]))), +(x2[5], 1))
F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0]) → COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])
F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2]) → COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])
F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4]) → COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])
F5290_1_HEAPSORT_INVOKEMETHOD'(f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0]) → COND_F5290_1_HEAPSORT_INVOKEMETHOD(&&(<(+(x2[0], 1), x0[0]), >(x2[0], -1)), f4806_0_Ajouter_Return(EOS(STATIC_4806(x0[0]))), x2[0])
F5290_1_HEAPSORT_INVOKEMETHOD'(f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2]) → COND_F5290_1_HEAPSORT_INVOKEMETHOD1(&&(<(+(x2[2], 1), x0[2]), >(x2[2], -1)), f5320_0_Ajouter_Return(EOS(STATIC_5320(x0[2]))), x2[2])
F5290_1_HEAPSORT_INVOKEMETHOD'(f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4]) → COND_F5290_1_HEAPSORT_INVOKEMETHOD2(&&(<(+(x2[4], 1), x0[4]), >(x2[4], -1)), f7598_0_Ajouter_Return(EOS(STATIC_7598(x0[4]))), x2[4])
f5311_0_Ajouter_FieldAccess(EOS(STATIC_5311(x0)))1 → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), -(x2, 1))1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), 0)1 → Cond_f4539_0_Ajouter_LE(>(x0, 0), EOS(STATIC_4539(x0)), 0)1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2)1 → Cond_f4539_0_Ajouter_LE1(&&(<=(x2, -1), <=(x2, 0)), EOS(STATIC_4539(x0)), x2, x1)1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), 0)1 → Cond_f4539_0_Ajouter_LE2(<=(x0, 0), EOS(STATIC_4539(x0)), 0, x1)1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2)1 → Cond_f4539_0_Ajouter_LE3(&&(>=(/(-(x2, 1), 2), x0), >(x2, 0)), EOS(STATIC_4539(x0)), x2, x1)1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2)1 → Cond_f4539_0_Ajouter_LE4(&&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x0)), <(/(-(x2, 1), 2), x2)), EOS(STATIC_4539(x0)), x2)1
Cond_f4539_0_Ajouter_LE4(TRUE, EOS(STATIC_4539(x0)), x2)1 → f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), /(-(x2, 1), 2))1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2)1 ↔ Cond_f4539_0_Ajouter_LE5(&&(<(/(-(x2, 1), 2), x0), >(x2, 0)), EOS(STATIC_4539(x0)), x2)1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2)1 ↔ Cond_f4539_0_Ajouter_LE6(&&(&&(&&(>(x2, 0), <(x2, x0)), <(/(-(x2, 1), 2), x0)), >=(/(-(x2, 1), 2), x2)), EOS(STATIC_4539(x0)), x2)1
f4539_0_Ajouter_LE(EOS(STATIC_4539(x0)), x2)1 → Cond_f4539_0_Ajouter_LE7(&&(&&(>=(x2, x0), <(/(-(x2, 1), 2), x0)), >(x2, 0)), EOS(STATIC_4539(x0)), x2, x1)1
/1 →
Cond_f4539_0_Ajouter_LE(TRUE, EOS(STATIC_4539(x0)), 0)1 ↔ f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)))1
Cond_f4539_0_Ajouter_LE1(TRUE, EOS(STATIC_4539(x0)), x2, x1)1 → f6913_0_Ajouter_ArrayAccess(EOS(STATIC_6913(x0)), java.lang.Object(ARRAY(x0)), x2, x1)1
Cond_f4539_0_Ajouter_LE2(TRUE, EOS(STATIC_4539(x0)), 0, x1)1 ↔ f6985_0_Ajouter_ArrayAccess(EOS(STATIC_6985(x0)), java.lang.Object(ARRAY(x0)), x1)1
Cond_f4539_0_Ajouter_LE3(TRUE, EOS(STATIC_4539(x0)), x2, x1)1 → f7354_0_Ajouter_ArrayAccess(EOS(STATIC_7354(x0)), x1, java.lang.Object(ARRAY(x0)), /(-(x2, 1), 2))1
Cond_f4539_0_Ajouter_LE5(TRUE, EOS(STATIC_4539(x0)), x2)1 → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)1
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)1 ↔ Cond_f7463_0_Ajouter_ArrayAccess(<(x2, x0), EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)1
f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)1 → Cond_f7463_0_Ajouter_ArrayAccess1(>=(x2, x0), EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2, x1)1
Cond_f4539_0_Ajouter_LE6(TRUE, EOS(STATIC_4539(x0)), x2)1 → f7463_0_Ajouter_ArrayAccess(EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)1
Cond_f7463_0_Ajouter_ArrayAccess(TRUE, EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2)1 ↔ f7598_0_Ajouter_Return(EOS(STATIC_7598(x0)))1
Cond_f4539_0_Ajouter_LE7(TRUE, EOS(STATIC_4539(x0)), x2, x1)1 ↔ f8243_0_Ajouter_ArrayAccess(EOS(STATIC_8243(x0)), x1, java.lang.Object(ARRAY(x0)), x2)1
Cond_f7463_0_Ajouter_ArrayAccess1(TRUE, EOS(STATIC_7463(x0)), java.lang.Object(ARRAY(x0)), x2, x1)1 ↔ f8814_0_Ajouter_ArrayAccess(EOS(STATIC_8814(x0)), java.lang.Object(ARRAY(x0)), x2, x1)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
!= | ~ | 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
Generated rules. Obtained 43 IRules
P rules:
f4165_0_main_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, i686) → f4172_0_main_GE(EOS, java.lang.Object(ARRAY(i27)), i686, i686, i27)
f4172_0_main_GE(EOS, java.lang.Object(ARRAY(i27)), i686, i686, i27) → f4179_0_main_GE(EOS, java.lang.Object(ARRAY(i27)), i686, i686, i27)
f4179_0_main_GE(EOS, java.lang.Object(ARRAY(i27)), i686, i686, i27) → f4206_0_main_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686) | <(i686, i27)
f4206_0_main_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686) → f4224_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)))
f4224_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27))) → f4290_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f4290_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4311_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f4311_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4352_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685)
f4352_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685) → f4368_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, java.lang.Object(ARRAY(i27)))
f4368_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, java.lang.Object(ARRAY(i27))) → f4395_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27) | >=(i27, 0)
f4395_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27) → f4397_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27)
f4395_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27) → f4398_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27)
f4397_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27) → f4404_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) | <(i685, i27)
f4404_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4414_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)))
f4414_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27))) → f4426_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i685)
f4426_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i685) → f4460_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i685)
f4460_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i685) → f4512_0_random_Store(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715)
f4512_0_random_Store(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715) → f4543_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715)
f4543_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715) → f4585_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715, i685)
f4585_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715, i685) → f4617_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715, i685, 1)
f4617_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715, i685, matching1) → f4784_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715, +(i685, 1)) | &&(>=(i685, 0), =(matching1, 1))
f4784_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715, i872) → f4804_0_random_Load(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715)
f4804_0_random_Load(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715) → f4829_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, o715)
f4829_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(o756sub)) → f4850_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(o756sub))
f4850_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(o756sub)) → f4887_0_length_Load(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(o756sub), java.lang.Object(o756sub))
f4887_0_length_Load(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(o756sub), java.lang.Object(o756sub)) → f5017_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(o756sub), java.lang.Object(o756sub))
f5017_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(java.lang.String(o814sub, i947)), java.lang.Object(java.lang.String(o814sub, i947))) → f5053_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(java.lang.String(o814sub, i947)), java.lang.Object(java.lang.String(o814sub, i947)))
f5053_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(java.lang.String(o814sub, i947)), java.lang.Object(java.lang.String(o814sub, i947))) → f5111_0_length_Return(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(java.lang.String(o814sub, i947)))
f5111_0_length_Return(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(java.lang.String(o814sub, i947))) → f5148_0_random_Return(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f5148_0_random_Return(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f5187_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f5187_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f5245_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f5245_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f5293_0_main_Inc(EOS, java.lang.Object(ARRAY(i27)), i686) | <(i686, i27)
f5293_0_main_Inc(EOS, java.lang.Object(ARRAY(i27)), i686) → f5337_0_main_JMP(EOS, java.lang.Object(ARRAY(i27)), +(i686, 1)) | >=(i686, 0)
f5337_0_main_JMP(EOS, java.lang.Object(ARRAY(i27)), i1024) → f5408_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i1024)
f5408_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i1024) → f4105_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i1024)
f4105_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i686) → f4165_0_main_FieldAccess(EOS, java.lang.Object(ARRAY(i27)), i686, i686)
f4398_0_random_LT(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686, i685, i27) → f4407_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) | >=(i685, i27)
f4407_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4421_0_random_Return(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f4421_0_random_Return(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4442_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f4442_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4505_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686)
f4505_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i27)), i686, java.lang.Object(ARRAY(i27)), i686) → f4529_0_main_Inc(EOS, java.lang.Object(ARRAY(i27)), i686) | <(i686, i27)
f4529_0_main_Inc(EOS, java.lang.Object(ARRAY(i27)), i686) → f4575_0_main_JMP(EOS, java.lang.Object(ARRAY(i27)), +(i686, 1)) | >=(i686, 0)
f4575_0_main_JMP(EOS, java.lang.Object(ARRAY(i27)), i837) → f4600_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i837)
f4600_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i837) → f4105_0_main_Load(EOS, java.lang.Object(ARRAY(i27)), i837)
Combined rules. Obtained 1 IRules
P rules:
f4165_0_main_FieldAccess(EOS, java.lang.Object(ARRAY(x0)), x1, x1) → f4165_0_main_FieldAccess(EOS, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), <(x1, x0)), >(+(x0, 1), 0))
Filtered ground terms:
f4165_0_main_FieldAccess(x1, x2, x3, x4) → f4165_0_main_FieldAccess(x2, x3, x4)
Cond_f4165_0_main_FieldAccess(x1, x2, x3, x4, x5) → Cond_f4165_0_main_FieldAccess(x1, x3, x4, x5)
Filtered duplicate terms:
f4165_0_main_FieldAccess(x1, x2, x3) → f4165_0_main_FieldAccess(x1, x3)
Cond_f4165_0_main_FieldAccess(x1, x2, x3, x4) → Cond_f4165_0_main_FieldAccess(x1, x2, x4)
Prepared 1 rules for path length conversion:
P rules:
f4165_0_main_FieldAccess(java.lang.Object(ARRAY(x0)), x1, x0) → f4165_0_main_FieldAccess(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), <(x1, x0)), >(+(x0, 1), 0))
Finished conversion. Obtained 1 rules.
P rules:
f4165_0_main_FieldAccess(v5, x1, x0) → f4165_0_main_FieldAccess(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))
Found the following polynomial interpretation:
Therefore the following rule(s) have been dropped: