(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Test11
public class Test11 {
public static void main(String[] args) {
Random.args = args;

int x = args.length * 100, y = args.length * 200 / 13;

while (x + y > 0) {
if (Random.random() * Random.random() > 9)
x--;
else
y--;
}
}
}

public class Random {
static String[] args;
static int index = 0;

public static int random() {
if (index >= args.length)
return 0;

String string = args[index];
index++;
return string.length();
}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test11.main([Ljava/lang/String;)V: Graph of 360 nodes with 1 SCC.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test11.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 114 rules for P and 0 rules for R.


P rules:
3897_0_main_Load(EOS(STATIC_3897(i1332)), i1333, i443, i1333) → 3899_0_main_IntArithmetic(EOS(STATIC_3899(i1332)), i1333, i443, i1333, i443)
3899_0_main_IntArithmetic(EOS(STATIC_3899(i1332)), i1333, i443, i1333, i443) → 3900_0_main_LE(EOS(STATIC_3900(i1332)), i1333, i443, +(i1333, i443))
3900_0_main_LE(EOS(STATIC_3900(i1332)), i1333, i443, i1343) → 3902_0_main_LE(EOS(STATIC_3902(i1332)), i1333, i443, i1343)
3902_0_main_LE(EOS(STATIC_3902(i1332)), i1333, i443, i1343) → 3905_0_main_InvokeMethod(EOS(STATIC_3905(i1332)), i1333, i443) | >(i1343, 0)
3905_0_main_InvokeMethod(EOS(STATIC_3905(i1332)), i1333, i443) → 3907_0_random_FieldAccess(EOS(STATIC_3907(i1332)), i1333, i443)
3907_0_random_FieldAccess(EOS(STATIC_3907(i1332)), i1333, i443) → 3909_0_random_FieldAccess(EOS(STATIC_3909(i1332)), i1333, i443, i1332)
3909_0_random_FieldAccess(EOS(STATIC_3909(i1332)), i1333, i443, i1332) → 3910_0_random_ArrayLength(EOS(STATIC_3910(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183)))
3910_0_random_ArrayLength(EOS(STATIC_3910(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183))) → 3911_0_random_LT(EOS(STATIC_3911(i1332)), i1333, i443, i1332, i183) | >=(i183, 0)
3911_0_random_LT(EOS(STATIC_3911(i1332)), i1333, i443, i1332, i183) → 3913_0_random_LT(EOS(STATIC_3913(i1332)), i1333, i443, i1332, i183)
3911_0_random_LT(EOS(STATIC_3911(i1332)), i1333, i443, i1332, i183) → 3914_0_random_LT(EOS(STATIC_3914(i1332)), i1333, i443, i1332, i183)
3913_0_random_LT(EOS(STATIC_3913(i1332)), i1333, i443, i1332, i183) → 3915_0_random_FieldAccess(EOS(STATIC_3915(i1332)), i1333, i443) | <(i1332, i183)
3915_0_random_FieldAccess(EOS(STATIC_3915(i1332)), i1333, i443) → 3917_0_random_FieldAccess(EOS(STATIC_3917(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)))
3917_0_random_FieldAccess(EOS(STATIC_3917(i1332)), i1333, i443, java.lang.Object(ARRAY(i183))) → 3920_0_random_ArrayAccess(EOS(STATIC_3920(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)), i1332)
3920_0_random_ArrayAccess(EOS(STATIC_3920(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348) → 3923_0_random_ArrayAccess(EOS(STATIC_3923(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348)
3923_0_random_ArrayAccess(EOS(STATIC_3923(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348) → 3927_0_random_ArrayAccess(EOS(STATIC_3927(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348)
3927_0_random_ArrayAccess(EOS(STATIC_3927(i1348)), i1333, i443, java.lang.Object(ARRAY(i183)), i1348) → 3930_0_random_Store(EOS(STATIC_3930(i1348)), i1333, i443, o2532)
3930_0_random_Store(EOS(STATIC_3930(i1348)), i1333, i443, o2532) → 3935_0_random_FieldAccess(EOS(STATIC_3935(i1348)), i1333, i443, o2532)
3935_0_random_FieldAccess(EOS(STATIC_3935(i1348)), i1333, i443, o2532) → 3939_0_random_ConstantStackPush(EOS(STATIC_3939(i1348)), i1333, i443, o2532, i1348)
3939_0_random_ConstantStackPush(EOS(STATIC_3939(i1348)), i1333, i443, o2532, i1348) → 3944_0_random_IntArithmetic(EOS(STATIC_3944(i1348)), i1333, i443, o2532, i1348, 1)
3944_0_random_IntArithmetic(EOS(STATIC_3944(i1348)), i1333, i443, o2532, i1348, matching1) → 3950_0_random_FieldAccess(EOS(STATIC_3950(i1348)), i1333, i443, o2532, +(i1348, 1)) | &&(>=(i1348, 0), =(matching1, 1))
3950_0_random_FieldAccess(EOS(STATIC_3950(i1348)), i1333, i443, o2532, i1350) → 3955_0_random_Load(EOS(STATIC_3955(i1350)), i1333, i443, o2532)
3955_0_random_Load(EOS(STATIC_3955(i1350)), i1333, i443, o2532) → 3961_0_random_InvokeMethod(EOS(STATIC_3961(i1350)), i1333, i443, o2532)
3961_0_random_InvokeMethod(EOS(STATIC_3961(i1350)), i1333, i443, java.lang.Object(o2547sub)) → 3968_0_random_InvokeMethod(EOS(STATIC_3968(i1350)), i1333, i443, java.lang.Object(o2547sub))
3968_0_random_InvokeMethod(EOS(STATIC_3968(i1350)), i1333, i443, java.lang.Object(o2547sub)) → 3976_0_length_Load(EOS(STATIC_3976(i1350)), i1333, i443, java.lang.Object(o2547sub), java.lang.Object(o2547sub))
3976_0_length_Load(EOS(STATIC_3976(i1350)), i1333, i443, java.lang.Object(o2547sub), java.lang.Object(o2547sub)) → 3993_0_length_FieldAccess(EOS(STATIC_3993(i1350)), i1333, i443, java.lang.Object(o2547sub), java.lang.Object(o2547sub))
3993_0_length_FieldAccess(EOS(STATIC_3993(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), java.lang.Object(java.lang.String(o2562sub, i1370))) → 4000_0_length_FieldAccess(EOS(STATIC_4000(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), java.lang.Object(java.lang.String(o2562sub, i1370))) | &&(>=(i1370, 0), >=(i1371, 0))
4000_0_length_FieldAccess(EOS(STATIC_4000(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), java.lang.Object(java.lang.String(o2562sub, i1370))) → 4011_0_length_Return(EOS(STATIC_4011(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), i1370)
4011_0_length_Return(EOS(STATIC_4011(i1350)), i1333, i443, java.lang.Object(java.lang.String(o2562sub, i1370)), i1370) → 4019_0_random_Return(EOS(STATIC_4019(i1350)), i1333, i443, i1370)
4019_0_random_Return(EOS(STATIC_4019(i1350)), i1333, i443, i1370) → 4025_0_main_InvokeMethod(EOS(STATIC_4025(i1350)), i1333, i443, i1370)
4025_0_main_InvokeMethod(EOS(STATIC_4025(i1350)), i1333, i443, i1370) → 4035_0_random_FieldAccess(EOS(STATIC_4035(i1350)), i1333, i443, i1370)
4035_0_random_FieldAccess(EOS(STATIC_4035(i1350)), i1333, i443, i1370) → 4053_0_random_FieldAccess(EOS(STATIC_4053(i1350)), i1333, i443, i1370, i1350)
4053_0_random_FieldAccess(EOS(STATIC_4053(i1350)), i1333, i443, i1370, i1350) → 4065_0_random_ArrayLength(EOS(STATIC_4065(i1350)), i1333, i443, i1370, i1350, java.lang.Object(ARRAY(i183)))
4065_0_random_ArrayLength(EOS(STATIC_4065(i1350)), i1333, i443, i1370, i1350, java.lang.Object(ARRAY(i183))) → 4075_0_random_LT(EOS(STATIC_4075(i1350)), i1333, i443, i1370, i1350, i183) | >=(i183, 0)
4075_0_random_LT(EOS(STATIC_4075(i1350)), i1333, i443, i1370, i1350, i183) → 4083_0_random_LT(EOS(STATIC_4083(i1350)), i1333, i443, i1370, i1350, i183)
4075_0_random_LT(EOS(STATIC_4075(i1350)), i1333, i443, i1370, i1350, i183) → 4084_0_random_LT(EOS(STATIC_4084(i1350)), i1333, i443, i1370, i1350, i183)
4083_0_random_LT(EOS(STATIC_4083(i1350)), i1333, i443, i1370, i1350, i183) → 4097_0_random_FieldAccess(EOS(STATIC_4097(i1350)), i1333, i443, i1370) | <(i1350, i183)
4097_0_random_FieldAccess(EOS(STATIC_4097(i1350)), i1333, i443, i1370) → 4109_0_random_FieldAccess(EOS(STATIC_4109(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)))
4109_0_random_FieldAccess(EOS(STATIC_4109(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183))) → 4121_0_random_ArrayAccess(EOS(STATIC_4121(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350)
4121_0_random_ArrayAccess(EOS(STATIC_4121(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350) → 4135_0_random_ArrayAccess(EOS(STATIC_4135(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350)
4135_0_random_ArrayAccess(EOS(STATIC_4135(i1350)), i1333, i443, i1370, java.lang.Object(ARRAY(i183)), i1350) → 4153_0_random_Store(EOS(STATIC_4153(i1350)), i1333, i443, i1370, o2708)
4153_0_random_Store(EOS(STATIC_4153(i1350)), i1333, i443, i1370, o2708) → 4166_0_random_FieldAccess(EOS(STATIC_4166(i1350)), i1333, i443, i1370, o2708)
4166_0_random_FieldAccess(EOS(STATIC_4166(i1350)), i1333, i443, i1370, o2708) → 4183_0_random_ConstantStackPush(EOS(STATIC_4183(i1350)), i1333, i443, i1370, o2708, i1350)
4183_0_random_ConstantStackPush(EOS(STATIC_4183(i1350)), i1333, i443, i1370, o2708, i1350) → 4198_0_random_IntArithmetic(EOS(STATIC_4198(i1350)), i1333, i443, i1370, o2708, i1350, 1)
4198_0_random_IntArithmetic(EOS(STATIC_4198(i1350)), i1333, i443, i1370, o2708, i1350, matching1) → 4210_0_random_FieldAccess(EOS(STATIC_4210(i1350)), i1333, i443, i1370, o2708, +(i1350, 1)) | &&(>(i1350, 0), =(matching1, 1))
4210_0_random_FieldAccess(EOS(STATIC_4210(i1350)), i1333, i443, i1370, o2708, i1456) → 4220_0_random_Load(EOS(STATIC_4220(i1456)), i1333, i443, i1370, o2708)
4220_0_random_Load(EOS(STATIC_4220(i1456)), i1333, i443, i1370, o2708) → 4232_0_random_InvokeMethod(EOS(STATIC_4232(i1456)), i1333, i443, i1370, o2708)
4232_0_random_InvokeMethod(EOS(STATIC_4232(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub)) → 4244_0_random_InvokeMethod(EOS(STATIC_4244(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub))
4244_0_random_InvokeMethod(EOS(STATIC_4244(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub)) → 4254_0_length_Load(EOS(STATIC_4254(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub), java.lang.Object(o2862sub))
4254_0_length_Load(EOS(STATIC_4254(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub), java.lang.Object(o2862sub)) → 4278_0_length_FieldAccess(EOS(STATIC_4278(i1456)), i1333, i443, i1370, java.lang.Object(o2862sub), java.lang.Object(o2862sub))
4278_0_length_FieldAccess(EOS(STATIC_4278(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), java.lang.Object(java.lang.String(o2951sub, i1514))) → 4291_0_length_FieldAccess(EOS(STATIC_4291(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), java.lang.Object(java.lang.String(o2951sub, i1514))) | &&(>=(i1514, 0), >=(i1515, 0))
4291_0_length_FieldAccess(EOS(STATIC_4291(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), java.lang.Object(java.lang.String(o2951sub, i1514))) → 4301_0_length_Return(EOS(STATIC_4301(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), i1514)
4301_0_length_Return(EOS(STATIC_4301(i1456)), i1333, i443, i1370, java.lang.Object(java.lang.String(o2951sub, i1514)), i1514) → 4308_0_random_Return(EOS(STATIC_4308(i1456)), i1333, i443, i1370, i1514)
4308_0_random_Return(EOS(STATIC_4308(i1456)), i1333, i443, i1370, i1514) → 4312_0_main_IntArithmetic(EOS(STATIC_4312(i1456)), i1333, i443, i1370, i1514)
4312_0_main_IntArithmetic(EOS(STATIC_4312(i1456)), i1333, i443, i1370, i1514) → 4320_0_main_ConstantStackPush(EOS(STATIC_4320(i1456)), i1333, i443, *(i1370, i1514))
4320_0_main_ConstantStackPush(EOS(STATIC_4320(i1456)), i1333, i443, i1528) → 4328_0_main_LE(EOS(STATIC_4328(i1456)), i1333, i443, i1528, 9)
4328_0_main_LE(EOS(STATIC_4328(i1456)), i1333, i443, i1541, matching1) → 4333_0_main_LE(EOS(STATIC_4333(i1456)), i1333, i443, i1541, 9) | =(matching1, 9)
4328_0_main_LE(EOS(STATIC_4328(i1456)), i1333, i443, i1542, matching1) → 4334_0_main_LE(EOS(STATIC_4334(i1456)), i1333, i443, i1542, 9) | =(matching1, 9)
4333_0_main_LE(EOS(STATIC_4333(i1456)), i1333, i443, i1541, matching1) → 4341_0_main_Inc(EOS(STATIC_4341(i1456)), i1333, i443) | &&(<=(i1541, 9), =(matching1, 9))
4341_0_main_Inc(EOS(STATIC_4341(i1456)), i1333, i443) → 4348_0_main_JMP(EOS(STATIC_4348(i1456)), i1333, +(i443, -1))
4348_0_main_JMP(EOS(STATIC_4348(i1456)), i1333, i1547) → 4354_0_main_Load(EOS(STATIC_4354(i1456)), i1333, i1547)
4354_0_main_Load(EOS(STATIC_4354(i1456)), i1333, i1547) → 3893_0_main_Load(EOS(STATIC_3893(i1456)), i1333, i1547)
3893_0_main_Load(EOS(STATIC_3893(i1332)), i1333, i443) → 3897_0_main_Load(EOS(STATIC_3897(i1332)), i1333, i443, i1333)
4334_0_main_LE(EOS(STATIC_4334(i1456)), i1333, i443, i1542, matching1) → 4342_0_main_Inc(EOS(STATIC_4342(i1456)), i1333, i443) | &&(>(i1542, 9), =(matching1, 9))
4342_0_main_Inc(EOS(STATIC_4342(i1456)), i1333, i443) → 4350_0_main_JMP(EOS(STATIC_4350(i1456)), +(i1333, -1), i443)
4350_0_main_JMP(EOS(STATIC_4350(i1456)), i1548, i443) → 4356_0_main_Load(EOS(STATIC_4356(i1456)), i1548, i443)
4356_0_main_Load(EOS(STATIC_4356(i1456)), i1548, i443) → 3893_0_main_Load(EOS(STATIC_3893(i1456)), i1548, i443)
4084_0_random_LT(EOS(STATIC_4084(i1350)), i1333, i443, i1370, i1350, i183) → 4098_0_random_ConstantStackPush(EOS(STATIC_4098(i1350)), i1333, i443, i1370) | >=(i1350, i183)
4098_0_random_ConstantStackPush(EOS(STATIC_4098(i1350)), i1333, i443, i1370) → 4110_0_random_Return(EOS(STATIC_4110(i1350)), i1333, i443, i1370)
4110_0_random_Return(EOS(STATIC_4110(i1350)), i1333, i443, i1370) → 4122_0_main_IntArithmetic(EOS(STATIC_4122(i1350)), i1333, i443, i1370)
4122_0_main_IntArithmetic(EOS(STATIC_4122(i1350)), i1333, i443, i1370) → 4138_0_main_ConstantStackPush(EOS(STATIC_4138(i1350)), i1333, i443)
4138_0_main_ConstantStackPush(EOS(STATIC_4138(i1350)), i1333, i443) → 4146_0_main_ConstantStackPush(EOS(STATIC_4146(i1350)), i1333, i443)
4146_0_main_ConstantStackPush(EOS(STATIC_4146(i1377)), i1333, i443) → 4161_0_main_LE(EOS(STATIC_4161(i1377)), i1333, i443)
4161_0_main_LE(EOS(STATIC_4161(i1377)), i1333, i443) → 4176_0_main_Inc(EOS(STATIC_4176(i1377)), i1333, i443)
4176_0_main_Inc(EOS(STATIC_4176(i1377)), i1333, i443) → 4192_0_main_JMP(EOS(STATIC_4192(i1377)), i1333, +(i443, -1))
4192_0_main_JMP(EOS(STATIC_4192(i1377)), i1333, i1448) → 4206_0_main_Load(EOS(STATIC_4206(i1377)), i1333, i1448)
4206_0_main_Load(EOS(STATIC_4206(i1377)), i1333, i1448) → 3893_0_main_Load(EOS(STATIC_3893(i1377)), i1333, i1448)
3914_0_random_LT(EOS(STATIC_3914(i1332)), i1333, i443, i1332, i183) → 3916_0_random_ConstantStackPush(EOS(STATIC_3916(i1332)), i1333, i443) | >=(i1332, i183)
3916_0_random_ConstantStackPush(EOS(STATIC_3916(i1332)), i1333, i443) → 3918_0_random_Return(EOS(STATIC_3918(i1332)), i1333, i443)
3918_0_random_Return(EOS(STATIC_3918(i1332)), i1333, i443) → 3921_0_main_InvokeMethod(EOS(STATIC_3921(i1332)), i1333, i443)
3921_0_main_InvokeMethod(EOS(STATIC_3921(i1332)), i1333, i443) → 3925_0_random_FieldAccess(EOS(STATIC_3925(i1332)), i1333, i443)
3925_0_random_FieldAccess(EOS(STATIC_3925(i1332)), i1333, i443) → 3933_0_random_FieldAccess(EOS(STATIC_3933(i1332)), i1333, i443, i1332)
3933_0_random_FieldAccess(EOS(STATIC_3933(i1332)), i1333, i443, i1332) → 3937_0_random_ArrayLength(EOS(STATIC_3937(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183)))
3937_0_random_ArrayLength(EOS(STATIC_3937(i1332)), i1333, i443, i1332, java.lang.Object(ARRAY(i183))) → 3943_0_random_LT(EOS(STATIC_3943(i1332)), i1333, i443, i1332, i183) | >=(i183, 0)
3943_0_random_LT(EOS(STATIC_3943(i1332)), i1333, i443, i1332, i183) → 3946_0_random_LT(EOS(STATIC_3946(i1332)), i1333, i443, i1332, i183)
3943_0_random_LT(EOS(STATIC_3943(i1332)), i1333, i443, i1332, i183) → 3947_0_random_LT(EOS(STATIC_3947(i1332)), i1333, i443, i1332, i183)
3946_0_random_LT(EOS(STATIC_3946(i1332)), i1333, i443, i1332, i183) → 3951_0_random_FieldAccess(EOS(STATIC_3951(i1332)), i1333, i443) | <(i1332, i183)
3951_0_random_FieldAccess(EOS(STATIC_3951(i1332)), i1333, i443) → 3958_0_random_FieldAccess(EOS(STATIC_3958(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)))
3958_0_random_FieldAccess(EOS(STATIC_3958(i1332)), i1333, i443, java.lang.Object(ARRAY(i183))) → 3964_0_random_ArrayAccess(EOS(STATIC_3964(i1332)), i1333, i443, java.lang.Object(ARRAY(i183)), i1332)
3964_0_random_ArrayAccess(EOS(STATIC_3964(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355) → 3972_0_random_ArrayAccess(EOS(STATIC_3972(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355)
3972_0_random_ArrayAccess(EOS(STATIC_3972(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355) → 3981_0_random_ArrayAccess(EOS(STATIC_3981(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355)
3981_0_random_ArrayAccess(EOS(STATIC_3981(i1355)), i1333, i443, java.lang.Object(ARRAY(i183)), i1355) → 3988_0_random_Store(EOS(STATIC_3988(i1355)), i1333, i443, o2552)
3988_0_random_Store(EOS(STATIC_3988(i1355)), i1333, i443, o2552) → 3996_0_random_FieldAccess(EOS(STATIC_3996(i1355)), i1333, i443, o2552)
3996_0_random_FieldAccess(EOS(STATIC_3996(i1355)), i1333, i443, o2552) → 4006_0_random_ConstantStackPush(EOS(STATIC_4006(i1355)), i1333, i443, o2552, i1355)
4006_0_random_ConstantStackPush(EOS(STATIC_4006(i1355)), i1333, i443, o2552, i1355) → 4015_0_random_IntArithmetic(EOS(STATIC_4015(i1355)), i1333, i443, o2552, i1355, 1)
4015_0_random_IntArithmetic(EOS(STATIC_4015(i1355)), i1333, i443, o2552, i1355, matching1) → 4022_0_random_FieldAccess(EOS(STATIC_4022(i1355)), i1333, i443, o2552, +(i1355, 1)) | &&(>=(i1355, 0), =(matching1, 1))
4022_0_random_FieldAccess(EOS(STATIC_4022(i1355)), i1333, i443, o2552, i1377) → 4031_0_random_Load(EOS(STATIC_4031(i1377)), i1333, i443, o2552)
4031_0_random_Load(EOS(STATIC_4031(i1377)), i1333, i443, o2552) → 4040_0_random_InvokeMethod(EOS(STATIC_4040(i1377)), i1333, i443, o2552)
4040_0_random_InvokeMethod(EOS(STATIC_4040(i1377)), i1333, i443, java.lang.Object(o2603sub)) → 4048_0_random_InvokeMethod(EOS(STATIC_4048(i1377)), i1333, i443, java.lang.Object(o2603sub))
4048_0_random_InvokeMethod(EOS(STATIC_4048(i1377)), i1333, i443, java.lang.Object(o2603sub)) → 4059_0_length_Load(EOS(STATIC_4059(i1377)), i1333, i443, java.lang.Object(o2603sub), java.lang.Object(o2603sub))
4059_0_length_Load(EOS(STATIC_4059(i1377)), i1333, i443, java.lang.Object(o2603sub), java.lang.Object(o2603sub)) → 4081_0_length_FieldAccess(EOS(STATIC_4081(i1377)), i1333, i443, java.lang.Object(o2603sub), java.lang.Object(o2603sub))
4081_0_length_FieldAccess(EOS(STATIC_4081(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)), java.lang.Object(java.lang.String(o2636sub, i1404))) → 4090_0_length_FieldAccess(EOS(STATIC_4090(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)), java.lang.Object(java.lang.String(o2636sub, i1404))) | &&(>=(i1404, 0), >=(i1405, 0))
4090_0_length_FieldAccess(EOS(STATIC_4090(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)), java.lang.Object(java.lang.String(o2636sub, i1404))) → 4103_0_length_Return(EOS(STATIC_4103(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404)))
4103_0_length_Return(EOS(STATIC_4103(i1377)), i1333, i443, java.lang.Object(java.lang.String(o2636sub, i1404))) → 4117_0_random_Return(EOS(STATIC_4117(i1377)), i1333, i443)
4117_0_random_Return(EOS(STATIC_4117(i1377)), i1333, i443) → 4129_0_main_IntArithmetic(EOS(STATIC_4129(i1377)), i1333, i443)
4129_0_main_IntArithmetic(EOS(STATIC_4129(i1377)), i1333, i443) → 4146_0_main_ConstantStackPush(EOS(STATIC_4146(i1377)), i1333, i443)
3947_0_random_LT(EOS(STATIC_3947(i1332)), i1333, i443, i1332, i183) → 3953_0_random_ConstantStackPush(EOS(STATIC_3953(i1332)), i1333, i443) | >=(i1332, i183)
3953_0_random_ConstantStackPush(EOS(STATIC_3953(i1332)), i1333, i443) → 3960_0_random_Return(EOS(STATIC_3960(i1332)), i1333, i443)
3960_0_random_Return(EOS(STATIC_3960(i1332)), i1333, i443) → 3966_0_main_IntArithmetic(EOS(STATIC_3966(i1332)), i1333, i443)
3966_0_main_IntArithmetic(EOS(STATIC_3966(i1332)), i1333, i443) → 3973_0_main_ConstantStackPush(EOS(STATIC_3973(i1332)), i1333, i443)
3973_0_main_ConstantStackPush(EOS(STATIC_3973(i1332)), i1333, i443) → 3983_0_main_LE(EOS(STATIC_3983(i1332)), i1333, i443)
3983_0_main_LE(EOS(STATIC_3983(i1332)), i1333, i443) → 3990_0_main_Inc(EOS(STATIC_3990(i1332)), i1333, i443)
3990_0_main_Inc(EOS(STATIC_3990(i1332)), i1333, i443) → 3998_0_main_JMP(EOS(STATIC_3998(i1332)), i1333, +(i443, -1))
3998_0_main_JMP(EOS(STATIC_3998(i1332)), i1333, i1366) → 4009_0_main_Load(EOS(STATIC_4009(i1332)), i1333, i1366)
4009_0_main_Load(EOS(STATIC_4009(i1332)), i1333, i1366) → 3893_0_main_Load(EOS(STATIC_3893(i1332)), i1333, i1366)
R rules:

Combined rules. Obtained 4 conditional rules for P and 0 conditional rules for R.


P rules:
3897_0_main_Load(EOS(STATIC_3897(x0)), x1, x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(+(x0, 2))), x1, +(x2, -1), x1) | &&(>(+(x0, 1), 0), <(0, +(x1, x2)))
3897_0_main_Load(EOS(STATIC_3897(x0)), x1, x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(+(x0, 2))), +(x1, -1), x2, +(x1, -1)) | &&(>(+(x0, 1), 0), <(0, +(x1, x2)))
3897_0_main_Load(EOS(STATIC_3897(x0)), x1, x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(+(x0, 1))), x1, +(x2, -1), x1) | &&(>(+(x0, 1), 0), <(0, +(x1, x2)))
3897_0_main_Load(EOS(STATIC_3897(x0)), x1, x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(x0)), x1, +(x2, -1), x1) | <(0, +(x1, x2))
R rules:

Filtered duplicate args:



3897_0_main_Load(x1, x2, x3, x4) → 3897_0_main_Load(x1, x3, x4)
Cond_3897_0_main_Load(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load(x1, x2, x4, x5)
Cond_3897_0_main_Load1(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load1(x1, x2, x4, x5)
Cond_3897_0_main_Load2(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load2(x1, x2, x4, x5)
Cond_3897_0_main_Load3(x1, x2, x3, x4, x5) → Cond_3897_0_main_Load3(x1, x2, x4, x5)

Combined rules. Obtained 4 conditional rules for P and 0 conditional rules for R.


P rules:
3897_0_main_Load(EOS(STATIC_3897(x0)), x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1) | &&(>(x0, -1), <(0, +(x1, x2)))
3897_0_main_Load(EOS(STATIC_3897(x0)), x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1)) | &&(>(x0, -1), <(0, +(x1, x2)))
3897_0_main_Load(EOS(STATIC_3897(x0)), x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1) | &&(>(x0, -1), <(0, +(x1, x2)))
3897_0_main_Load(EOS(STATIC_3897(x0)), x2, x1) → 3897_0_main_Load(EOS(STATIC_3897(x0)), +(x2, -1), x1) | <(0, +(x1, x2))
R rules:

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_3897_0_main_Load_4, Cond_3897_0_main_Load1_4, Cond_3897_0_main_Load2_4]=Cond_3897_0_main_Load_4}


Finished conversion. Obtained 6 rules for P and 0 rules for R. System has predefined symbols.


P rules:
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_3897(x0)), x2, x1)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1)
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1))
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1)
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_3897(x0)), x2, x1)
COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), +(x2, -1), x1)
R rules:

(6) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~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


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(x0[0] > -1 && 0 < x1[0] + x2[0], EOS(STATIC_3897(x0[0])), x2[0], x1[0])
(1): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[1] + 2)), x2[1] + -1, x1[1])
(2): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[2] + 2)), x2[2], x1[2] + -1)
(3): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[3] + 1)), x2[3] + -1, x1[3])
(4): 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(0 < x1[4] + x2[4], EOS(STATIC_3897(x0[4])), x2[4], x1[4])
(5): COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), x2[5] + -1, x1[5])

(0) -> (1), if (x0[0] > -1 && 0 < x1[0] + x2[0]EOS(STATIC_3897(x0[0])) →* EOS(STATIC_3897(x0[1]))∧x2[0]* x2[1]x1[0]* x1[1])


(0) -> (2), if (x0[0] > -1 && 0 < x1[0] + x2[0]EOS(STATIC_3897(x0[0])) →* EOS(STATIC_3897(x0[2]))∧x2[0]* x2[2]x1[0]* x1[2])


(0) -> (3), if (x0[0] > -1 && 0 < x1[0] + x2[0]EOS(STATIC_3897(x0[0])) →* EOS(STATIC_3897(x0[3]))∧x2[0]* x2[3]x1[0]* x1[3])


(1) -> (0), if (EOS(STATIC_3897(x0[1] + 2)) →* EOS(STATIC_3897(x0[0]))∧x2[1] + -1* x2[0]x1[1]* x1[0])


(1) -> (4), if (EOS(STATIC_3897(x0[1] + 2)) →* EOS(STATIC_3897(x0[4]))∧x2[1] + -1* x2[4]x1[1]* x1[4])


(2) -> (0), if (EOS(STATIC_3897(x0[2] + 2)) →* EOS(STATIC_3897(x0[0]))∧x2[2]* x2[0]x1[2] + -1* x1[0])


(2) -> (4), if (EOS(STATIC_3897(x0[2] + 2)) →* EOS(STATIC_3897(x0[4]))∧x2[2]* x2[4]x1[2] + -1* x1[4])


(3) -> (0), if (EOS(STATIC_3897(x0[3] + 1)) →* EOS(STATIC_3897(x0[0]))∧x2[3] + -1* x2[0]x1[3]* x1[0])


(3) -> (4), if (EOS(STATIC_3897(x0[3] + 1)) →* EOS(STATIC_3897(x0[4]))∧x2[3] + -1* x2[4]x1[3]* x1[4])


(4) -> (5), if (0 < x1[4] + x2[4]EOS(STATIC_3897(x0[4])) →* EOS(STATIC_3897(x0[5]))∧x2[4]* x2[5]x1[4]* x1[5])


(5) -> (0), if (EOS(STATIC_3897(x0[5])) →* EOS(STATIC_3897(x0[0]))∧x2[5] + -1* x2[0]x1[5]* x1[0])


(5) -> (4), if (EOS(STATIC_3897(x0[5])) →* EOS(STATIC_3897(x0[4]))∧x2[5] + -1* x2[4]x1[5]* x1[4])



The set Q is empty.

(7) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@2b68c70e Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_3897(x0)), x2, x1) the following chains were created:
  • We consider the chain 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0]), COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1]) which results in the following constraint:

    (1)    (&&(>(x0[0], -1), <(0, +(x1[0], x2[0])))=TRUEEOS(STATIC_3897(x0[0]))=EOS(STATIC_3897(x0[1]))∧x2[0]=x2[1]x1[0]=x1[1]3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥))



    We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>(x0[0], -1)=TRUE<(0, +(x1[0], x2[0]))=TRUE3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (7)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)


    (8)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)



  • We consider the chain 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0]), COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1)) which results in the following constraint:

    (9)    (&&(>(x0[0], -1), <(0, +(x1[0], x2[0])))=TRUEEOS(STATIC_3897(x0[0]))=EOS(STATIC_3897(x0[2]))∧x2[0]=x2[2]x1[0]=x1[2]3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥))



    We simplified constraint (9) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (10)    (>(x0[0], -1)=TRUE<(0, +(x1[0], x2[0]))=TRUE3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥))



    We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (11)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (12)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (13)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (15)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)


    (16)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)



  • We consider the chain 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0]), COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3]) which results in the following constraint:

    (17)    (&&(>(x0[0], -1), <(0, +(x1[0], x2[0])))=TRUEEOS(STATIC_3897(x0[0]))=EOS(STATIC_3897(x0[3]))∧x2[0]=x2[3]x1[0]=x1[3]3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥))



    We simplified constraint (17) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (18)    (>(x0[0], -1)=TRUE<(0, +(x1[0], x2[0]))=TRUE3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0])≥COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])∧(UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥))



    We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (19)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (20)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (21)    (x0[0] ≥ 0∧x1[0] + [-1] + x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] + [bni_12]x2[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (22)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)



    We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (23)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)


    (24)    (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)







