0 JBC
↳1 JBCToGraph (⇒, 4380 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 10 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 1440 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 300 ms)
↳9 AND
↳10 IDP
↳11 IDependencyGraphProof (⇔, 0 ms)
↳12 IDP
↳13 IDPNonInfProof (⇒, 220 ms)
↳14 AND
↳15 IDP
↳16 IDependencyGraphProof (⇔, 0 ms)
↳17 TRUE
↳18 IDP
↳19 IDependencyGraphProof (⇔, 0 ms)
↳20 TRUE
↳21 IDP
↳22 IDependencyGraphProof (⇔, 0 ms)
↳23 TRUE
↳24 JBCTerminationSCC
↳25 SCCToIDPv1Proof (⇒, 360 ms)
↳26 IDP
↳27 IDPNonInfProof (⇒, 130 ms)
↳28 AND
↳29 IDP
↳30 IDependencyGraphProof (⇔, 0 ms)
↳31 TRUE
↳32 IDP
↳33 IDependencyGraphProof (⇔, 0 ms)
↳34 TRUE
↳35 JBCTerminationSCC
↳36 SCCToIDPv1Proof (⇒, 370 ms)
↳37 IDP
↳38 IDPNonInfProof (⇒, 1130 ms)
↳39 IDP
↳40 IDependencyGraphProof (⇔, 0 ms)
↳41 IDP
↳42 IDPNonInfProof (⇒, 470 ms)
↳43 IDP
↳44 IDependencyGraphProof (⇔, 0 ms)
↳45 TRUE
↳46 JBCTerminationSCC
↳47 SCCToIDPv1Proof (⇒, 270 ms)
↳48 IDP
↳49 IDPNonInfProof (⇒, 1830 ms)
↳50 IDP
↳51 IDependencyGraphProof (⇔, 0 ms)
↳52 IDP
↳53 IDPNonInfProof (⇒, 400 ms)
↳54 IDP
↳55 IDependencyGraphProof (⇔, 0 ms)
↳56 TRUE
class KnapsackDP
{
static int nbObjects;
static int [] weight={2,3,5,2,4,6,3,1};
static int [] utility={5,8,14,6,13,17,10,4};
static int weightmax=12;
static int [] [] array;
// Display the table
static void consoleDisplay()
{
int i,j;
for(i=0;i<nbObjects;i++)
{
for(j=0;j<=weightmax;j++)
{
//System.out.print(array[i][j]+"\t");
}
//System.out.println("");
}
}
// LateX
static void Display()
{
int i,j;
for(i=0;i<nbObjects;i++)
{
for(j=0;j<=weightmax;j++)
{
if (j!=weightmax) {} //System.out.print(array[i][j]+" & ");
else {} //System.out.print(array[i][j]+" ");
}
//System.out.println("\\\\");
}
}
// Extract the solution from the table
static void InterpretArray()
{
int i,u,w;
u=0;
w=weightmax;
for(i=nbObjects-1;i>=1;i--)
{
if (array[i][w]!=array[i-1][w])
{
//System.out.print((i+1)+" ");
w=w-weight[i];
u=u+utility[i];
}
}
if (array[0][w]!=0);
{
//System.out.println("1");
w=w-weight[0];
u=u+utility[0];
}
//System.out.println("Cross check:"+u+" remaining weight "+w);
}
static int max(int a, int b)
{
//if (a>b) return a; else return b;
return ( (a>b) ? (a) : (b) );
}
static void SolveDP()
{
int i,j;
array=new int[nbObjects][weightmax+1];
// initialize the first row
for(j=0;j<=weightmax;j++)
if (j<weight[0]) array[0][j]=0;
else array[0][j]=utility[0];
// for all other rows
for(i=1;i<nbObjects;i++)
{
for(j=0;j<=weightmax;j++)
if (j-weight[i]<0) array[i][j]=array[i-1][j];
else
array[i][j]=max( array[i-1][j],
array[i-1][j-weight[i]]+utility[i]);
}
}
public static void main(String[] args)
{
//System.out.println("Solving knapsack using the dynamic programming paradigm.");
nbObjects = args.length;
SolveDP();
Display();
//System.out.println("Reading solution:");
InterpretArray();
}
}
Generated 111 rules for P and 0 rules for R.
P rules:
9950_0_SolveDP_FieldAccess(EOS(STATIC_9950(i322, matching1)), i5568, i5568) → 9952_0_SolveDP_GE(EOS(STATIC_9952(i322, 12)), i5568, i5568, i322) | =(matching1, 12)
9952_0_SolveDP_GE(EOS(STATIC_9952(i322, matching1)), i5568, i5568, i322) → 9954_0_SolveDP_GE(EOS(STATIC_9954(i322, 12)), i5568, i5568, i322) | =(matching1, 12)
9954_0_SolveDP_GE(EOS(STATIC_9954(i322, matching1)), i5568, i5568, i322) → 9956_0_SolveDP_ConstantStackPush(EOS(STATIC_9956(i322, 12)), i5568) | &&(<(i5568, i322), =(matching1, 12))
9956_0_SolveDP_ConstantStackPush(EOS(STATIC_9956(i322, matching1)), i5568) → 9959_0_SolveDP_Store(EOS(STATIC_9959(i322, 12)), i5568, 0) | =(matching1, 12)
9959_0_SolveDP_Store(EOS(STATIC_9959(i322, matching1)), i5568, matching2) → 9961_0_SolveDP_Load(EOS(STATIC_9961(i322, 12)), i5568, 0) | &&(=(matching1, 12), =(matching2, 0))
9961_0_SolveDP_Load(EOS(STATIC_9961(i322, matching1)), i5568, matching2) → 10320_0_SolveDP_Load(EOS(STATIC_10320(i322, 12)), i5568, 0) | &&(=(matching1, 12), =(matching2, 0))
10320_0_SolveDP_Load(EOS(STATIC_10320(i322, matching1)), i6010, i6011) → 10667_0_SolveDP_Load(EOS(STATIC_10667(i322, 12)), i6010, i6011) | =(matching1, 12)
10667_0_SolveDP_Load(EOS(STATIC_10667(i322, matching1)), i6452, i6453) → 11030_0_SolveDP_Load(EOS(STATIC_11030(i322, 12)), i6452, i6453) | =(matching1, 12)
11030_0_SolveDP_Load(EOS(STATIC_11030(i322, matching1)), i6894, i6895) → 11383_0_SolveDP_Load(EOS(STATIC_11383(i322, 12)), i6894, i6895) | =(matching1, 12)
11383_0_SolveDP_Load(EOS(STATIC_11383(i322, matching1)), i7336, i7337) → 11388_0_SolveDP_FieldAccess(EOS(STATIC_11388(i322, 12)), i7336, i7337, i7337) | =(matching1, 12)
11388_0_SolveDP_FieldAccess(EOS(STATIC_11388(i322, matching1)), i7336, i7337, i7337) → 11389_0_SolveDP_GT(EOS(STATIC_11389(i322, 12)), i7336, i7337, i7337, 12) | =(matching1, 12)
11389_0_SolveDP_GT(EOS(STATIC_11389(i322, matching1)), i7336, i7345, i7345, matching2) → 11390_0_SolveDP_GT(EOS(STATIC_11390(i322, 12)), i7336, i7345, i7345, 12) | &&(=(matching1, 12), =(matching2, 12))
11389_0_SolveDP_GT(EOS(STATIC_11389(i322, matching1)), i7336, matching2, matching3, matching4) → 11391_0_SolveDP_GT(EOS(STATIC_11391(i322, 12)), i7336, 13, 13, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
11390_0_SolveDP_GT(EOS(STATIC_11390(i322, matching1)), i7336, i7345, i7345, matching2) → 11392_0_SolveDP_Load(EOS(STATIC_11392(i322, 12)), i7336, i7345) | &&(&&(<=(i7345, 12), =(matching1, 12)), =(matching2, 12))
11392_0_SolveDP_Load(EOS(STATIC_11392(i322, matching1)), i7336, i7345) → 11395_0_SolveDP_FieldAccess(EOS(STATIC_11395(i322, 12)), i7336, i7345, i7345) | =(matching1, 12)
11395_0_SolveDP_FieldAccess(EOS(STATIC_11395(i322, matching1)), i7336, i7345, i7345) → 11397_0_SolveDP_Load(EOS(STATIC_11397(i322, 12)), i7336, i7345, i7345, java.lang.Object(ARRAY(8))) | =(matching1, 12)
11397_0_SolveDP_Load(EOS(STATIC_11397(i322, matching1)), i7336, i7345, i7345, java.lang.Object(ARRAY(matching2))) → 11400_0_SolveDP_ArrayAccess(EOS(STATIC_11400(i322, 12)), i7336, i7345, i7345, java.lang.Object(ARRAY(8)), i7336) | &&(=(matching1, 12), =(matching2, 8))
11400_0_SolveDP_ArrayAccess(EOS(STATIC_11400(i322, matching1)), i7351, i7345, i7345, java.lang.Object(ARRAY(matching2)), i7351) → 11402_0_SolveDP_ArrayAccess(EOS(STATIC_11402(i322, 12)), i7351, i7345, i7345, java.lang.Object(ARRAY(8)), i7351) | &&(=(matching1, 12), =(matching2, 8))
11402_0_SolveDP_ArrayAccess(EOS(STATIC_11402(i322, matching1)), i7352, i7345, i7345, java.lang.Object(ARRAY(matching2)), i7352) → 11404_0_SolveDP_ArrayAccess(EOS(STATIC_11404(i322, 12)), i7352, i7345, i7345, java.lang.Object(ARRAY(8)), i7352) | &&(=(matching1, 12), =(matching2, 8))
11404_0_SolveDP_ArrayAccess(EOS(STATIC_11404(i322, matching1)), i7352, i7345, i7345, java.lang.Object(ARRAY(matching2)), i7352) → 11407_0_SolveDP_IntArithmetic(EOS(STATIC_11407(i322, 12)), i7352, i7345, i7345, i7354) | &&(&&(<(i7352, 8), =(matching1, 12)), =(matching2, 8))
11407_0_SolveDP_IntArithmetic(EOS(STATIC_11407(i322, matching1)), i7352, i7345, i7345, i7354) → 11410_0_SolveDP_GE(EOS(STATIC_11410(i322, 12)), i7352, i7345, -(i7345, i7354)) | &&(>=(i7345, 0), =(matching1, 12))
11410_0_SolveDP_GE(EOS(STATIC_11410(i322, matching1)), i7352, i7345, i7362) → 11413_0_SolveDP_GE(EOS(STATIC_11413(i322, 12)), i7352, i7345, i7362) | =(matching1, 12)
11410_0_SolveDP_GE(EOS(STATIC_11410(i322, matching1)), i7352, i7345, i7363) → 11414_0_SolveDP_GE(EOS(STATIC_11414(i322, 12)), i7352, i7345, i7363) | =(matching1, 12)
11413_0_SolveDP_GE(EOS(STATIC_11413(i322, matching1)), i7352, i7345, i7362) → 11417_0_SolveDP_FieldAccess(EOS(STATIC_11417(i322, 12)), i7352, i7345) | &&(<(i7362, 0), =(matching1, 12))
11417_0_SolveDP_FieldAccess(EOS(STATIC_11417(i322, matching1)), i7352, i7345) → 11422_0_SolveDP_Load(EOS(STATIC_11422(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i322))) | =(matching1, 12)
11422_0_SolveDP_Load(EOS(STATIC_11422(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i322))) → 11425_0_SolveDP_ArrayAccess(EOS(STATIC_11425(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11425_0_SolveDP_ArrayAccess(EOS(STATIC_11425(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) → 11429_0_SolveDP_ArrayAccess(EOS(STATIC_11429(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11429_0_SolveDP_ArrayAccess(EOS(STATIC_11429(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) → 11437_0_SolveDP_Load(EOS(STATIC_11437(i322, 12)), i7352, i7345, o17989) | &&(<(i7352, i322), =(matching1, 12))
11437_0_SolveDP_Load(EOS(STATIC_11437(i322, matching1)), i7352, i7345, o17989) → 11442_0_SolveDP_FieldAccess(EOS(STATIC_11442(i322, 12)), i7352, i7345, o17989, i7345) | =(matching1, 12)
11442_0_SolveDP_FieldAccess(EOS(STATIC_11442(i322, matching1)), i7352, i7345, o17989, i7345) → 11447_0_SolveDP_Load(EOS(STATIC_11447(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322))) | =(matching1, 12)
11447_0_SolveDP_Load(EOS(STATIC_11447(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322))) → 11456_0_SolveDP_ConstantStackPush(EOS(STATIC_11456(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11456_0_SolveDP_ConstantStackPush(EOS(STATIC_11456(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7352) → 11462_0_SolveDP_IntArithmetic(EOS(STATIC_11462(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7352, 1) | =(matching1, 12)
11462_0_SolveDP_IntArithmetic(EOS(STATIC_11462(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7352, matching2) → 11466_0_SolveDP_ArrayAccess(EOS(STATIC_11466(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), -(i7352, 1)) | &&(&&(>=(i7352, 0), =(matching1, 12)), =(matching2, 1))
11466_0_SolveDP_ArrayAccess(EOS(STATIC_11466(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7426) → 11476_0_SolveDP_ArrayAccess(EOS(STATIC_11476(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7426) | =(matching1, 12)
11476_0_SolveDP_ArrayAccess(EOS(STATIC_11476(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7426) → 11485_0_SolveDP_ArrayAccess(EOS(STATIC_11485(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7426) | =(matching1, 12)
11485_0_SolveDP_ArrayAccess(EOS(STATIC_11485(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i322)), i7426) → 11494_0_SolveDP_Load(EOS(STATIC_11494(i322, 12)), i7352, i7345, o17989, i7345, o18123) | &&(<(i7426, i322), =(matching1, 12))
11494_0_SolveDP_Load(EOS(STATIC_11494(i322, matching1)), i7352, i7345, o17989, i7345, o18123) → 11510_0_SolveDP_ArrayAccess(EOS(STATIC_11510(i322, 12)), i7352, i7345, o17989, i7345, o18123, i7345) | =(matching1, 12)
11510_0_SolveDP_ArrayAccess(EOS(STATIC_11510(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(o18237put), i7345) → 11523_0_SolveDP_ArrayAccess(EOS(STATIC_11523(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(o18237put), i7345) | =(matching1, 12)
11523_0_SolveDP_ArrayAccess(EOS(STATIC_11523(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i7510)), i7345) → 11536_0_SolveDP_ArrayAccess(EOS(STATIC_11536(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i7510)), i7345) | &&(>=(i7510, 0), =(matching1, 12))
11536_0_SolveDP_ArrayAccess(EOS(STATIC_11536(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i7510)), i7345) → 11553_0_SolveDP_ArrayAccess(EOS(STATIC_11553(i322, 12)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i7510)), i7345) | =(matching1, 12)
11553_0_SolveDP_ArrayAccess(EOS(STATIC_11553(i322, matching1)), i7352, i7345, o17989, i7345, java.lang.Object(ARRAY(i7510)), i7345) → 11569_0_SolveDP_ArrayAccess(EOS(STATIC_11569(i322, 12)), i7352, i7345, o17989, i7345) | &&(<(i7345, i7510), =(matching1, 12))
11569_0_SolveDP_ArrayAccess(EOS(STATIC_11569(i322, matching1)), i7352, i7345, java.lang.Object(o18484put), i7345) → 11583_0_SolveDP_ArrayAccess(EOS(STATIC_11583(i322, 12)), i7352, i7345, java.lang.Object(o18484put), i7345) | =(matching1, 12)
11583_0_SolveDP_ArrayAccess(EOS(STATIC_11583(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) → 11602_0_SolveDP_ArrayAccess(EOS(STATIC_11602(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) | &&(>=(i7612, 0), =(matching1, 12))
11602_0_SolveDP_ArrayAccess(EOS(STATIC_11602(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) → 11624_0_SolveDP_ArrayAccess(EOS(STATIC_11624(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) | =(matching1, 12)
11624_0_SolveDP_ArrayAccess(EOS(STATIC_11624(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) → 11644_0_SolveDP_JMP(EOS(STATIC_11644(i322, 12)), i7352, i7345) | &&(<(i7345, i7612), =(matching1, 12))
11644_0_SolveDP_JMP(EOS(STATIC_11644(i322, matching1)), i7352, i7345) → 11664_0_SolveDP_Inc(EOS(STATIC_11664(i322, 12)), i7352, i7345) | =(matching1, 12)
11664_0_SolveDP_Inc(EOS(STATIC_11664(i322, matching1)), i7352, i7345) → 12637_0_SolveDP_Inc(EOS(STATIC_12637(i322, 12)), i7352, i7345) | =(matching1, 12)
12637_0_SolveDP_Inc(EOS(STATIC_12637(i322, matching1)), i7352, i7345) → 12663_0_SolveDP_JMP(EOS(STATIC_12663(i322, 12)), i7352, +(i7345, 1)) | &&(>=(i7345, 0), =(matching1, 12))
12663_0_SolveDP_JMP(EOS(STATIC_12663(i322, matching1)), i7352, i9052) → 12684_0_SolveDP_Load(EOS(STATIC_12684(i322, 12)), i7352, i9052) | =(matching1, 12)
12684_0_SolveDP_Load(EOS(STATIC_12684(i322, matching1)), i7352, i9052) → 11383_0_SolveDP_Load(EOS(STATIC_11383(i322, 12)), i7352, i9052) | =(matching1, 12)
11414_0_SolveDP_GE(EOS(STATIC_11414(i322, matching1)), i7352, i7345, i7363) → 11418_0_SolveDP_FieldAccess(EOS(STATIC_11418(i322, 12)), i7352, i7345) | &&(>=(i7363, 0), =(matching1, 12))
11418_0_SolveDP_FieldAccess(EOS(STATIC_11418(i322, matching1)), i7352, i7345) → 11423_0_SolveDP_Load(EOS(STATIC_11423(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i322))) | =(matching1, 12)
11423_0_SolveDP_Load(EOS(STATIC_11423(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i322))) → 11426_0_SolveDP_ArrayAccess(EOS(STATIC_11426(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11426_0_SolveDP_ArrayAccess(EOS(STATIC_11426(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) → 11431_0_SolveDP_ArrayAccess(EOS(STATIC_11431(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11431_0_SolveDP_ArrayAccess(EOS(STATIC_11431(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i322)), i7352) → 11439_0_SolveDP_Load(EOS(STATIC_11439(i322, 12)), i7352, i7345, o17991) | &&(<(i7352, i322), =(matching1, 12))
11439_0_SolveDP_Load(EOS(STATIC_11439(i322, matching1)), i7352, i7345, o17991) → 11444_0_SolveDP_FieldAccess(EOS(STATIC_11444(i322, 12)), i7352, i7345, o17991, i7345) | =(matching1, 12)
11444_0_SolveDP_FieldAccess(EOS(STATIC_11444(i322, matching1)), i7352, i7345, o17991, i7345) → 11450_0_SolveDP_Load(EOS(STATIC_11450(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322))) | =(matching1, 12)
11450_0_SolveDP_Load(EOS(STATIC_11450(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322))) → 11458_0_SolveDP_ConstantStackPush(EOS(STATIC_11458(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11458_0_SolveDP_ConstantStackPush(EOS(STATIC_11458(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7352) → 11463_0_SolveDP_IntArithmetic(EOS(STATIC_11463(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7352, 1) | =(matching1, 12)
11463_0_SolveDP_IntArithmetic(EOS(STATIC_11463(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7352, matching2) → 11469_0_SolveDP_ArrayAccess(EOS(STATIC_11469(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), -(i7352, 1)) | &&(&&(>=(i7352, 0), =(matching1, 12)), =(matching2, 1))
11469_0_SolveDP_ArrayAccess(EOS(STATIC_11469(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7427) → 11480_0_SolveDP_ArrayAccess(EOS(STATIC_11480(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7427) | =(matching1, 12)
11480_0_SolveDP_ArrayAccess(EOS(STATIC_11480(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7427) → 11488_0_SolveDP_ArrayAccess(EOS(STATIC_11488(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7427) | =(matching1, 12)
11488_0_SolveDP_ArrayAccess(EOS(STATIC_11488(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i322)), i7427) → 11499_0_SolveDP_Load(EOS(STATIC_11499(i322, 12)), i7352, i7345, o17991, i7345, o18139) | &&(<(i7427, i322), =(matching1, 12))
11499_0_SolveDP_Load(EOS(STATIC_11499(i322, matching1)), i7352, i7345, o17991, i7345, o18139) → 11515_0_SolveDP_ArrayAccess(EOS(STATIC_11515(i322, 12)), i7352, i7345, o17991, i7345, o18139, i7345) | =(matching1, 12)
11515_0_SolveDP_ArrayAccess(EOS(STATIC_11515(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(o18259put), i7345) → 11528_0_SolveDP_ArrayAccess(EOS(STATIC_11528(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(o18259put), i7345) | =(matching1, 12)
11528_0_SolveDP_ArrayAccess(EOS(STATIC_11528(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i7517)), i7345) → 11542_0_SolveDP_ArrayAccess(EOS(STATIC_11542(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i7517)), i7345) | &&(>=(i7517, 0), =(matching1, 12))
11542_0_SolveDP_ArrayAccess(EOS(STATIC_11542(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i7517)), i7345) → 11559_0_SolveDP_ArrayAccess(EOS(STATIC_11559(i322, 12)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i7517)), i7345) | =(matching1, 12)
11559_0_SolveDP_ArrayAccess(EOS(STATIC_11559(i322, matching1)), i7352, i7345, o17991, i7345, java.lang.Object(ARRAY(i7517)), i7345) → 11575_0_SolveDP_FieldAccess(EOS(STATIC_11575(i322, 12)), i7352, i7345, o17991, i7345, i7561) | &&(<(i7345, i7517), =(matching1, 12))
11575_0_SolveDP_FieldAccess(EOS(STATIC_11575(i322, matching1)), i7352, i7345, o17991, i7345, i7561) → 11590_0_SolveDP_Load(EOS(STATIC_11590(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322))) | =(matching1, 12)
11590_0_SolveDP_Load(EOS(STATIC_11590(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322))) → 11612_0_SolveDP_ConstantStackPush(EOS(STATIC_11612(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7352) | =(matching1, 12)
11612_0_SolveDP_ConstantStackPush(EOS(STATIC_11612(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7352) → 11634_0_SolveDP_IntArithmetic(EOS(STATIC_11634(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7352, 1) | =(matching1, 12)
11634_0_SolveDP_IntArithmetic(EOS(STATIC_11634(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7352, matching2) → 11652_0_SolveDP_ArrayAccess(EOS(STATIC_11652(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), -(i7352, 1)) | &&(&&(>=(i7352, 0), =(matching1, 12)), =(matching2, 1))
11652_0_SolveDP_ArrayAccess(EOS(STATIC_11652(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7737) → 11675_0_SolveDP_ArrayAccess(EOS(STATIC_11675(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7737) | =(matching1, 12)
11675_0_SolveDP_ArrayAccess(EOS(STATIC_11675(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7737) → 11699_0_SolveDP_ArrayAccess(EOS(STATIC_11699(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7737) | =(matching1, 12)
11699_0_SolveDP_ArrayAccess(EOS(STATIC_11699(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i322)), i7737) → 11717_0_SolveDP_Load(EOS(STATIC_11717(i322, 12)), i7352, i7345, o17991, i7345, i7561, o19129) | &&(<(i7737, i322), =(matching1, 12))
11717_0_SolveDP_Load(EOS(STATIC_11717(i322, matching1)), i7352, i7345, o17991, i7345, i7561, o19129) → 11746_0_SolveDP_FieldAccess(EOS(STATIC_11746(i322, 12)), i7352, i7345, o17991, i7345, i7561, o19129, i7345) | =(matching1, 12)
11746_0_SolveDP_FieldAccess(EOS(STATIC_11746(i322, matching1)), i7352, i7345, o17991, i7345, i7561, o19129, i7345) → 11769_0_SolveDP_Load(EOS(STATIC_11769(i322, 12)), i7352, i7345, o17991, i7345, i7561, o19129, i7345, java.lang.Object(ARRAY(8))) | =(matching1, 12)
11769_0_SolveDP_Load(EOS(STATIC_11769(i322, matching1)), i7352, i7345, o17991, i7345, i7561, o19129, i7345, java.lang.Object(ARRAY(matching2))) → 11795_0_SolveDP_ArrayAccess(EOS(STATIC_11795(i322, 12)), i7352, i7345, o17991, i7345, i7561, o19129, i7345, java.lang.Object(ARRAY(8)), i7352) | &&(=(matching1, 12), =(matching2, 8))
11795_0_SolveDP_ArrayAccess(EOS(STATIC_11795(i322, matching1)), i7352, i7345, o17991, i7345, i7561, o19129, i7345, java.lang.Object(ARRAY(matching2)), i7352) → 11824_0_SolveDP_IntArithmetic(EOS(STATIC_11824(i322, 12)), i7352, i7345, o17991, i7345, i7561, o19129, i7345, i8004) | &&(&&(<(i7352, 8), =(matching1, 12)), =(matching2, 8))
11824_0_SolveDP_IntArithmetic(EOS(STATIC_11824(i322, matching1)), i7352, i7345, o17991, i7345, i7561, o19129, i7345, i8004) → 11859_0_SolveDP_ArrayAccess(EOS(STATIC_11859(i322, 12)), i7352, i7345, o17991, i7345, i7561, o19129, -(i7345, i8004)) | &&(>=(i7345, 0), =(matching1, 12))
11859_0_SolveDP_ArrayAccess(EOS(STATIC_11859(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(o20211put), i8061) → 11891_0_SolveDP_ArrayAccess(EOS(STATIC_11891(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(o20211put), i8061) | =(matching1, 12)
11891_0_SolveDP_ArrayAccess(EOS(STATIC_11891(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8061) → 11929_0_SolveDP_ArrayAccess(EOS(STATIC_11929(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8061) | &&(>=(i8160, 0), =(matching1, 12))
11929_0_SolveDP_ArrayAccess(EOS(STATIC_11929(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8223) → 11972_0_SolveDP_ArrayAccess(EOS(STATIC_11972(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8223) | =(matching1, 12)
11972_0_SolveDP_ArrayAccess(EOS(STATIC_11972(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8223) → 12013_0_SolveDP_ArrayAccess(EOS(STATIC_12013(i322, 12)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8223) | =(matching1, 12)
12013_0_SolveDP_ArrayAccess(EOS(STATIC_12013(i322, matching1)), i7352, i7345, o17991, i7345, i7561, java.lang.Object(ARRAY(i8160)), i8223) → 12052_0_SolveDP_FieldAccess(EOS(STATIC_12052(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8348) | &&(<(i8223, i8160), =(matching1, 12))
12052_0_SolveDP_FieldAccess(EOS(STATIC_12052(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8348) → 12097_0_SolveDP_Load(EOS(STATIC_12097(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8348, java.lang.Object(ARRAY(8))) | =(matching1, 12)
12097_0_SolveDP_Load(EOS(STATIC_12097(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8348, java.lang.Object(ARRAY(matching2))) → 12138_0_SolveDP_ArrayAccess(EOS(STATIC_12138(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8348, java.lang.Object(ARRAY(8)), i7352) | &&(=(matching1, 12), =(matching2, 8))
12138_0_SolveDP_ArrayAccess(EOS(STATIC_12138(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8348, java.lang.Object(ARRAY(matching2)), i7352) → 12177_0_SolveDP_IntArithmetic(EOS(STATIC_12177(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8348, i8524) | &&(&&(<(i7352, 8), =(matching1, 12)), =(matching2, 8))
12177_0_SolveDP_IntArithmetic(EOS(STATIC_12177(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8348, i8524) → 12222_0_SolveDP_InvokeMethod(EOS(STATIC_12222(i322, 12)), i7352, i7345, o17991, i7345, i7561, +(i8348, i8524)) | =(matching1, 12)
12222_0_SolveDP_InvokeMethod(EOS(STATIC_12222(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574) → 12276_0_max_Load(EOS(STATIC_12276(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574) | =(matching1, 12)
12276_0_max_Load(EOS(STATIC_12276(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574) → 12380_0_max_Load(EOS(STATIC_12380(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561) | =(matching1, 12)
12380_0_max_Load(EOS(STATIC_12380(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561) → 12418_0_max_LE(EOS(STATIC_12418(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) | =(matching1, 12)
12418_0_max_LE(EOS(STATIC_12418(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) → 12450_0_max_LE(EOS(STATIC_12450(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) | =(matching1, 12)
12418_0_max_LE(EOS(STATIC_12418(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) → 12451_0_max_LE(EOS(STATIC_12451(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) | =(matching1, 12)
12450_0_max_LE(EOS(STATIC_12450(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) → 12480_0_max_Load(EOS(STATIC_12480(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i8574) | &&(<=(i7561, i8574), =(matching1, 12))
12480_0_max_Load(EOS(STATIC_12480(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i8574) → 12503_0_max_Return(EOS(STATIC_12503(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i8574) | =(matching1, 12)
12503_0_max_Return(EOS(STATIC_12503(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i8574) → 12533_0_SolveDP_ArrayAccess(EOS(STATIC_12533(i322, 12)), i7352, i7345, o17991, i7345, i8574) | =(matching1, 12)
12533_0_SolveDP_ArrayAccess(EOS(STATIC_12533(i322, matching1)), i7352, i7345, java.lang.Object(o23791put), i7345, i8574) → 12563_0_SolveDP_ArrayAccess(EOS(STATIC_12563(i322, 12)), i7352, i7345, java.lang.Object(o23791put), i7345, i8574) | =(matching1, 12)
12563_0_SolveDP_ArrayAccess(EOS(STATIC_12563(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i8968)), i7345, i8574) → 12588_0_SolveDP_ArrayAccess(EOS(STATIC_12588(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i8968)), i7345, i8574) | &&(>=(i8968, 0), =(matching1, 12))
12588_0_SolveDP_ArrayAccess(EOS(STATIC_12588(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i8968)), i7345, i8574) → 12612_0_SolveDP_ArrayAccess(EOS(STATIC_12612(i322, 12)), i7352, i7345, java.lang.Object(ARRAY(i8968)), i7345, i8574) | =(matching1, 12)
12612_0_SolveDP_ArrayAccess(EOS(STATIC_12612(i322, matching1)), i7352, i7345, java.lang.Object(ARRAY(i8968)), i7345, i8574) → 12637_0_SolveDP_Inc(EOS(STATIC_12637(i322, 12)), i7352, i7345) | &&(<(i7345, i8968), =(matching1, 12))
12451_0_max_LE(EOS(STATIC_12451(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561, i8574, i7561, i8574) → 12481_0_max_Load(EOS(STATIC_12481(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561) | &&(>(i7561, i8574), =(matching1, 12))
12481_0_max_Load(EOS(STATIC_12481(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561) → 12504_0_max_JMP(EOS(STATIC_12504(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561) | =(matching1, 12)
12504_0_max_JMP(EOS(STATIC_12504(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561) → 12534_0_max_Return(EOS(STATIC_12534(i322, 12)), i7352, i7345, o17991, i7345, i7561, i8574, i7561) | =(matching1, 12)
12534_0_max_Return(EOS(STATIC_12534(i322, matching1)), i7352, i7345, o17991, i7345, i7561, i8574, i7561) → 12566_0_SolveDP_ArrayAccess(EOS(STATIC_12566(i322, 12)), i7352, i7345, o17991, i7345, i7561) | =(matching1, 12)
12566_0_SolveDP_ArrayAccess(EOS(STATIC_12566(i322, matching1)), i7352, i7345, o17991, i7345, i7561) → 12533_0_SolveDP_ArrayAccess(EOS(STATIC_12533(i322, 12)), i7352, i7345, o17991, i7345, i7561) | =(matching1, 12)
11391_0_SolveDP_GT(EOS(STATIC_11391(i322, matching1)), i7336, matching2, matching3, matching4) → 11394_0_SolveDP_Inc(EOS(STATIC_11394(i322, 12)), i7336) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
11394_0_SolveDP_Inc(EOS(STATIC_11394(i322, matching1)), i7336) → 11396_0_SolveDP_JMP(EOS(STATIC_11396(i322, 12)), +(i7336, 1)) | =(matching1, 12)
11396_0_SolveDP_JMP(EOS(STATIC_11396(i322, matching1)), i7346) → 11398_0_SolveDP_Load(EOS(STATIC_11398(i322, 12)), i7346) | =(matching1, 12)
11398_0_SolveDP_Load(EOS(STATIC_11398(i322, matching1)), i7346) → 9949_0_SolveDP_Load(EOS(STATIC_9949(i322, 12)), i7346) | =(matching1, 12)
9949_0_SolveDP_Load(EOS(STATIC_9949(i322, matching1)), i5568) → 9950_0_SolveDP_FieldAccess(EOS(STATIC_9950(i322, 12)), i5568, i5568) | =(matching1, 12)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
11389_0_SolveDP_GT(EOS(STATIC_11389(x0, 12)), x2, x3, x3, 12) → 11389_0_SolveDP_GT(EOS(STATIC_11389(x0, 12)), x2, +(x3, 1), +(x3, 1), 12) | &&(&&(&&(&&(>(+(x3, 1), 0), <=(x3, 12)), >(+(x2, 1), 0)), <(x2, 8)), >(x0, -(x2, 1)))
11389_0_SolveDP_GT(EOS(STATIC_11389(x0, 12)), x2, 13, 13, 12) → 11389_0_SolveDP_GT(EOS(STATIC_11389(x0, 12)), +(x2, 1), 0, 0, 12) | >(x0, +(x2, 1))
R rules:
Filtered ground terms:
11389_0_SolveDP_GT(x1, x2, x3, x4, x5) → 11389_0_SolveDP_GT(x1, x2, x3, x4)
STATIC_11389(x1, x2) → STATIC_11389(x1)
Cond_11389_0_SolveDP_GT1(x1, x2, x3, x4, x5, x6) → Cond_11389_0_SolveDP_GT1(x1, x2, x3)
Cond_11389_0_SolveDP_GT(x1, x2, x3, x4, x5, x6) → Cond_11389_0_SolveDP_GT(x1, x2, x3, x4, x5)
Filtered duplicate args:
11389_0_SolveDP_GT(x1, x2, x3, x4) → 11389_0_SolveDP_GT(x1, x2, x4)
Cond_11389_0_SolveDP_GT(x1, x2, x3, x4, x5) → Cond_11389_0_SolveDP_GT(x1, x2, x3, x5)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
11389_0_SolveDP_GT(EOS(STATIC_11389(x0)), x2, x3) → 11389_0_SolveDP_GT(EOS(STATIC_11389(x0)), x2, +(x3, 1)) | &&(&&(&&(&&(>(x3, -1), <=(x3, 12)), >(x2, -1)), <(x2, 8)), >(x0, -(x2, 1)))
11389_0_SolveDP_GT(EOS(STATIC_11389(x0)), x2, 13) → 11389_0_SolveDP_GT(EOS(STATIC_11389(x0)), +(x2, 1), 0) | >(x0, +(x2, 1))
R rules:
Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.
P rules:
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0)), x2, x3) → COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3, -1), <=(x3, 12)), >(x2, -1)), <(x2, 8)), >(x0, -(x2, 1))), EOS(STATIC_11389(x0)), x2, x3)
COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0)), x2, x3) → 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0)), x2, +(x3, 1))
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0)), x2, 13) → COND_11389_0_SOLVEDP_GT1(>(x0, +(x2, 1)), EOS(STATIC_11389(x0)), x2, 13)
COND_11389_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11389(x0)), x2, 13) → 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0)), +(x2, 1), 0)
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 (x3[0] > -1 && x3[0] <= 12 && x2[0] > -1 && x2[0] < 8 && x0[0] > x2[0] - 1 ∧EOS(STATIC_11389(x0[0])) →* EOS(STATIC_11389(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (0), if (EOS(STATIC_11389(x0[1])) →* EOS(STATIC_11389(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(1) -> (2), if (EOS(STATIC_11389(x0[1])) →* EOS(STATIC_11389(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 13)
(2) -> (3), if (x0[2] > x2[2] + 1 ∧EOS(STATIC_11389(x0[2])) →* EOS(STATIC_11389(x0[3]))∧x2[2] →* x2[3])
(3) -> (0), if (EOS(STATIC_11389(x0[3])) →* EOS(STATIC_11389(x0[0]))∧x2[3] + 1 →* x2[0]∧0 →* x3[0])
(3) -> (2), if (EOS(STATIC_11389(x0[3])) →* EOS(STATIC_11389(x0[2]))∧x2[3] + 1 →* x2[2]∧0 →* 13)
(1) (&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1)))=TRUE∧EOS(STATIC_11389(x0[0]))=EOS(STATIC_11389(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥NonInfC∧11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥))
(2) (>(x0[0], -(x2[0], 1))=TRUE∧<(x2[0], 8)=TRUE∧>(x2[0], -1)=TRUE∧>(x3[0], -1)=TRUE∧<=(x3[0], 12)=TRUE ⇒ 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥NonInfC∧11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥))
(3) (x0[0] + [-1]x2[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[0] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(4) (x0[0] + [-1]x2[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[0] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(5) (x0[0] + [-1]x2[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[0] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(6) (x0[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(7) (COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0[1])), x2[1], x3[1])≥NonInfC∧COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0[1])), x2[1], x3[1])≥11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥))
(8) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧[(-1)bso_16] ≥ 0)
(9) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧[(-1)bso_16] ≥ 0)
(10) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧[(-1)bso_16] ≥ 0)
(11) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)
(12) (>(x0[2], +(x2[2], 1))=TRUE∧EOS(STATIC_11389(x0[2]))=EOS(STATIC_11389(x0[3]))∧x2[2]=x2[3] ⇒ 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[2])), x2[2], 13)≥NonInfC∧11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[2])), x2[2], 13)≥COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)∧(UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥))
(13) (>(x0[2], +(x2[2], 1))=TRUE ⇒ 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[2])), x2[2], 13)≥NonInfC∧11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[2])), x2[2], 13)≥COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)∧(UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥))
(14) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] + [bni_17]x0[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(15) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] + [bni_17]x0[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(16) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] + [bni_17]x0[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(17) (x0[2] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥)∧[bni_17 + (-1)Bound*bni_17] + [bni_17]x0[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(18) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥)∧[bni_17 + (-1)Bound*bni_17] + [bni_17]x0[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(19) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)), ≥)∧[bni_17 + (-1)Bound*bni_17] + [bni_17]x0[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(20) (COND_11389_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11389(x0[3])), x2[3], 13)≥NonInfC∧COND_11389_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11389(x0[3])), x2[3], 13)≥11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)∧(UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)), ≥))
(21) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(22) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(23) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(24) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(11389_0_SOLVEDP_GT(x1, x2, x3)) = [-1] + [-1]x2 + x1
POL(EOS(x1)) = x1
POL(STATIC_11389(x1)) = x1
POL(COND_11389_0_SOLVEDP_GT(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<=(x1, x2)) = [-1]
POL(12) = [12]
POL(<(x1, x2)) = [-1]
POL(8) = [8]
POL(-(x1, x2)) = x1 + [-1]x2
POL(1) = [1]
POL(+(x1, x2)) = x1 + x2
POL(13) = [13]
POL(COND_11389_0_SOLVEDP_GT1(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2
POL(0) = 0
COND_11389_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11389(x0[3])), x2[3], 13) → 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[3])), +(x2[3], 1), 0)
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0]) → COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[2])), x2[2], 13) → COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0]) → COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])
COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0[1])), x2[1], x3[1]) → 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[2])), x2[2], 13) → COND_11389_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11389(x0[2])), x2[2], 13)
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(1) -> (0), if (EOS(STATIC_11389(x0[1])) →* EOS(STATIC_11389(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(0) -> (1), if (x3[0] > -1 && x3[0] <= 12 && x2[0] > -1 && x2[0] < 8 && x0[0] > x2[0] - 1 ∧EOS(STATIC_11389(x0[0])) →* EOS(STATIC_11389(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (2), if (EOS(STATIC_11389(x0[1])) →* EOS(STATIC_11389(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 13)
!= | ~ | 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
(1) -> (0), if (EOS(STATIC_11389(x0[1])) →* EOS(STATIC_11389(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(0) -> (1), if (x3[0] > -1 && x3[0] <= 12 && x2[0] > -1 && x2[0] < 8 && x0[0] > x2[0] - 1 ∧EOS(STATIC_11389(x0[0])) →* EOS(STATIC_11389(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) (COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0[1])), x2[1], x3[1])≥NonInfC∧COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0[1])), x2[1], x3[1])≥11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥))
(2) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧[1 + (-1)bso_12] ≥ 0)
(3) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧[1 + (-1)bso_12] ≥ 0)
(4) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧[1 + (-1)bso_12] ≥ 0)
(5) ((UIncreasing(11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_12] ≥ 0)
(6) (&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1)))=TRUE∧EOS(STATIC_11389(x0[0]))=EOS(STATIC_11389(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥NonInfC∧11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥))
(7) (>(x0[0], -(x2[0], 1))=TRUE∧<(x2[0], 8)=TRUE∧>(x2[0], -1)=TRUE∧>(x3[0], -1)=TRUE∧<=(x3[0], 12)=TRUE ⇒ 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥NonInfC∧11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0])≥COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥))
(8) (x0[0] + [-1]x2[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x3[0] + [(-1)bni_13]x2[0] + [(2)bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(9) (x0[0] + [-1]x2[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x3[0] + [(-1)bni_13]x2[0] + [(2)bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(10) (x0[0] + [-1]x2[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x3[0] + [(-1)bni_13]x2[0] + [(2)bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(11) (x0[0] ≥ 0∧[7] + [-1]x2[0] ≥ 0∧x2[0] ≥ 0∧x3[0] ≥ 0∧[12] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x3[0] + [bni_13]x2[0] + [(2)bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_11389_0_SOLVEDP_GT(x1, x2, x3, x4)) = [-1] + [-1]x3 + [2]x2 + [-1]x4
POL(EOS(x1)) = x1
POL(STATIC_11389(x1)) = x1
POL(11389_0_SOLVEDP_GT(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [2]x1
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<=(x1, x2)) = [-1]
POL(12) = [12]
POL(<(x1, x2)) = [-1]
POL(8) = [8]
POL(-(x1, x2)) = x1 + [-1]x2
COND_11389_0_SOLVEDP_GT(TRUE, EOS(STATIC_11389(x0[1])), x2[1], x3[1]) → 11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[1])), x2[1], +(x3[1], 1))
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0]) → COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])
11389_0_SOLVEDP_GT(EOS(STATIC_11389(x0[0])), x2[0], x3[0]) → COND_11389_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11389(x0[0])), x2[0], x3[0])
!= | ~ | 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
!= | ~ | 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
!= | ~ | 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
Generated 41 rules for P and 0 rules for R.
P rules:
737_0_SolveDP_FieldAccess(EOS(STATIC_737(matching1)), i72, i72) → 739_0_SolveDP_GT(EOS(STATIC_739(12)), i72, i72, 12) | =(matching1, 12)
739_0_SolveDP_GT(EOS(STATIC_739(matching1)), i77, i77, matching2) → 741_0_SolveDP_GT(EOS(STATIC_741(12)), i77, i77, 12) | &&(=(matching1, 12), =(matching2, 12))
741_0_SolveDP_GT(EOS(STATIC_741(matching1)), i77, i77, matching2) → 743_0_SolveDP_Load(EOS(STATIC_743(12)), i77) | &&(&&(<=(i77, 12), =(matching1, 12)), =(matching2, 12))
743_0_SolveDP_Load(EOS(STATIC_743(matching1)), i77) → 745_0_SolveDP_FieldAccess(EOS(STATIC_745(12)), i77, i77) | =(matching1, 12)
745_0_SolveDP_FieldAccess(EOS(STATIC_745(matching1)), i77, i77) → 748_0_SolveDP_ConstantStackPush(EOS(STATIC_748(12)), i77, i77, java.lang.Object(ARRAY(8))) | =(matching1, 12)
748_0_SolveDP_ConstantStackPush(EOS(STATIC_748(matching1)), i77, i77, java.lang.Object(ARRAY(matching2))) → 752_0_SolveDP_ArrayAccess(EOS(STATIC_752(12)), i77, i77, java.lang.Object(ARRAY(8)), 0) | &&(=(matching1, 12), =(matching2, 8))
752_0_SolveDP_ArrayAccess(EOS(STATIC_752(matching1)), i77, i77, java.lang.Object(ARRAY(matching2)), matching3) → 757_0_SolveDP_GE(EOS(STATIC_757(12)), i77, i77, 2) | &&(&&(&&(<(0, 8), =(matching1, 12)), =(matching2, 8)), =(matching3, 0))
757_0_SolveDP_GE(EOS(STATIC_757(matching1)), i84, i84, matching2) → 761_0_SolveDP_GE(EOS(STATIC_761(12)), i84, i84, 2) | &&(=(matching1, 12), =(matching2, 2))
757_0_SolveDP_GE(EOS(STATIC_757(matching1)), i85, i85, matching2) → 762_0_SolveDP_GE(EOS(STATIC_762(12)), i85, i85, 2) | &&(=(matching1, 12), =(matching2, 2))
761_0_SolveDP_GE(EOS(STATIC_761(matching1)), i84, i84, matching2) → 768_0_SolveDP_FieldAccess(EOS(STATIC_768(12)), i84) | &&(&&(<(i84, 2), =(matching1, 12)), =(matching2, 2))
768_0_SolveDP_FieldAccess(EOS(STATIC_768(matching1)), i84) → 775_0_SolveDP_ConstantStackPush(EOS(STATIC_775(12)), i84, java.lang.Object(ARRAY(i71))) | =(matching1, 12)
775_0_SolveDP_ConstantStackPush(EOS(STATIC_775(matching1)), i84, java.lang.Object(ARRAY(i71))) → 783_0_SolveDP_ArrayAccess(EOS(STATIC_783(12)), i84, java.lang.Object(ARRAY(i71)), 0) | =(matching1, 12)
783_0_SolveDP_ArrayAccess(EOS(STATIC_783(matching1)), i84, java.lang.Object(ARRAY(i96)), matching2) → 798_0_SolveDP_ArrayAccess(EOS(STATIC_798(12)), i84, java.lang.Object(ARRAY(i96)), 0) | &&(=(matching1, 12), =(matching2, 0))
798_0_SolveDP_ArrayAccess(EOS(STATIC_798(matching1)), i84, java.lang.Object(ARRAY(i96)), matching2) → 808_0_SolveDP_Load(EOS(STATIC_808(12)), i84, o110) | &&(&&(<(0, i96), =(matching1, 12)), =(matching2, 0))
808_0_SolveDP_Load(EOS(STATIC_808(matching1)), i84, o110) → 819_0_SolveDP_ConstantStackPush(EOS(STATIC_819(12)), i84, o110, i84) | =(matching1, 12)
819_0_SolveDP_ConstantStackPush(EOS(STATIC_819(matching1)), i84, o110, i84) → 832_0_SolveDP_ArrayAccess(EOS(STATIC_832(12)), i84, o110, i84, 0) | =(matching1, 12)
832_0_SolveDP_ArrayAccess(EOS(STATIC_832(matching1)), i84, java.lang.Object(o116put), i84, matching2) → 845_0_SolveDP_ArrayAccess(EOS(STATIC_845(12)), i84, java.lang.Object(o116put), i84, 0) | &&(=(matching1, 12), =(matching2, 0))
845_0_SolveDP_ArrayAccess(EOS(STATIC_845(matching1)), i84, java.lang.Object(ARRAY(i100)), i84, matching2) → 855_0_SolveDP_ArrayAccess(EOS(STATIC_855(12)), i84, java.lang.Object(ARRAY(i100)), i84, 0) | &&(&&(>=(i100, 0), =(matching1, 12)), =(matching2, 0))
855_0_SolveDP_ArrayAccess(EOS(STATIC_855(matching1)), i84, java.lang.Object(ARRAY(i100)), i84, matching2) → 866_0_SolveDP_ArrayAccess(EOS(STATIC_866(12)), i84, java.lang.Object(ARRAY(i100)), i84, 0) | &&(=(matching1, 12), =(matching2, 0))
866_0_SolveDP_ArrayAccess(EOS(STATIC_866(matching1)), i84, java.lang.Object(ARRAY(i100)), i84, matching2) → 880_0_SolveDP_JMP(EOS(STATIC_880(12)), i84) | &&(&&(<(i84, i100), =(matching1, 12)), =(matching2, 0))
880_0_SolveDP_JMP(EOS(STATIC_880(matching1)), i84) → 893_0_SolveDP_Inc(EOS(STATIC_893(12)), i84) | =(matching1, 12)
893_0_SolveDP_Inc(EOS(STATIC_893(matching1)), i84) → 908_0_SolveDP_JMP(EOS(STATIC_908(12)), +(i84, 1)) | &&(>=(i84, 0), =(matching1, 12))
908_0_SolveDP_JMP(EOS(STATIC_908(matching1)), i106) → 935_0_SolveDP_Load(EOS(STATIC_935(12)), i106) | =(matching1, 12)
935_0_SolveDP_Load(EOS(STATIC_935(matching1)), i106) → 733_0_SolveDP_Load(EOS(STATIC_733(12)), i106) | =(matching1, 12)
733_0_SolveDP_Load(EOS(STATIC_733(matching1)), i72) → 737_0_SolveDP_FieldAccess(EOS(STATIC_737(12)), i72, i72) | =(matching1, 12)
762_0_SolveDP_GE(EOS(STATIC_762(matching1)), i85, i85, matching2) → 770_0_SolveDP_FieldAccess(EOS(STATIC_770(12)), i85) | &&(&&(>=(i85, 2), =(matching1, 12)), =(matching2, 2))
770_0_SolveDP_FieldAccess(EOS(STATIC_770(matching1)), i85) → 777_0_SolveDP_ConstantStackPush(EOS(STATIC_777(12)), i85, java.lang.Object(ARRAY(i71))) | =(matching1, 12)
777_0_SolveDP_ConstantStackPush(EOS(STATIC_777(matching1)), i85, java.lang.Object(ARRAY(i71))) → 785_0_SolveDP_ArrayAccess(EOS(STATIC_785(12)), i85, java.lang.Object(ARRAY(i71)), 0) | =(matching1, 12)
785_0_SolveDP_ArrayAccess(EOS(STATIC_785(matching1)), i85, java.lang.Object(ARRAY(i98)), matching2) → 801_0_SolveDP_ArrayAccess(EOS(STATIC_801(12)), i85, java.lang.Object(ARRAY(i98)), 0) | &&(=(matching1, 12), =(matching2, 0))
801_0_SolveDP_ArrayAccess(EOS(STATIC_801(matching1)), i85, java.lang.Object(ARRAY(i98)), matching2) → 812_0_SolveDP_Load(EOS(STATIC_812(12)), i85, o112) | &&(&&(<(0, i98), =(matching1, 12)), =(matching2, 0))
812_0_SolveDP_Load(EOS(STATIC_812(matching1)), i85, o112) → 821_0_SolveDP_FieldAccess(EOS(STATIC_821(12)), i85, o112, i85) | =(matching1, 12)
821_0_SolveDP_FieldAccess(EOS(STATIC_821(matching1)), i85, o112, i85) → 839_0_SolveDP_ConstantStackPush(EOS(STATIC_839(12)), i85, o112, i85, java.lang.Object(ARRAY(8))) | =(matching1, 12)
839_0_SolveDP_ConstantStackPush(EOS(STATIC_839(matching1)), i85, o112, i85, java.lang.Object(ARRAY(matching2))) → 850_0_SolveDP_ArrayAccess(EOS(STATIC_850(12)), i85, o112, i85, java.lang.Object(ARRAY(8)), 0) | &&(=(matching1, 12), =(matching2, 8))
850_0_SolveDP_ArrayAccess(EOS(STATIC_850(matching1)), i85, o112, i85, java.lang.Object(ARRAY(matching2)), matching3) → 858_0_SolveDP_ArrayAccess(EOS(STATIC_858(12)), i85, o112, i85) | &&(&&(&&(<(0, 8), =(matching1, 12)), =(matching2, 8)), =(matching3, 0))
858_0_SolveDP_ArrayAccess(EOS(STATIC_858(matching1)), i85, java.lang.Object(o122put), i85) → 875_0_SolveDP_ArrayAccess(EOS(STATIC_875(12)), i85, java.lang.Object(o122put), i85) | =(matching1, 12)
875_0_SolveDP_ArrayAccess(EOS(STATIC_875(matching1)), i85, java.lang.Object(ARRAY(i102)), i85) → 885_0_SolveDP_ArrayAccess(EOS(STATIC_885(12)), i85, java.lang.Object(ARRAY(i102)), i85) | &&(>=(i102, 0), =(matching1, 12))
885_0_SolveDP_ArrayAccess(EOS(STATIC_885(matching1)), i85, java.lang.Object(ARRAY(i102)), i85) → 897_0_SolveDP_ArrayAccess(EOS(STATIC_897(12)), i85, java.lang.Object(ARRAY(i102)), i85) | =(matching1, 12)
897_0_SolveDP_ArrayAccess(EOS(STATIC_897(matching1)), i85, java.lang.Object(ARRAY(i102)), i85) → 919_0_SolveDP_Inc(EOS(STATIC_919(12)), i85) | &&(<(i85, i102), =(matching1, 12))
919_0_SolveDP_Inc(EOS(STATIC_919(matching1)), i85) → 941_0_SolveDP_JMP(EOS(STATIC_941(12)), +(i85, 1)) | &&(>(i85, 0), =(matching1, 12))
941_0_SolveDP_JMP(EOS(STATIC_941(matching1)), i111) → 959_0_SolveDP_Load(EOS(STATIC_959(12)), i111) | =(matching1, 12)
959_0_SolveDP_Load(EOS(STATIC_959(matching1)), i111) → 733_0_SolveDP_Load(EOS(STATIC_733(12)), i111) | =(matching1, 12)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
737_0_SolveDP_FieldAccess(EOS(STATIC_737(12)), x1, x1) → 737_0_SolveDP_FieldAccess(EOS(STATIC_737(12)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), <=(x1, 12)), <(x1, 2))
737_0_SolveDP_FieldAccess(EOS(STATIC_737(12)), x1, x1) → 737_0_SolveDP_FieldAccess(EOS(STATIC_737(12)), +(x1, 1), +(x1, 1)) | &&(>(+(x1, 1), 2), <=(x1, 12))
R rules:
Filtered ground terms:
737_0_SolveDP_FieldAccess(x1, x2, x3) → 737_0_SolveDP_FieldAccess(x2, x3)
STATIC_737(x1) → STATIC_737
EOS(x1) → EOS
Cond_737_0_SolveDP_FieldAccess1(x1, x2, x3, x4) → Cond_737_0_SolveDP_FieldAccess1(x1, x3, x4)
Cond_737_0_SolveDP_FieldAccess(x1, x2, x3, x4) → Cond_737_0_SolveDP_FieldAccess(x1, x3, x4)
Filtered duplicate args:
737_0_SolveDP_FieldAccess(x1, x2) → 737_0_SolveDP_FieldAccess(x2)
Cond_737_0_SolveDP_FieldAccess(x1, x2, x3) → Cond_737_0_SolveDP_FieldAccess(x1, x3)
Cond_737_0_SolveDP_FieldAccess1(x1, x2, x3) → Cond_737_0_SolveDP_FieldAccess1(x1, x3)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
737_0_SolveDP_FieldAccess(x1) → 737_0_SolveDP_FieldAccess(+(x1, 1)) | &&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2))
737_0_SolveDP_FieldAccess(x1) → 737_0_SolveDP_FieldAccess(+(x1, 1)) | &&(>(x1, 1), <=(x1, 12))
R rules:
Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.
P rules:
737_0_SOLVEDP_FIELDACCESS(x1) → COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2)), x1)
COND_737_0_SOLVEDP_FIELDACCESS(TRUE, x1) → 737_0_SOLVEDP_FIELDACCESS(+(x1, 1))
737_0_SOLVEDP_FIELDACCESS(x1) → COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1, 1), <=(x1, 12)), x1)
COND_737_0_SOLVEDP_FIELDACCESS1(TRUE, x1) → 737_0_SOLVEDP_FIELDACCESS(+(x1, 1))
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 (x1[0] > -1 && x1[0] <= 12 && x1[0] < 2 ∧x1[0] →* x1[1])
(1) -> (0), if (x1[1] + 1 →* x1[0])
(1) -> (2), if (x1[1] + 1 →* x1[2])
(2) -> (3), if (x1[2] > 1 && x1[2] <= 12 ∧x1[2] →* x1[3])
(3) -> (0), if (x1[3] + 1 →* x1[0])
(3) -> (2), if (x1[3] + 1 →* x1[2])
(1) (&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2))=TRUE∧x1[0]=x1[1] ⇒ 737_0_SOLVEDP_FIELDACCESS(x1[0])≥NonInfC∧737_0_SOLVEDP_FIELDACCESS(x1[0])≥COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])∧(UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])), ≥))
(2) (<(x1[0], 2)=TRUE∧>(x1[0], -1)=TRUE∧<=(x1[0], 12)=TRUE ⇒ 737_0_SOLVEDP_FIELDACCESS(x1[0])≥NonInfC∧737_0_SOLVEDP_FIELDACCESS(x1[0])≥COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])∧(UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])), ≥))
(3) ([1] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0∧[12] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x1[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(4) ([1] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0∧[12] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x1[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(5) ([1] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0∧[12] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x1[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(6) (COND_737_0_SOLVEDP_FIELDACCESS(TRUE, x1[1])≥NonInfC∧COND_737_0_SOLVEDP_FIELDACCESS(TRUE, x1[1])≥737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))∧(UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥))
(7) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧[1 + (-1)bso_16] ≥ 0)
(8) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧[1 + (-1)bso_16] ≥ 0)
(9) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧[1 + (-1)bso_16] ≥ 0)
(10) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)
(11) (&&(>(x1[2], 1), <=(x1[2], 12))=TRUE∧x1[2]=x1[3] ⇒ 737_0_SOLVEDP_FIELDACCESS(x1[2])≥NonInfC∧737_0_SOLVEDP_FIELDACCESS(x1[2])≥COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])∧(UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥))
(12) (>(x1[2], 1)=TRUE∧<=(x1[2], 12)=TRUE ⇒ 737_0_SOLVEDP_FIELDACCESS(x1[2])≥NonInfC∧737_0_SOLVEDP_FIELDACCESS(x1[2])≥COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])∧(UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥))
(13) (x1[2] + [-2] ≥ 0∧[12] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x1[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(14) (x1[2] + [-2] ≥ 0∧[12] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x1[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(15) (x1[2] + [-2] ≥ 0∧[12] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x1[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(16) (x1[2] ≥ 0∧[10] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥)∧[(-3)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x1[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(17) (COND_737_0_SOLVEDP_FIELDACCESS1(TRUE, x1[3])≥NonInfC∧COND_737_0_SOLVEDP_FIELDACCESS1(TRUE, x1[3])≥737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))∧(UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥))
(18) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(19) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(20) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(21) ((UIncreasing(737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(737_0_SOLVEDP_FIELDACCESS(x1)) = [-1] + [-1]x1
POL(COND_737_0_SOLVEDP_FIELDACCESS(x1, x2)) = [-1] + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<=(x1, x2)) = [-1]
POL(12) = [12]
POL(<(x1, x2)) = [-1]
POL(2) = [2]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(COND_737_0_SOLVEDP_FIELDACCESS1(x1, x2)) = [-1] + [-1]x2
COND_737_0_SOLVEDP_FIELDACCESS(TRUE, x1[1]) → 737_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))
COND_737_0_SOLVEDP_FIELDACCESS1(TRUE, x1[3]) → 737_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))
737_0_SOLVEDP_FIELDACCESS(x1[0]) → COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])
737_0_SOLVEDP_FIELDACCESS(x1[2]) → COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])
737_0_SOLVEDP_FIELDACCESS(x1[0]) → COND_737_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])
737_0_SOLVEDP_FIELDACCESS(x1[2]) → COND_737_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])
!= | ~ | 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
!= | ~ | 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
Generated 48 rules for P and 0 rules for R.
P rules:
6518_0_InterpretArray_ConstantStackPush(EOS(STATIC_6518), i2277, i2279, i2277) → 6537_0_InterpretArray_LT(EOS(STATIC_6537), i2277, i2279, i2277, 1)
6537_0_InterpretArray_LT(EOS(STATIC_6537), i2357, i2279, i2357, matching1) → 6558_0_InterpretArray_LT(EOS(STATIC_6558), i2357, i2279, i2357, 1) | =(matching1, 1)
6558_0_InterpretArray_LT(EOS(STATIC_6558), i2357, i2279, i2357, matching1) → 6580_0_InterpretArray_FieldAccess(EOS(STATIC_6580), i2357, i2279) | &&(>=(i2357, 1), =(matching1, 1))
6580_0_InterpretArray_FieldAccess(EOS(STATIC_6580), i2357, i2279) → 6606_0_InterpretArray_Load(EOS(STATIC_6606), i2357, i2279, java.lang.Object(ARRAY(i583)))
6606_0_InterpretArray_Load(EOS(STATIC_6606), i2357, i2279, java.lang.Object(ARRAY(i583))) → 6614_0_InterpretArray_ArrayAccess(EOS(STATIC_6614), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357)
6614_0_InterpretArray_ArrayAccess(EOS(STATIC_6614), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357) → 6619_0_InterpretArray_ArrayAccess(EOS(STATIC_6619), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357)
6619_0_InterpretArray_ArrayAccess(EOS(STATIC_6619), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357) → 6624_0_InterpretArray_Load(EOS(STATIC_6624), i2357, i2279, o5335) | <(i2357, i583)
6624_0_InterpretArray_Load(EOS(STATIC_6624), i2357, i2279, o5335) → 6630_0_InterpretArray_ArrayAccess(EOS(STATIC_6630), i2357, i2279, o5335, i2279)
6630_0_InterpretArray_ArrayAccess(EOS(STATIC_6630), i2357, i2279, java.lang.Object(o5340put), i2279) → 6636_0_InterpretArray_ArrayAccess(EOS(STATIC_6636), i2357, i2279, java.lang.Object(o5340put), i2279)
6636_0_InterpretArray_ArrayAccess(EOS(STATIC_6636), i2357, i2279, java.lang.Object(ARRAY(i2415)), i2279) → 6644_0_InterpretArray_ArrayAccess(EOS(STATIC_6644), i2357, i2279, java.lang.Object(ARRAY(i2415)), i2279) | >=(i2415, 0)
6644_0_InterpretArray_ArrayAccess(EOS(STATIC_6644), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419) → 6653_0_InterpretArray_ArrayAccess(EOS(STATIC_6653), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419)
6653_0_InterpretArray_ArrayAccess(EOS(STATIC_6653), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419) → 6663_0_InterpretArray_ArrayAccess(EOS(STATIC_6663), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419)
6663_0_InterpretArray_ArrayAccess(EOS(STATIC_6663), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419) → 6673_0_InterpretArray_FieldAccess(EOS(STATIC_6673), i2357, i2419, i2427) | <(i2419, i2415)
6673_0_InterpretArray_FieldAccess(EOS(STATIC_6673), i2357, i2419, i2427) → 6687_0_InterpretArray_Load(EOS(STATIC_6687), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)))
6687_0_InterpretArray_Load(EOS(STATIC_6687), i2357, i2419, i2427, java.lang.Object(ARRAY(i583))) → 6700_0_InterpretArray_ConstantStackPush(EOS(STATIC_6700), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357)
6700_0_InterpretArray_ConstantStackPush(EOS(STATIC_6700), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357) → 6712_0_InterpretArray_IntArithmetic(EOS(STATIC_6712), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357, 1)
6712_0_InterpretArray_IntArithmetic(EOS(STATIC_6712), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357, matching1) → 6725_0_InterpretArray_ArrayAccess(EOS(STATIC_6725), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), -(i2357, 1)) | &&(>(i2357, 0), =(matching1, 1))
6725_0_InterpretArray_ArrayAccess(EOS(STATIC_6725), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2442) → 6739_0_InterpretArray_ArrayAccess(EOS(STATIC_6739), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2442)
6739_0_InterpretArray_ArrayAccess(EOS(STATIC_6739), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2442) → 6754_0_InterpretArray_Load(EOS(STATIC_6754), i2357, i2419, i2427, o5402) | <(i2442, i583)
6754_0_InterpretArray_Load(EOS(STATIC_6754), i2357, i2419, i2427, o5402) → 6770_0_InterpretArray_ArrayAccess(EOS(STATIC_6770), i2357, i2419, i2427, o5402, i2419)
6770_0_InterpretArray_ArrayAccess(EOS(STATIC_6770), i2357, i2419, i2427, java.lang.Object(o5439put), i2419) → 6785_0_InterpretArray_ArrayAccess(EOS(STATIC_6785), i2357, i2419, i2427, java.lang.Object(o5439put), i2419)
6785_0_InterpretArray_ArrayAccess(EOS(STATIC_6785), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) → 6805_0_InterpretArray_ArrayAccess(EOS(STATIC_6805), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) | >=(i2469, 0)
6805_0_InterpretArray_ArrayAccess(EOS(STATIC_6805), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) → 6822_0_InterpretArray_ArrayAccess(EOS(STATIC_6822), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419)
6822_0_InterpretArray_ArrayAccess(EOS(STATIC_6822), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) → 6843_0_InterpretArray_EQ(EOS(STATIC_6843), i2357, i2419, i2427, i2489) | <(i2419, i2469)
6843_0_InterpretArray_EQ(EOS(STATIC_6843), i2357, i2419, i2489, i2489) → 6866_0_InterpretArray_EQ(EOS(STATIC_6866), i2357, i2419, i2489, i2489)
6843_0_InterpretArray_EQ(EOS(STATIC_6843), i2357, i2419, i2427, i2489) → 6867_0_InterpretArray_EQ(EOS(STATIC_6867), i2357, i2419, i2427, i2489)
6866_0_InterpretArray_EQ(EOS(STATIC_6866), i2357, i2419, i2489, i2489) → 6888_0_InterpretArray_Inc(EOS(STATIC_6888), i2357, i2419)
6888_0_InterpretArray_Inc(EOS(STATIC_6888), i2357, i2419) → 6914_0_InterpretArray_JMP(EOS(STATIC_6914), +(i2357, -1), i2419) | >(i2357, 0)
6914_0_InterpretArray_JMP(EOS(STATIC_6914), i2529, i2419) → 6947_0_InterpretArray_Load(EOS(STATIC_6947), i2529, i2419)
6947_0_InterpretArray_Load(EOS(STATIC_6947), i2529, i2419) → 6495_0_InterpretArray_Load(EOS(STATIC_6495), i2529, i2419)
6495_0_InterpretArray_Load(EOS(STATIC_6495), i2277, i2279) → 6518_0_InterpretArray_ConstantStackPush(EOS(STATIC_6518), i2277, i2279, i2277)
6867_0_InterpretArray_EQ(EOS(STATIC_6867), i2357, i2419, i2427, i2489) → 6889_0_InterpretArray_Load(EOS(STATIC_6889), i2357, i2419) | !(=(i2427, i2489))
6889_0_InterpretArray_Load(EOS(STATIC_6889), i2357, i2419) → 6915_0_InterpretArray_FieldAccess(EOS(STATIC_6915), i2357, i2419)
6915_0_InterpretArray_FieldAccess(EOS(STATIC_6915), i2357, i2419) → 6948_0_InterpretArray_Load(EOS(STATIC_6948), i2357, i2419, java.lang.Object(ARRAY(8)))
6948_0_InterpretArray_Load(EOS(STATIC_6948), i2357, i2419, java.lang.Object(ARRAY(matching1))) → 6974_0_InterpretArray_ArrayAccess(EOS(STATIC_6974), i2357, i2419, java.lang.Object(ARRAY(8)), i2357) | =(matching1, 8)
6974_0_InterpretArray_ArrayAccess(EOS(STATIC_6974), i2597, i2419, java.lang.Object(ARRAY(matching1)), i2597) → 7004_0_InterpretArray_ArrayAccess(EOS(STATIC_7004), i2597, i2419, java.lang.Object(ARRAY(8)), i2597) | =(matching1, 8)
7004_0_InterpretArray_ArrayAccess(EOS(STATIC_7004), i2597, i2419, java.lang.Object(ARRAY(matching1)), i2597) → 7037_0_InterpretArray_IntArithmetic(EOS(STATIC_7037), i2597, i2419, i2623) | &&(<(i2597, 8), =(matching1, 8))
7037_0_InterpretArray_IntArithmetic(EOS(STATIC_7037), i2597, i2419, i2623) → 7066_0_InterpretArray_Store(EOS(STATIC_7066), i2597, -(i2419, i2623)) | >=(i2419, 0)
7066_0_InterpretArray_Store(EOS(STATIC_7066), i2597, i2642) → 7099_0_InterpretArray_Load(EOS(STATIC_7099), i2597, i2642)
7099_0_InterpretArray_Load(EOS(STATIC_7099), i2597, i2642) → 7134_0_InterpretArray_FieldAccess(EOS(STATIC_7134), i2597, i2642)
7134_0_InterpretArray_FieldAccess(EOS(STATIC_7134), i2597, i2642) → 7167_0_InterpretArray_Load(EOS(STATIC_7167), i2597, i2642, java.lang.Object(ARRAY(8)))
7167_0_InterpretArray_Load(EOS(STATIC_7167), i2597, i2642, java.lang.Object(ARRAY(matching1))) → 7202_0_InterpretArray_ArrayAccess(EOS(STATIC_7202), i2597, i2642, java.lang.Object(ARRAY(8)), i2597) | =(matching1, 8)
7202_0_InterpretArray_ArrayAccess(EOS(STATIC_7202), i2597, i2642, java.lang.Object(ARRAY(matching1)), i2597) → 7238_0_InterpretArray_IntArithmetic(EOS(STATIC_7238), i2597, i2642) | &&(<(i2597, 8), =(matching1, 8))
7238_0_InterpretArray_IntArithmetic(EOS(STATIC_7238), i2597, i2642) → 7256_0_InterpretArray_Store(EOS(STATIC_7256), i2597, i2642)
7256_0_InterpretArray_Store(EOS(STATIC_7256), i2597, i2642) → 7275_0_InterpretArray_Inc(EOS(STATIC_7275), i2597, i2642)
7275_0_InterpretArray_Inc(EOS(STATIC_7275), i2597, i2642) → 7294_0_InterpretArray_JMP(EOS(STATIC_7294), +(i2597, -1), i2642) | >(i2597, 0)
7294_0_InterpretArray_JMP(EOS(STATIC_7294), i2894, i2642) → 7310_0_InterpretArray_Load(EOS(STATIC_7310), i2894, i2642)
7310_0_InterpretArray_Load(EOS(STATIC_7310), i2894, i2642) → 6495_0_InterpretArray_Load(EOS(STATIC_6495), i2894, i2642)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
6518_0_InterpretArray_ConstantStackPush(EOS(STATIC_6518), x0, x1, x0) → 6518_0_InterpretArray_ConstantStackPush(EOS(STATIC_6518), +(x0, -1), x1, +(x0, -1)) | >(+(x0, 1), 1)
6518_0_InterpretArray_ConstantStackPush(EOS(STATIC_6518), x0, x1, x0) → 6518_0_InterpretArray_ConstantStackPush(EOS(STATIC_6518), +(x0, -1), -(x1, x2), +(x0, -1)) | &&(&&(>(+(x1, 1), 0), >(+(x0, 1), 1)), <(x0, 8))
R rules:
Filtered ground terms:
6518_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4) → 6518_0_InterpretArray_ConstantStackPush(x2, x3, x4)
EOS(x1) → EOS
Cond_6518_0_InterpretArray_ConstantStackPush1(x1, x2, x3, x4, x5, x6) → Cond_6518_0_InterpretArray_ConstantStackPush1(x1, x3, x4, x5, x6)
Cond_6518_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_6518_0_InterpretArray_ConstantStackPush(x1, x3, x4, x5)
Filtered duplicate args:
6518_0_InterpretArray_ConstantStackPush(x1, x2, x3) → 6518_0_InterpretArray_ConstantStackPush(x2, x3)
Cond_6518_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4) → Cond_6518_0_InterpretArray_ConstantStackPush(x1, x3, x4)
Cond_6518_0_InterpretArray_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_6518_0_InterpretArray_ConstantStackPush1(x1, x3, x4, x5)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
6518_0_InterpretArray_ConstantStackPush(x1, x0) → 6518_0_InterpretArray_ConstantStackPush(x1, +(x0, -1)) | >(x0, 0)
6518_0_InterpretArray_ConstantStackPush(x1, x0) → 6518_0_InterpretArray_ConstantStackPush(-(x1, x2), +(x0, -1)) | &&(&&(>(x1, -1), >(x0, 0)), <(x0, 8))
R rules:
Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.
P rules:
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x0) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0, 0), x1, x0)
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1, x0) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, +(x0, -1))
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x0) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1, -1), >(x0, 0)), <(x0, 8)), x1, x0, x2)
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1, x0, x2) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1, x2), +(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if (x0[0] > 0 ∧x1[0] →* x1[1]∧x0[0] →* x0[1])
(1) -> (0), if (x1[1] →* x1[0]∧x0[1] + -1 →* x0[0])
(1) -> (2), if (x1[1] →* x1[2]∧x0[1] + -1 →* x0[2])
(2) -> (3), if (x1[2] > -1 && x0[2] > 0 && x0[2] < 8 ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(3) -> (0), if (x1[3] - x2[3] →* x1[0]∧x0[3] + -1 →* x0[0])
(3) -> (2), if (x1[3] - x2[3] →* x1[2]∧x0[3] + -1 →* x0[2])
(1) (>(x0[0], 0)=TRUE∧x1[0]=x1[1]∧x0[0]=x0[1] ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧[(-1)bso_19] ≥ 0)
(6) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥)∧0 = 0∧[(-1)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)
(7) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥)∧0 = 0∧[(-1)Bound*bni_18] + [bni_18]x0[0] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)
(8) (>(x0[0], 0)=TRUE∧x1[0]=x1[1]∧x0[0]=x0[1]∧x1[1]=x1[0]1∧+(x0[1], -1)=x0[0]1 ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(9) (>(x0[0], 0)=TRUE ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], +(x0[0], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(10) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_21] ≥ 0)
(11) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_21] ≥ 0)
(12) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_21] ≥ 0)
(13) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧0 = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)
(14) (x0[0] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)
(15) (>(x0[0], 0)=TRUE∧x1[0]=x1[1]∧x0[0]=x0[1]∧x1[1]=x1[2]∧+(x0[1], -1)=x0[2] ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(16) (>(x0[0], 0)=TRUE ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], +(x0[0], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(17) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_21] ≥ 0)
(18) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_21] ≥ 0)
(19) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[1 + (-1)bso_21] ≥ 0)
(20) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧0 = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)
(21) (x0[0] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)
(22) (x1[1]=x1[2]∧+(x0[1], -1)=x0[2]∧&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3] ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥))
(23) (<(+(x0[1], -1), 8)=TRUE∧>(x1[2], -1)=TRUE∧>(+(x0[1], -1), 0)=TRUE ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], +(x0[1], -1))≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], +(x0[1], -1))≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(+(x0[1], -1), 0)), <(+(x0[1], -1), 8)), x1[2], +(x0[1], -1), x2[2])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥))
(24) ([8] + [-1]x0[1] ≥ 0∧x1[2] ≥ 0∧x0[1] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[1] ≥ 0∧[(-1)bso_23] ≥ 0)
(25) ([8] + [-1]x0[1] ≥ 0∧x1[2] ≥ 0∧x0[1] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[1] ≥ 0∧[(-1)bso_23] ≥ 0)
(26) ([8] + [-1]x0[1] ≥ 0∧x1[2] ≥ 0∧x0[1] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[1] ≥ 0∧[(-1)bso_23] ≥ 0)
(27) ([8] + [-1]x0[1] ≥ 0∧x1[2] ≥ 0∧x0[1] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[1] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(28) ([6] + [-1]x0[1] ≥ 0∧x1[2] ≥ 0∧x0[1] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x0[1] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(29) (-(x1[3], x2[3])=x1[2]∧+(x0[3], -1)=x0[2]∧&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8))=TRUE∧x1[2]=x1[3]1∧x0[2]=x0[3]1∧x2[2]=x2[3]1 ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥))
(30) (<(+(x0[3], -1), 8)=TRUE∧>(-(x1[3], x2[3]), -1)=TRUE∧>(+(x0[3], -1), 0)=TRUE ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(-(x1[3], x2[3]), -1), >(+(x0[3], -1), 0)), <(+(x0[3], -1), 8)), -(x1[3], x2[3]), +(x0[3], -1), x2[2])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥))
(31) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)
(32) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)
(33) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)
(34) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(35) ([6] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(36) ([6] + [-1]x0[3] ≥ 0∧x1[3] ≥ 0∧x0[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(37) ([6] + [-1]x0[3] ≥ 0∧x1[3] ≥ 0∧x0[3] ≥ 0∧x2[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(38) ([6] + [-1]x0[3] ≥ 0∧x1[3] ≥ 0∧x0[3] ≥ 0∧x2[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_22] + [bni_22]x0[3] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
(39) (&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧-(x1[3], x2[3])=x1[0]∧+(x0[3], -1)=x0[0] ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(40) (<(x0[2], 8)=TRUE∧>(x1[2], -1)=TRUE∧>(x0[2], 0)=TRUE ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[2], x2[2]), +(x0[2], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(41) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)
(42) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)
(43) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)
(44) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)
(45) ([6] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)
(46) (&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧-(x1[3], x2[3])=x1[2]1∧+(x0[3], -1)=x0[2]1 ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(47) (<(x0[2], 8)=TRUE∧>(x1[2], -1)=TRUE∧>(x0[2], 0)=TRUE ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[2], x2[2]), +(x0[2], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(48) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)
(49) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)
(50) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)
(51) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-2)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)
(52) ([6] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)
POL(TRUE) = [1]
POL(FALSE) = [1]
POL(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x2)) = [-1] + x2
POL(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x2, x3)) = [-1] + x3
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(x1, x2, x3, x4)) = [-1] + x3 + [-1]x1
POL(&&(x1, x2)) = 0
POL(<(x1, x2)) = [-1]
POL(8) = [8]
POL(-(x1, x2)) = x1 + [-1]x2
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1]) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0]) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1]) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2]) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3]) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0]) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2]) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3]) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(3) -> (0), if (x1[3] - x2[3] →* x1[0]∧x0[3] + -1 →* x0[0])
(3) -> (2), if (x1[3] - x2[3] →* x1[2]∧x0[3] + -1 →* x0[2])
(2) -> (3), if (x1[2] > -1 && x0[2] > 0 && x0[2] < 8 ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(3) -> (2), if (x1[3] - x2[3] →* x1[2]∧x0[3] + -1 →* x0[2])
(2) -> (3), if (x1[2] > -1 && x0[2] > 0 && x0[2] < 8 ∧x1[2] →* x1[3]∧x0[2] →* x0[3]∧x2[2] →* x2[3])
(1) (&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3]∧x2[2]=x2[3]∧-(x1[3], x2[3])=x1[2]1∧+(x0[3], -1)=x0[2]1 ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(2) (<(x0[2], 8)=TRUE∧>(x1[2], -1)=TRUE∧>(x0[2], 0)=TRUE ⇒ COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[2], x2[2]), +(x0[2], -1))∧(UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(3) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)
(4) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)
(5) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x0[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)
(6) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
(7) ([6] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_14] + [bni_14]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
(8) (-(x1[3], x2[3])=x1[2]∧+(x0[3], -1)=x0[2]∧&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8))=TRUE∧x1[2]=x1[3]1∧x0[2]=x0[3]1∧x2[2]=x2[3]1 ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥))
(9) (<(+(x0[3], -1), 8)=TRUE∧>(-(x1[3], x2[3]), -1)=TRUE∧>(+(x0[3], -1), 0)=TRUE ⇒ 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))≥NonInfC∧6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))≥COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(-(x1[3], x2[3]), -1), >(+(x0[3], -1), 0)), <(+(x0[3], -1), 8)), -(x1[3], x2[3]), +(x0[3], -1), x2[2])∧(UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥))
(10) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧[(-1)bso_17] ≥ 0)
(11) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧[(-1)bso_17] ≥ 0)
(12) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧[(-1)bso_17] ≥ 0)
(13) ([8] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-2)bni_16 + (-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(14) ([6] + [-1]x0[3] ≥ 0∧x1[3] + [-1]x2[3] ≥ 0∧x0[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(15) ([6] + [-1]x0[3] ≥ 0∧x1[3] ≥ 0∧x0[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(16) ([6] + [-1]x0[3] ≥ 0∧x1[3] ≥ 0∧x0[3] ≥ 0∧x2[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
(17) ([6] + [-1]x0[3] ≥ 0∧x1[3] ≥ 0∧x0[3] ≥ 0∧x2[3] ≥ 0 ⇒ (UIncreasing(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]x0[3] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(x1, x2, x3, x4)) = [-1] + x3 + [-1]x1
POL(6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x2)) = [-1] + x2
POL(-(x1, x2)) = x1 + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<(x1, x2)) = [-1]
POL(8) = [8]
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3]) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))
COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3]) → 6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2]) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])
6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2]) → COND_6518_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])
&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1
!= | ~ | 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 31 rules for P and 0 rules for R.
P rules:
5610_0_Display_FieldAccess(EOS(STATIC_5610(i583, matching1)), i1751, i1751) → 5613_0_Display_GE(EOS(STATIC_5613(i583, 12)), i1751, i1751, i583) | =(matching1, 12)
5613_0_Display_GE(EOS(STATIC_5613(i583, matching1)), i1751, i1751, i583) → 5616_0_Display_GE(EOS(STATIC_5616(i583, 12)), i1751, i1751, i583) | =(matching1, 12)
5616_0_Display_GE(EOS(STATIC_5616(i583, matching1)), i1751, i1751, i583) → 5620_0_Display_ConstantStackPush(EOS(STATIC_5620(i583, 12)), i1751) | &&(<(i1751, i583), =(matching1, 12))
5620_0_Display_ConstantStackPush(EOS(STATIC_5620(i583, matching1)), i1751) → 5625_0_Display_Store(EOS(STATIC_5625(i583, 12)), i1751, 0) | =(matching1, 12)
5625_0_Display_Store(EOS(STATIC_5625(i583, matching1)), i1751, matching2) → 5630_0_Display_Load(EOS(STATIC_5630(i583, 12)), i1751, 0) | &&(=(matching1, 12), =(matching2, 0))
5630_0_Display_Load(EOS(STATIC_5630(i583, matching1)), i1751, matching2) → 5682_0_Display_Load(EOS(STATIC_5682(i583, 12)), i1751, 0) | &&(=(matching1, 12), =(matching2, 0))
5682_0_Display_Load(EOS(STATIC_5682(i583, matching1)), i1751, i1769) → 5785_0_Display_Load(EOS(STATIC_5785(i583, 12)), i1751, i1769) | =(matching1, 12)
5785_0_Display_Load(EOS(STATIC_5785(i583, matching1)), i1751, i1837) → 5969_0_Display_Load(EOS(STATIC_5969(i583, 12)), i1751, i1837) | =(matching1, 12)
5969_0_Display_Load(EOS(STATIC_5969(i583, matching1)), i1751, i1998) → 6066_0_Display_Load(EOS(STATIC_6066(i583, 12)), i1751, i1998) | =(matching1, 12)
6066_0_Display_Load(EOS(STATIC_6066(i583, matching1)), i1751, i2030) → 6086_0_Display_FieldAccess(EOS(STATIC_6086(i583, 12)), i1751, i2030, i2030) | =(matching1, 12)
6086_0_Display_FieldAccess(EOS(STATIC_6086(i583, matching1)), i1751, i2030, i2030) → 6106_0_Display_GT(EOS(STATIC_6106(i583, 12)), i1751, i2030, i2030, 12) | =(matching1, 12)
6106_0_Display_GT(EOS(STATIC_6106(i583, matching1)), i1751, i2051, i2051, matching2) → 6125_0_Display_GT(EOS(STATIC_6125(i583, 12)), i1751, i2051, i2051, 12) | &&(=(matching1, 12), =(matching2, 12))
6106_0_Display_GT(EOS(STATIC_6106(i583, matching1)), i1751, matching2, matching3, matching4) → 6126_0_Display_GT(EOS(STATIC_6126(i583, 12)), i1751, 13, 13, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
6125_0_Display_GT(EOS(STATIC_6125(i583, matching1)), i1751, i2051, i2051, matching2) → 6150_0_Display_Load(EOS(STATIC_6150(i583, 12)), i1751, i2051) | &&(&&(<=(i2051, 12), =(matching1, 12)), =(matching2, 12))
6150_0_Display_Load(EOS(STATIC_6150(i583, matching1)), i1751, i2051) → 6176_0_Display_FieldAccess(EOS(STATIC_6176(i583, 12)), i1751, i2051, i2051) | =(matching1, 12)
6176_0_Display_FieldAccess(EOS(STATIC_6176(i583, matching1)), i1751, i2051, i2051) → 6198_0_Display_EQ(EOS(STATIC_6198(i583, 12)), i1751, i2051, i2051, 12) | =(matching1, 12)
6198_0_Display_EQ(EOS(STATIC_6198(i583, matching1)), i1751, i2104, i2104, matching2) → 6223_0_Display_EQ(EOS(STATIC_6223(i583, 12)), i1751, i2104, i2104, 12) | &&(=(matching1, 12), =(matching2, 12))
6198_0_Display_EQ(EOS(STATIC_6198(i583, matching1)), i1751, matching2, matching3, matching4) → 6224_0_Display_EQ(EOS(STATIC_6224(i583, 12)), i1751, 12, 12, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 12)), =(matching3, 12)), =(matching4, 12))
6223_0_Display_EQ(EOS(STATIC_6223(i583, matching1)), i1751, i2104, i2104, matching2) → 6247_0_Display_Inc(EOS(STATIC_6247(i583, 12)), i1751, i2104) | &&(&&(!(=(i2104, 12)), =(matching1, 12)), =(matching2, 12))
6247_0_Display_Inc(EOS(STATIC_6247(i583, matching1)), i1751, i2104) → 6267_0_Display_JMP(EOS(STATIC_6267(i583, 12)), i1751, +(i2104, 1)) | &&(>=(i2104, 0), =(matching1, 12))
6267_0_Display_JMP(EOS(STATIC_6267(i583, matching1)), i1751, i2125) → 6296_0_Display_Load(EOS(STATIC_6296(i583, 12)), i1751, i2125) | =(matching1, 12)
6296_0_Display_Load(EOS(STATIC_6296(i583, matching1)), i1751, i2125) → 6066_0_Display_Load(EOS(STATIC_6066(i583, 12)), i1751, i2125) | =(matching1, 12)
6224_0_Display_EQ(EOS(STATIC_6224(i583, matching1)), i1751, matching2, matching3, matching4) → 6248_0_Display_Inc(EOS(STATIC_6248(i583, 12)), i1751, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 12)), =(matching3, 12)), =(matching4, 12))
6248_0_Display_Inc(EOS(STATIC_6248(i583, matching1)), i1751, matching2) → 6269_0_Display_JMP(EOS(STATIC_6269(i583, 12)), i1751, 13) | &&(=(matching1, 12), =(matching2, 12))
6269_0_Display_JMP(EOS(STATIC_6269(i583, matching1)), i1751, matching2) → 6298_0_Display_Load(EOS(STATIC_6298(i583, 12)), i1751, 13) | &&(=(matching1, 12), =(matching2, 13))
6298_0_Display_Load(EOS(STATIC_6298(i583, matching1)), i1751, matching2) → 6066_0_Display_Load(EOS(STATIC_6066(i583, 12)), i1751, 13) | &&(=(matching1, 12), =(matching2, 13))
6126_0_Display_GT(EOS(STATIC_6126(i583, matching1)), i1751, matching2, matching3, matching4) → 6151_0_Display_Inc(EOS(STATIC_6151(i583, 12)), i1751) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
6151_0_Display_Inc(EOS(STATIC_6151(i583, matching1)), i1751) → 6178_0_Display_JMP(EOS(STATIC_6178(i583, 12)), +(i1751, 1)) | &&(>=(i1751, 0), =(matching1, 12))
6178_0_Display_JMP(EOS(STATIC_6178(i583, matching1)), i2072) → 6199_0_Display_Load(EOS(STATIC_6199(i583, 12)), i2072) | =(matching1, 12)
6199_0_Display_Load(EOS(STATIC_6199(i583, matching1)), i2072) → 5605_0_Display_Load(EOS(STATIC_5605(i583, 12)), i2072) | =(matching1, 12)
5605_0_Display_Load(EOS(STATIC_5605(i583, matching1)), i1751) → 5610_0_Display_FieldAccess(EOS(STATIC_5610(i583, 12)), i1751, i1751) | =(matching1, 12)
R rules:
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
6106_0_Display_GT(EOS(STATIC_6106(x0, 12)), x2, x3, x3, 12) → 6106_0_Display_GT(EOS(STATIC_6106(x0, 12)), x2, +(x3, 1), +(x3, 1), 12) | &&(>(+(x3, 1), 0), <(x3, 12))
6106_0_Display_GT(EOS(STATIC_6106(x0, 12)), x2, 12, 12, 12) → 6106_0_Display_GT(EOS(STATIC_6106(x0, 12)), x2, 13, 13, 12)
6106_0_Display_GT(EOS(STATIC_6106(x0, 12)), x2, 13, 13, 12) → 6106_0_Display_GT(EOS(STATIC_6106(x0, 12)), +(x2, 1), 0, 0, 12) | &&(>(+(x2, 1), 0), >(x0, +(x2, 1)))
R rules:
Filtered ground terms:
6106_0_Display_GT(x1, x2, x3, x4, x5) → 6106_0_Display_GT(x1, x2, x3, x4)
STATIC_6106(x1, x2) → STATIC_6106(x1)
Cond_6106_0_Display_GT1(x1, x2, x3, x4, x5, x6) → Cond_6106_0_Display_GT1(x1, x2, x3)
Cond_6106_0_Display_GT(x1, x2, x3, x4, x5, x6) → Cond_6106_0_Display_GT(x1, x2, x3, x4, x5)
Filtered duplicate args:
6106_0_Display_GT(x1, x2, x3, x4) → 6106_0_Display_GT(x1, x2, x4)
Cond_6106_0_Display_GT(x1, x2, x3, x4, x5) → Cond_6106_0_Display_GT(x1, x2, x3, x5)
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
6106_0_Display_GT(EOS(STATIC_6106(x0)), x2, x3) → 6106_0_Display_GT(EOS(STATIC_6106(x0)), x2, +(x3, 1)) | &&(>(x3, -1), <(x3, 12))
6106_0_Display_GT(EOS(STATIC_6106(x0)), x2, 12) → 6106_0_Display_GT(EOS(STATIC_6106(x0)), x2, 13)
6106_0_Display_GT(EOS(STATIC_6106(x0)), x2, 13) → 6106_0_Display_GT(EOS(STATIC_6106(x0)), +(x2, 1), 0) | &&(>(x2, -1), >(x0, +(x2, 1)))
R rules:
Finished conversion. Obtained 5 rules for P and 0 rules for R. System has predefined symbols.
P rules:
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0)), x2, x3) → COND_6106_0_DISPLAY_GT(&&(>(x3, -1), <(x3, 12)), EOS(STATIC_6106(x0)), x2, x3)
COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0)), x2, x3) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0)), x2, +(x3, 1))
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0)), x2, 12) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0)), x2, 13)
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0)), x2, 13) → COND_6106_0_DISPLAY_GT1(&&(>(x2, -1), >(x0, +(x2, 1))), EOS(STATIC_6106(x0)), x2, 13)
COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0)), x2, 13) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0)), +(x2, 1), 0)
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 (x3[0] > -1 && x3[0] < 12 ∧EOS(STATIC_6106(x0[0])) →* EOS(STATIC_6106(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (0), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(1) -> (2), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 12)
(1) -> (3), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[3]))∧x2[1] →* x2[3]∧x3[1] + 1 →* 13)
(2) -> (0), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[0]))∧x2[2] →* x2[0]∧13 →* x3[0])
(2) -> (2), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[2]'))∧x2[2] →* x2[2]'∧13 →* 12)
(2) -> (3), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[3]))∧x2[2] →* x2[3])
(3) -> (4), if (x2[3] > -1 && x0[3] > x2[3] + 1 ∧EOS(STATIC_6106(x0[3])) →* EOS(STATIC_6106(x0[4]))∧x2[3] →* x2[4])
(4) -> (0), if (EOS(STATIC_6106(x0[4])) →* EOS(STATIC_6106(x0[0]))∧x2[4] + 1 →* x2[0]∧0 →* x3[0])
(4) -> (2), if (EOS(STATIC_6106(x0[4])) →* EOS(STATIC_6106(x0[2]))∧x2[4] + 1 →* x2[2]∧0 →* 12)
(4) -> (3), if (EOS(STATIC_6106(x0[4])) →* EOS(STATIC_6106(x0[3]))∧x2[4] + 1 →* x2[3]∧0 →* 13)
(1) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥))
(2) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥))
(3) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x2[0] + [bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)
(4) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x2[0] + [bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)
(5) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x2[0] + [bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)
(6) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
(7) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[0]1))∧x2[1]=x2[0]1∧+(x3[1], 1)=x3[0]1 ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(8) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(9) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(10) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(11) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(12) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(13) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12 ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(14) (+(x3[0], 1)=12∧>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(15) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(16) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(17) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(18) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(19) (x3[0] ≥ 0∧[11] + x3[0] ≥ 0∧[-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(20) (0 ≥ 0∧[11] ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(21) (0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(22) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[3]))∧x2[1]=x2[3]∧+(x3[1], 1)=13 ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(23) (+(x3[0], 1)=13∧>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(24) (x3[0] + [-12] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(25) (x3[0] + [-12] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(26) (x3[0] + [-12] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x2[0] + [bni_26]x0[0] ≥ 0∧[(-1)bso_27] ≥ 0)
(27) (x3[0] + [-12] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(28) (EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[0]))∧x2[2]=x2[0]∧13=x3[0] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(29) (+(x3[1], 1)=12 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(30) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[1] + [bni_28]x0[1] ≥ 0∧[(-1)bso_29] ≥ 0)
(31) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[1] + [bni_28]x0[1] ≥ 0∧[(-1)bso_29] ≥ 0)
(32) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[1] + [bni_28]x0[1] ≥ 0∧[(-1)bso_29] ≥ 0)
(33) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28] = 0∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
(34) (EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6106(x0[2]1))=EOS(STATIC_6106(x0[0]))∧x2[2]1=x2[0]∧13=x3[0] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)), ≥))
(35) (EOS(STATIC_6106(x0[4]))=EOS(STATIC_6106(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[0]))∧x2[2]=x2[0]∧13=x3[0] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(36) (EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(37) (EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[3]))∧x2[2]=x2[3] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(38) (+(x3[1], 1)=12 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(39) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[1] + [bni_28]x0[1] ≥ 0∧[(-1)bso_29] ≥ 0)
(40) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[1] + [bni_28]x0[1] ≥ 0∧[(-1)bso_29] ≥ 0)
(41) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x2[1] + [bni_28]x0[1] ≥ 0∧[(-1)bso_29] ≥ 0)
(42) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28] = 0∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
(43) (EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6106(x0[2]1))=EOS(STATIC_6106(x0[2]2))∧x2[2]1=x2[2]2 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)), ≥))
(44) (EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6106(x0[2]1))=EOS(STATIC_6106(x0[3]))∧x2[2]1=x2[3] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)), ≥))
(45) (EOS(STATIC_6106(x0[4]))=EOS(STATIC_6106(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(46) (EOS(STATIC_6106(x0[4]))=EOS(STATIC_6106(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[3]))∧x2[2]=x2[3] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(47) (&&(>(x2[3], -1), >(x0[3], +(x2[3], 1)))=TRUE∧EOS(STATIC_6106(x0[3]))=EOS(STATIC_6106(x0[4]))∧x2[3]=x2[4] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), x2[3], 13)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), x2[3], 13)≥COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)∧(UIncreasing(COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)), ≥))
(48) (>(x2[3], -1)=TRUE∧>(x0[3], +(x2[3], 1))=TRUE ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), x2[3], 13)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), x2[3], 13)≥COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)∧(UIncreasing(COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)), ≥))
(49) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x2[3] + [bni_30]x0[3] ≥ 0∧[(-1)bso_31] ≥ 0)
(50) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x2[3] + [bni_30]x0[3] ≥ 0∧[(-1)bso_31] ≥ 0)
(51) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x2[3] + [bni_30]x0[3] ≥ 0∧[(-1)bso_31] ≥ 0)
(52) (x2[3] ≥ 0∧x0[3] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)), ≥)∧[bni_30 + (-1)Bound*bni_30] + [bni_30]x0[3] ≥ 0∧[(-1)bso_31] ≥ 0)
(53) (&&(>(x2[3], -1), >(x0[3], +(x2[3], 1)))=TRUE∧EOS(STATIC_6106(x0[3]))=EOS(STATIC_6106(x0[4]))∧x2[3]=x2[4]∧EOS(STATIC_6106(x0[4]))=EOS(STATIC_6106(x0[0]))∧+(x2[4], 1)=x2[0]∧0=x3[0] ⇒ COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13)≥NonInfC∧COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥))
(54) (>(x2[3], -1)=TRUE∧>(x0[3], +(x2[3], 1))=TRUE ⇒ COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[3])), x2[3], 13)≥NonInfC∧COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[3])), x2[3], 13)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), +(x2[3], 1), 0)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥))
(55) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x2[3] + [bni_32]x0[3] ≥ 0∧[1 + (-1)bso_33] ≥ 0)
(56) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x2[3] + [bni_32]x0[3] ≥ 0∧[1 + (-1)bso_33] ≥ 0)
(57) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x2[3] + [bni_32]x0[3] ≥ 0∧[1 + (-1)bso_33] ≥ 0)
(58) (x2[3] ≥ 0∧x0[3] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[3] ≥ 0∧[1 + (-1)bso_33] ≥ 0)
(59) (&&(>(x2[3], -1), >(x0[3], +(x2[3], 1)))=TRUE∧EOS(STATIC_6106(x0[3]))=EOS(STATIC_6106(x0[4]))∧x2[3]=x2[4]∧EOS(STATIC_6106(x0[4]))=EOS(STATIC_6106(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12 ⇒ COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13)≥NonInfC∧COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥))
(60) (&&(>(x2[3], -1), >(x0[3], +(x2[3], 1)))=TRUE∧EOS(STATIC_6106(x0[3]))=EOS(STATIC_6106(x0[4]))∧x2[3]=x2[4]∧EOS(STATIC_6106(x0[4]))=EOS(STATIC_6106(x0[3]1))∧+(x2[4], 1)=x2[3]1∧0=13 ⇒ COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13)≥NonInfC∧COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)), ≥))
POL(TRUE) = 0
POL(FALSE) = 0
POL(6106_0_DISPLAY_GT(x1, x2, x3)) = [-1] + [-1]x2 + [-1]x1
POL(EOS(x1)) = [-1] + [-1]x1
POL(STATIC_6106(x1)) = [-1] + x1
POL(COND_6106_0_DISPLAY_GT(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<(x1, x2)) = [-1]
POL(12) = [12]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(13) = [13]
POL(COND_6106_0_DISPLAY_GT1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(0) = 0
COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), x2[3], 13) → COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)
COND_6106_0_DISPLAY_GT1(TRUE, EOS(STATIC_6106(x0[4])), x2[4], 13) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[4])), +(x2[4], 1), 0)
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0]) → COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])
COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1]) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[3])), x2[3], 13) → COND_6106_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6106(x0[3])), x2[3], 13)
&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(1) -> (0), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(2) -> (0), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[0]))∧x2[2] →* x2[0]∧13 →* x3[0])
(0) -> (1), if (x3[0] > -1 && x3[0] < 12 ∧EOS(STATIC_6106(x0[0])) →* EOS(STATIC_6106(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (2), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 12)
(2) -> (2), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[2]'))∧x2[2] →* x2[2]'∧13 →* 12)
(1) -> (3), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[3]))∧x2[1] →* x2[3]∧x3[1] + 1 →* 13)
(2) -> (3), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[3]))∧x2[2] →* x2[3])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(1) -> (0), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(2) -> (0), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[0]))∧x2[2] →* x2[0]∧13 →* x3[0])
(0) -> (1), if (x3[0] > -1 && x3[0] < 12 ∧EOS(STATIC_6106(x0[0])) →* EOS(STATIC_6106(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (2), if (EOS(STATIC_6106(x0[1])) →* EOS(STATIC_6106(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 12)
(2) -> (2), if (EOS(STATIC_6106(x0[2])) →* EOS(STATIC_6106(x0[2]'))∧x2[2] →* x2[2]'∧13 →* 12)
(1) (EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[0]))∧x2[2]=x2[0]∧13=x3[0] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(2) (+(x3[1], 1)=12 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(3) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧[1 + (-1)bso_20] ≥ 0)
(4) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧[1 + (-1)bso_20] ≥ 0)
(5) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧[1 + (-1)bso_20] ≥ 0)
(6) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥)∧0 = 0∧0 = 0∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)
(7) (EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6106(x0[2]1))=EOS(STATIC_6106(x0[0]))∧x2[2]1=x2[0]∧13=x3[0] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)), ≥))
(8) (EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)), ≥))
(9) (EOS(STATIC_6106(x0[2]))=EOS(STATIC_6106(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6106(x0[2]1))=EOS(STATIC_6106(x0[2]2))∧x2[2]1=x2[2]2 ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 12)≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2]1)), x2[2]1, 13)), ≥))
(10) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[0]1))∧x2[1]=x2[0]1∧+(x3[1], 1)=x3[0]1 ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(11) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(12) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)
(13) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)
(14) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)
(15) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
(16) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6106(x0[1]))=EOS(STATIC_6106(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12 ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(17) (+(x3[0], 1)=12∧>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥))
(18) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)
(19) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)
(20) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)
(21) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
(22) (x3[0] ≥ 0∧[11] + x3[0] ≥ 0∧[-1]x3[0] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-12)bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x3[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
(23) (0 ≥ 0∧[11] ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-12)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
(24) (0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-12)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
(25) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6106(x0[0]))=EOS(STATIC_6106(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥))
(26) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥NonInfC∧6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0])≥COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥))
(27) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x3[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(28) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x3[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(29) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x3[0] ≥ 0∧[(-1)bso_24] ≥ 0)
(30) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x3[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_24] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [2]
POL(6106_0_DISPLAY_GT(x1, x2, x3)) = [-1] + [-1]x3
POL(EOS(x1)) = [-1] + [-1]x1
POL(STATIC_6106(x1)) = [-1] + [-1]x1
POL(12) = [12]
POL(13) = [13]
POL(COND_6106_0_DISPLAY_GT(x1, x2, x3, x4)) = [-1] + [-1]x4
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<(x1, x2)) = [-1]
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)
COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1]) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 12) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[2])), x2[2], 13)
COND_6106_0_DISPLAY_GT(TRUE, EOS(STATIC_6106(x0[1])), x2[1], x3[1]) → 6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[1])), x2[1], +(x3[1], 1))
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0]) → COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])
6106_0_DISPLAY_GT(EOS(STATIC_6106(x0[0])), x2[0], x3[0]) → COND_6106_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6106(x0[0])), x2[0], x3[0])
TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer