0 JBC
↳1 JBCToGraph (⇒, 4730 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 1630 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 210 ms)
↳9 AND
↳10 IDP
↳11 IDependencyGraphProof (⇔, 0 ms)
↳12 IDP
↳13 IDPNonInfProof (⇒, 160 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 IDP
↳24 IDPNonInfProof (⇒, 70 ms)
↳25 AND
↳26 IDP
↳27 IDependencyGraphProof (⇔, 0 ms)
↳28 TRUE
↳29 IDP
↳30 IDependencyGraphProof (⇔, 0 ms)
↳31 TRUE
↳32 JBCTerminationSCC
↳33 SCCToIDPv1Proof (⇒, 420 ms)
↳34 IDP
↳35 IDPNonInfProof (⇒, 180 ms)
↳36 AND
↳37 IDP
↳38 IDependencyGraphProof (⇔, 0 ms)
↳39 TRUE
↳40 IDP
↳41 IDependencyGraphProof (⇔, 0 ms)
↳42 TRUE
↳43 JBCTerminationSCC
↳44 SCCToIDPv1Proof (⇒, 340 ms)
↳45 IDP
↳46 IDPNonInfProof (⇒, 790 ms)
↳47 IDP
↳48 IDependencyGraphProof (⇔, 0 ms)
↳49 TRUE
↳50 JBCTerminationSCC
↳51 SCCToIDPv1Proof (⇒, 240 ms)
↳52 IDP
↳53 IDPNonInfProof (⇒, 1630 ms)
↳54 IDP
↳55 IDependencyGraphProof (⇔, 0 ms)
↳56 IDP
↳57 IDPNonInfProof (⇒, 420 ms)
↳58 IDP
↳59 IDependencyGraphProof (⇔, 0 ms)
↳60 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:
10097_0_SolveDP_FieldAccess(EOS(STATIC_10097(i326, matching1)), i5570, i5570) → 10098_0_SolveDP_GE(EOS(STATIC_10098(i326, 12)), i5570, i5570, i326) | =(matching1, 12)
10098_0_SolveDP_GE(EOS(STATIC_10098(i326, matching1)), i5570, i5570, i326) → 10100_0_SolveDP_GE(EOS(STATIC_10100(i326, 12)), i5570, i5570, i326) | =(matching1, 12)
10100_0_SolveDP_GE(EOS(STATIC_10100(i326, matching1)), i5570, i5570, i326) → 10102_0_SolveDP_ConstantStackPush(EOS(STATIC_10102(i326, 12)), i5570) | &&(<(i5570, i326), =(matching1, 12))
10102_0_SolveDP_ConstantStackPush(EOS(STATIC_10102(i326, matching1)), i5570) → 10105_0_SolveDP_Store(EOS(STATIC_10105(i326, 12)), i5570, 0) | =(matching1, 12)
10105_0_SolveDP_Store(EOS(STATIC_10105(i326, matching1)), i5570, matching2) → 10107_0_SolveDP_Load(EOS(STATIC_10107(i326, 12)), i5570, 0) | &&(=(matching1, 12), =(matching2, 0))
10107_0_SolveDP_Load(EOS(STATIC_10107(i326, matching1)), i5570, matching2) → 10479_0_SolveDP_Load(EOS(STATIC_10479(i326, 12)), i5570, 0) | &&(=(matching1, 12), =(matching2, 0))
10479_0_SolveDP_Load(EOS(STATIC_10479(i326, matching1)), i6010, i6011) → 10842_0_SolveDP_Load(EOS(STATIC_10842(i326, 12)), i6010, i6011) | =(matching1, 12)
10842_0_SolveDP_Load(EOS(STATIC_10842(i326, matching1)), i6452, i6453) → 11199_0_SolveDP_Load(EOS(STATIC_11199(i326, 12)), i6452, i6453) | =(matching1, 12)
11199_0_SolveDP_Load(EOS(STATIC_11199(i326, matching1)), i6894, i6895) → 11550_0_SolveDP_Load(EOS(STATIC_11550(i326, 12)), i6894, i6895) | =(matching1, 12)
11550_0_SolveDP_Load(EOS(STATIC_11550(i326, matching1)), i7336, i7337) → 11554_0_SolveDP_FieldAccess(EOS(STATIC_11554(i326, 12)), i7336, i7337, i7337) | =(matching1, 12)
11554_0_SolveDP_FieldAccess(EOS(STATIC_11554(i326, matching1)), i7336, i7337, i7337) → 11556_0_SolveDP_GT(EOS(STATIC_11556(i326, 12)), i7336, i7337, i7337, 12) | =(matching1, 12)
11556_0_SolveDP_GT(EOS(STATIC_11556(i326, matching1)), i7336, i7345, i7345, matching2) → 11557_0_SolveDP_GT(EOS(STATIC_11557(i326, 12)), i7336, i7345, i7345, 12) | &&(=(matching1, 12), =(matching2, 12))
11556_0_SolveDP_GT(EOS(STATIC_11556(i326, matching1)), i7336, matching2, matching3, matching4) → 11558_0_SolveDP_GT(EOS(STATIC_11558(i326, 12)), i7336, 13, 13, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
11557_0_SolveDP_GT(EOS(STATIC_11557(i326, matching1)), i7336, i7345, i7345, matching2) → 11559_0_SolveDP_Load(EOS(STATIC_11559(i326, 12)), i7336, i7345) | &&(&&(<=(i7345, 12), =(matching1, 12)), =(matching2, 12))
11559_0_SolveDP_Load(EOS(STATIC_11559(i326, matching1)), i7336, i7345) → 11561_0_SolveDP_FieldAccess(EOS(STATIC_11561(i326, 12)), i7336, i7345, i7345) | =(matching1, 12)
11561_0_SolveDP_FieldAccess(EOS(STATIC_11561(i326, matching1)), i7336, i7345, i7345) → 11563_0_SolveDP_Load(EOS(STATIC_11563(i326, 12)), i7336, i7345, i7345, java.lang.Object(ARRAY(8))) | =(matching1, 12)
11563_0_SolveDP_Load(EOS(STATIC_11563(i326, matching1)), i7336, i7345, i7345, java.lang.Object(ARRAY(matching2))) → 11566_0_SolveDP_ArrayAccess(EOS(STATIC_11566(i326, 12)), i7336, i7345, i7345, java.lang.Object(ARRAY(8)), i7336) | &&(=(matching1, 12), =(matching2, 8))
11566_0_SolveDP_ArrayAccess(EOS(STATIC_11566(i326, matching1)), i7351, i7345, i7345, java.lang.Object(ARRAY(matching2)), i7351) → 11568_0_SolveDP_ArrayAccess(EOS(STATIC_11568(i326, 12)), i7351, i7345, i7345, java.lang.Object(ARRAY(8)), i7351) | &&(=(matching1, 12), =(matching2, 8))
11568_0_SolveDP_ArrayAccess(EOS(STATIC_11568(i326, matching1)), i7352, i7345, i7345, java.lang.Object(ARRAY(matching2)), i7352) → 11571_0_SolveDP_ArrayAccess(EOS(STATIC_11571(i326, 12)), i7352, i7345, i7345, java.lang.Object(ARRAY(8)), i7352) | &&(=(matching1, 12), =(matching2, 8))
11571_0_SolveDP_ArrayAccess(EOS(STATIC_11571(i326, matching1)), i7352, i7345, i7345, java.lang.Object(ARRAY(matching2)), i7352) → 11573_0_SolveDP_IntArithmetic(EOS(STATIC_11573(i326, 12)), i7352, i7345, i7345, i7354) | &&(&&(<(i7352, 8), =(matching1, 12)), =(matching2, 8))
11573_0_SolveDP_IntArithmetic(EOS(STATIC_11573(i326, matching1)), i7352, i7345, i7345, i7354) → 11577_0_SolveDP_GE(EOS(STATIC_11577(i326, 12)), i7352, i7345, -(i7345, i7354)) | &&(>=(i7345, 0), =(matching1, 12))
11577_0_SolveDP_GE(EOS(STATIC_11577(i326, matching1)), i7352, i7345, i7362) → 11579_0_SolveDP_GE(EOS(STATIC_11579(i326, 12)), i7352, i7345, i7362) | =(matching1, 12)
11577_0_SolveDP_GE(EOS(STATIC_11577(i326, matching1)), i7352, i7345, i7363) → 11580_0_SolveDP_GE(EOS(STATIC_11580(i326, 12)), i7352, i7345, i7363) | =(matching1, 12)
11579_0_SolveDP_GE(EOS(STATIC_11579(i326, matching1)), i7352, i7345, i7362) → 11583_0_SolveDP_FieldAccess(EOS(STATIC_11583(i326, 12)), i7352, i7345) | &&(<(i7362, 0), =(matching1, 12))
11583_0_SolveDP_FieldAccess(EOS(STATIC_11583(i326, matching1)), i7352, i7345) → 11588_0_SolveDP_Load(EOS(STATIC_11588(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i326))) | =(matching1, 12)
11588_0_SolveDP_Load(EOS(STATIC_11588(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i326))) → 11592_0_SolveDP_ArrayAccess(EOS(STATIC_11592(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11592_0_SolveDP_ArrayAccess(EOS(STATIC_11592(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) → 11596_0_SolveDP_ArrayAccess(EOS(STATIC_11596(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11596_0_SolveDP_ArrayAccess(EOS(STATIC_11596(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) → 11603_0_SolveDP_Load(EOS(STATIC_11603(i326, 12)), i7352, i7345, o18003) | &&(<(i7352, i326), =(matching1, 12))
11603_0_SolveDP_Load(EOS(STATIC_11603(i326, matching1)), i7352, i7345, o18003) → 11609_0_SolveDP_FieldAccess(EOS(STATIC_11609(i326, 12)), i7352, i7345, o18003, i7345) | =(matching1, 12)
11609_0_SolveDP_FieldAccess(EOS(STATIC_11609(i326, matching1)), i7352, i7345, o18003, i7345) → 11614_0_SolveDP_Load(EOS(STATIC_11614(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326))) | =(matching1, 12)
11614_0_SolveDP_Load(EOS(STATIC_11614(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326))) → 11623_0_SolveDP_ConstantStackPush(EOS(STATIC_11623(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11623_0_SolveDP_ConstantStackPush(EOS(STATIC_11623(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7352) → 11629_0_SolveDP_IntArithmetic(EOS(STATIC_11629(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7352, 1) | =(matching1, 12)
11629_0_SolveDP_IntArithmetic(EOS(STATIC_11629(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7352, matching2) → 11634_0_SolveDP_ArrayAccess(EOS(STATIC_11634(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), -(i7352, 1)) | &&(&&(>=(i7352, 0), =(matching1, 12)), =(matching2, 1))
11634_0_SolveDP_ArrayAccess(EOS(STATIC_11634(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7426) → 11644_0_SolveDP_ArrayAccess(EOS(STATIC_11644(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7426) | =(matching1, 12)
11644_0_SolveDP_ArrayAccess(EOS(STATIC_11644(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7426) → 11653_0_SolveDP_ArrayAccess(EOS(STATIC_11653(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7426) | =(matching1, 12)
11653_0_SolveDP_ArrayAccess(EOS(STATIC_11653(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i326)), i7426) → 11663_0_SolveDP_Load(EOS(STATIC_11663(i326, 12)), i7352, i7345, o18003, i7345, o18137) | &&(<(i7426, i326), =(matching1, 12))
11663_0_SolveDP_Load(EOS(STATIC_11663(i326, matching1)), i7352, i7345, o18003, i7345, o18137) → 11679_0_SolveDP_ArrayAccess(EOS(STATIC_11679(i326, 12)), i7352, i7345, o18003, i7345, o18137, i7345) | =(matching1, 12)
11679_0_SolveDP_ArrayAccess(EOS(STATIC_11679(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(o18251put), i7345) → 11691_0_SolveDP_ArrayAccess(EOS(STATIC_11691(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(o18251put), i7345) | =(matching1, 12)
11691_0_SolveDP_ArrayAccess(EOS(STATIC_11691(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i7510)), i7345) → 11705_0_SolveDP_ArrayAccess(EOS(STATIC_11705(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i7510)), i7345) | &&(>=(i7510, 0), =(matching1, 12))
11705_0_SolveDP_ArrayAccess(EOS(STATIC_11705(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i7510)), i7345) → 11722_0_SolveDP_ArrayAccess(EOS(STATIC_11722(i326, 12)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i7510)), i7345) | =(matching1, 12)
11722_0_SolveDP_ArrayAccess(EOS(STATIC_11722(i326, matching1)), i7352, i7345, o18003, i7345, java.lang.Object(ARRAY(i7510)), i7345) → 11737_0_SolveDP_ArrayAccess(EOS(STATIC_11737(i326, 12)), i7352, i7345, o18003, i7345) | &&(<(i7345, i7510), =(matching1, 12))
11737_0_SolveDP_ArrayAccess(EOS(STATIC_11737(i326, matching1)), i7352, i7345, java.lang.Object(o18495put), i7345) → 11751_0_SolveDP_ArrayAccess(EOS(STATIC_11751(i326, 12)), i7352, i7345, java.lang.Object(o18495put), i7345) | =(matching1, 12)
11751_0_SolveDP_ArrayAccess(EOS(STATIC_11751(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) → 11769_0_SolveDP_ArrayAccess(EOS(STATIC_11769(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) | &&(>=(i7612, 0), =(matching1, 12))
11769_0_SolveDP_ArrayAccess(EOS(STATIC_11769(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) → 11791_0_SolveDP_ArrayAccess(EOS(STATIC_11791(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) | =(matching1, 12)
11791_0_SolveDP_ArrayAccess(EOS(STATIC_11791(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i7612)), i7345) → 11811_0_SolveDP_JMP(EOS(STATIC_11811(i326, 12)), i7352, i7345) | &&(<(i7345, i7612), =(matching1, 12))
11811_0_SolveDP_JMP(EOS(STATIC_11811(i326, matching1)), i7352, i7345) → 11831_0_SolveDP_Inc(EOS(STATIC_11831(i326, 12)), i7352, i7345) | =(matching1, 12)
11831_0_SolveDP_Inc(EOS(STATIC_11831(i326, matching1)), i7352, i7345) → 12881_0_SolveDP_Inc(EOS(STATIC_12881(i326, 12)), i7352, i7345) | =(matching1, 12)
12881_0_SolveDP_Inc(EOS(STATIC_12881(i326, matching1)), i7352, i7345) → 12907_0_SolveDP_JMP(EOS(STATIC_12907(i326, 12)), i7352, +(i7345, 1)) | &&(>=(i7345, 0), =(matching1, 12))
12907_0_SolveDP_JMP(EOS(STATIC_12907(i326, matching1)), i7352, i9059) → 12927_0_SolveDP_Load(EOS(STATIC_12927(i326, 12)), i7352, i9059) | =(matching1, 12)
12927_0_SolveDP_Load(EOS(STATIC_12927(i326, matching1)), i7352, i9059) → 11550_0_SolveDP_Load(EOS(STATIC_11550(i326, 12)), i7352, i9059) | =(matching1, 12)
11580_0_SolveDP_GE(EOS(STATIC_11580(i326, matching1)), i7352, i7345, i7363) → 11584_0_SolveDP_FieldAccess(EOS(STATIC_11584(i326, 12)), i7352, i7345) | &&(>=(i7363, 0), =(matching1, 12))
11584_0_SolveDP_FieldAccess(EOS(STATIC_11584(i326, matching1)), i7352, i7345) → 11589_0_SolveDP_Load(EOS(STATIC_11589(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i326))) | =(matching1, 12)
11589_0_SolveDP_Load(EOS(STATIC_11589(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i326))) → 11593_0_SolveDP_ArrayAccess(EOS(STATIC_11593(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11593_0_SolveDP_ArrayAccess(EOS(STATIC_11593(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) → 11598_0_SolveDP_ArrayAccess(EOS(STATIC_11598(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11598_0_SolveDP_ArrayAccess(EOS(STATIC_11598(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i326)), i7352) → 11606_0_SolveDP_Load(EOS(STATIC_11606(i326, 12)), i7352, i7345, o18005) | &&(<(i7352, i326), =(matching1, 12))
11606_0_SolveDP_Load(EOS(STATIC_11606(i326, matching1)), i7352, i7345, o18005) → 11610_0_SolveDP_FieldAccess(EOS(STATIC_11610(i326, 12)), i7352, i7345, o18005, i7345) | =(matching1, 12)
11610_0_SolveDP_FieldAccess(EOS(STATIC_11610(i326, matching1)), i7352, i7345, o18005, i7345) → 11617_0_SolveDP_Load(EOS(STATIC_11617(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326))) | =(matching1, 12)
11617_0_SolveDP_Load(EOS(STATIC_11617(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326))) → 11626_0_SolveDP_ConstantStackPush(EOS(STATIC_11626(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11626_0_SolveDP_ConstantStackPush(EOS(STATIC_11626(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7352) → 11630_0_SolveDP_IntArithmetic(EOS(STATIC_11630(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7352, 1) | =(matching1, 12)
11630_0_SolveDP_IntArithmetic(EOS(STATIC_11630(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7352, matching2) → 11637_0_SolveDP_ArrayAccess(EOS(STATIC_11637(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), -(i7352, 1)) | &&(&&(>=(i7352, 0), =(matching1, 12)), =(matching2, 1))
11637_0_SolveDP_ArrayAccess(EOS(STATIC_11637(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7427) → 11648_0_SolveDP_ArrayAccess(EOS(STATIC_11648(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7427) | =(matching1, 12)
11648_0_SolveDP_ArrayAccess(EOS(STATIC_11648(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7427) → 11657_0_SolveDP_ArrayAccess(EOS(STATIC_11657(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7427) | =(matching1, 12)
11657_0_SolveDP_ArrayAccess(EOS(STATIC_11657(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i326)), i7427) → 11668_0_SolveDP_Load(EOS(STATIC_11668(i326, 12)), i7352, i7345, o18005, i7345, o18153) | &&(<(i7427, i326), =(matching1, 12))
11668_0_SolveDP_Load(EOS(STATIC_11668(i326, matching1)), i7352, i7345, o18005, i7345, o18153) → 11684_0_SolveDP_ArrayAccess(EOS(STATIC_11684(i326, 12)), i7352, i7345, o18005, i7345, o18153, i7345) | =(matching1, 12)
11684_0_SolveDP_ArrayAccess(EOS(STATIC_11684(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(o18272put), i7345) → 11697_0_SolveDP_ArrayAccess(EOS(STATIC_11697(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(o18272put), i7345) | =(matching1, 12)
11697_0_SolveDP_ArrayAccess(EOS(STATIC_11697(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i7517)), i7345) → 11711_0_SolveDP_ArrayAccess(EOS(STATIC_11711(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i7517)), i7345) | &&(>=(i7517, 0), =(matching1, 12))
11711_0_SolveDP_ArrayAccess(EOS(STATIC_11711(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i7517)), i7345) → 11728_0_SolveDP_ArrayAccess(EOS(STATIC_11728(i326, 12)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i7517)), i7345) | =(matching1, 12)
11728_0_SolveDP_ArrayAccess(EOS(STATIC_11728(i326, matching1)), i7352, i7345, o18005, i7345, java.lang.Object(ARRAY(i7517)), i7345) → 11743_0_SolveDP_FieldAccess(EOS(STATIC_11743(i326, 12)), i7352, i7345, o18005, i7345, i7561) | &&(<(i7345, i7517), =(matching1, 12))
11743_0_SolveDP_FieldAccess(EOS(STATIC_11743(i326, matching1)), i7352, i7345, o18005, i7345, i7561) → 11758_0_SolveDP_Load(EOS(STATIC_11758(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326))) | =(matching1, 12)
11758_0_SolveDP_Load(EOS(STATIC_11758(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326))) → 11780_0_SolveDP_ConstantStackPush(EOS(STATIC_11780(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7352) | =(matching1, 12)
11780_0_SolveDP_ConstantStackPush(EOS(STATIC_11780(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7352) → 11801_0_SolveDP_IntArithmetic(EOS(STATIC_11801(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7352, 1) | =(matching1, 12)
11801_0_SolveDP_IntArithmetic(EOS(STATIC_11801(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7352, matching2) → 11819_0_SolveDP_ArrayAccess(EOS(STATIC_11819(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), -(i7352, 1)) | &&(&&(>=(i7352, 0), =(matching1, 12)), =(matching2, 1))
11819_0_SolveDP_ArrayAccess(EOS(STATIC_11819(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7737) → 11843_0_SolveDP_ArrayAccess(EOS(STATIC_11843(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7737) | =(matching1, 12)
11843_0_SolveDP_ArrayAccess(EOS(STATIC_11843(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7737) → 11866_0_SolveDP_ArrayAccess(EOS(STATIC_11866(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7737) | =(matching1, 12)
11866_0_SolveDP_ArrayAccess(EOS(STATIC_11866(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i326)), i7737) → 11885_0_SolveDP_Load(EOS(STATIC_11885(i326, 12)), i7352, i7345, o18005, i7345, i7561, o19136) | &&(<(i7737, i326), =(matching1, 12))
11885_0_SolveDP_Load(EOS(STATIC_11885(i326, matching1)), i7352, i7345, o18005, i7345, i7561, o19136) → 11911_0_SolveDP_FieldAccess(EOS(STATIC_11911(i326, 12)), i7352, i7345, o18005, i7345, i7561, o19136, i7345) | =(matching1, 12)
11911_0_SolveDP_FieldAccess(EOS(STATIC_11911(i326, matching1)), i7352, i7345, o18005, i7345, i7561, o19136, i7345) → 11933_0_SolveDP_Load(EOS(STATIC_11933(i326, 12)), i7352, i7345, o18005, i7345, i7561, o19136, i7345, java.lang.Object(ARRAY(8))) | =(matching1, 12)
11933_0_SolveDP_Load(EOS(STATIC_11933(i326, matching1)), i7352, i7345, o18005, i7345, i7561, o19136, i7345, java.lang.Object(ARRAY(matching2))) → 11959_0_SolveDP_ArrayAccess(EOS(STATIC_11959(i326, 12)), i7352, i7345, o18005, i7345, i7561, o19136, i7345, java.lang.Object(ARRAY(8)), i7352) | &&(=(matching1, 12), =(matching2, 8))
11959_0_SolveDP_ArrayAccess(EOS(STATIC_11959(i326, matching1)), i7352, i7345, o18005, i7345, i7561, o19136, i7345, java.lang.Object(ARRAY(matching2)), i7352) → 11995_0_SolveDP_IntArithmetic(EOS(STATIC_11995(i326, 12)), i7352, i7345, o18005, i7345, i7561, o19136, i7345, i8004) | &&(&&(<(i7352, 8), =(matching1, 12)), =(matching2, 8))
11995_0_SolveDP_IntArithmetic(EOS(STATIC_11995(i326, matching1)), i7352, i7345, o18005, i7345, i7561, o19136, i7345, i8004) → 12040_0_SolveDP_ArrayAccess(EOS(STATIC_12040(i326, 12)), i7352, i7345, o18005, i7345, i7561, o19136, -(i7345, i8004)) | &&(>=(i7345, 0), =(matching1, 12))
12040_0_SolveDP_ArrayAccess(EOS(STATIC_12040(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(o20221put), i8061) → 12074_0_SolveDP_ArrayAccess(EOS(STATIC_12074(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(o20221put), i8061) | =(matching1, 12)
12074_0_SolveDP_ArrayAccess(EOS(STATIC_12074(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8061) → 12116_0_SolveDP_ArrayAccess(EOS(STATIC_12116(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8061) | &&(>=(i8161, 0), =(matching1, 12))
12116_0_SolveDP_ArrayAccess(EOS(STATIC_12116(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8224) → 12162_0_SolveDP_ArrayAccess(EOS(STATIC_12162(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8224) | =(matching1, 12)
12162_0_SolveDP_ArrayAccess(EOS(STATIC_12162(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8224) → 12211_0_SolveDP_ArrayAccess(EOS(STATIC_12211(i326, 12)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8224) | =(matching1, 12)
12211_0_SolveDP_ArrayAccess(EOS(STATIC_12211(i326, matching1)), i7352, i7345, o18005, i7345, i7561, java.lang.Object(ARRAY(i8161)), i8224) → 12259_0_SolveDP_FieldAccess(EOS(STATIC_12259(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8355) | &&(<(i8224, i8161), =(matching1, 12))
12259_0_SolveDP_FieldAccess(EOS(STATIC_12259(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8355) → 12308_0_SolveDP_Load(EOS(STATIC_12308(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8355, java.lang.Object(ARRAY(8))) | =(matching1, 12)
12308_0_SolveDP_Load(EOS(STATIC_12308(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8355, java.lang.Object(ARRAY(matching2))) → 12353_0_SolveDP_ArrayAccess(EOS(STATIC_12353(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8355, java.lang.Object(ARRAY(8)), i7352) | &&(=(matching1, 12), =(matching2, 8))
12353_0_SolveDP_ArrayAccess(EOS(STATIC_12353(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8355, java.lang.Object(ARRAY(matching2)), i7352) → 12393_0_SolveDP_IntArithmetic(EOS(STATIC_12393(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8355, i8553) | &&(&&(<(i7352, 8), =(matching1, 12)), =(matching2, 8))
12393_0_SolveDP_IntArithmetic(EOS(STATIC_12393(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8355, i8553) → 12442_0_SolveDP_InvokeMethod(EOS(STATIC_12442(i326, 12)), i7352, i7345, o18005, i7345, i7561, +(i8355, i8553)) | =(matching1, 12)
12442_0_SolveDP_InvokeMethod(EOS(STATIC_12442(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614) → 12500_0_max_Load(EOS(STATIC_12500(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614) | =(matching1, 12)
12500_0_max_Load(EOS(STATIC_12500(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614) → 12613_0_max_Load(EOS(STATIC_12613(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561) | =(matching1, 12)
12613_0_max_Load(EOS(STATIC_12613(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561) → 12653_0_max_LE(EOS(STATIC_12653(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) | =(matching1, 12)
12653_0_max_LE(EOS(STATIC_12653(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) → 12686_0_max_LE(EOS(STATIC_12686(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) | =(matching1, 12)
12653_0_max_LE(EOS(STATIC_12653(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) → 12687_0_max_LE(EOS(STATIC_12687(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) | =(matching1, 12)
12686_0_max_LE(EOS(STATIC_12686(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) → 12718_0_max_Load(EOS(STATIC_12718(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i8614) | &&(<=(i7561, i8614), =(matching1, 12))
12718_0_max_Load(EOS(STATIC_12718(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i8614) → 12742_0_max_Return(EOS(STATIC_12742(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i8614) | =(matching1, 12)
12742_0_max_Return(EOS(STATIC_12742(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i8614) → 12773_0_SolveDP_ArrayAccess(EOS(STATIC_12773(i326, 12)), i7352, i7345, o18005, i7345, i8614) | =(matching1, 12)
12773_0_SolveDP_ArrayAccess(EOS(STATIC_12773(i326, matching1)), i7352, i7345, java.lang.Object(o23812put), i7345, i8614) → 12806_0_SolveDP_ArrayAccess(EOS(STATIC_12806(i326, 12)), i7352, i7345, java.lang.Object(o23812put), i7345, i8614) | =(matching1, 12)
12806_0_SolveDP_ArrayAccess(EOS(STATIC_12806(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i8988)), i7345, i8614) → 12831_0_SolveDP_ArrayAccess(EOS(STATIC_12831(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i8988)), i7345, i8614) | &&(>=(i8988, 0), =(matching1, 12))
12831_0_SolveDP_ArrayAccess(EOS(STATIC_12831(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i8988)), i7345, i8614) → 12855_0_SolveDP_ArrayAccess(EOS(STATIC_12855(i326, 12)), i7352, i7345, java.lang.Object(ARRAY(i8988)), i7345, i8614) | =(matching1, 12)
12855_0_SolveDP_ArrayAccess(EOS(STATIC_12855(i326, matching1)), i7352, i7345, java.lang.Object(ARRAY(i8988)), i7345, i8614) → 12881_0_SolveDP_Inc(EOS(STATIC_12881(i326, 12)), i7352, i7345) | &&(<(i7345, i8988), =(matching1, 12))
12687_0_max_LE(EOS(STATIC_12687(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561, i8614, i7561, i8614) → 12720_0_max_Load(EOS(STATIC_12720(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561) | &&(>(i7561, i8614), =(matching1, 12))
12720_0_max_Load(EOS(STATIC_12720(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561) → 12744_0_max_JMP(EOS(STATIC_12744(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561) | =(matching1, 12)
12744_0_max_JMP(EOS(STATIC_12744(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561) → 12775_0_max_Return(EOS(STATIC_12775(i326, 12)), i7352, i7345, o18005, i7345, i7561, i8614, i7561) | =(matching1, 12)
12775_0_max_Return(EOS(STATIC_12775(i326, matching1)), i7352, i7345, o18005, i7345, i7561, i8614, i7561) → 12809_0_SolveDP_ArrayAccess(EOS(STATIC_12809(i326, 12)), i7352, i7345, o18005, i7345, i7561) | =(matching1, 12)
12809_0_SolveDP_ArrayAccess(EOS(STATIC_12809(i326, matching1)), i7352, i7345, o18005, i7345, i7561) → 12773_0_SolveDP_ArrayAccess(EOS(STATIC_12773(i326, 12)), i7352, i7345, o18005, i7345, i7561) | =(matching1, 12)
11558_0_SolveDP_GT(EOS(STATIC_11558(i326, matching1)), i7336, matching2, matching3, matching4) → 11560_0_SolveDP_Inc(EOS(STATIC_11560(i326, 12)), i7336) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
11560_0_SolveDP_Inc(EOS(STATIC_11560(i326, matching1)), i7336) → 11562_0_SolveDP_JMP(EOS(STATIC_11562(i326, 12)), +(i7336, 1)) | =(matching1, 12)
11562_0_SolveDP_JMP(EOS(STATIC_11562(i326, matching1)), i7346) → 11565_0_SolveDP_Load(EOS(STATIC_11565(i326, 12)), i7346) | =(matching1, 12)
11565_0_SolveDP_Load(EOS(STATIC_11565(i326, matching1)), i7346) → 10095_0_SolveDP_Load(EOS(STATIC_10095(i326, 12)), i7346) | =(matching1, 12)
10095_0_SolveDP_Load(EOS(STATIC_10095(i326, matching1)), i5570) → 10097_0_SolveDP_FieldAccess(EOS(STATIC_10097(i326, 12)), i5570, i5570) | =(matching1, 12)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
11556_0_SolveDP_GT(EOS(STATIC_11556(x0, 12)), x2, x3, x3, 12) → 11556_0_SolveDP_GT(EOS(STATIC_11556(x0, 12)), x2, +(x3, 1), +(x3, 1), 12) | &&(&&(&&(&&(>(+(x3, 1), 0), <=(x3, 12)), >(+(x2, 1), 0)), <(x2, 8)), >(x0, -(x2, 1)))
11556_0_SolveDP_GT(EOS(STATIC_11556(x0, 12)), x2, 13, 13, 12) → 11556_0_SolveDP_GT(EOS(STATIC_11556(x0, 12)), +(x2, 1), 0, 0, 12) | >(x0, +(x2, 1))
R rules:
Filtered ground terms:
11556_0_SolveDP_GT(x1, x2, x3, x4, x5) → 11556_0_SolveDP_GT(x1, x2, x3, x4)
STATIC_11556(x1, x2) → STATIC_11556(x1)
Cond_11556_0_SolveDP_GT1(x1, x2, x3, x4, x5, x6) → Cond_11556_0_SolveDP_GT1(x1, x2, x3)
Cond_11556_0_SolveDP_GT(x1, x2, x3, x4, x5, x6) → Cond_11556_0_SolveDP_GT(x1, x2, x3, x4, x5)
Filtered duplicate args:
11556_0_SolveDP_GT(x1, x2, x3, x4) → 11556_0_SolveDP_GT(x1, x2, x4)
Cond_11556_0_SolveDP_GT(x1, x2, x3, x4, x5) → Cond_11556_0_SolveDP_GT(x1, x2, x3, x5)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
11556_0_SolveDP_GT(EOS(STATIC_11556(x0)), x2, x3) → 11556_0_SolveDP_GT(EOS(STATIC_11556(x0)), x2, +(x3, 1)) | &&(&&(&&(&&(>(x3, -1), <=(x3, 12)), >(x2, -1)), <(x2, 8)), >(x0, -(x2, 1)))
11556_0_SolveDP_GT(EOS(STATIC_11556(x0)), x2, 13) → 11556_0_SolveDP_GT(EOS(STATIC_11556(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:
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0)), x2, x3) → COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3, -1), <=(x3, 12)), >(x2, -1)), <(x2, 8)), >(x0, -(x2, 1))), EOS(STATIC_11556(x0)), x2, x3)
COND_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0)), x2, x3) → 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0)), x2, +(x3, 1))
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0)), x2, 13) → COND_11556_0_SOLVEDP_GT1(>(x0, +(x2, 1)), EOS(STATIC_11556(x0)), x2, 13)
COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0)), x2, 13) → 11556_0_SOLVEDP_GT(EOS(STATIC_11556(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_11556(x0[0])) →* EOS(STATIC_11556(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (0), if (EOS(STATIC_11556(x0[1])) →* EOS(STATIC_11556(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(1) -> (2), if (EOS(STATIC_11556(x0[1])) →* EOS(STATIC_11556(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 13)
(2) -> (3), if (x0[2] > x2[2] + 1 ∧EOS(STATIC_11556(x0[2])) →* EOS(STATIC_11556(x0[3]))∧x2[2] →* x2[3])
(3) -> (0), if (EOS(STATIC_11556(x0[3])) →* EOS(STATIC_11556(x0[0]))∧x2[3] + 1 →* x2[0]∧0 →* x3[0])
(3) -> (2), if (EOS(STATIC_11556(x0[3])) →* EOS(STATIC_11556(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_11556(x0[0]))=EOS(STATIC_11556(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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 ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [(-1)bni_13]x2[0] ≥ 0∧[(-1)bso_14] ≥ 0)
(7) (COND_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0[1])), x2[1], x3[1])≥NonInfC∧COND_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0[1])), x2[1], x3[1])≥11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥))
(8) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧[(-1)bso_16] ≥ 0)
(9) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧[(-1)bso_16] ≥ 0)
(10) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_15] = 0∧[(-1)bso_16] ≥ 0)
(11) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(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_11556(x0[2]))=EOS(STATIC_11556(x0[3]))∧x2[2]=x2[3] ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)∧(UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥))
(13) (>(x0[2], +(x2[2], 1))=TRUE ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)∧(UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥))
(14) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(15) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(16) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(17) (x0[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(18) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [bni_17]x2[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(19) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_17 + (-1)Bound*bni_17] + [(-1)bni_17]x2[2] ≥ 0∧[(-1)bso_18] ≥ 0)
(20) (COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0[3])), x2[3], 13)≥NonInfC∧COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0[3])), x2[3], 13)≥11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)∧(UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥))
(21) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(22) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(23) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(24) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(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(11556_0_SOLVEDP_GT(x1, x2, x3)) = [-1] + [-1]x2
POL(EOS(x1)) = x1
POL(STATIC_11556(x1)) = x1
POL(COND_11556_0_SOLVEDP_GT(x1, x2, x3, x4)) = [-1] + [-1]x3
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_11556_0_SOLVEDP_GT1(x1, x2, x3, x4)) = [-1] + [-1]x3
POL(0) = 0
COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0[3])), x2[3], 13) → 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0]) → COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0]) → COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])
COND_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0[1])), x2[1], x3[1]) → 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13) → COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(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_11556(x0[1])) →* EOS(STATIC_11556(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_11556(x0[0])) →* EOS(STATIC_11556(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (2), if (EOS(STATIC_11556(x0[1])) →* EOS(STATIC_11556(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_11556(x0[1])) →* EOS(STATIC_11556(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_11556(x0[0])) →* EOS(STATIC_11556(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) (COND_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0[1])), x2[1], x3[1])≥NonInfC∧COND_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0[1])), x2[1], x3[1])≥11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥))
(2) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧[1 + (-1)bso_12] ≥ 0)
(3) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧[1 + (-1)bso_12] ≥ 0)
(4) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[bni_11] = 0∧[1 + (-1)bso_12] ≥ 0)
(5) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(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_11556(x0[0]))=EOS(STATIC_11556(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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 ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0])≥COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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_11556_0_SOLVEDP_GT(x1, x2, x3, x4)) = [-1] + [-1]x3 + [2]x2 + [-1]x4
POL(EOS(x1)) = x1
POL(STATIC_11556(x1)) = x1
POL(11556_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_11556_0_SOLVEDP_GT(TRUE, EOS(STATIC_11556(x0[1])), x2[1], x3[1]) → 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[1])), x2[1], +(x3[1], 1))
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0]) → COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(x0[0])), x2[0], x3[0])
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[0])), x2[0], x3[0]) → COND_11556_0_SOLVEDP_GT(&&(&&(&&(&&(>(x3[0], -1), <=(x3[0], 12)), >(x2[0], -1)), <(x2[0], 8)), >(x0[0], -(x2[0], 1))), EOS(STATIC_11556(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
(1) -> (2), if (EOS(STATIC_11556(x0[1])) →* EOS(STATIC_11556(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 13)
(3) -> (2), if (EOS(STATIC_11556(x0[3])) →* EOS(STATIC_11556(x0[2]))∧x2[3] + 1 →* x2[2]∧0 →* 13)
(2) -> (3), if (x0[2] > x2[2] + 1 ∧EOS(STATIC_11556(x0[2])) →* EOS(STATIC_11556(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
(3) -> (2), if (EOS(STATIC_11556(x0[3])) →* EOS(STATIC_11556(x0[2]))∧x2[3] + 1 →* x2[2]∧0 →* 13)
(2) -> (3), if (x0[2] > x2[2] + 1 ∧EOS(STATIC_11556(x0[2])) →* EOS(STATIC_11556(x0[3]))∧x2[2] →* x2[3])
(1) (COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0[3])), x2[3], 13)≥NonInfC∧COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0[3])), x2[3], 13)≥11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)∧(UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥))
(2) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_7] = 0∧[1 + (-1)bso_8] ≥ 0)
(3) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_7] = 0∧[1 + (-1)bso_8] ≥ 0)
(4) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_7] = 0∧[1 + (-1)bso_8] ≥ 0)
(5) ((UIncreasing(11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)), ≥)∧[bni_7] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_8] ≥ 0)
(6) (>(x0[2], +(x2[2], 1))=TRUE∧EOS(STATIC_11556(x0[2]))=EOS(STATIC_11556(x0[3]))∧x2[2]=x2[3] ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)∧(UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥))
(7) (>(x0[2], +(x2[2], 1))=TRUE ⇒ 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥NonInfC∧11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13)≥COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)∧(UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥))
(8) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_9 + (-1)Bound*bni_9] + [(-1)bni_9]x2[2] + [bni_9]x0[2] ≥ 0∧[(-1)bso_10] ≥ 0)
(9) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_9 + (-1)Bound*bni_9] + [(-1)bni_9]x2[2] + [bni_9]x0[2] ≥ 0∧[(-1)bso_10] ≥ 0)
(10) (x0[2] + [-2] + [-1]x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_9 + (-1)Bound*bni_9] + [(-1)bni_9]x2[2] + [bni_9]x0[2] ≥ 0∧[(-1)bso_10] ≥ 0)
(11) (x0[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[(-1)bso_10] ≥ 0)
(12) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[(-1)bso_10] ≥ 0)
(13) (x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)), ≥)∧[bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[(-1)bso_10] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_11556_0_SOLVEDP_GT1(x1, x2, x3, x4)) = [-1] + x2 + [-1]x3
POL(EOS(x1)) = x1
POL(STATIC_11556(x1)) = x1
POL(13) = [13]
POL(11556_0_SOLVEDP_GT(x1, x2, x3)) = [-1] + [-1]x2 + x1
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(0) = 0
POL(>(x1, x2)) = [1]
COND_11556_0_SOLVEDP_GT1(TRUE, EOS(STATIC_11556(x0[3])), x2[3], 13) → 11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[3])), +(x2[3], 1), 0)
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13) → COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(x0[2])), x2[2], 13)
11556_0_SOLVEDP_GT(EOS(STATIC_11556(x0[2])), x2[2], 13) → COND_11556_0_SOLVEDP_GT1(>(x0[2], +(x2[2], 1)), EOS(STATIC_11556(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 |
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:
752_0_SolveDP_FieldAccess(EOS(STATIC_752(matching1)), i72, i72) → 755_0_SolveDP_GT(EOS(STATIC_755(12)), i72, i72, 12) | =(matching1, 12)
755_0_SolveDP_GT(EOS(STATIC_755(matching1)), i80, i80, matching2) → 756_0_SolveDP_GT(EOS(STATIC_756(12)), i80, i80, 12) | &&(=(matching1, 12), =(matching2, 12))
756_0_SolveDP_GT(EOS(STATIC_756(matching1)), i80, i80, matching2) → 759_0_SolveDP_Load(EOS(STATIC_759(12)), i80) | &&(&&(<=(i80, 12), =(matching1, 12)), =(matching2, 12))
759_0_SolveDP_Load(EOS(STATIC_759(matching1)), i80) → 762_0_SolveDP_FieldAccess(EOS(STATIC_762(12)), i80, i80) | =(matching1, 12)
762_0_SolveDP_FieldAccess(EOS(STATIC_762(matching1)), i80, i80) → 765_0_SolveDP_ConstantStackPush(EOS(STATIC_765(12)), i80, i80, java.lang.Object(ARRAY(8))) | =(matching1, 12)
765_0_SolveDP_ConstantStackPush(EOS(STATIC_765(matching1)), i80, i80, java.lang.Object(ARRAY(matching2))) → 768_0_SolveDP_ArrayAccess(EOS(STATIC_768(12)), i80, i80, java.lang.Object(ARRAY(8)), 0) | &&(=(matching1, 12), =(matching2, 8))
768_0_SolveDP_ArrayAccess(EOS(STATIC_768(matching1)), i80, i80, java.lang.Object(ARRAY(matching2)), matching3) → 772_0_SolveDP_GE(EOS(STATIC_772(12)), i80, i80, 2) | &&(&&(&&(<(0, 8), =(matching1, 12)), =(matching2, 8)), =(matching3, 0))
772_0_SolveDP_GE(EOS(STATIC_772(matching1)), i86, i86, matching2) → 777_0_SolveDP_GE(EOS(STATIC_777(12)), i86, i86, 2) | &&(=(matching1, 12), =(matching2, 2))
772_0_SolveDP_GE(EOS(STATIC_772(matching1)), i87, i87, matching2) → 778_0_SolveDP_GE(EOS(STATIC_778(12)), i87, i87, 2) | &&(=(matching1, 12), =(matching2, 2))
777_0_SolveDP_GE(EOS(STATIC_777(matching1)), i86, i86, matching2) → 784_0_SolveDP_FieldAccess(EOS(STATIC_784(12)), i86) | &&(&&(<(i86, 2), =(matching1, 12)), =(matching2, 2))
784_0_SolveDP_FieldAccess(EOS(STATIC_784(matching1)), i86) → 791_0_SolveDP_ConstantStackPush(EOS(STATIC_791(12)), i86, java.lang.Object(ARRAY(i71))) | =(matching1, 12)
791_0_SolveDP_ConstantStackPush(EOS(STATIC_791(matching1)), i86, java.lang.Object(ARRAY(i71))) → 800_0_SolveDP_ArrayAccess(EOS(STATIC_800(12)), i86, java.lang.Object(ARRAY(i71)), 0) | =(matching1, 12)
800_0_SolveDP_ArrayAccess(EOS(STATIC_800(matching1)), i86, java.lang.Object(ARRAY(i96)), matching2) → 816_0_SolveDP_ArrayAccess(EOS(STATIC_816(12)), i86, java.lang.Object(ARRAY(i96)), 0) | &&(=(matching1, 12), =(matching2, 0))
816_0_SolveDP_ArrayAccess(EOS(STATIC_816(matching1)), i86, java.lang.Object(ARRAY(i96)), matching2) → 825_0_SolveDP_Load(EOS(STATIC_825(12)), i86, o110) | &&(&&(<(0, i96), =(matching1, 12)), =(matching2, 0))
825_0_SolveDP_Load(EOS(STATIC_825(matching1)), i86, o110) → 834_0_SolveDP_ConstantStackPush(EOS(STATIC_834(12)), i86, o110, i86) | =(matching1, 12)
834_0_SolveDP_ConstantStackPush(EOS(STATIC_834(matching1)), i86, o110, i86) → 844_0_SolveDP_ArrayAccess(EOS(STATIC_844(12)), i86, o110, i86, 0) | =(matching1, 12)
844_0_SolveDP_ArrayAccess(EOS(STATIC_844(matching1)), i86, java.lang.Object(o117put), i86, matching2) → 850_0_SolveDP_ArrayAccess(EOS(STATIC_850(12)), i86, java.lang.Object(o117put), i86, 0) | &&(=(matching1, 12), =(matching2, 0))
850_0_SolveDP_ArrayAccess(EOS(STATIC_850(matching1)), i86, java.lang.Object(ARRAY(i100)), i86, matching2) → 860_0_SolveDP_ArrayAccess(EOS(STATIC_860(12)), i86, java.lang.Object(ARRAY(i100)), i86, 0) | &&(&&(>=(i100, 0), =(matching1, 12)), =(matching2, 0))
860_0_SolveDP_ArrayAccess(EOS(STATIC_860(matching1)), i86, java.lang.Object(ARRAY(i100)), i86, matching2) → 871_0_SolveDP_ArrayAccess(EOS(STATIC_871(12)), i86, java.lang.Object(ARRAY(i100)), i86, 0) | &&(=(matching1, 12), =(matching2, 0))
871_0_SolveDP_ArrayAccess(EOS(STATIC_871(matching1)), i86, java.lang.Object(ARRAY(i100)), i86, matching2) → 882_0_SolveDP_JMP(EOS(STATIC_882(12)), i86) | &&(&&(<(i86, i100), =(matching1, 12)), =(matching2, 0))
882_0_SolveDP_JMP(EOS(STATIC_882(matching1)), i86) → 895_0_SolveDP_Inc(EOS(STATIC_895(12)), i86) | =(matching1, 12)
895_0_SolveDP_Inc(EOS(STATIC_895(matching1)), i86) → 910_0_SolveDP_JMP(EOS(STATIC_910(12)), +(i86, 1)) | &&(>=(i86, 0), =(matching1, 12))
910_0_SolveDP_JMP(EOS(STATIC_910(matching1)), i106) → 935_0_SolveDP_Load(EOS(STATIC_935(12)), i106) | =(matching1, 12)
935_0_SolveDP_Load(EOS(STATIC_935(matching1)), i106) → 749_0_SolveDP_Load(EOS(STATIC_749(12)), i106) | =(matching1, 12)
749_0_SolveDP_Load(EOS(STATIC_749(matching1)), i72) → 752_0_SolveDP_FieldAccess(EOS(STATIC_752(12)), i72, i72) | =(matching1, 12)
778_0_SolveDP_GE(EOS(STATIC_778(matching1)), i87, i87, matching2) → 785_0_SolveDP_FieldAccess(EOS(STATIC_785(12)), i87) | &&(&&(>=(i87, 2), =(matching1, 12)), =(matching2, 2))
785_0_SolveDP_FieldAccess(EOS(STATIC_785(matching1)), i87) → 794_0_SolveDP_ConstantStackPush(EOS(STATIC_794(12)), i87, java.lang.Object(ARRAY(i71))) | =(matching1, 12)
794_0_SolveDP_ConstantStackPush(EOS(STATIC_794(matching1)), i87, java.lang.Object(ARRAY(i71))) → 803_0_SolveDP_ArrayAccess(EOS(STATIC_803(12)), i87, java.lang.Object(ARRAY(i71)), 0) | =(matching1, 12)
803_0_SolveDP_ArrayAccess(EOS(STATIC_803(matching1)), i87, java.lang.Object(ARRAY(i98)), matching2) → 818_0_SolveDP_ArrayAccess(EOS(STATIC_818(12)), i87, java.lang.Object(ARRAY(i98)), 0) | &&(=(matching1, 12), =(matching2, 0))
818_0_SolveDP_ArrayAccess(EOS(STATIC_818(matching1)), i87, java.lang.Object(ARRAY(i98)), matching2) → 828_0_SolveDP_Load(EOS(STATIC_828(12)), i87, o112) | &&(&&(<(0, i98), =(matching1, 12)), =(matching2, 0))
828_0_SolveDP_Load(EOS(STATIC_828(matching1)), i87, o112) → 836_0_SolveDP_FieldAccess(EOS(STATIC_836(12)), i87, o112, i87) | =(matching1, 12)
836_0_SolveDP_FieldAccess(EOS(STATIC_836(matching1)), i87, o112, i87) → 846_0_SolveDP_ConstantStackPush(EOS(STATIC_846(12)), i87, o112, i87, java.lang.Object(ARRAY(8))) | =(matching1, 12)
846_0_SolveDP_ConstantStackPush(EOS(STATIC_846(matching1)), i87, o112, i87, java.lang.Object(ARRAY(matching2))) → 855_0_SolveDP_ArrayAccess(EOS(STATIC_855(12)), i87, o112, i87, java.lang.Object(ARRAY(8)), 0) | &&(=(matching1, 12), =(matching2, 8))
855_0_SolveDP_ArrayAccess(EOS(STATIC_855(matching1)), i87, o112, i87, java.lang.Object(ARRAY(matching2)), matching3) → 864_0_SolveDP_ArrayAccess(EOS(STATIC_864(12)), i87, o112, i87) | &&(&&(&&(<(0, 8), =(matching1, 12)), =(matching2, 8)), =(matching3, 0))
864_0_SolveDP_ArrayAccess(EOS(STATIC_864(matching1)), i87, java.lang.Object(o122put), i87) → 875_0_SolveDP_ArrayAccess(EOS(STATIC_875(12)), i87, java.lang.Object(o122put), i87) | =(matching1, 12)
875_0_SolveDP_ArrayAccess(EOS(STATIC_875(matching1)), i87, java.lang.Object(ARRAY(i102)), i87) → 887_0_SolveDP_ArrayAccess(EOS(STATIC_887(12)), i87, java.lang.Object(ARRAY(i102)), i87) | &&(>=(i102, 0), =(matching1, 12))
887_0_SolveDP_ArrayAccess(EOS(STATIC_887(matching1)), i87, java.lang.Object(ARRAY(i102)), i87) → 898_0_SolveDP_ArrayAccess(EOS(STATIC_898(12)), i87, java.lang.Object(ARRAY(i102)), i87) | =(matching1, 12)
898_0_SolveDP_ArrayAccess(EOS(STATIC_898(matching1)), i87, java.lang.Object(ARRAY(i102)), i87) → 920_0_SolveDP_Inc(EOS(STATIC_920(12)), i87) | &&(<(i87, i102), =(matching1, 12))
920_0_SolveDP_Inc(EOS(STATIC_920(matching1)), i87) → 941_0_SolveDP_JMP(EOS(STATIC_941(12)), +(i87, 1)) | &&(>(i87, 0), =(matching1, 12))
941_0_SolveDP_JMP(EOS(STATIC_941(matching1)), i111) → 958_0_SolveDP_Load(EOS(STATIC_958(12)), i111) | =(matching1, 12)
958_0_SolveDP_Load(EOS(STATIC_958(matching1)), i111) → 749_0_SolveDP_Load(EOS(STATIC_749(12)), i111) | =(matching1, 12)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
752_0_SolveDP_FieldAccess(EOS(STATIC_752(12)), x1, x1) → 752_0_SolveDP_FieldAccess(EOS(STATIC_752(12)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), <=(x1, 12)), <(x1, 2))
752_0_SolveDP_FieldAccess(EOS(STATIC_752(12)), x1, x1) → 752_0_SolveDP_FieldAccess(EOS(STATIC_752(12)), +(x1, 1), +(x1, 1)) | &&(>(+(x1, 1), 2), <=(x1, 12))
R rules:
Filtered ground terms:
752_0_SolveDP_FieldAccess(x1, x2, x3) → 752_0_SolveDP_FieldAccess(x2, x3)
STATIC_752(x1) → STATIC_752
EOS(x1) → EOS
Cond_752_0_SolveDP_FieldAccess1(x1, x2, x3, x4) → Cond_752_0_SolveDP_FieldAccess1(x1, x3, x4)
Cond_752_0_SolveDP_FieldAccess(x1, x2, x3, x4) → Cond_752_0_SolveDP_FieldAccess(x1, x3, x4)
Filtered duplicate args:
752_0_SolveDP_FieldAccess(x1, x2) → 752_0_SolveDP_FieldAccess(x2)
Cond_752_0_SolveDP_FieldAccess(x1, x2, x3) → Cond_752_0_SolveDP_FieldAccess(x1, x3)
Cond_752_0_SolveDP_FieldAccess1(x1, x2, x3) → Cond_752_0_SolveDP_FieldAccess1(x1, x3)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
752_0_SolveDP_FieldAccess(x1) → 752_0_SolveDP_FieldAccess(+(x1, 1)) | &&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2))
752_0_SolveDP_FieldAccess(x1) → 752_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:
752_0_SOLVEDP_FIELDACCESS(x1) → COND_752_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2)), x1)
COND_752_0_SOLVEDP_FIELDACCESS(TRUE, x1) → 752_0_SOLVEDP_FIELDACCESS(+(x1, 1))
752_0_SOLVEDP_FIELDACCESS(x1) → COND_752_0_SOLVEDP_FIELDACCESS1(&&(>(x1, 1), <=(x1, 12)), x1)
COND_752_0_SOLVEDP_FIELDACCESS1(TRUE, x1) → 752_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] ⇒ 752_0_SOLVEDP_FIELDACCESS(x1[0])≥NonInfC∧752_0_SOLVEDP_FIELDACCESS(x1[0])≥COND_752_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])∧(UIncreasing(COND_752_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 ⇒ 752_0_SOLVEDP_FIELDACCESS(x1[0])≥NonInfC∧752_0_SOLVEDP_FIELDACCESS(x1[0])≥COND_752_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])∧(UIncreasing(COND_752_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_752_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_752_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_752_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_752_0_SOLVEDP_FIELDACCESS(TRUE, x1[1])≥NonInfC∧COND_752_0_SOLVEDP_FIELDACCESS(TRUE, x1[1])≥752_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))∧(UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥))
(7) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧[1 + (-1)bso_16] ≥ 0)
(8) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧[1 + (-1)bso_16] ≥ 0)
(9) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))), ≥)∧[bni_15] = 0∧[1 + (-1)bso_16] ≥ 0)
(10) ((UIncreasing(752_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] ⇒ 752_0_SOLVEDP_FIELDACCESS(x1[2])≥NonInfC∧752_0_SOLVEDP_FIELDACCESS(x1[2])≥COND_752_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])∧(UIncreasing(COND_752_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥))
(12) (>(x1[2], 1)=TRUE∧<=(x1[2], 12)=TRUE ⇒ 752_0_SOLVEDP_FIELDACCESS(x1[2])≥NonInfC∧752_0_SOLVEDP_FIELDACCESS(x1[2])≥COND_752_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])∧(UIncreasing(COND_752_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])), ≥))
(13) (x1[2] + [-2] ≥ 0∧[12] + [-1]x1[2] ≥ 0 ⇒ (UIncreasing(COND_752_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_752_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_752_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_752_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_752_0_SOLVEDP_FIELDACCESS1(TRUE, x1[3])≥NonInfC∧COND_752_0_SOLVEDP_FIELDACCESS1(TRUE, x1[3])≥752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))∧(UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥))
(18) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(19) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(20) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧[1 + (-1)bso_20] ≥ 0)
(21) ((UIncreasing(752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))), ≥)∧[bni_19] = 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(752_0_SOLVEDP_FIELDACCESS(x1)) = [-1] + [-1]x1
POL(COND_752_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_752_0_SOLVEDP_FIELDACCESS1(x1, x2)) = [-1] + [-1]x2
COND_752_0_SOLVEDP_FIELDACCESS(TRUE, x1[1]) → 752_0_SOLVEDP_FIELDACCESS(+(x1[1], 1))
COND_752_0_SOLVEDP_FIELDACCESS1(TRUE, x1[3]) → 752_0_SOLVEDP_FIELDACCESS(+(x1[3], 1))
752_0_SOLVEDP_FIELDACCESS(x1[0]) → COND_752_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])
752_0_SOLVEDP_FIELDACCESS(x1[2]) → COND_752_0_SOLVEDP_FIELDACCESS1(&&(>(x1[2], 1), <=(x1[2], 12)), x1[2])
752_0_SOLVEDP_FIELDACCESS(x1[0]) → COND_752_0_SOLVEDP_FIELDACCESS(&&(&&(>(x1[0], -1), <=(x1[0], 12)), <(x1[0], 2)), x1[0])
752_0_SOLVEDP_FIELDACCESS(x1[2]) → COND_752_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:
6579_0_InterpretArray_ConstantStackPush(EOS(STATIC_6579), i2277, i2279, i2277) → 6599_0_InterpretArray_LT(EOS(STATIC_6599), i2277, i2279, i2277, 1)
6599_0_InterpretArray_LT(EOS(STATIC_6599), i2357, i2279, i2357, matching1) → 6619_0_InterpretArray_LT(EOS(STATIC_6619), i2357, i2279, i2357, 1) | =(matching1, 1)
6619_0_InterpretArray_LT(EOS(STATIC_6619), i2357, i2279, i2357, matching1) → 6643_0_InterpretArray_FieldAccess(EOS(STATIC_6643), i2357, i2279) | &&(>=(i2357, 1), =(matching1, 1))
6643_0_InterpretArray_FieldAccess(EOS(STATIC_6643), i2357, i2279) → 6668_0_InterpretArray_Load(EOS(STATIC_6668), i2357, i2279, java.lang.Object(ARRAY(i583)))
6668_0_InterpretArray_Load(EOS(STATIC_6668), i2357, i2279, java.lang.Object(ARRAY(i583))) → 6676_0_InterpretArray_ArrayAccess(EOS(STATIC_6676), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357)
6676_0_InterpretArray_ArrayAccess(EOS(STATIC_6676), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357) → 6681_0_InterpretArray_ArrayAccess(EOS(STATIC_6681), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357)
6681_0_InterpretArray_ArrayAccess(EOS(STATIC_6681), i2357, i2279, java.lang.Object(ARRAY(i583)), i2357) → 6687_0_InterpretArray_Load(EOS(STATIC_6687), i2357, i2279, o5336) | <(i2357, i583)
6687_0_InterpretArray_Load(EOS(STATIC_6687), i2357, i2279, o5336) → 6692_0_InterpretArray_ArrayAccess(EOS(STATIC_6692), i2357, i2279, o5336, i2279)
6692_0_InterpretArray_ArrayAccess(EOS(STATIC_6692), i2357, i2279, java.lang.Object(o5341put), i2279) → 6698_0_InterpretArray_ArrayAccess(EOS(STATIC_6698), i2357, i2279, java.lang.Object(o5341put), i2279)
6698_0_InterpretArray_ArrayAccess(EOS(STATIC_6698), i2357, i2279, java.lang.Object(ARRAY(i2415)), i2279) → 6707_0_InterpretArray_ArrayAccess(EOS(STATIC_6707), i2357, i2279, java.lang.Object(ARRAY(i2415)), i2279) | >=(i2415, 0)
6707_0_InterpretArray_ArrayAccess(EOS(STATIC_6707), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419) → 6717_0_InterpretArray_ArrayAccess(EOS(STATIC_6717), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419)
6717_0_InterpretArray_ArrayAccess(EOS(STATIC_6717), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419) → 6726_0_InterpretArray_ArrayAccess(EOS(STATIC_6726), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419)
6726_0_InterpretArray_ArrayAccess(EOS(STATIC_6726), i2357, i2419, java.lang.Object(ARRAY(i2415)), i2419) → 6736_0_InterpretArray_FieldAccess(EOS(STATIC_6736), i2357, i2419, i2427) | <(i2419, i2415)
6736_0_InterpretArray_FieldAccess(EOS(STATIC_6736), i2357, i2419, i2427) → 6749_0_InterpretArray_Load(EOS(STATIC_6749), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)))
6749_0_InterpretArray_Load(EOS(STATIC_6749), i2357, i2419, i2427, java.lang.Object(ARRAY(i583))) → 6762_0_InterpretArray_ConstantStackPush(EOS(STATIC_6762), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357)
6762_0_InterpretArray_ConstantStackPush(EOS(STATIC_6762), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357) → 6775_0_InterpretArray_IntArithmetic(EOS(STATIC_6775), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357, 1)
6775_0_InterpretArray_IntArithmetic(EOS(STATIC_6775), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2357, matching1) → 6788_0_InterpretArray_ArrayAccess(EOS(STATIC_6788), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), -(i2357, 1)) | &&(>(i2357, 0), =(matching1, 1))
6788_0_InterpretArray_ArrayAccess(EOS(STATIC_6788), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2442) → 6801_0_InterpretArray_ArrayAccess(EOS(STATIC_6801), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2442)
6801_0_InterpretArray_ArrayAccess(EOS(STATIC_6801), i2357, i2419, i2427, java.lang.Object(ARRAY(i583)), i2442) → 6817_0_InterpretArray_Load(EOS(STATIC_6817), i2357, i2419, i2427, o5406) | <(i2442, i583)
6817_0_InterpretArray_Load(EOS(STATIC_6817), i2357, i2419, i2427, o5406) → 6832_0_InterpretArray_ArrayAccess(EOS(STATIC_6832), i2357, i2419, i2427, o5406, i2419)
6832_0_InterpretArray_ArrayAccess(EOS(STATIC_6832), i2357, i2419, i2427, java.lang.Object(o5444put), i2419) → 6848_0_InterpretArray_ArrayAccess(EOS(STATIC_6848), i2357, i2419, i2427, java.lang.Object(o5444put), i2419)
6848_0_InterpretArray_ArrayAccess(EOS(STATIC_6848), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) → 6868_0_InterpretArray_ArrayAccess(EOS(STATIC_6868), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) | >=(i2469, 0)
6868_0_InterpretArray_ArrayAccess(EOS(STATIC_6868), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) → 6886_0_InterpretArray_ArrayAccess(EOS(STATIC_6886), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419)
6886_0_InterpretArray_ArrayAccess(EOS(STATIC_6886), i2357, i2419, i2427, java.lang.Object(ARRAY(i2469)), i2419) → 6909_0_InterpretArray_EQ(EOS(STATIC_6909), i2357, i2419, i2427, i2489) | <(i2419, i2469)
6909_0_InterpretArray_EQ(EOS(STATIC_6909), i2357, i2419, i2489, i2489) → 6933_0_InterpretArray_EQ(EOS(STATIC_6933), i2357, i2419, i2489, i2489)
6909_0_InterpretArray_EQ(EOS(STATIC_6909), i2357, i2419, i2427, i2489) → 6934_0_InterpretArray_EQ(EOS(STATIC_6934), i2357, i2419, i2427, i2489)
6933_0_InterpretArray_EQ(EOS(STATIC_6933), i2357, i2419, i2489, i2489) → 6955_0_InterpretArray_Inc(EOS(STATIC_6955), i2357, i2419)
6955_0_InterpretArray_Inc(EOS(STATIC_6955), i2357, i2419) → 6980_0_InterpretArray_JMP(EOS(STATIC_6980), +(i2357, -1), i2419) | >(i2357, 0)
6980_0_InterpretArray_JMP(EOS(STATIC_6980), i2529, i2419) → 7013_0_InterpretArray_Load(EOS(STATIC_7013), i2529, i2419)
7013_0_InterpretArray_Load(EOS(STATIC_7013), i2529, i2419) → 6558_0_InterpretArray_Load(EOS(STATIC_6558), i2529, i2419)
6558_0_InterpretArray_Load(EOS(STATIC_6558), i2277, i2279) → 6579_0_InterpretArray_ConstantStackPush(EOS(STATIC_6579), i2277, i2279, i2277)
6934_0_InterpretArray_EQ(EOS(STATIC_6934), i2357, i2419, i2427, i2489) → 6956_0_InterpretArray_Load(EOS(STATIC_6956), i2357, i2419) | !(=(i2427, i2489))
6956_0_InterpretArray_Load(EOS(STATIC_6956), i2357, i2419) → 6982_0_InterpretArray_FieldAccess(EOS(STATIC_6982), i2357, i2419)
6982_0_InterpretArray_FieldAccess(EOS(STATIC_6982), i2357, i2419) → 7014_0_InterpretArray_Load(EOS(STATIC_7014), i2357, i2419, java.lang.Object(ARRAY(8)))
7014_0_InterpretArray_Load(EOS(STATIC_7014), i2357, i2419, java.lang.Object(ARRAY(matching1))) → 7040_0_InterpretArray_ArrayAccess(EOS(STATIC_7040), i2357, i2419, java.lang.Object(ARRAY(8)), i2357) | =(matching1, 8)
7040_0_InterpretArray_ArrayAccess(EOS(STATIC_7040), i2597, i2419, java.lang.Object(ARRAY(matching1)), i2597) → 7070_0_InterpretArray_ArrayAccess(EOS(STATIC_7070), i2597, i2419, java.lang.Object(ARRAY(8)), i2597) | =(matching1, 8)
7070_0_InterpretArray_ArrayAccess(EOS(STATIC_7070), i2597, i2419, java.lang.Object(ARRAY(matching1)), i2597) → 7101_0_InterpretArray_IntArithmetic(EOS(STATIC_7101), i2597, i2419, i2623) | &&(<(i2597, 8), =(matching1, 8))
7101_0_InterpretArray_IntArithmetic(EOS(STATIC_7101), i2597, i2419, i2623) → 7130_0_InterpretArray_Store(EOS(STATIC_7130), i2597, -(i2419, i2623)) | >=(i2419, 0)
7130_0_InterpretArray_Store(EOS(STATIC_7130), i2597, i2642) → 7164_0_InterpretArray_Load(EOS(STATIC_7164), i2597, i2642)
7164_0_InterpretArray_Load(EOS(STATIC_7164), i2597, i2642) → 7201_0_InterpretArray_FieldAccess(EOS(STATIC_7201), i2597, i2642)
7201_0_InterpretArray_FieldAccess(EOS(STATIC_7201), i2597, i2642) → 7236_0_InterpretArray_Load(EOS(STATIC_7236), i2597, i2642, java.lang.Object(ARRAY(8)))
7236_0_InterpretArray_Load(EOS(STATIC_7236), i2597, i2642, java.lang.Object(ARRAY(matching1))) → 7272_0_InterpretArray_ArrayAccess(EOS(STATIC_7272), i2597, i2642, java.lang.Object(ARRAY(8)), i2597) | =(matching1, 8)
7272_0_InterpretArray_ArrayAccess(EOS(STATIC_7272), i2597, i2642, java.lang.Object(ARRAY(matching1)), i2597) → 7307_0_InterpretArray_IntArithmetic(EOS(STATIC_7307), i2597, i2642) | &&(<(i2597, 8), =(matching1, 8))
7307_0_InterpretArray_IntArithmetic(EOS(STATIC_7307), i2597, i2642) → 7325_0_InterpretArray_Store(EOS(STATIC_7325), i2597, i2642)
7325_0_InterpretArray_Store(EOS(STATIC_7325), i2597, i2642) → 7344_0_InterpretArray_Inc(EOS(STATIC_7344), i2597, i2642)
7344_0_InterpretArray_Inc(EOS(STATIC_7344), i2597, i2642) → 7362_0_InterpretArray_JMP(EOS(STATIC_7362), +(i2597, -1), i2642) | >(i2597, 0)
7362_0_InterpretArray_JMP(EOS(STATIC_7362), i2899, i2642) → 7378_0_InterpretArray_Load(EOS(STATIC_7378), i2899, i2642)
7378_0_InterpretArray_Load(EOS(STATIC_7378), i2899, i2642) → 6558_0_InterpretArray_Load(EOS(STATIC_6558), i2899, i2642)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
6579_0_InterpretArray_ConstantStackPush(EOS(STATIC_6579), x0, x1, x0) → 6579_0_InterpretArray_ConstantStackPush(EOS(STATIC_6579), +(x0, -1), x1, +(x0, -1)) | >(+(x0, 1), 1)
6579_0_InterpretArray_ConstantStackPush(EOS(STATIC_6579), x0, x1, x0) → 6579_0_InterpretArray_ConstantStackPush(EOS(STATIC_6579), +(x0, -1), -(x1, x2), +(x0, -1)) | &&(&&(>(+(x1, 1), 0), >(+(x0, 1), 1)), <(x0, 8))
R rules:
Filtered ground terms:
6579_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4) → 6579_0_InterpretArray_ConstantStackPush(x2, x3, x4)
EOS(x1) → EOS
Cond_6579_0_InterpretArray_ConstantStackPush1(x1, x2, x3, x4, x5, x6) → Cond_6579_0_InterpretArray_ConstantStackPush1(x1, x3, x4, x5, x6)
Cond_6579_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_6579_0_InterpretArray_ConstantStackPush(x1, x3, x4, x5)
Filtered duplicate args:
6579_0_InterpretArray_ConstantStackPush(x1, x2, x3) → 6579_0_InterpretArray_ConstantStackPush(x2, x3)
Cond_6579_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4) → Cond_6579_0_InterpretArray_ConstantStackPush(x1, x3, x4)
Cond_6579_0_InterpretArray_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_6579_0_InterpretArray_ConstantStackPush1(x1, x3, x4, x5)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
6579_0_InterpretArray_ConstantStackPush(x1, x0) → 6579_0_InterpretArray_ConstantStackPush(x1, +(x0, -1)) | >(x0, 0)
6579_0_InterpretArray_ConstantStackPush(x1, x0) → 6579_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:
6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x0) → COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0, 0), x1, x0)
COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1, x0) → 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, +(x0, -1))
6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x0) → COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1, -1), >(x0, 0)), <(x0, 8)), x1, x0, x2)
COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1, x0, x2) → 6579_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] ⇒ 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥NonInfC∧6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])∧(UIncreasing(COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥NonInfC∧6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0])≥COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])∧(UIncreasing(COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_6579_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_6579_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_6579_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_6579_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_6579_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_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(9) (>(x0[0], 0)=TRUE ⇒ COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], +(x0[0], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(10) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6579_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(6579_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(6579_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(6579_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(6579_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_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(16) (>(x0[0], 0)=TRUE ⇒ COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[0], x0[0])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], +(x0[0], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))), ≥))
(17) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(6579_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(6579_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(6579_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(6579_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(6579_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] ⇒ 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥NonInfC∧6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])∧(UIncreasing(COND_6579_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 ⇒ 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], +(x0[1], -1))≥NonInfC∧6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], +(x0[1], -1))≥COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(+(x0[1], -1), 0)), <(+(x0[1], -1), 8)), x1[2], +(x0[1], -1), x2[2])∧(UIncreasing(COND_6579_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_6579_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_6579_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_6579_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_6579_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_6579_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 ⇒ 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥NonInfC∧6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2])≥COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])∧(UIncreasing(COND_6579_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 ⇒ 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))≥NonInfC∧6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))≥COND_6579_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_6579_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_6579_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_6579_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_6579_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_6579_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_6579_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_6579_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_6579_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_6579_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_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(40) (<(x0[2], 8)=TRUE∧>(x1[2], -1)=TRUE∧>(x0[2], 0)=TRUE ⇒ COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[2], x2[2]), +(x0[2], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(41) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(42) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(43) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(44) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_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 + (-1)bso_25] ≥ 0)
(45) ([6] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧0 = 0∧[1 + (-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_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(47) (<(x0[2], 8)=TRUE∧>(x1[2], -1)=TRUE∧>(x0[2], 0)=TRUE ⇒ COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥NonInfC∧COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[2], x0[2], x2[2])≥6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[2], x2[2]), +(x0[2], -1))∧(UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥))
(48) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(49) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(50) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧[1 + (-1)bso_25] ≥ 0)
(51) ([7] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(6579_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 + (-1)bso_25] ≥ 0)
(52) ([6] + [-1]x0[2] ≥ 0∧x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (UIncreasing(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))), ≥)∧0 = 0∧[(-1)Bound*bni_24] + [bni_24]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1, x2)) = [-1] + x2
POL(COND_6579_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_6579_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_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1]) → 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))
COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3]) → 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))
6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0]) → COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])
COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(TRUE, x1[1], x0[1]) → 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[1], +(x0[1], -1))
6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2]) → COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(&&(&&(>(x1[2], -1), >(x0[2], 0)), <(x0[2], 8)), x1[2], x0[2], x2[2])
COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH1(TRUE, x1[3], x0[3], x2[3]) → 6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(-(x1[3], x2[3]), +(x0[3], -1))
6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[0], x0[0]) → COND_6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(>(x0[0], 0), x1[0], x0[0])
6579_0_INTERPRETARRAY_CONSTANTSTACKPUSH(x1[2], x0[2]) → COND_6579_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 |
Integer, Boolean
Generated 31 rules for P and 0 rules for R.
P rules:
5673_0_Display_FieldAccess(EOS(STATIC_5673(i583, matching1)), i1757, i1757) → 5676_0_Display_GE(EOS(STATIC_5676(i583, 12)), i1757, i1757, i583) | =(matching1, 12)
5676_0_Display_GE(EOS(STATIC_5676(i583, matching1)), i1757, i1757, i583) → 5679_0_Display_GE(EOS(STATIC_5679(i583, 12)), i1757, i1757, i583) | =(matching1, 12)
5679_0_Display_GE(EOS(STATIC_5679(i583, matching1)), i1757, i1757, i583) → 5683_0_Display_ConstantStackPush(EOS(STATIC_5683(i583, 12)), i1757) | &&(<(i1757, i583), =(matching1, 12))
5683_0_Display_ConstantStackPush(EOS(STATIC_5683(i583, matching1)), i1757) → 5688_0_Display_Store(EOS(STATIC_5688(i583, 12)), i1757, 0) | =(matching1, 12)
5688_0_Display_Store(EOS(STATIC_5688(i583, matching1)), i1757, matching2) → 5692_0_Display_Load(EOS(STATIC_5692(i583, 12)), i1757, 0) | &&(=(matching1, 12), =(matching2, 0))
5692_0_Display_Load(EOS(STATIC_5692(i583, matching1)), i1757, matching2) → 5745_0_Display_Load(EOS(STATIC_5745(i583, 12)), i1757, 0) | &&(=(matching1, 12), =(matching2, 0))
5745_0_Display_Load(EOS(STATIC_5745(i583, matching1)), i1757, i1782) → 5848_0_Display_Load(EOS(STATIC_5848(i583, 12)), i1757, i1782) | =(matching1, 12)
5848_0_Display_Load(EOS(STATIC_5848(i583, matching1)), i1757, i1853) → 6033_0_Display_Load(EOS(STATIC_6033(i583, 12)), i1757, i1853) | =(matching1, 12)
6033_0_Display_Load(EOS(STATIC_6033(i583, matching1)), i1757, i2000) → 6132_0_Display_Load(EOS(STATIC_6132(i583, 12)), i1757, i2000) | =(matching1, 12)
6132_0_Display_Load(EOS(STATIC_6132(i583, matching1)), i1757, i2030) → 6152_0_Display_FieldAccess(EOS(STATIC_6152(i583, 12)), i1757, i2030, i2030) | =(matching1, 12)
6152_0_Display_FieldAccess(EOS(STATIC_6152(i583, matching1)), i1757, i2030, i2030) → 6171_0_Display_GT(EOS(STATIC_6171(i583, 12)), i1757, i2030, i2030, 12) | =(matching1, 12)
6171_0_Display_GT(EOS(STATIC_6171(i583, matching1)), i1757, i2051, i2051, matching2) → 6189_0_Display_GT(EOS(STATIC_6189(i583, 12)), i1757, i2051, i2051, 12) | &&(=(matching1, 12), =(matching2, 12))
6171_0_Display_GT(EOS(STATIC_6171(i583, matching1)), i1757, matching2, matching3, matching4) → 6190_0_Display_GT(EOS(STATIC_6190(i583, 12)), i1757, 13, 13, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
6189_0_Display_GT(EOS(STATIC_6189(i583, matching1)), i1757, i2051, i2051, matching2) → 6213_0_Display_Load(EOS(STATIC_6213(i583, 12)), i1757, i2051) | &&(&&(<=(i2051, 12), =(matching1, 12)), =(matching2, 12))
6213_0_Display_Load(EOS(STATIC_6213(i583, matching1)), i1757, i2051) → 6238_0_Display_FieldAccess(EOS(STATIC_6238(i583, 12)), i1757, i2051, i2051) | =(matching1, 12)
6238_0_Display_FieldAccess(EOS(STATIC_6238(i583, matching1)), i1757, i2051, i2051) → 6259_0_Display_EQ(EOS(STATIC_6259(i583, 12)), i1757, i2051, i2051, 12) | =(matching1, 12)
6259_0_Display_EQ(EOS(STATIC_6259(i583, matching1)), i1757, i2104, i2104, matching2) → 6285_0_Display_EQ(EOS(STATIC_6285(i583, 12)), i1757, i2104, i2104, 12) | &&(=(matching1, 12), =(matching2, 12))
6259_0_Display_EQ(EOS(STATIC_6259(i583, matching1)), i1757, matching2, matching3, matching4) → 6286_0_Display_EQ(EOS(STATIC_6286(i583, 12)), i1757, 12, 12, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 12)), =(matching3, 12)), =(matching4, 12))
6285_0_Display_EQ(EOS(STATIC_6285(i583, matching1)), i1757, i2104, i2104, matching2) → 6310_0_Display_Inc(EOS(STATIC_6310(i583, 12)), i1757, i2104) | &&(&&(!(=(i2104, 12)), =(matching1, 12)), =(matching2, 12))
6310_0_Display_Inc(EOS(STATIC_6310(i583, matching1)), i1757, i2104) → 6331_0_Display_JMP(EOS(STATIC_6331(i583, 12)), i1757, +(i2104, 1)) | &&(>=(i2104, 0), =(matching1, 12))
6331_0_Display_JMP(EOS(STATIC_6331(i583, matching1)), i1757, i2125) → 6360_0_Display_Load(EOS(STATIC_6360(i583, 12)), i1757, i2125) | =(matching1, 12)
6360_0_Display_Load(EOS(STATIC_6360(i583, matching1)), i1757, i2125) → 6132_0_Display_Load(EOS(STATIC_6132(i583, 12)), i1757, i2125) | =(matching1, 12)
6286_0_Display_EQ(EOS(STATIC_6286(i583, matching1)), i1757, matching2, matching3, matching4) → 6311_0_Display_Inc(EOS(STATIC_6311(i583, 12)), i1757, 12) | &&(&&(&&(=(matching1, 12), =(matching2, 12)), =(matching3, 12)), =(matching4, 12))
6311_0_Display_Inc(EOS(STATIC_6311(i583, matching1)), i1757, matching2) → 6333_0_Display_JMP(EOS(STATIC_6333(i583, 12)), i1757, 13) | &&(=(matching1, 12), =(matching2, 12))
6333_0_Display_JMP(EOS(STATIC_6333(i583, matching1)), i1757, matching2) → 6361_0_Display_Load(EOS(STATIC_6361(i583, 12)), i1757, 13) | &&(=(matching1, 12), =(matching2, 13))
6361_0_Display_Load(EOS(STATIC_6361(i583, matching1)), i1757, matching2) → 6132_0_Display_Load(EOS(STATIC_6132(i583, 12)), i1757, 13) | &&(=(matching1, 12), =(matching2, 13))
6190_0_Display_GT(EOS(STATIC_6190(i583, matching1)), i1757, matching2, matching3, matching4) → 6214_0_Display_Inc(EOS(STATIC_6214(i583, 12)), i1757) | &&(&&(&&(=(matching1, 12), =(matching2, 13)), =(matching3, 13)), =(matching4, 12))
6214_0_Display_Inc(EOS(STATIC_6214(i583, matching1)), i1757) → 6239_0_Display_JMP(EOS(STATIC_6239(i583, 12)), +(i1757, 1)) | &&(>=(i1757, 0), =(matching1, 12))
6239_0_Display_JMP(EOS(STATIC_6239(i583, matching1)), i2072) → 6261_0_Display_Load(EOS(STATIC_6261(i583, 12)), i2072) | =(matching1, 12)
6261_0_Display_Load(EOS(STATIC_6261(i583, matching1)), i2072) → 5668_0_Display_Load(EOS(STATIC_5668(i583, 12)), i2072) | =(matching1, 12)
5668_0_Display_Load(EOS(STATIC_5668(i583, matching1)), i1757) → 5673_0_Display_FieldAccess(EOS(STATIC_5673(i583, 12)), i1757, i1757) | =(matching1, 12)
R rules:
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
6171_0_Display_GT(EOS(STATIC_6171(x0, 12)), x2, x3, x3, 12) → 6171_0_Display_GT(EOS(STATIC_6171(x0, 12)), x2, +(x3, 1), +(x3, 1), 12) | &&(>(+(x3, 1), 0), <(x3, 12))
6171_0_Display_GT(EOS(STATIC_6171(x0, 12)), x2, 12, 12, 12) → 6171_0_Display_GT(EOS(STATIC_6171(x0, 12)), x2, 13, 13, 12)
6171_0_Display_GT(EOS(STATIC_6171(x0, 12)), x2, 13, 13, 12) → 6171_0_Display_GT(EOS(STATIC_6171(x0, 12)), +(x2, 1), 0, 0, 12) | &&(>(+(x2, 1), 0), >(x0, +(x2, 1)))
R rules:
Filtered ground terms:
6171_0_Display_GT(x1, x2, x3, x4, x5) → 6171_0_Display_GT(x1, x2, x3, x4)
STATIC_6171(x1, x2) → STATIC_6171(x1)
Cond_6171_0_Display_GT1(x1, x2, x3, x4, x5, x6) → Cond_6171_0_Display_GT1(x1, x2, x3)
Cond_6171_0_Display_GT(x1, x2, x3, x4, x5, x6) → Cond_6171_0_Display_GT(x1, x2, x3, x4, x5)
Filtered duplicate args:
6171_0_Display_GT(x1, x2, x3, x4) → 6171_0_Display_GT(x1, x2, x4)
Cond_6171_0_Display_GT(x1, x2, x3, x4, x5) → Cond_6171_0_Display_GT(x1, x2, x3, x5)
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
6171_0_Display_GT(EOS(STATIC_6171(x0)), x2, x3) → 6171_0_Display_GT(EOS(STATIC_6171(x0)), x2, +(x3, 1)) | &&(>(x3, -1), <(x3, 12))
6171_0_Display_GT(EOS(STATIC_6171(x0)), x2, 12) → 6171_0_Display_GT(EOS(STATIC_6171(x0)), x2, 13)
6171_0_Display_GT(EOS(STATIC_6171(x0)), x2, 13) → 6171_0_Display_GT(EOS(STATIC_6171(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:
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0)), x2, x3) → COND_6171_0_DISPLAY_GT(&&(>(x3, -1), <(x3, 12)), EOS(STATIC_6171(x0)), x2, x3)
COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0)), x2, x3) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0)), x2, +(x3, 1))
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0)), x2, 12) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0)), x2, 13)
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0)), x2, 13) → COND_6171_0_DISPLAY_GT1(&&(>(x2, -1), >(x0, +(x2, 1))), EOS(STATIC_6171(x0)), x2, 13)
COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0)), x2, 13) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(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_6171(x0[0])) →* EOS(STATIC_6171(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (0), if (EOS(STATIC_6171(x0[1])) →* EOS(STATIC_6171(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(1) -> (2), if (EOS(STATIC_6171(x0[1])) →* EOS(STATIC_6171(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 12)
(1) -> (3), if (EOS(STATIC_6171(x0[1])) →* EOS(STATIC_6171(x0[3]))∧x2[1] →* x2[3]∧x3[1] + 1 →* 13)
(2) -> (0), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[0]))∧x2[2] →* x2[0]∧13 →* x3[0])
(2) -> (2), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[2]'))∧x2[2] →* x2[2]'∧13 →* 12)
(2) -> (3), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[3]))∧x2[2] →* x2[3])
(3) -> (4), if (x2[3] > -1 && x0[3] > x2[3] + 1 ∧EOS(STATIC_6171(x0[3])) →* EOS(STATIC_6171(x0[4]))∧x2[3] →* x2[4])
(4) -> (0), if (EOS(STATIC_6171(x0[4])) →* EOS(STATIC_6171(x0[0]))∧x2[4] + 1 →* x2[0]∧0 →* x3[0])
(4) -> (2), if (EOS(STATIC_6171(x0[4])) →* EOS(STATIC_6171(x0[2]))∧x2[4] + 1 →* x2[2]∧0 →* 12)
(4) -> (3), if (EOS(STATIC_6171(x0[4])) →* EOS(STATIC_6171(x0[3]))∧x2[4] + 1 →* x2[3]∧0 →* 13)
(1) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥))
(2) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥))
(3) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥)∧[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_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥)∧[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_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥)∧[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_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[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_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[0]1))∧x2[1]=x2[0]1∧+(x3[1], 1)=x3[0]1 ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(8) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(9) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[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_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12 ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(14) (+(x3[0], 1)=12∧>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(15) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(20) (0 ≥ 0∧[11] ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(21) (0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[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_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[3]))∧x2[1]=x2[3]∧+(x3[1], 1)=13 ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(23) (+(x3[0], 1)=13∧>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(24) (x3[0] + [-12] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
(28) (EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[0]))∧x2[2]=x2[0]∧13=x3[0] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(29) (+(x3[1], 1)=12 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(30) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28] = 0∧[bni_28] = 0∧[bni_28 + (-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
(34) (EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6171(x0[2]1))=EOS(STATIC_6171(x0[0]))∧x2[2]1=x2[0]∧13=x3[0] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)), ≥))
(35) (EOS(STATIC_6171(x0[4]))=EOS(STATIC_6171(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[0]))∧x2[2]=x2[0]∧13=x3[0] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(36) (EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(37) (EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[3]))∧x2[2]=x2[3] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(38) (+(x3[1], 1)=12 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(39) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[(-1)bni_28] = 0∧[bni_28] = 0∧[bni_28 + (-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
(43) (EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6171(x0[2]1))=EOS(STATIC_6171(x0[2]2))∧x2[2]1=x2[2]2 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)), ≥))
(44) (EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6171(x0[2]1))=EOS(STATIC_6171(x0[3]))∧x2[2]1=x2[3] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)), ≥))
(45) (EOS(STATIC_6171(x0[4]))=EOS(STATIC_6171(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(46) (EOS(STATIC_6171(x0[4]))=EOS(STATIC_6171(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[3]))∧x2[2]=x2[3] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(47) (&&(>(x2[3], -1), >(x0[3], +(x2[3], 1)))=TRUE∧EOS(STATIC_6171(x0[3]))=EOS(STATIC_6171(x0[4]))∧x2[3]=x2[4] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), x2[3], 13)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), x2[3], 13)≥COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)∧(UIncreasing(COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)), ≥))
(48) (>(x2[3], -1)=TRUE∧>(x0[3], +(x2[3], 1))=TRUE ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), x2[3], 13)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), x2[3], 13)≥COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)∧(UIncreasing(COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)), ≥))
(49) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)), ≥)∧[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_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)), ≥)∧[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_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)), ≥)∧[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_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)), ≥)∧[(3)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_6171(x0[3]))=EOS(STATIC_6171(x0[4]))∧x2[3]=x2[4]∧EOS(STATIC_6171(x0[4]))=EOS(STATIC_6171(x0[0]))∧+(x2[4], 1)=x2[0]∧0=x3[0] ⇒ COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13)≥NonInfC∧COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥))
(54) (>(x2[3], -1)=TRUE∧>(x0[3], +(x2[3], 1))=TRUE ⇒ COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[3])), x2[3], 13)≥NonInfC∧COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[3])), x2[3], 13)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), +(x2[3], 1), 0)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥))
(55) (x2[3] ≥ 0∧x0[3] + [-2] + [-1]x2[3] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥)∧[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(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥)∧[(3)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_6171(x0[3]))=EOS(STATIC_6171(x0[4]))∧x2[3]=x2[4]∧EOS(STATIC_6171(x0[4]))=EOS(STATIC_6171(x0[2]))∧+(x2[4], 1)=x2[2]∧0=12 ⇒ COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13)≥NonInfC∧COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥))
(60) (&&(>(x2[3], -1), >(x0[3], +(x2[3], 1)))=TRUE∧EOS(STATIC_6171(x0[3]))=EOS(STATIC_6171(x0[4]))∧x2[3]=x2[4]∧EOS(STATIC_6171(x0[4]))=EOS(STATIC_6171(x0[3]1))∧+(x2[4], 1)=x2[3]1∧0=13 ⇒ COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13)≥NonInfC∧COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)), ≥))
POL(TRUE) = 0
POL(FALSE) = 0
POL(6171_0_DISPLAY_GT(x1, x2, x3)) = [-1] + [-1]x2 + [-1]x1
POL(EOS(x1)) = [-1] + x1
POL(STATIC_6171(x1)) = [-1] + [-1]x1
POL(COND_6171_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_6171_0_DISPLAY_GT1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(0) = 0
COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), x2[3], 13) → COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(x0[3])), x2[3], 13)
COND_6171_0_DISPLAY_GT1(TRUE, EOS(STATIC_6171(x0[4])), x2[4], 13) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[4])), +(x2[4], 1), 0)
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0]) → COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])
COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1]) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[3])), x2[3], 13) → COND_6171_0_DISPLAY_GT1(&&(>(x2[3], -1), >(x0[3], +(x2[3], 1))), EOS(STATIC_6171(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_6171(x0[1])) →* EOS(STATIC_6171(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(2) -> (0), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[0]))∧x2[2] →* x2[0]∧13 →* x3[0])
(0) -> (1), if (x3[0] > -1 && x3[0] < 12 ∧EOS(STATIC_6171(x0[0])) →* EOS(STATIC_6171(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (2), if (EOS(STATIC_6171(x0[1])) →* EOS(STATIC_6171(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 12)
(2) -> (2), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[2]'))∧x2[2] →* x2[2]'∧13 →* 12)
(1) -> (3), if (EOS(STATIC_6171(x0[1])) →* EOS(STATIC_6171(x0[3]))∧x2[1] →* x2[3]∧x3[1] + 1 →* 13)
(2) -> (3), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(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_6171(x0[1])) →* EOS(STATIC_6171(x0[0]))∧x2[1] →* x2[0]∧x3[1] + 1 →* x3[0])
(2) -> (0), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[0]))∧x2[2] →* x2[0]∧13 →* x3[0])
(0) -> (1), if (x3[0] > -1 && x3[0] < 12 ∧EOS(STATIC_6171(x0[0])) →* EOS(STATIC_6171(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (2), if (EOS(STATIC_6171(x0[1])) →* EOS(STATIC_6171(x0[2]))∧x2[1] →* x2[2]∧x3[1] + 1 →* 12)
(2) -> (2), if (EOS(STATIC_6171(x0[2])) →* EOS(STATIC_6171(x0[2]'))∧x2[2] →* x2[2]'∧13 →* 12)
(1) (EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[0]))∧x2[2]=x2[0]∧13=x3[0] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(2) (+(x3[1], 1)=12 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(3) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧[1 + (-1)bso_20] ≥ 0)
(4) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧[1 + (-1)bso_20] ≥ 0)
(5) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥)∧[(-13)bni_19 + (-1)Bound*bni_19] ≥ 0∧[1 + (-1)bso_20] ≥ 0)
(6) (x3[1] + [-11] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(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_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6171(x0[2]1))=EOS(STATIC_6171(x0[0]))∧x2[2]1=x2[0]∧13=x3[0] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)), ≥))
(8) (EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12∧EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)), ≥))
(9) (EOS(STATIC_6171(x0[2]))=EOS(STATIC_6171(x0[2]1))∧x2[2]=x2[2]1∧13=12∧EOS(STATIC_6171(x0[2]1))=EOS(STATIC_6171(x0[2]2))∧x2[2]1=x2[2]2 ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 12)≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2]1)), x2[2]1, 13)), ≥))
(10) (&&(>(x3[0], -1), <(x3[0], 12))=TRUE∧EOS(STATIC_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[0]1))∧x2[1]=x2[0]1∧+(x3[1], 1)=x3[0]1 ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(11) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(12) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1]∧EOS(STATIC_6171(x0[1]))=EOS(STATIC_6171(x0[2]))∧x2[1]=x2[2]∧+(x3[1], 1)=12 ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(17) (+(x3[0], 1)=12∧>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], +(x3[0], 1))∧(UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))), ≥))
(18) (x3[0] + [-11] ≥ 0∧x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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(6171_0_DISPLAY_GT(EOS(STATIC_6171(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_6171(x0[0]))=EOS(STATIC_6171(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥))
(26) (>(x3[0], -1)=TRUE∧<(x3[0], 12)=TRUE ⇒ 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥NonInfC∧6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0])≥COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])), ≥))
(27) (x3[0] ≥ 0∧[11] + [-1]x3[0] ≥ 0 ⇒ (UIncreasing(COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(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_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(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_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(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_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(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) = [3]
POL(6171_0_DISPLAY_GT(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x1
POL(EOS(x1)) = [-1] + [-1]x1
POL(STATIC_6171(x1)) = [-1]
POL(12) = [12]
POL(13) = [13]
POL(COND_6171_0_DISPLAY_GT(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x2 + [-1]x1
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<(x1, x2)) = [-1]
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)
COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1]) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 12) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[2])), x2[2], 13)
COND_6171_0_DISPLAY_GT(TRUE, EOS(STATIC_6171(x0[1])), x2[1], x3[1]) → 6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[1])), x2[1], +(x3[1], 1))
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0]) → COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(x0[0])), x2[0], x3[0])
6171_0_DISPLAY_GT(EOS(STATIC_6171(x0[0])), x2[0], x3[0]) → COND_6171_0_DISPLAY_GT(&&(>(x3[0], -1), <(x3[0], 12)), EOS(STATIC_6171(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