For Pair COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1) the following chains were created:
  • We consider the chain COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1]) which results in the following constraint:

    (25)    (COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1])≥NonInfC∧COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])∧(UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥))



    We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (26)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)



    We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (27)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)



    We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (28)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)



    We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (29)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)







For Pair COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1)) the following chains were created:
  • We consider the chain COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1)) which results in the following constraint:

    (30)    (COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2])≥NonInfC∧COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))∧(UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥))



    We simplified constraint (30) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (31)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (31) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (32)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (32) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (33)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (33) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (34)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)







For Pair COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1) the following chains were created:
  • We consider the chain COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3]) which results in the following constraint:

    (35)    (COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3])≥NonInfC∧COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])∧(UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥))



    We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (36)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)



    We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (37)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)



    We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (38)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)



    We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (39)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)







For Pair 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_3897(x0)), x2, x1) the following chains were created:
  • We consider the chain 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4]), COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5]) which results in the following constraint:

    (40)    (<(0, +(x1[4], x2[4]))=TRUEEOS(STATIC_3897(x0[4]))=EOS(STATIC_3897(x0[5]))∧x2[4]=x2[5]x1[4]=x1[5]3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])∧(UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥))



    We simplified constraint (40) using rules (I), (II), (IV) which results in the following new constraint:

    (41)    (<(0, +(x1[4], x2[4]))=TRUE3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥NonInfC∧3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4])≥COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])∧(UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥))



    We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (42)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (43)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (44)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (45)    (x1[4] + [-1] + x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] + [bni_20]x2[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (45) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (46)    (x1[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (47)    (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)


    (48)    (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)







For Pair COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), +(x2, -1), x1) the following chains were created:
  • We consider the chain COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5]) which results in the following constraint:

    (49)    (COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5])≥NonInfC∧COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5])≥3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])∧(UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])), ≥))



    We simplified constraint (49) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (50)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (50) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (51)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (51) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (52)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (52) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (53)    ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD(&&(>(x0, -1), <(0, +(x1, x2))), EOS(STATIC_3897(x0)), x2, x1)
    • (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    • (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    • (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    • (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    • (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)
    • (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])), ≥)∧[(2)bni_12 + (-1)Bound*bni_12] + [bni_12]x1[0] ≥ 0∧[(-1)bso_13] ≥ 0)

  • COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), +(x2, -1), x1)
    • ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

  • COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 2))), x2, +(x1, -1))
    • ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)

  • COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0, 1))), +(x2, -1), x1)
    • ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

  • 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), x2, x1) → COND_3897_0_MAIN_LOAD3(<(0, +(x1, x2)), EOS(STATIC_3897(x0)), x2, x1)
    • (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)
    • (x1[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])), ≥)∧0 = 0∧[(2)bni_20 + (-1)Bound*bni_20] + [bni_20]x1[4] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

  • COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0)), x2, x1) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0)), +(x2, -1), x1)
    • ((UIncreasing(3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])), ≥)∧[bni_22] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)




