0 JBC
↳1 JBCToGraph (⇒)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒)
↳7 IDP
↳8 IDPNonInfProof (⇒)
↳9 AND
↳10 IDP
↳11 IDependencyGraphProof (⇔)
↳12 TRUE
↳13 IDP
↳14 IDependencyGraphProof (⇔)
↳15 TRUE
↳16 JBCTerminationSCC
↳17 SCCToIDPv1Proof (⇒)
↳18 IDP
↳19 IDPNonInfProof (⇒)
↳20 AND
↳21 IDP
↳22 IDependencyGraphProof (⇔)
↳23 TRUE
↳24 IDP
↳25 IDependencyGraphProof (⇔)
↳26 TRUE
public class Array {
public static void main(String[] args) {
int[] a = new int[args.length + 2];
for (int i = 0; i < a.length; i++) {
a[i] = (args[i % args.length].length() * i) % args.length;
}
int firstDup = 2 + (args[args.length - 2].length() % (args.length - 3));
int secondDup = 3 + (args[args.length - 1].length() % (args.length - 3));
a[firstDup] = a[0];
a[secondDup] = a[1];
findDups(a);
}
public static void findDups(int[] a) {
int firstDup = -1;
int secondDup = -1;
for (int i = 0; i < a.length; i++) {
for (int j = i + 1; j < a.length; i++) {
if (a[i] == a[j]) {
if (firstDup > -1) {
firstDup = a[i];
} else if (firstDup != a[i]) {
secondDup = a[i];
break;
}
}
}
}
}
}
Generated 61 rules for P and 0 rules for R.
P rules:
1033_0_findDups_Load(EOS(STATIC_1033), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i726) → 1034_0_findDups_ArrayLength(EOS(STATIC_1034), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i726, java.lang.Object(ARRAY(i2))) | =(matching1, -1)
1034_0_findDups_ArrayLength(EOS(STATIC_1034), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i726, java.lang.Object(ARRAY(i2))) → 1035_0_findDups_GE(EOS(STATIC_1035), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i726, i2) | &&(>=(i2, 0), =(matching1, -1))
1035_0_findDups_GE(EOS(STATIC_1035), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i726, i2) → 1037_0_findDups_GE(EOS(STATIC_1037), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i726, i2) | =(matching1, -1)
1037_0_findDups_GE(EOS(STATIC_1037), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i726, i2) → 1039_0_findDups_Load(EOS(STATIC_1039), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726) | &&(<(i726, i2), =(matching1, -1))
1039_0_findDups_Load(EOS(STATIC_1039), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726) → 1041_0_findDups_ConstantStackPush(EOS(STATIC_1041), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i726) | =(matching1, -1)
1041_0_findDups_ConstantStackPush(EOS(STATIC_1041), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i726) → 1043_0_findDups_IntArithmetic(EOS(STATIC_1043), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i726, 1) | =(matching1, -1)
1043_0_findDups_IntArithmetic(EOS(STATIC_1043), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i726, matching2) → 1044_0_findDups_Store(EOS(STATIC_1044), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, +(i726, 1)) | &&(=(matching1, -1), =(matching2, 1))
1044_0_findDups_Store(EOS(STATIC_1044), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728) → 1045_0_findDups_Load(EOS(STATIC_1045), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728) | =(matching1, -1)
1045_0_findDups_Load(EOS(STATIC_1045), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728) → 1046_0_findDups_Load(EOS(STATIC_1046), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, i728) | =(matching1, -1)
1046_0_findDups_Load(EOS(STATIC_1046), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, i728) → 1047_0_findDups_ArrayLength(EOS(STATIC_1047), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, i728, java.lang.Object(ARRAY(i2))) | =(matching1, -1)
1047_0_findDups_ArrayLength(EOS(STATIC_1047), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, i728, java.lang.Object(ARRAY(i2))) → 1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, i728, i2) | &&(>=(i2, 0), =(matching1, -1))
1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, i728, i2) → 1049_0_findDups_GE(EOS(STATIC_1049), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, i728, i2) | =(matching1, -1)
1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, i728, i2) → 1050_0_findDups_GE(EOS(STATIC_1050), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, i728, i2) | =(matching1, -1)
1049_0_findDups_GE(EOS(STATIC_1049), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, i728, i2) → 1051_0_findDups_Inc(EOS(STATIC_1051), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726) | &&(>=(i728, i2), =(matching1, -1))
1051_0_findDups_Inc(EOS(STATIC_1051), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726) → 1053_0_findDups_JMP(EOS(STATIC_1053), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, +(i726, 1)) | =(matching1, -1)
1053_0_findDups_JMP(EOS(STATIC_1053), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i729) → 1055_0_findDups_Load(EOS(STATIC_1055), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i729) | =(matching1, -1)
1055_0_findDups_Load(EOS(STATIC_1055), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i729) → 1032_0_findDups_Load(EOS(STATIC_1032), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i729) | =(matching1, -1)
1032_0_findDups_Load(EOS(STATIC_1032), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726) → 1033_0_findDups_Load(EOS(STATIC_1033), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i726) | =(matching1, -1)
1050_0_findDups_GE(EOS(STATIC_1050), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, i728, i2) → 1052_0_findDups_Load(EOS(STATIC_1052), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728) | &&(<(i728, i2), =(matching1, -1))
1052_0_findDups_Load(EOS(STATIC_1052), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728) → 1054_0_findDups_Load(EOS(STATIC_1054), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, java.lang.Object(ARRAY(i2))) | =(matching1, -1)
1054_0_findDups_Load(EOS(STATIC_1054), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i726, i728, java.lang.Object(ARRAY(i2))) → 1056_0_findDups_ArrayAccess(EOS(STATIC_1056), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i726, i728, java.lang.Object(ARRAY(i2)), i726) | =(matching1, -1)
1056_0_findDups_ArrayAccess(EOS(STATIC_1056), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i728, java.lang.Object(ARRAY(i2)), i734) → 1058_0_findDups_ArrayAccess(EOS(STATIC_1058), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i728, java.lang.Object(ARRAY(i2)), i734) | =(matching1, -1)
1058_0_findDups_ArrayAccess(EOS(STATIC_1058), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i728, java.lang.Object(ARRAY(i2)), i734) → 1060_0_findDups_ArrayAccess(EOS(STATIC_1060), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i728, java.lang.Object(ARRAY(i2)), i734) | =(matching1, -1)
1060_0_findDups_ArrayAccess(EOS(STATIC_1060), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i728, java.lang.Object(ARRAY(i2)), i734) → 1062_0_findDups_Load(EOS(STATIC_1062), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i728, i735) | &&(<(i734, i2), =(matching1, -1))
1062_0_findDups_Load(EOS(STATIC_1062), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i728, i735) → 1065_0_findDups_Load(EOS(STATIC_1065), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i728, i735, java.lang.Object(ARRAY(i2))) | =(matching1, -1)
1065_0_findDups_Load(EOS(STATIC_1065), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i728, i735, java.lang.Object(ARRAY(i2))) → 1067_0_findDups_ArrayAccess(EOS(STATIC_1067), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i728, i735, java.lang.Object(ARRAY(i2)), i728) | =(matching1, -1)
1067_0_findDups_ArrayAccess(EOS(STATIC_1067), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i735, java.lang.Object(ARRAY(i2)), i743) → 1070_0_findDups_ArrayAccess(EOS(STATIC_1070), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, i735, java.lang.Object(ARRAY(i2)), i743) | =(matching1, -1)
1070_0_findDups_ArrayAccess(EOS(STATIC_1070), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i735, java.lang.Object(ARRAY(i2)), i743) → 1074_0_findDups_ArrayAccess(EOS(STATIC_1074), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, i735, java.lang.Object(ARRAY(i2)), i743) | =(matching1, -1)
1074_0_findDups_ArrayAccess(EOS(STATIC_1074), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i735, java.lang.Object(ARRAY(i2)), i743) → 1077_0_findDups_NE(EOS(STATIC_1077), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, i735, i746) | &&(<(i743, i2), =(matching1, -1))
1077_0_findDups_NE(EOS(STATIC_1077), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i735, i746) → 1081_0_findDups_NE(EOS(STATIC_1081), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, i735, i746) | =(matching1, -1)
1077_0_findDups_NE(EOS(STATIC_1077), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i746, i746) → 1082_0_findDups_NE(EOS(STATIC_1082), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, i746, i746) | =(matching1, -1)
1081_0_findDups_NE(EOS(STATIC_1081), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i735, i746) → 1086_0_findDups_Inc(EOS(STATIC_1086), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743) | &&(!(=(i735, i746)), =(matching1, -1))
1086_0_findDups_Inc(EOS(STATIC_1086), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743) → 1132_0_findDups_Inc(EOS(STATIC_1132), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743) | =(matching1, -1)
1132_0_findDups_Inc(EOS(STATIC_1132), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743) → 1139_0_findDups_JMP(EOS(STATIC_1139), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, +(i734, 1), i743) | &&(>=(i734, 0), =(matching1, -1))
1139_0_findDups_JMP(EOS(STATIC_1139), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i843, i743) → 1145_0_findDups_Load(EOS(STATIC_1145), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i843, i743) | =(matching1, -1)
1145_0_findDups_Load(EOS(STATIC_1145), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i843, i743) → 1045_0_findDups_Load(EOS(STATIC_1045), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i843, i743) | =(matching1, -1)
1082_0_findDups_NE(EOS(STATIC_1082), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, i746, i746) → 1087_0_findDups_Load(EOS(STATIC_1087), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743) | =(matching1, -1)
1087_0_findDups_Load(EOS(STATIC_1087), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743) → 1091_0_findDups_ConstantStackPush(EOS(STATIC_1091), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1) | =(matching1, -1)
1091_0_findDups_ConstantStackPush(EOS(STATIC_1091), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2) → 1096_0_findDups_LE(EOS(STATIC_1096), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, -1) | &&(=(matching1, -1), =(matching2, -1))
1096_0_findDups_LE(EOS(STATIC_1096), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, matching3) → 1100_0_findDups_Load(EOS(STATIC_1100), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743) | &&(&&(=(matching1, -1), =(matching2, -1)), =(matching3, -1))
1100_0_findDups_Load(EOS(STATIC_1100), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743) → 1103_0_findDups_Load(EOS(STATIC_1103), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1) | =(matching1, -1)
1103_0_findDups_Load(EOS(STATIC_1103), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2) → 1107_0_findDups_Load(EOS(STATIC_1107), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, java.lang.Object(ARRAY(i2))) | &&(=(matching1, -1), =(matching2, -1))
1107_0_findDups_Load(EOS(STATIC_1107), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, java.lang.Object(ARRAY(i2))) → 1111_0_findDups_ArrayAccess(EOS(STATIC_1111), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, java.lang.Object(ARRAY(i2)), i734) | &&(=(matching1, -1), =(matching2, -1))
1111_0_findDups_ArrayAccess(EOS(STATIC_1111), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, java.lang.Object(ARRAY(i2)), i734) → 1114_0_findDups_ArrayAccess(EOS(STATIC_1114), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, java.lang.Object(ARRAY(i2)), i734) | &&(=(matching1, -1), =(matching2, -1))
1114_0_findDups_ArrayAccess(EOS(STATIC_1114), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, java.lang.Object(ARRAY(i2)), i734) → 1120_0_findDups_EQ(EOS(STATIC_1120), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, i804) | &&(&&(<(i734, i2), =(matching1, -1)), =(matching2, -1))
1120_0_findDups_EQ(EOS(STATIC_1120), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, i815) → 1125_0_findDups_EQ(EOS(STATIC_1125), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, i815) | &&(=(matching1, -1), =(matching2, -1))
1120_0_findDups_EQ(EOS(STATIC_1120), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, matching3) → 1126_0_findDups_EQ(EOS(STATIC_1126), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, -1) | &&(&&(=(matching1, -1), =(matching2, -1)), =(matching3, -1))
1120_0_findDups_EQ(EOS(STATIC_1120), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, i816) → 1127_0_findDups_EQ(EOS(STATIC_1127), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743, -1, i816) | &&(=(matching1, -1), =(matching2, -1))
1125_0_findDups_EQ(EOS(STATIC_1125), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, i815) → 1131_0_findDups_Load(EOS(STATIC_1131), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734) | &&(&&(!(=(-1, i815)), =(matching1, -1)), =(matching2, -1))
1131_0_findDups_Load(EOS(STATIC_1131), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734) → 1133_0_findDups_Load(EOS(STATIC_1133), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734) | =(matching1, -1)
1133_0_findDups_Load(EOS(STATIC_1133), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734) → 1140_0_findDups_Load(EOS(STATIC_1140), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, java.lang.Object(ARRAY(i2))) | =(matching1, -1)
1140_0_findDups_Load(EOS(STATIC_1140), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, java.lang.Object(ARRAY(i2))) → 1146_0_findDups_ArrayAccess(EOS(STATIC_1146), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, java.lang.Object(ARRAY(i2)), i734) | =(matching1, -1)
1146_0_findDups_ArrayAccess(EOS(STATIC_1146), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, java.lang.Object(ARRAY(i2)), i734) → 1151_0_findDups_ArrayAccess(EOS(STATIC_1151), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, java.lang.Object(ARRAY(i2)), i734) | =(matching1, -1)
1151_0_findDups_ArrayAccess(EOS(STATIC_1151), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, java.lang.Object(ARRAY(i2)), i734) → 1158_0_findDups_Store(EOS(STATIC_1158), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734) | &&(<(i734, i2), =(matching1, -1))
1158_0_findDups_Store(EOS(STATIC_1158), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734) → 1165_0_findDups_JMP(EOS(STATIC_1165), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734) | =(matching1, -1)
1165_0_findDups_JMP(EOS(STATIC_1165), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734) → 1170_0_findDups_Inc(EOS(STATIC_1170), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734) | =(matching1, -1)
1170_0_findDups_Inc(EOS(STATIC_1170), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734) → 1177_0_findDups_JMP(EOS(STATIC_1177), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, +(i734, 1)) | &&(>=(i734, 0), =(matching1, -1))
1177_0_findDups_JMP(EOS(STATIC_1177), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i943) → 1184_0_findDups_Load(EOS(STATIC_1184), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i943) | =(matching1, -1)
1184_0_findDups_Load(EOS(STATIC_1184), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i943) → 1032_0_findDups_Load(EOS(STATIC_1032), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i943) | =(matching1, -1)
1126_0_findDups_EQ(EOS(STATIC_1126), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, matching3) → 1132_0_findDups_Inc(EOS(STATIC_1132), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734, i743) | &&(&&(=(matching1, -1), =(matching2, -1)), =(matching3, -1))
1127_0_findDups_EQ(EOS(STATIC_1127), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), matching1, i734, i743, matching2, i816) → 1133_0_findDups_Load(EOS(STATIC_1133), java.lang.Object(ARRAY(i2)), java.lang.Object(ARRAY(i2)), -1, i734) | &&(&&(!(=(-1, i816)), =(matching1, -1)), =(matching2, -1))
R rules:
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), -1, x2, x3, x3, x0) → 1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), -1, +(x2, 1), +(x2, 2), +(x2, 2), x0) | &&(&&(>=(x3, x0), >(+(x0, 1), 0)), >(x0, +(x2, 1)))
1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), -1, x2, x3, x3, x0) → 1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), -1, +(x2, 1), x3, x3, x0) | &&(&&(&&(<(x3, x0), >(+(x2, 1), 0)), <(x2, x0)), >(+(x0, 1), 0))
1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), -1, x2, x3, x3, x0) → 1048_0_findDups_GE(EOS(STATIC_1048), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), -1, +(x2, 1), +(x2, 2), +(x2, 2), x0) | &&(&&(&&(<(x3, x0), >(+(x2, 1), 0)), >(+(x0, 1), 0)), >(x0, +(x2, 1)))
R rules:
Filtered ground terms:
1048_0_findDups_GE(x1, x2, x3, x4, x5, x6, x7, x8) → 1048_0_findDups_GE(x2, x3, x5, x6, x7, x8)
EOS(x1) → EOS
Cond_1048_0_findDups_GE2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1048_0_findDups_GE2(x1, x3, x4, x6, x7, x8, x9)
Cond_1048_0_findDups_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1048_0_findDups_GE1(x1, x3, x4, x6, x7, x8, x9)
Cond_1048_0_findDups_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1048_0_findDups_GE(x1, x3, x4, x6, x7, x8, x9)
Filtered duplicate args:
1048_0_findDups_GE(x1, x2, x3, x4, x5, x6) → 1048_0_findDups_GE(x2, x3, x5)
Cond_1048_0_findDups_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_1048_0_findDups_GE(x1, x3, x4, x6)
Cond_1048_0_findDups_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_1048_0_findDups_GE1(x1, x3, x4, x6)
Cond_1048_0_findDups_GE2(x1, x2, x3, x4, x5, x6, x7) → Cond_1048_0_findDups_GE2(x1, x3, x4, x6)
Filtered unneeded arguments:
Cond_1048_0_findDups_GE(x1, x2, x3, x4) → Cond_1048_0_findDups_GE(x1, x2, x3)
Cond_1048_0_findDups_GE2(x1, x2, x3, x4) → Cond_1048_0_findDups_GE2(x1, x2, x3)
Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.
P rules:
1048_0_findDups_GE(java.lang.Object(ARRAY(x0)), x2, x3) → 1048_0_findDups_GE(java.lang.Object(ARRAY(x0)), +(x2, 1), +(x2, 2)) | &&(&&(>=(x3, x0), >(x0, -1)), >(x0, +(x2, 1)))
1048_0_findDups_GE(java.lang.Object(ARRAY(x0)), x2, x3) → 1048_0_findDups_GE(java.lang.Object(ARRAY(x0)), +(x2, 1), x3) | &&(&&(&&(<(x3, x0), >(x2, -1)), <(x2, x0)), >(x0, -1))
1048_0_findDups_GE(java.lang.Object(ARRAY(x0)), x2, x3) → 1048_0_findDups_GE(java.lang.Object(ARRAY(x0)), +(x2, 1), +(x2, 2)) | &&(&&(&&(<(x3, x0), >(x2, -1)), >(x0, -1)), >(x0, +(x2, 1)))
R rules:
Finished conversion. Obtained 6 rules for P and 0 rules for R. System has predefined symbols.
P rules:
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0)), x2, x3) → COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3, x0), >(x0, -1)), >(x0, +(x2, 1))), java.lang.Object(ARRAY(x0)), x2, x3)
COND_1048_0_FINDDUPS_GE(TRUE, java.lang.Object(ARRAY(x0)), x2, x3) → 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0)), +(x2, 1), +(x2, 2))
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0)), x2, x3) → COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3, x0), >(x2, -1)), <(x2, x0)), >(x0, -1)), java.lang.Object(ARRAY(x0)), x2, x3)
COND_1048_0_FINDDUPS_GE1(TRUE, java.lang.Object(ARRAY(x0)), x2, x3) → 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0)), +(x2, 1), x3)
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0)), x2, x3) → COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3, x0), >(x2, -1)), >(x0, -1)), >(x0, +(x2, 1))), java.lang.Object(ARRAY(x0)), x2, x3)
COND_1048_0_FINDDUPS_GE2(TRUE, java.lang.Object(ARRAY(x0)), x2, x3) → 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0)), +(x2, 1), +(x2, 2))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Boolean, Integer
(0) -> (1), if (x3[0] >= x0[0] && x0[0] > -1 && x0[0] > x2[0] + 1 ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧x2[0] →* x2[1]∧x3[0] →* x3[1])
(1) -> (0), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[0]))∧x2[1] + 1 →* x2[0]∧x2[1] + 2 →* x3[0])
(1) -> (2), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[2]))∧x2[1] + 1 →* x2[2]∧x2[1] + 2 →* x3[2])
(1) -> (4), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[4]))∧x2[1] + 1 →* x2[4]∧x2[1] + 2 →* x3[4])
(2) -> (3), if (x3[2] < x0[2] && x2[2] > -1 && x2[2] < x0[2] && x0[2] > -1 ∧java.lang.Object(ARRAY(x0[2])) →* java.lang.Object(ARRAY(x0[3]))∧x2[2] →* x2[3]∧x3[2] →* x3[3])
(3) -> (0), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[0]))∧x2[3] + 1 →* x2[0]∧x3[3] →* x3[0])
(3) -> (2), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[2]))∧x2[3] + 1 →* x2[2]∧x3[3] →* x3[2])
(3) -> (4), if (java.lang.Object(ARRAY(x0[3])) →* java.lang.Object(ARRAY(x0[4]))∧x2[3] + 1 →* x2[4]∧x3[3] →* x3[4])
(4) -> (5), if (x3[4] < x0[4] && x2[4] > -1 && x0[4] > -1 && x0[4] > x2[4] + 1 ∧java.lang.Object(ARRAY(x0[4])) →* java.lang.Object(ARRAY(x0[5]))∧x2[4] →* x2[5]∧x3[4] →* x3[5])
(5) -> (0), if (java.lang.Object(ARRAY(x0[5])) →* java.lang.Object(ARRAY(x0[0]))∧x2[5] + 1 →* x2[0]∧x2[5] + 2 →* x3[0])
(5) -> (2), if (java.lang.Object(ARRAY(x0[5])) →* java.lang.Object(ARRAY(x0[2]))∧x2[5] + 1 →* x2[2]∧x2[5] + 2 →* x3[2])
(5) -> (4), if (java.lang.Object(ARRAY(x0[5])) →* java.lang.Object(ARRAY(x0[4]))∧x2[5] + 1 →* x2[4]∧x2[5] + 2 →* x3[4])
(1) (&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1)))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧x2[0]=x2[1]∧x3[0]=x3[1] ⇒ 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])≥NonInfC∧1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])≥COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥))
(2) (>(x0[0], +(x2[0], 1))=TRUE∧>=(x3[0], x0[0])=TRUE∧>(x0[0], -1)=TRUE ⇒ 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])≥NonInfC∧1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])≥COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])∧(UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥))
(3) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x3[0] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(4) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x3[0] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(5) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x3[0] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(6) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x3[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]x0[0] + [(-1)bni_14]x2[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(7) (x0[0] + [-2] + [-1]x2[0] ≥ 0∧x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]x0[0] + [(-1)bni_14]x2[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(8) (x0[0] + [-2] + x2[0] ≥ 0∧x3[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]x0[0] + [bni_14]x2[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(9) (x0[0] ≥ 0∧x3[0] ≥ 0∧[2] + x2[0] + x0[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])), ≥)∧[(3)bni_14 + (-1)Bound*bni_14] + [bni_14]x2[0] + [(2)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(10) (COND_1048_0_FINDDUPS_GE(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x3[1])≥NonInfC∧COND_1048_0_FINDDUPS_GE(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x3[1])≥1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))∧(UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))), ≥))
(11) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)
(12) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)
(13) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))), ≥)∧[bni_16] = 0∧[1 + (-1)bso_17] ≥ 0)
(14) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))), ≥)∧[bni_16] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_17] ≥ 0)
(15) (&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1))=TRUE∧java.lang.Object(ARRAY(x0[2]))=java.lang.Object(ARRAY(x0[3]))∧x2[2]=x2[3]∧x3[2]=x3[3] ⇒ 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])≥NonInfC∧1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])≥COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])∧(UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥))
(16) (>(x0[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE∧<(x3[2], x0[2])=TRUE∧>(x2[2], -1)=TRUE ⇒ 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])≥NonInfC∧1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])≥COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])∧(UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥))
(17) (x0[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] + [-1] + [-1]x3[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(18) (x0[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] + [-1] + [-1]x3[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(19) (x0[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] + [-1] + [-1]x3[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥)∧[(-1)bni_18 + (-1)Bound*bni_18] + [(-1)bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(20) ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x2[2] + x0[2] + [-1]x3[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(21) ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x2[2] + x0[2] + x3[2] ≥ 0∧x2[2] ≥ 0∧x3[2] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(22) ([1] + x2[2] + x0[2] ≥ 0∧x0[2] ≥ 0∧x2[2] + x0[2] + [-1]x3[2] ≥ 0∧x2[2] ≥ 0∧x3[2] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x2[2] + [(2)bni_18]x0[2] ≥ 0∧[(-1)bso_19] ≥ 0)
(23) (COND_1048_0_FINDDUPS_GE1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x3[3])≥NonInfC∧COND_1048_0_FINDDUPS_GE1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x3[3])≥1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])∧(UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])), ≥))
(24) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])), ≥)∧[bni_20] = 0∧[1 + (-1)bso_21] ≥ 0)
(25) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])), ≥)∧[bni_20] = 0∧[1 + (-1)bso_21] ≥ 0)
(26) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])), ≥)∧[bni_20] = 0∧[1 + (-1)bso_21] ≥ 0)
(27) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])), ≥)∧[bni_20] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_21] ≥ 0)
(28) (&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1)))=TRUE∧java.lang.Object(ARRAY(x0[4]))=java.lang.Object(ARRAY(x0[5]))∧x2[4]=x2[5]∧x3[4]=x3[5] ⇒ 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])≥NonInfC∧1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])≥COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])∧(UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥))
(29) (>(x0[4], +(x2[4], 1))=TRUE∧>(x0[4], -1)=TRUE∧<(x3[4], x0[4])=TRUE∧>(x2[4], -1)=TRUE ⇒ 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])≥NonInfC∧1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])≥COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])∧(UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥))
(30) (x0[4] + [-2] + [-1]x2[4] ≥ 0∧x0[4] ≥ 0∧x0[4] + [-1] + [-1]x3[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x2[4] + [(2)bni_22]x0[4] ≥ 0∧[(-1)bso_23] ≥ 0)
(31) (x0[4] + [-2] + [-1]x2[4] ≥ 0∧x0[4] ≥ 0∧x0[4] + [-1] + [-1]x3[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x2[4] + [(2)bni_22]x0[4] ≥ 0∧[(-1)bso_23] ≥ 0)
(32) (x0[4] + [-2] + [-1]x2[4] ≥ 0∧x0[4] ≥ 0∧x0[4] + [-1] + [-1]x3[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x2[4] + [(2)bni_22]x0[4] ≥ 0∧[(-1)bso_23] ≥ 0)
(33) (x0[4] ≥ 0∧[2] + x2[4] + x0[4] ≥ 0∧[1] + x2[4] + x0[4] + [-1]x3[4] ≥ 0∧x2[4] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[4] + [(2)bni_22]x0[4] ≥ 0∧[(-1)bso_23] ≥ 0)
(34) (x0[4] ≥ 0∧[2] + x2[4] + x0[4] ≥ 0∧[1] + x2[4] + x0[4] + [-1]x3[4] ≥ 0∧x2[4] ≥ 0∧x3[4] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[4] + [(2)bni_22]x0[4] ≥ 0∧[(-1)bso_23] ≥ 0)
(35) (x0[4] ≥ 0∧[2] + x2[4] + x0[4] ≥ 0∧[1] + x2[4] + x0[4] + x3[4] ≥ 0∧x2[4] ≥ 0∧x3[4] ≥ 0 ⇒ (UIncreasing(COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [bni_22]x2[4] + [(2)bni_22]x0[4] ≥ 0∧[(-1)bso_23] ≥ 0)
(36) (COND_1048_0_FINDDUPS_GE2(TRUE, java.lang.Object(ARRAY(x0[5])), x2[5], x3[5])≥NonInfC∧COND_1048_0_FINDDUPS_GE2(TRUE, java.lang.Object(ARRAY(x0[5])), x2[5], x3[5])≥1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))∧(UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))), ≥))
(37) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))), ≥)∧[bni_24] = 0∧[1 + (-1)bso_25] ≥ 0)
(38) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))), ≥)∧[bni_24] = 0∧[1 + (-1)bso_25] ≥ 0)
(39) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))), ≥)∧[bni_24] = 0∧[1 + (-1)bso_25] ≥ 0)
(40) ((UIncreasing(1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))), ≥)∧[bni_24] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1048_0_FINDDUPS_GE(x1, x2, x3)) = [-1] + [-1]x2 + [2]x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1)) = x1
POL(COND_1048_0_FINDDUPS_GE(x1, x2, x3, x4)) = [-1] + [-1]x3 + [2]x2
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(2) = [2]
POL(COND_1048_0_FINDDUPS_GE1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [2]x2
POL(<(x1, x2)) = [-1]
POL(COND_1048_0_FINDDUPS_GE2(x1, x2, x3, x4)) = [-1] + [-1]x3 + [2]x2
COND_1048_0_FINDDUPS_GE(TRUE, java.lang.Object(ARRAY(x0[1])), x2[1], x3[1]) → 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[1])), +(x2[1], 1), +(x2[1], 2))
COND_1048_0_FINDDUPS_GE1(TRUE, java.lang.Object(ARRAY(x0[3])), x2[3], x3[3]) → 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[3])), +(x2[3], 1), x3[3])
COND_1048_0_FINDDUPS_GE2(TRUE, java.lang.Object(ARRAY(x0[5])), x2[5], x3[5]) → 1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[5])), +(x2[5], 1), +(x2[5], 2))
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[0])), x2[0], x3[0]) → COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[2])), x2[2], x3[2]) → COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[4])), x2[4], x3[4]) → COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[0])), x2[0], x3[0]) → COND_1048_0_FINDDUPS_GE(&&(&&(>=(x3[0], x0[0]), >(x0[0], -1)), >(x0[0], +(x2[0], 1))), java.lang.Object(ARRAY(x0[0])), x2[0], x3[0])
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[2])), x2[2], x3[2]) → COND_1048_0_FINDDUPS_GE1(&&(&&(&&(<(x3[2], x0[2]), >(x2[2], -1)), <(x2[2], x0[2])), >(x0[2], -1)), java.lang.Object(ARRAY(x0[2])), x2[2], x3[2])
1048_0_FINDDUPS_GE(java.lang.Object(ARRAY(x0[4])), x2[4], x3[4]) → COND_1048_0_FINDDUPS_GE2(&&(&&(&&(<(x3[4], x0[4]), >(x2[4], -1)), >(x0[4], -1)), >(x0[4], +(x2[4], 1))), java.lang.Object(ARRAY(x0[4])), x2[4], x3[4])
!= | ~ | 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 31 rules for P and 0 rules for R.
P rules:
442_0_main_Load(EOS(STATIC_442), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161) → 443_0_main_ArrayLength(EOS(STATIC_443), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161, java.lang.Object(ARRAY(i2)))
443_0_main_ArrayLength(EOS(STATIC_443), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161, java.lang.Object(ARRAY(i2))) → 444_0_main_GE(EOS(STATIC_444), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161, i2) | >=(i2, 0)
444_0_main_GE(EOS(STATIC_444), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161, i2) → 446_0_main_GE(EOS(STATIC_446), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161, i2)
446_0_main_GE(EOS(STATIC_446), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161, i2) → 448_0_main_Load(EOS(STATIC_448), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161) | <(i161, i2)
448_0_main_Load(EOS(STATIC_448), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161) → 450_0_main_Load(EOS(STATIC_450), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)))
450_0_main_Load(EOS(STATIC_450), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2))) → 452_0_main_Load(EOS(STATIC_452), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161)
452_0_main_Load(EOS(STATIC_452), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161) → 454_0_main_Load(EOS(STATIC_454), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160)))
454_0_main_Load(EOS(STATIC_454), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160))) → 456_0_main_Load(EOS(STATIC_456), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160)), i161)
456_0_main_Load(EOS(STATIC_456), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160)), i161) → 458_0_main_ArrayLength(EOS(STATIC_458), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160)), i161, java.lang.Object(ARRAY(i160)))
458_0_main_ArrayLength(EOS(STATIC_458), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160)), i161, java.lang.Object(ARRAY(i160))) → 460_0_main_IntArithmetic(EOS(STATIC_460), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i160)), i161, i160) | >=(i160, 0)
460_0_main_IntArithmetic(EOS(STATIC_460), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), i161, i170) → 464_0_main_IntArithmetic(EOS(STATIC_464), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), i161, i170)
464_0_main_IntArithmetic(EOS(STATIC_464), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), i161, i170) → 469_0_main_ArrayAccess(EOS(STATIC_469), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), %(i161, i170))
469_0_main_ArrayAccess(EOS(STATIC_469), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), i171) → 473_0_main_ArrayAccess(EOS(STATIC_473), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), i171)
473_0_main_ArrayAccess(EOS(STATIC_473), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)), i171) → 478_0_main_InvokeMethod(EOS(STATIC_478), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, o189) | <(i171, i170)
478_0_main_InvokeMethod(EOS(STATIC_478), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(o195sub)) → 485_0_main_InvokeMethod(EOS(STATIC_485), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(o195sub))
485_0_main_InvokeMethod(EOS(STATIC_485), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(o195sub)) → 490_0_length_Load(EOS(STATIC_490), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(o195sub), java.lang.Object(o195sub))
490_0_length_Load(EOS(STATIC_490), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(o195sub), java.lang.Object(o195sub)) → 502_0_length_FieldAccess(EOS(STATIC_502), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(o195sub), java.lang.Object(o195sub))
502_0_length_FieldAccess(EOS(STATIC_502), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(java.lang.String(o206sub, i191)), java.lang.Object(java.lang.String(o206sub, i191))) → 507_0_length_FieldAccess(EOS(STATIC_507), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(java.lang.String(o206sub, i191)), java.lang.Object(java.lang.String(o206sub, i191))) | &&(>=(i191, 0), >=(i192, 0))
507_0_length_FieldAccess(EOS(STATIC_507), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(java.lang.String(o206sub, i191)), java.lang.Object(java.lang.String(o206sub, i191))) → 512_0_length_Return(EOS(STATIC_512), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(java.lang.String(o206sub, i191)))
512_0_length_Return(EOS(STATIC_512), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(java.lang.String(o206sub, i191))) → 520_0_main_Load(EOS(STATIC_520), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161)
520_0_main_Load(EOS(STATIC_520), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161) → 525_0_main_IntArithmetic(EOS(STATIC_525), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, i161)
525_0_main_IntArithmetic(EOS(STATIC_525), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, i161) → 530_0_main_Load(EOS(STATIC_530), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161)
530_0_main_Load(EOS(STATIC_530), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161) → 538_0_main_ArrayLength(EOS(STATIC_538), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170)))
538_0_main_ArrayLength(EOS(STATIC_538), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i170))) → 544_0_main_IntArithmetic(EOS(STATIC_544), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, i170) | >=(i170, 0)
544_0_main_IntArithmetic(EOS(STATIC_544), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161, i170) → 551_0_main_ArrayAccess(EOS(STATIC_551), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161)
551_0_main_ArrayAccess(EOS(STATIC_551), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161) → 560_0_main_ArrayAccess(EOS(STATIC_560), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161)
560_0_main_ArrayAccess(EOS(STATIC_560), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161, java.lang.Object(ARRAY(i2)), i161) → 567_0_main_Inc(EOS(STATIC_567), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161) | <(i161, i2)
567_0_main_Inc(EOS(STATIC_567), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i161) → 577_0_main_JMP(EOS(STATIC_577), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), +(i161, 1)) | >=(i161, 0)
577_0_main_JMP(EOS(STATIC_577), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i217) → 586_0_main_Load(EOS(STATIC_586), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i217)
586_0_main_Load(EOS(STATIC_586), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i217) → 441_0_main_Load(EOS(STATIC_441), java.lang.Object(ARRAY(i170)), java.lang.Object(ARRAY(i2)), i217)
441_0_main_Load(EOS(STATIC_441), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161) → 442_0_main_Load(EOS(STATIC_442), java.lang.Object(ARRAY(i160)), java.lang.Object(ARRAY(i2)), i161, i161)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
442_0_main_Load(EOS(STATIC_442), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), x2, x2) → 442_0_main_Load(EOS(STATIC_442), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), +(x2, 1), +(x2, 1)) | &&(&&(&&(&&(>(+(x2, 1), 0), <(x2, x1)), >(+(x1, 1), 0)), >(+(x0, 1), 0)), >(x0, %(x2, x0)))
R rules:
Filtered ground terms:
442_0_main_Load(x1, x2, x3, x4, x5) → 442_0_main_Load(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_442_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_442_0_main_Load(x1, x3, x4, x5, x6)
Filtered duplicate args:
442_0_main_Load(x1, x2, x3, x4) → 442_0_main_Load(x1, x2, x4)
Cond_442_0_main_Load(x1, x2, x3, x4, x5) → Cond_442_0_main_Load(x1, x2, x3, x5)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
442_0_main_Load(java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), x2) → 442_0_main_Load(java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), +(x2, 1)) | &&(&&(&&(&&(>(x2, -1), <(x2, x1)), >(x1, -1)), >(x0, -1)), >(x0, %(x2, x0)))
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), x2) → COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2, -1), <(x2, x1)), >(x1, -1)), >(x0, -1)), >(x0, %(x2, x0))), java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), x2)
COND_442_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), x2) → 442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x1)), +(x2, 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 (x2[0] > -1 && x2[0] < x1[0] && x1[0] > -1 && x0[0] > -1 && x0[0] > x2[0] % x0[0] ∧java.lang.Object(ARRAY(x0[0])) →* java.lang.Object(ARRAY(x0[1]))∧java.lang.Object(ARRAY(x1[0])) →* java.lang.Object(ARRAY(x1[1]))∧x2[0] →* x2[1])
(1) -> (0), if (java.lang.Object(ARRAY(x0[1])) →* java.lang.Object(ARRAY(x0[0]))∧java.lang.Object(ARRAY(x1[1])) →* java.lang.Object(ARRAY(x1[0]))∧x2[1] + 1 →* x2[0])
(1) (&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0])))=TRUE∧java.lang.Object(ARRAY(x0[0]))=java.lang.Object(ARRAY(x0[1]))∧java.lang.Object(ARRAY(x1[0]))=java.lang.Object(ARRAY(x1[1]))∧x2[0]=x2[1] ⇒ 442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])≥NonInfC∧442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])≥COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])∧(UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥))
(2) (>(x0[0], %(x2[0], x0[0]))=TRUE∧>(x0[0], -1)=TRUE∧>(x1[0], -1)=TRUE∧>(x2[0], -1)=TRUE∧<(x2[0], x1[0])=TRUE ⇒ 442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])≥NonInfC∧442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])≥COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])∧(UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥))
(3) (x0[0] + [-1] + [-1]min{x0[0], [-1]x0[0]} ≥ 0∧x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(-1)bni_11]x2[0] + [(2)bni_11]x1[0] + [bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)
(4) (x0[0] + [-1] + [-1]min{x0[0], [-1]x0[0]} ≥ 0∧x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(-1)bni_11]x2[0] + [(2)bni_11]x1[0] + [bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)
(5) (x0[0] ≥ 0∧x1[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + [-1] + [-1]x2[0] ≥ 0∧[2]x0[0] ≥ 0∧[2]x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(-1)bni_11]x2[0] + [(2)bni_11]x1[0] + [bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)
(6) (x0[0] ≥ 0∧[1] + x2[0] + x1[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0∧[2]x0[0] ≥ 0∧[2]x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥)∧[bni_11 + (-1)Bound*bni_11] + [bni_11]x2[0] + [(2)bni_11]x1[0] + [bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)
(7) (x0[0] ≥ 0∧[1] + x2[0] + x1[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0∧[2]x0[0] + [-1] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])), ≥)∧[bni_11 + (-1)Bound*bni_11] + [bni_11]x2[0] + [(2)bni_11]x1[0] + [bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)
(8) (COND_442_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), x2[1])≥NonInfC∧COND_442_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), x2[1])≥442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))∧(UIncreasing(442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))), ≥))
(9) ((UIncreasing(442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))), ≥)∧[bni_13] = 0∧[1 + (-1)bso_14] ≥ 0)
(10) ((UIncreasing(442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))), ≥)∧[bni_13] = 0∧[1 + (-1)bso_14] ≥ 0)
(11) ((UIncreasing(442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))), ≥)∧[bni_13] = 0∧[1 + (-1)bso_14] ≥ 0)
(12) ((UIncreasing(442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))), ≥)∧[bni_13] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(442_0_MAIN_LOAD(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1)) = x1
POL(COND_442_0_MAIN_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x4 + [2]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(<(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(TermCSAR-Mode @ Context)
POL(%(x1, x0[0])-1 @ {}) = min{x2, [-1]x2}
COND_442_0_MAIN_LOAD(TRUE, java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), x2[1]) → 442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[1])), java.lang.Object(ARRAY(x1[1])), +(x2[1], 1))
442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0]) → COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0])
442_0_MAIN_LOAD(java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[0]) → COND_442_0_MAIN_LOAD(&&(&&(&&(&&(>(x2[0], -1), <(x2[0], x1[0])), >(x1[0], -1)), >(x0[0], -1)), >(x0[0], %(x2[0], x0[0]))), java.lang.Object(ARRAY(x0[0])), java.lang.Object(ARRAY(x1[0])), x2[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