The constraints for P> respective Pbound are constructed from P where we just replace every occurence of "t ≥ s" in P by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(3897_0_MAIN_LOAD(x1, x2, x3)) = [1] + x3 + x2   
POL(EOS(x1)) = x1   
POL(STATIC_3897(x1)) = x1   
POL(COND_3897_0_MAIN_LOAD(x1, x2, x3, x4)) = [1] + x4 + x3   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(-1) = [-1]   
POL(<(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(2) = [2]   
POL(1) = [1]   
POL(COND_3897_0_MAIN_LOAD3(x1, x2, x3, x4)) = [1] + x4 + x3   

The following pairs are in P>:

COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[1], 2))), +(x2[1], -1), x1[1])
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[2], 2))), x2[2], +(x1[2], -1))
COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(+(x0[3], 1))), +(x2[3], -1), x1[3])
COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), +(x2[5], -1), x1[5])

The following pairs are in Pbound:

3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])

The following pairs are in P:

3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(&&(>(x0[0], -1), <(0, +(x1[0], x2[0]))), EOS(STATIC_3897(x0[0])), x2[0], x1[0])
3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(<(0, +(x1[4], x2[4])), EOS(STATIC_3897(x0[4])), x2[4], x1[4])

There are no usable rules.

(8) Complex Obligation (AND)

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~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


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[0])), x2[0], x1[0]) → COND_3897_0_MAIN_LOAD(x0[0] > -1 && 0 < x1[0] + x2[0], EOS(STATIC_3897(x0[0])), x2[0], x1[0])
(4): 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[4])), x2[4], x1[4]) → COND_3897_0_MAIN_LOAD3(0 < x1[4] + x2[4], EOS(STATIC_3897(x0[4])), x2[4], x1[4])


The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(11) TRUE

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~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


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[1])), x2[1], x1[1]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[1] + 2)), x2[1] + -1, x1[1])
(2): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[2])), x2[2], x1[2]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[2] + 2)), x2[2], x1[2] + -1)
(3): COND_3897_0_MAIN_LOAD(TRUE, EOS(STATIC_3897(x0[3])), x2[3], x1[3]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[3] + 1)), x2[3] + -1, x1[3])
(5): COND_3897_0_MAIN_LOAD3(TRUE, EOS(STATIC_3897(x0[5])), x2[5], x1[5]) → 3897_0_MAIN_LOAD(EOS(STATIC_3897(x0[5])), x2[5] + -1, x1[5])


The set Q is empty.

(13) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(14) TRUE