0 JBC
↳1 JBCToGraph (⇒, 530 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 1540 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 660 ms)
↳9 IDP
↳10 IDependencyGraphProof (⇔, 0 ms)
↳11 TRUE
↳12 JBCTerminationSCC
↳13 SCCToIDPv1Proof (⇒, 130 ms)
↳14 IDP
↳15 IDPtoQDPProof (⇒, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES
↳19 JBCTerminationSCC
↳20 SCCToIDPv1Proof (⇒, 120 ms)
↳21 IDP
↳22 IDPNonInfProof (⇒, 150 ms)
↳23 AND
↳24 IDP
↳25 IDependencyGraphProof (⇔, 0 ms)
↳26 TRUE
↳27 IDP
↳28 IDependencyGraphProof (⇔, 0 ms)
↳29 TRUE
↳30 JBCTerminationSCC
↳31 SCCToIDPv1Proof (⇒, 2190 ms)
↳32 IDP
↳33 IDPNonInfProof (⇒, 2260 ms)
↳34 IDP
↳35 IDependencyGraphProof (⇔, 0 ms)
↳36 IDP
↳37 UsableRulesProof (⇔, 0 ms)
↳38 IDP
↳39 IDPNonInfProof (⇒, 320 ms)
↳40 AND
↳41 IDP
↳42 IDependencyGraphProof (⇔, 0 ms)
↳43 TRUE
↳44 IDP
↳45 IDependencyGraphProof (⇔, 0 ms)
↳46 TRUE
public class Test7 {
public static void main(String[] args) {
List[] ls = { List.mk(args.length), List.mk(args.length), List.mk(args.length) };
for (int k = 0; k < ls.length; k++) {
int len = length(ls[0]);
for (int i = 0; i < len; i++)
bubble(ls[0]);
}
}
private static void bubble(List l) {
for (List cursor = l; cursor != null && cursor.getTail() != null; cursor = cursor.getTail())
if (cursor.head > cursor.getTail().head) {
int temp = cursor.head;
cursor.head = cursor.getTail().head;
cursor.getTail().head = temp;
}
}
private static int length(List list) {
int len = 0;
while (list != null) {
list = list.getTail();
len++;
}
return len;
}
}
public class List {
public int head;
private List tail;
public List(int head, List tail) {
this.head = head;
this.tail = tail;
}
public List getTail() {
return tail;
}
public static List mk(int len) {
List result = null;
while (len-- > 0)
result = new List(len, result);
return result;
}
}
Generated 131 rules for P and 0 rules for R.
P rules:
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1630_0_bubble_NULL(EOS(STATIC_1630), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1630_0_bubble_NULL(EOS(STATIC_1630), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1633_0_bubble_Load(EOS(STATIC_1633), java.lang.Object(o1109sub))
1633_0_bubble_Load(EOS(STATIC_1633), java.lang.Object(o1109sub)) → 1636_0_bubble_InvokeMethod(EOS(STATIC_1636), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1636_0_bubble_InvokeMethod(EOS(STATIC_1636), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1638_0_getTail_Load(EOS(STATIC_1638), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1638_0_getTail_Load(EOS(STATIC_1638), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1645_0_getTail_FieldAccess(EOS(STATIC_1645), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1645_0_getTail_FieldAccess(EOS(STATIC_1645), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1647_0_getTail_FieldAccess(EOS(STATIC_1647), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1645_0_getTail_FieldAccess(EOS(STATIC_1645), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1648_0_getTail_FieldAccess(EOS(STATIC_1648), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1647_0_getTail_FieldAccess(EOS(STATIC_1647), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316))) → 1649_0_getTail_FieldAccess(EOS(STATIC_1649), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316)))
1649_0_getTail_FieldAccess(EOS(STATIC_1649), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316))) → 1652_0_getTail_Return(EOS(STATIC_1652), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316)), o1116)
1652_0_getTail_Return(EOS(STATIC_1652), java.lang.Object(List(EOC, o1116, i316)), java.lang.Object(List(EOC, o1116, i316)), o1116) → 1656_0_bubble_NULL(EOS(STATIC_1656), java.lang.Object(List(EOC, o1116, i316)), o1116)
1656_0_bubble_NULL(EOS(STATIC_1656), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(o1126sub)) → 1660_0_bubble_NULL(EOS(STATIC_1660), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(o1126sub))
1660_0_bubble_NULL(EOS(STATIC_1660), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(o1126sub)) → 1665_0_bubble_Load(EOS(STATIC_1665), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)))
1665_0_bubble_Load(EOS(STATIC_1665), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316))) → 1671_0_bubble_FieldAccess(EOS(STATIC_1671), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)))
1671_0_bubble_FieldAccess(EOS(STATIC_1671), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316))) → 1677_0_bubble_Load(EOS(STATIC_1677), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316)
1677_0_bubble_Load(EOS(STATIC_1677), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316) → 1683_0_bubble_InvokeMethod(EOS(STATIC_1683), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)))
1683_0_bubble_InvokeMethod(EOS(STATIC_1683), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316))) → 1693_0_getTail_Load(EOS(STATIC_1693), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)))
1693_0_getTail_Load(EOS(STATIC_1693), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316))) → 1696_0_getTail_FieldAccess(EOS(STATIC_1696), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)))
1696_0_getTail_FieldAccess(EOS(STATIC_1696), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316))) → 1700_0_getTail_Return(EOS(STATIC_1700), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(o1126sub))
1700_0_getTail_Return(EOS(STATIC_1700), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), java.lang.Object(o1126sub)) → 1703_0_bubble_FieldAccess(EOS(STATIC_1703), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(o1126sub))
1703_0_bubble_FieldAccess(EOS(STATIC_1703), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(o1126sub)) → 1707_0_bubble_FieldAccess(EOS(STATIC_1707), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(o1126sub))
1703_0_bubble_FieldAccess(EOS(STATIC_1703), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(o1126sub)) → 1708_0_bubble_FieldAccess(EOS(STATIC_1708), java.lang.Object(List(EOC, java.lang.Object(o1126sub), i316)), i316, java.lang.Object(o1126sub))
1707_0_bubble_FieldAccess(EOS(STATIC_1707), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, o1169, i320))) → 1711_0_bubble_FieldAccess(EOS(STATIC_1711), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, o1169, i320)))
1711_0_bubble_FieldAccess(EOS(STATIC_1711), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, o1169, i320))) → 1717_0_bubble_LE(EOS(STATIC_1717), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320)
1717_0_bubble_LE(EOS(STATIC_1717), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320) → 1724_0_bubble_LE(EOS(STATIC_1724), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320)
1717_0_bubble_LE(EOS(STATIC_1717), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320) → 1725_0_bubble_LE(EOS(STATIC_1725), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320)
1724_0_bubble_LE(EOS(STATIC_1724), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320) → 1732_0_bubble_Load(EOS(STATIC_1732), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) | <=(i316, i320)
1732_0_bubble_Load(EOS(STATIC_1732), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1894_0_bubble_Load(EOS(STATIC_1894), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)))
1894_0_bubble_Load(EOS(STATIC_1894), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320))) → 1902_0_bubble_InvokeMethod(EOS(STATIC_1902), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)))
1902_0_bubble_InvokeMethod(EOS(STATIC_1902), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320))) → 1907_0_getTail_Load(EOS(STATIC_1907), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)))
1907_0_getTail_Load(EOS(STATIC_1907), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320))) → 1917_0_getTail_FieldAccess(EOS(STATIC_1917), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)))
1917_0_getTail_FieldAccess(EOS(STATIC_1917), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320))) → 1928_0_getTail_Return(EOS(STATIC_1928), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)), java.lang.Object(List(EOC, o1169, i316)))
1928_0_getTail_Return(EOS(STATIC_1928), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)), java.lang.Object(List(EOC, o1169, i316))) → 1936_0_bubble_Store(EOS(STATIC_1936), java.lang.Object(List(EOC, o1169, i316)))
1936_0_bubble_Store(EOS(STATIC_1936), java.lang.Object(List(EOC, o1169, i316))) → 1939_0_bubble_JMP(EOS(STATIC_1939), java.lang.Object(List(EOC, o1169, i316)))
1939_0_bubble_JMP(EOS(STATIC_1939), java.lang.Object(List(EOC, o1169, i316))) → 1942_0_bubble_Load(EOS(STATIC_1942), java.lang.Object(List(EOC, o1169, i316)))
1942_0_bubble_Load(EOS(STATIC_1942), java.lang.Object(List(EOC, o1169, i316))) → 1626_0_bubble_Load(EOS(STATIC_1626), java.lang.Object(List(EOC, o1169, i316)))
1626_0_bubble_Load(EOS(STATIC_1626), o1104) → 1629_0_bubble_NULL(EOS(STATIC_1629), o1104, o1104)
1725_0_bubble_LE(EOS(STATIC_1725), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, i320) → 1734_0_bubble_Load(EOS(STATIC_1734), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) | >(i316, i320)
1734_0_bubble_Load(EOS(STATIC_1734), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1744_0_bubble_FieldAccess(EOS(STATIC_1744), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)))
1744_0_bubble_FieldAccess(EOS(STATIC_1744), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1753_0_bubble_Store(EOS(STATIC_1753), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316)
1753_0_bubble_Store(EOS(STATIC_1753), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316) → 1760_0_bubble_Load(EOS(STATIC_1760), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316)
1760_0_bubble_Load(EOS(STATIC_1760), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316) → 1770_0_bubble_Load(EOS(STATIC_1770), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)))
1770_0_bubble_Load(EOS(STATIC_1770), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1782_0_bubble_InvokeMethod(EOS(STATIC_1782), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)))
1782_0_bubble_InvokeMethod(EOS(STATIC_1782), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1793_0_getTail_Load(EOS(STATIC_1793), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)))
1793_0_getTail_Load(EOS(STATIC_1793), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1808_0_getTail_FieldAccess(EOS(STATIC_1808), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)))
1808_0_getTail_FieldAccess(EOS(STATIC_1808), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316))) → 1819_0_getTail_Return(EOS(STATIC_1819), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, o1169, i320)))
1819_0_getTail_Return(EOS(STATIC_1819), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, o1169, i320))) → 1825_0_bubble_FieldAccess(EOS(STATIC_1825), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, o1169, i320)))
1825_0_bubble_FieldAccess(EOS(STATIC_1825), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), java.lang.Object(List(EOC, o1169, i320))) → 1829_0_bubble_FieldAccess(EOS(STATIC_1829), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i320)
1829_0_bubble_FieldAccess(EOS(STATIC_1829), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i316)), i320) → 1834_0_bubble_Load(EOS(STATIC_1834), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316)
1834_0_bubble_Load(EOS(STATIC_1834), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316) → 1839_0_bubble_InvokeMethod(EOS(STATIC_1839), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)))
1839_0_bubble_InvokeMethod(EOS(STATIC_1839), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320))) → 1844_0_getTail_Load(EOS(STATIC_1844), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)))
1844_0_getTail_Load(EOS(STATIC_1844), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320))) → 1854_0_getTail_FieldAccess(EOS(STATIC_1854), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)))
1854_0_getTail_FieldAccess(EOS(STATIC_1854), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320))) → 1866_0_getTail_Return(EOS(STATIC_1866), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, o1169, i320)))
1866_0_getTail_Return(EOS(STATIC_1866), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, o1169, i320))) → 1875_0_bubble_Load(EOS(STATIC_1875), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, o1169, i320)))
1875_0_bubble_Load(EOS(STATIC_1875), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), i316, java.lang.Object(List(EOC, o1169, i320))) → 1881_0_bubble_FieldAccess(EOS(STATIC_1881), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, o1169, i320)), i316)
1881_0_bubble_FieldAccess(EOS(STATIC_1881), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i320)), i320)), java.lang.Object(List(EOC, o1169, i320)), i316) → 1894_0_bubble_Load(EOS(STATIC_1894), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1169, i316)), i320)))
1708_0_bubble_FieldAccess(EOS(STATIC_1708), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, o1171, i321))) → 1713_0_bubble_FieldAccess(EOS(STATIC_1713), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, o1171, i321)))
1713_0_bubble_FieldAccess(EOS(STATIC_1713), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, o1171, i321))) → 1720_0_bubble_LE(EOS(STATIC_1720), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321)
1720_0_bubble_LE(EOS(STATIC_1720), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321) → 1727_0_bubble_LE(EOS(STATIC_1727), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321)
1720_0_bubble_LE(EOS(STATIC_1720), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321) → 1728_0_bubble_LE(EOS(STATIC_1728), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321)
1727_0_bubble_LE(EOS(STATIC_1727), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321) → 1736_0_bubble_Load(EOS(STATIC_1736), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) | <=(i316, i321)
1736_0_bubble_Load(EOS(STATIC_1736), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1898_0_bubble_Load(EOS(STATIC_1898), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)))
1898_0_bubble_Load(EOS(STATIC_1898), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321))) → 1904_0_bubble_InvokeMethod(EOS(STATIC_1904), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)))
1904_0_bubble_InvokeMethod(EOS(STATIC_1904), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321))) → 1908_0_getTail_Load(EOS(STATIC_1908), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)))
1908_0_getTail_Load(EOS(STATIC_1908), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321))) → 1922_0_getTail_FieldAccess(EOS(STATIC_1922), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)))
1922_0_getTail_FieldAccess(EOS(STATIC_1922), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321))) → 1933_0_getTail_Return(EOS(STATIC_1933), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)), java.lang.Object(List(EOC, o1171, i316)))
1933_0_getTail_Return(EOS(STATIC_1933), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)), java.lang.Object(List(EOC, o1171, i316))) → 1938_0_bubble_Store(EOS(STATIC_1938), java.lang.Object(List(EOC, o1171, i316)))
1938_0_bubble_Store(EOS(STATIC_1938), java.lang.Object(List(EOC, o1171, i316))) → 1940_0_bubble_JMP(EOS(STATIC_1940), java.lang.Object(List(EOC, o1171, i316)))
1940_0_bubble_JMP(EOS(STATIC_1940), java.lang.Object(List(EOC, o1171, i316))) → 1944_0_bubble_Load(EOS(STATIC_1944), java.lang.Object(List(EOC, o1171, i316)))
1944_0_bubble_Load(EOS(STATIC_1944), java.lang.Object(List(EOC, o1171, i316))) → 1626_0_bubble_Load(EOS(STATIC_1626), java.lang.Object(List(EOC, o1171, i316)))
1728_0_bubble_LE(EOS(STATIC_1728), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, i321) → 1738_0_bubble_Load(EOS(STATIC_1738), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) | >(i316, i321)
1738_0_bubble_Load(EOS(STATIC_1738), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1747_0_bubble_FieldAccess(EOS(STATIC_1747), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)))
1747_0_bubble_FieldAccess(EOS(STATIC_1747), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1757_0_bubble_Store(EOS(STATIC_1757), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316)
1757_0_bubble_Store(EOS(STATIC_1757), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316) → 1762_0_bubble_Load(EOS(STATIC_1762), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316)
1762_0_bubble_Load(EOS(STATIC_1762), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316) → 1774_0_bubble_Load(EOS(STATIC_1774), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)))
1774_0_bubble_Load(EOS(STATIC_1774), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1787_0_bubble_InvokeMethod(EOS(STATIC_1787), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)))
1787_0_bubble_InvokeMethod(EOS(STATIC_1787), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1796_0_getTail_Load(EOS(STATIC_1796), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)))
1796_0_getTail_Load(EOS(STATIC_1796), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1813_0_getTail_FieldAccess(EOS(STATIC_1813), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)))
1813_0_getTail_FieldAccess(EOS(STATIC_1813), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316))) → 1822_0_getTail_Return(EOS(STATIC_1822), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, o1171, i321)))
1822_0_getTail_Return(EOS(STATIC_1822), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, o1171, i321))) → 1826_0_bubble_FieldAccess(EOS(STATIC_1826), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, o1171, i321)))
1826_0_bubble_FieldAccess(EOS(STATIC_1826), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), java.lang.Object(List(EOC, o1171, i321))) → 1831_0_bubble_FieldAccess(EOS(STATIC_1831), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i321)
1831_0_bubble_FieldAccess(EOS(STATIC_1831), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i316)), i321) → 1835_0_bubble_Load(EOS(STATIC_1835), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316)
1835_0_bubble_Load(EOS(STATIC_1835), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316) → 1841_0_bubble_InvokeMethod(EOS(STATIC_1841), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)))
1841_0_bubble_InvokeMethod(EOS(STATIC_1841), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321))) → 1845_0_getTail_Load(EOS(STATIC_1845), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)))
1845_0_getTail_Load(EOS(STATIC_1845), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321))) → 1858_0_getTail_FieldAccess(EOS(STATIC_1858), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)))
1858_0_getTail_FieldAccess(EOS(STATIC_1858), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321))) → 1871_0_getTail_Return(EOS(STATIC_1871), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, o1171, i321)))
1871_0_getTail_Return(EOS(STATIC_1871), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, o1171, i321))) → 1878_0_bubble_Load(EOS(STATIC_1878), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, o1171, i321)))
1878_0_bubble_Load(EOS(STATIC_1878), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), i316, java.lang.Object(List(EOC, o1171, i321))) → 1884_0_bubble_FieldAccess(EOS(STATIC_1884), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, o1171, i321)), i316)
1884_0_bubble_FieldAccess(EOS(STATIC_1884), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i321)), i321)), java.lang.Object(List(EOC, o1171, i321)), i316) → 1898_0_bubble_Load(EOS(STATIC_1898), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1171, i316)), i321)))
1648_0_getTail_FieldAccess(EOS(STATIC_1648), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317))) → 1651_0_getTail_FieldAccess(EOS(STATIC_1651), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317)))
1651_0_getTail_FieldAccess(EOS(STATIC_1651), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317))) → 1654_0_getTail_Return(EOS(STATIC_1654), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317)), o1118)
1654_0_getTail_Return(EOS(STATIC_1654), java.lang.Object(List(EOC, o1118, i317)), java.lang.Object(List(EOC, o1118, i317)), o1118) → 1658_0_bubble_NULL(EOS(STATIC_1658), java.lang.Object(List(EOC, o1118, i317)), o1118)
1658_0_bubble_NULL(EOS(STATIC_1658), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(o1127sub)) → 1662_0_bubble_NULL(EOS(STATIC_1662), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(o1127sub))
1662_0_bubble_NULL(EOS(STATIC_1662), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(o1127sub)) → 1668_0_bubble_Load(EOS(STATIC_1668), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)))
1668_0_bubble_Load(EOS(STATIC_1668), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317))) → 1674_0_bubble_FieldAccess(EOS(STATIC_1674), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)))
1674_0_bubble_FieldAccess(EOS(STATIC_1674), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317))) → 1680_0_bubble_Load(EOS(STATIC_1680), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317)
1680_0_bubble_Load(EOS(STATIC_1680), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317) → 1688_0_bubble_InvokeMethod(EOS(STATIC_1688), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)))
1688_0_bubble_InvokeMethod(EOS(STATIC_1688), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317))) → 1694_0_getTail_Load(EOS(STATIC_1694), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)))
1694_0_getTail_Load(EOS(STATIC_1694), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317))) → 1698_0_getTail_FieldAccess(EOS(STATIC_1698), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)))
1698_0_getTail_FieldAccess(EOS(STATIC_1698), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317))) → 1701_0_getTail_Return(EOS(STATIC_1701), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(o1127sub))
1701_0_getTail_Return(EOS(STATIC_1701), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), java.lang.Object(o1127sub)) → 1705_0_bubble_FieldAccess(EOS(STATIC_1705), java.lang.Object(List(EOC, java.lang.Object(o1127sub), i317)), i317, java.lang.Object(o1127sub))
1705_0_bubble_FieldAccess(EOS(STATIC_1705), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, o1167, i319))) → 1709_0_bubble_FieldAccess(EOS(STATIC_1709), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, o1167, i319)))
1709_0_bubble_FieldAccess(EOS(STATIC_1709), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, o1167, i319))) → 1715_0_bubble_LE(EOS(STATIC_1715), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319)
1715_0_bubble_LE(EOS(STATIC_1715), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319) → 1722_0_bubble_LE(EOS(STATIC_1722), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319)
1715_0_bubble_LE(EOS(STATIC_1715), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319) → 1723_0_bubble_LE(EOS(STATIC_1723), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319)
1722_0_bubble_LE(EOS(STATIC_1722), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319) → 1729_0_bubble_Load(EOS(STATIC_1729), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) | <=(i317, i319)
1729_0_bubble_Load(EOS(STATIC_1729), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1887_0_bubble_Load(EOS(STATIC_1887), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)))
1887_0_bubble_Load(EOS(STATIC_1887), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319))) → 1901_0_bubble_InvokeMethod(EOS(STATIC_1901), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)))
1901_0_bubble_InvokeMethod(EOS(STATIC_1901), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319))) → 1905_0_getTail_Load(EOS(STATIC_1905), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)))
1905_0_getTail_Load(EOS(STATIC_1905), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319))) → 1911_0_getTail_FieldAccess(EOS(STATIC_1911), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)))
1911_0_getTail_FieldAccess(EOS(STATIC_1911), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319))) → 1925_0_getTail_Return(EOS(STATIC_1925), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)), java.lang.Object(List(EOC, o1167, i317)))
1925_0_getTail_Return(EOS(STATIC_1925), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)), java.lang.Object(List(EOC, o1167, i317))) → 1934_0_bubble_Store(EOS(STATIC_1934), java.lang.Object(List(EOC, o1167, i317)))
1934_0_bubble_Store(EOS(STATIC_1934), java.lang.Object(List(EOC, o1167, i317))) → 1936_0_bubble_Store(EOS(STATIC_1936), java.lang.Object(List(EOC, o1167, i317)))
1723_0_bubble_LE(EOS(STATIC_1723), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, i319) → 1731_0_bubble_Load(EOS(STATIC_1731), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) | >(i317, i319)
1731_0_bubble_Load(EOS(STATIC_1731), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1740_0_bubble_FieldAccess(EOS(STATIC_1740), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)))
1740_0_bubble_FieldAccess(EOS(STATIC_1740), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1750_0_bubble_Store(EOS(STATIC_1750), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317)
1750_0_bubble_Store(EOS(STATIC_1750), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317) → 1758_0_bubble_Load(EOS(STATIC_1758), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317)
1758_0_bubble_Load(EOS(STATIC_1758), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317) → 1765_0_bubble_Load(EOS(STATIC_1765), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)))
1765_0_bubble_Load(EOS(STATIC_1765), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1777_0_bubble_InvokeMethod(EOS(STATIC_1777), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)))
1777_0_bubble_InvokeMethod(EOS(STATIC_1777), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1789_0_getTail_Load(EOS(STATIC_1789), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)))
1789_0_getTail_Load(EOS(STATIC_1789), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1801_0_getTail_FieldAccess(EOS(STATIC_1801), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)))
1801_0_getTail_FieldAccess(EOS(STATIC_1801), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317))) → 1816_0_getTail_Return(EOS(STATIC_1816), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, o1167, i319)))
1816_0_getTail_Return(EOS(STATIC_1816), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, o1167, i319))) → 1824_0_bubble_FieldAccess(EOS(STATIC_1824), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, o1167, i319)))
1824_0_bubble_FieldAccess(EOS(STATIC_1824), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), java.lang.Object(List(EOC, o1167, i319))) → 1828_0_bubble_FieldAccess(EOS(STATIC_1828), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i319)
1828_0_bubble_FieldAccess(EOS(STATIC_1828), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i317)), i319) → 1832_0_bubble_Load(EOS(STATIC_1832), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317)
1832_0_bubble_Load(EOS(STATIC_1832), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317) → 1837_0_bubble_InvokeMethod(EOS(STATIC_1837), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)))
1837_0_bubble_InvokeMethod(EOS(STATIC_1837), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319))) → 1842_0_getTail_Load(EOS(STATIC_1842), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)))
1842_0_getTail_Load(EOS(STATIC_1842), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319))) → 1849_0_getTail_FieldAccess(EOS(STATIC_1849), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)))
1849_0_getTail_FieldAccess(EOS(STATIC_1849), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319))) → 1862_0_getTail_Return(EOS(STATIC_1862), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, o1167, i319)))
1862_0_getTail_Return(EOS(STATIC_1862), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, o1167, i319))) → 1873_0_bubble_Load(EOS(STATIC_1873), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, o1167, i319)))
1873_0_bubble_Load(EOS(STATIC_1873), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), i317, java.lang.Object(List(EOC, o1167, i319))) → 1879_0_bubble_FieldAccess(EOS(STATIC_1879), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, o1167, i319)), i317)
1879_0_bubble_FieldAccess(EOS(STATIC_1879), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i319)), i319)), java.lang.Object(List(EOC, o1167, i319)), i317) → 1887_0_bubble_Load(EOS(STATIC_1887), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1167, i317)), i319)))
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, x0, x1))) | <=(x2, x1)
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC, x0, x2)), java.lang.Object(List(EOC, x0, x2))) | >(x2, x1)
R rules:
Filtered ground terms:
1629_0_bubble_NULL(x1, x2, x3) → 1629_0_bubble_NULL(x2, x3)
List(x1, x2, x3) → List(x2, x3)
EOS(x1) → EOS
Cond_1629_0_bubble_NULL1(x1, x2, x3, x4) → Cond_1629_0_bubble_NULL1(x1, x3, x4)
Cond_1629_0_bubble_NULL(x1, x2, x3, x4) → Cond_1629_0_bubble_NULL(x1, x3, x4)
Filtered duplicate args:
1629_0_bubble_NULL(x1, x2) → 1629_0_bubble_NULL(x2)
Cond_1629_0_bubble_NULL(x1, x2, x3) → Cond_1629_0_bubble_NULL(x1, x3)
Cond_1629_0_bubble_NULL1(x1, x2, x3) → Cond_1629_0_bubble_NULL1(x1, x3)
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
1629_0_bubble_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 1629_0_bubble_NULL(java.lang.Object(List(x0, x1))) | <=(x2, x1)
1629_0_bubble_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 1629_0_bubble_NULL(java.lang.Object(List(x0, x2))) | >(x2, x1)
R rules:
Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.
P rules:
1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_1629_0_BUBBLE_NULL(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 1629_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)))
1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_1629_0_BUBBLE_NULL1(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 1629_0_BUBBLE_NULL(java.lang.Object(List(x0, x2)))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x2[0] <= x1[0] ∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) →* java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))
(1) -> (0), if (java.lang.Object(List(x0[1], x1[1])) →* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
(1) -> (2), if (java.lang.Object(List(x0[1], x1[1])) →* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
(2) -> (3), if (x2[2] > x1[2] ∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) →* java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))
(3) -> (0), if (java.lang.Object(List(x0[3], x2[3])) →* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
(3) -> (2), if (java.lang.Object(List(x0[3], x2[3])) →* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
(1) (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])) ⇒ 1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥NonInfC∧1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))∧(UIncreasing(COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥))
(2) (<=(x2[0], x1[0])=TRUE ⇒ 1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥NonInfC∧1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))∧(UIncreasing(COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥))
(3) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(43)bni_14 + (-1)Bound*bni_14] + [(12)bni_14]x2[0] + [(72)bni_14]x1[0] + [(72)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(4) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(43)bni_14 + (-1)Bound*bni_14] + [(12)bni_14]x2[0] + [(72)bni_14]x1[0] + [(72)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(5) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(43)bni_14 + (-1)Bound*bni_14] + [(12)bni_14]x2[0] + [(72)bni_14]x1[0] + [(72)bni_14]x0[0] ≥ 0∧[(-1)bso_15] ≥ 0)
(6) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(12)bni_14] ≥ 0∧[(72)bni_14] ≥ 0∧[(72)bni_14] ≥ 0∧[(43)bni_14 + (-1)Bound*bni_14] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_15] ≥ 0)
(7) (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x2[0]1)) ⇒ COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))
(8) (<=(x2[0], x1[0])=TRUE ⇒ COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])), x2[0])))≥NonInfC∧COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])), x2[0])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))
(9) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(259)bni_16 + (-1)Bound*bni_16] + [(12)bni_16]x2[0] + [(72)bni_16]x1[0] + [(432)bni_16]x1[0]1 + [(432)bni_16]x0[0]1 ≥ 0∧[216 + (-1)bso_17] + [12]x2[0] + [60]x1[0] + [360]x1[0]1 + [360]x0[0]1 ≥ 0)
(10) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(259)bni_16 + (-1)Bound*bni_16] + [(12)bni_16]x2[0] + [(72)bni_16]x1[0] + [(432)bni_16]x1[0]1 + [(432)bni_16]x0[0]1 ≥ 0∧[216 + (-1)bso_17] + [12]x2[0] + [60]x1[0] + [360]x1[0]1 + [360]x0[0]1 ≥ 0)
(11) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(259)bni_16 + (-1)Bound*bni_16] + [(12)bni_16]x2[0] + [(72)bni_16]x1[0] + [(432)bni_16]x1[0]1 + [(432)bni_16]x0[0]1 ≥ 0∧[216 + (-1)bso_17] + [12]x2[0] + [60]x1[0] + [360]x1[0]1 + [360]x0[0]1 ≥ 0)
(12) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(12)bni_16] ≥ 0∧[(72)bni_16] ≥ 0∧[(432)bni_16] ≥ 0∧[(432)bni_16] ≥ 0∧[(259)bni_16 + (-1)Bound*bni_16] ≥ 0∧[216 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(13) (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) ⇒ COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))
(14) (<=(x2[0], x1[0])=TRUE ⇒ COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])), x2[0])))≥NonInfC∧COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])), x2[0])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))
(15) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(259)bni_16 + (-1)Bound*bni_16] + [(12)bni_16]x2[0] + [(72)bni_16]x1[0] + [(432)bni_16]x1[2] + [(432)bni_16]x0[2] ≥ 0∧[216 + (-1)bso_17] + [12]x2[0] + [60]x1[0] + [360]x1[2] + [360]x0[2] ≥ 0)
(16) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(259)bni_16 + (-1)Bound*bni_16] + [(12)bni_16]x2[0] + [(72)bni_16]x1[0] + [(432)bni_16]x1[2] + [(432)bni_16]x0[2] ≥ 0∧[216 + (-1)bso_17] + [12]x2[0] + [60]x1[0] + [360]x1[2] + [360]x0[2] ≥ 0)
(17) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(259)bni_16 + (-1)Bound*bni_16] + [(12)bni_16]x2[0] + [(72)bni_16]x1[0] + [(432)bni_16]x1[2] + [(432)bni_16]x0[2] ≥ 0∧[216 + (-1)bso_17] + [12]x2[0] + [60]x1[0] + [360]x1[2] + [360]x0[2] ≥ 0)
(18) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(12)bni_16] ≥ 0∧[(72)bni_16] ≥ 0∧[(432)bni_16] ≥ 0∧[(432)bni_16] ≥ 0∧[(259)bni_16 + (-1)Bound*bni_16] ≥ 0∧[216 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(19) (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])) ⇒ 1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥NonInfC∧1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))∧(UIncreasing(COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥))
(20) (>(x2[2], x1[2])=TRUE ⇒ 1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥NonInfC∧1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))∧(UIncreasing(COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥))
(21) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(43)bni_18 + (-1)Bound*bni_18] + [(12)bni_18]x2[2] + [(72)bni_18]x1[2] + [(72)bni_18]x0[2] ≥ 0∧[2 + (-1)bso_19] ≥ 0)
(22) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(43)bni_18 + (-1)Bound*bni_18] + [(12)bni_18]x2[2] + [(72)bni_18]x1[2] + [(72)bni_18]x0[2] ≥ 0∧[2 + (-1)bso_19] ≥ 0)
(23) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(43)bni_18 + (-1)Bound*bni_18] + [(12)bni_18]x2[2] + [(72)bni_18]x1[2] + [(72)bni_18]x0[2] ≥ 0∧[2 + (-1)bso_19] ≥ 0)
(24) (0 ≥ 0 ⇒ (UIncreasing(COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(12)bni_18] ≥ 0∧[(72)bni_18] ≥ 0∧[(72)bni_18] ≥ 0∧[(43)bni_18 + (-1)Bound*bni_18] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[2 + (-1)bso_19] ≥ 0)
(25) (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) ⇒ COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))
(26) (>(x2[2], x1[2])=TRUE ⇒ COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x1[2])), x2[2])))≥NonInfC∧COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x1[2])), x2[2])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[2])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))
(27) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(257)bni_20 + (-1)Bound*bni_20] + [(12)bni_20]x2[2] + [(72)bni_20]x1[2] + [(432)bni_20]x1[0] + [(432)bni_20]x0[0] ≥ 0∧[214 + (-1)bso_21] + [72]x1[2] + [360]x1[0] + [360]x0[0] ≥ 0)
(28) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(257)bni_20 + (-1)Bound*bni_20] + [(12)bni_20]x2[2] + [(72)bni_20]x1[2] + [(432)bni_20]x1[0] + [(432)bni_20]x0[0] ≥ 0∧[214 + (-1)bso_21] + [72]x1[2] + [360]x1[0] + [360]x0[0] ≥ 0)
(29) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(257)bni_20 + (-1)Bound*bni_20] + [(12)bni_20]x2[2] + [(72)bni_20]x1[2] + [(432)bni_20]x1[0] + [(432)bni_20]x0[0] ≥ 0∧[214 + (-1)bso_21] + [72]x1[2] + [360]x1[0] + [360]x0[0] ≥ 0)
(30) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(12)bni_20] ≥ 0∧[(72)bni_20] ≥ 0∧[(432)bni_20] ≥ 0∧[(432)bni_20] ≥ 0∧[(257)bni_20 + (-1)Bound*bni_20] ≥ 0∧0 ≥ 0∧[214 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
(31) (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x2[2]1)) ⇒ COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))
(32) (>(x2[2], x1[2])=TRUE ⇒ COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x1[2])), x2[2])))≥NonInfC∧COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x1[2])), x2[2])))≥1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x2[2])))∧(UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))
(33) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(257)bni_20 + (-1)Bound*bni_20] + [(12)bni_20]x2[2] + [(72)bni_20]x1[2] + [(432)bni_20]x1[2]1 + [(432)bni_20]x0[2]1 ≥ 0∧[214 + (-1)bso_21] + [72]x1[2] + [360]x1[2]1 + [360]x0[2]1 ≥ 0)
(34) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(257)bni_20 + (-1)Bound*bni_20] + [(12)bni_20]x2[2] + [(72)bni_20]x1[2] + [(432)bni_20]x1[2]1 + [(432)bni_20]x0[2]1 ≥ 0∧[214 + (-1)bso_21] + [72]x1[2] + [360]x1[2]1 + [360]x0[2]1 ≥ 0)
(35) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(257)bni_20 + (-1)Bound*bni_20] + [(12)bni_20]x2[2] + [(72)bni_20]x1[2] + [(432)bni_20]x1[2]1 + [(432)bni_20]x0[2]1 ≥ 0∧[214 + (-1)bso_21] + [72]x1[2] + [360]x1[2]1 + [360]x0[2]1 ≥ 0)
(36) (0 ≥ 0 ⇒ (UIncreasing(1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(12)bni_20] ≥ 0∧[(72)bni_20] ≥ 0∧[(432)bni_20] ≥ 0∧[(432)bni_20] ≥ 0∧[(257)bni_20 + (-1)Bound*bni_20] ≥ 0∧0 ≥ 0∧[214 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1629_0_BUBBLE_NULL(x1)) = [1] + [2]x1
POL(java.lang.Object(x1)) = [3] + [3]x1
POL(List(x1, x2)) = [2]x2 + [2]x1
POL(COND_1629_0_BUBBLE_NULL(x1, x2)) = [1] + [2]x2
POL(<=(x1, x2)) = 0
POL(COND_1629_0_BUBBLE_NULL1(x1, x2)) = [-1] + [2]x2
POL(>(x1, x2)) = 0
COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
COND_1629_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 1629_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_1629_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
COND_1629_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 1629_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
1629_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_1629_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], 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 |
Integer
Generated 22 rules for P and 0 rules for R.
P rules:
874_0_length_NULL(EOS(STATIC_874), java.lang.Object(o199sub), java.lang.Object(o199sub)) → 876_0_length_NULL(EOS(STATIC_876), java.lang.Object(o199sub), java.lang.Object(o199sub))
876_0_length_NULL(EOS(STATIC_876), java.lang.Object(o199sub), java.lang.Object(o199sub)) → 879_0_length_Load(EOS(STATIC_879), java.lang.Object(o199sub))
879_0_length_Load(EOS(STATIC_879), java.lang.Object(o199sub)) → 883_0_length_InvokeMethod(EOS(STATIC_883), java.lang.Object(o199sub))
883_0_length_InvokeMethod(EOS(STATIC_883), java.lang.Object(o199sub)) → 886_0_getTail_Load(EOS(STATIC_886), java.lang.Object(o199sub), java.lang.Object(o199sub))
886_0_getTail_Load(EOS(STATIC_886), java.lang.Object(o199sub), java.lang.Object(o199sub)) → 893_0_getTail_FieldAccess(EOS(STATIC_893), java.lang.Object(o199sub), java.lang.Object(o199sub))
893_0_getTail_FieldAccess(EOS(STATIC_893), java.lang.Object(o199sub), java.lang.Object(o199sub)) → 897_0_getTail_FieldAccess(EOS(STATIC_897), java.lang.Object(o199sub), java.lang.Object(o199sub))
893_0_getTail_FieldAccess(EOS(STATIC_893), java.lang.Object(o199sub), java.lang.Object(o199sub)) → 898_0_getTail_FieldAccess(EOS(STATIC_898), java.lang.Object(o199sub), java.lang.Object(o199sub))
897_0_getTail_FieldAccess(EOS(STATIC_897), java.lang.Object(List(EOC, o203)), java.lang.Object(List(EOC, o203))) → 902_0_getTail_FieldAccess(EOS(STATIC_902), java.lang.Object(List(EOC, o203)), java.lang.Object(List(EOC, o203)))
902_0_getTail_FieldAccess(EOS(STATIC_902), java.lang.Object(List(EOC, o203)), java.lang.Object(List(EOC, o203))) → 907_0_getTail_Return(EOS(STATIC_907), java.lang.Object(List(EOC, o203)), o203)
907_0_getTail_Return(EOS(STATIC_907), java.lang.Object(List(EOC, o203)), o203) → 911_0_length_Store(EOS(STATIC_911), o203)
911_0_length_Store(EOS(STATIC_911), o203) → 916_0_length_Inc(EOS(STATIC_916), o203)
916_0_length_Inc(EOS(STATIC_916), o203) → 920_0_length_JMP(EOS(STATIC_920), o203)
920_0_length_JMP(EOS(STATIC_920), o203) → 925_0_length_Load(EOS(STATIC_925), o203)
925_0_length_Load(EOS(STATIC_925), o203) → 870_0_length_Load(EOS(STATIC_870), o203)
870_0_length_Load(EOS(STATIC_870), o186) → 874_0_length_NULL(EOS(STATIC_874), o186, o186)
898_0_getTail_FieldAccess(EOS(STATIC_898), java.lang.Object(List(EOC, o205)), java.lang.Object(List(EOC, o205))) → 904_0_getTail_FieldAccess(EOS(STATIC_904), java.lang.Object(List(EOC, o205)), java.lang.Object(List(EOC, o205)))
904_0_getTail_FieldAccess(EOS(STATIC_904), java.lang.Object(List(EOC, o205)), java.lang.Object(List(EOC, o205))) → 909_0_getTail_Return(EOS(STATIC_909), java.lang.Object(List(EOC, o205)), o205)
909_0_getTail_Return(EOS(STATIC_909), java.lang.Object(List(EOC, o205)), o205) → 912_0_length_Store(EOS(STATIC_912), o205)
912_0_length_Store(EOS(STATIC_912), o205) → 917_0_length_Inc(EOS(STATIC_917), o205)
917_0_length_Inc(EOS(STATIC_917), o205) → 921_0_length_JMP(EOS(STATIC_921), o205)
921_0_length_JMP(EOS(STATIC_921), o205) → 926_0_length_Load(EOS(STATIC_926), o205)
926_0_length_Load(EOS(STATIC_926), o205) → 870_0_length_Load(EOS(STATIC_870), o205)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
874_0_length_NULL(EOS(STATIC_874), java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → 874_0_length_NULL(EOS(STATIC_874), x0, x0)
R rules:
Filtered ground terms:
874_0_length_NULL(x1, x2, x3) → 874_0_length_NULL(x2, x3)
EOS(x1) → EOS
List(x1, x2) → List(x2)
Filtered duplicate args:
874_0_length_NULL(x1, x2) → 874_0_length_NULL(x2)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
874_0_length_NULL(java.lang.Object(List(x0))) → 874_0_length_NULL(x0)
R rules:
Finished conversion. Obtained 1 rules for P and 0 rules for R. System has no predefined symbols.
P rules:
874_0_LENGTH_NULL(java.lang.Object(List(x0))) → 874_0_LENGTH_NULL(x0)
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 |
(0) -> (0), if (x0[0] →* java.lang.Object(List(x0[0]')))
874_0_LENGTH_NULL(java.lang.Object(List(x0[0]))) → 874_0_LENGTH_NULL(x0[0])
From the DPs we obtained the following set of size-change graphs:
Generated 21 rules for P and 0 rules for R.
P rules:
595_0_mk_Inc(EOS(STATIC_595), i73, o86, i73) → 602_0_mk_LE(EOS(STATIC_602), +(i73, -1), o86, i73)
602_0_mk_LE(EOS(STATIC_602), i80, o86, i84) → 611_0_mk_LE(EOS(STATIC_611), i80, o86, i84)
611_0_mk_LE(EOS(STATIC_611), i80, o86, i84) → 616_0_mk_New(EOS(STATIC_616), i80, o86) | >(i84, 0)
616_0_mk_New(EOS(STATIC_616), i80, o86) → 626_0_mk_Duplicate(EOS(STATIC_626), i80, o86, java.lang.Object(List(EOC)))
626_0_mk_Duplicate(EOS(STATIC_626), i80, o86, java.lang.Object(List(EOC))) → 635_0_mk_Load(EOS(STATIC_635), i80, o86, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
635_0_mk_Load(EOS(STATIC_635), i80, o86, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 650_0_mk_Load(EOS(STATIC_650), i80, o86, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80)
650_0_mk_Load(EOS(STATIC_650), i80, o86, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80) → 672_0_mk_InvokeMethod(EOS(STATIC_672), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86)
672_0_mk_InvokeMethod(EOS(STATIC_672), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86) → 680_0_<init>_Load(EOS(STATIC_680), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86)
680_0_<init>_Load(EOS(STATIC_680), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86) → 692_0_<init>_InvokeMethod(EOS(STATIC_692), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)))
692_0_<init>_InvokeMethod(EOS(STATIC_692), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC))) → 702_0_<init>_Load(EOS(STATIC_702), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86)
702_0_<init>_Load(EOS(STATIC_702), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86) → 705_0_<init>_Load(EOS(STATIC_705), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)))
705_0_<init>_Load(EOS(STATIC_705), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC))) → 708_0_<init>_FieldAccess(EOS(STATIC_708), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), o86, java.lang.Object(List(EOC)), i80)
708_0_<init>_FieldAccess(EOS(STATIC_708), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), o86, java.lang.Object(List(EOC)), i80) → 714_0_<init>_Load(EOS(STATIC_714), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), o86)
714_0_<init>_Load(EOS(STATIC_714), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), o86) → 720_0_<init>_Load(EOS(STATIC_720), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, o86, java.lang.Object(List(EOC)))
720_0_<init>_Load(EOS(STATIC_720), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, o86, java.lang.Object(List(EOC))) → 725_0_<init>_FieldAccess(EOS(STATIC_725), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), o86)
725_0_<init>_FieldAccess(EOS(STATIC_725), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86, java.lang.Object(List(EOC)), o86) → 731_0_<init>_Return(EOS(STATIC_731), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86)
731_0_<init>_Return(EOS(STATIC_731), i80, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i80, o86) → 737_0_mk_Store(EOS(STATIC_737), i80, java.lang.Object(List(EOC)))
737_0_mk_Store(EOS(STATIC_737), i80, java.lang.Object(List(EOC))) → 745_0_mk_JMP(EOS(STATIC_745), i80, java.lang.Object(List(EOC)))
745_0_mk_JMP(EOS(STATIC_745), i80, java.lang.Object(List(EOC))) → 753_0_mk_Load(EOS(STATIC_753), i80, java.lang.Object(List(EOC)))
753_0_mk_Load(EOS(STATIC_753), i80, java.lang.Object(List(EOC))) → 570_0_mk_Load(EOS(STATIC_570), i80, java.lang.Object(List(EOC)))
570_0_mk_Load(EOS(STATIC_570), i73, o86) → 595_0_mk_Inc(EOS(STATIC_595), i73, o86, i73)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
595_0_mk_Inc(EOS(STATIC_595), x0, x1, x0) → 595_0_mk_Inc(EOS(STATIC_595), +(x0, -1), java.lang.Object(List(EOC)), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
595_0_mk_Inc(x1, x2, x3, x4) → 595_0_mk_Inc(x2, x3, x4)
List(x1) → List
java.lang.Object(x1) → java.lang.Object
EOS(x1) → EOS
Cond_595_0_mk_Inc(x1, x2, x3, x4, x5) → Cond_595_0_mk_Inc(x1, x3, x4, x5)
Filtered duplicate args:
595_0_mk_Inc(x1, x2, x3) → 595_0_mk_Inc(x2, x3)
Cond_595_0_mk_Inc(x1, x2, x3, x4) → Cond_595_0_mk_Inc(x1, x3, x4)
Filtered unneeded arguments:
Cond_595_0_mk_Inc(x1, x2, x3) → Cond_595_0_mk_Inc(x1, x3)
595_0_mk_Inc(x1, x2) → 595_0_mk_Inc(x2)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
595_0_mk_Inc(x0) → 595_0_mk_Inc(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
595_0_MK_INC(x0) → COND_595_0_MK_INC(>(x0, 0), x0)
COND_595_0_MK_INC(TRUE, x0) → 595_0_MK_INC(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 595_0_MK_INC(x0[0])≥NonInfC∧595_0_MK_INC(x0[0])≥COND_595_0_MK_INC(>(x0[0], 0), x0[0])∧(UIncreasing(COND_595_0_MK_INC(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 595_0_MK_INC(x0[0])≥NonInfC∧595_0_MK_INC(x0[0])≥COND_595_0_MK_INC(>(x0[0], 0), x0[0])∧(UIncreasing(COND_595_0_MK_INC(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_595_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_595_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_595_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_595_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_595_0_MK_INC(TRUE, x0[1])≥NonInfC∧COND_595_0_MK_INC(TRUE, x0[1])≥595_0_MK_INC(+(x0[1], -1))∧(UIncreasing(595_0_MK_INC(+(x0[1], -1))), ≥))
(8) ((UIncreasing(595_0_MK_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(595_0_MK_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(595_0_MK_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(595_0_MK_INC(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(595_0_MK_INC(x1)) = [2]x1
POL(COND_595_0_MK_INC(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_595_0_MK_INC(TRUE, x0[1]) → 595_0_MK_INC(+(x0[1], -1))
595_0_MK_INC(x0[0]) → COND_595_0_MK_INC(>(x0[0], 0), x0[0])
595_0_MK_INC(x0[0]) → COND_595_0_MK_INC(>(x0[0], 0), x0[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 |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 41 rules for P and 177 rules for R.
P rules:
948_0_main_Load(EOS(STATIC_948), java.lang.Object(ARRAY(matching1)), i137, i137) → 950_0_main_ArrayLength(EOS(STATIC_950), java.lang.Object(ARRAY(3)), i137, i137, java.lang.Object(ARRAY(3))) | =(matching1, 3)
950_0_main_ArrayLength(EOS(STATIC_950), java.lang.Object(ARRAY(matching1)), i137, i137, java.lang.Object(ARRAY(matching2))) → 953_0_main_GE(EOS(STATIC_953), java.lang.Object(ARRAY(3)), i137, i137, 3) | &&(&&(>=(3, 0), =(matching1, 3)), =(matching2, 3))
953_0_main_GE(EOS(STATIC_953), java.lang.Object(ARRAY(matching1)), i140, i140, matching2) → 955_0_main_GE(EOS(STATIC_955), java.lang.Object(ARRAY(3)), i140, i140, 3) | &&(=(matching1, 3), =(matching2, 3))
955_0_main_GE(EOS(STATIC_955), java.lang.Object(ARRAY(matching1)), i140, i140, matching2) → 958_0_main_Load(EOS(STATIC_958), java.lang.Object(ARRAY(3)), i140) | &&(&&(<(i140, 3), =(matching1, 3)), =(matching2, 3))
958_0_main_Load(EOS(STATIC_958), java.lang.Object(ARRAY(matching1)), i140) → 961_0_main_ConstantStackPush(EOS(STATIC_961), java.lang.Object(ARRAY(3)), i140, java.lang.Object(ARRAY(3))) | =(matching1, 3)
961_0_main_ConstantStackPush(EOS(STATIC_961), java.lang.Object(ARRAY(matching1)), i140, java.lang.Object(ARRAY(matching2))) → 965_0_main_ArrayAccess(EOS(STATIC_965), java.lang.Object(ARRAY(3)), i140, java.lang.Object(ARRAY(3)), 0) | &&(=(matching1, 3), =(matching2, 3))
965_0_main_ArrayAccess(EOS(STATIC_965), java.lang.Object(ARRAY(matching1)), i140, java.lang.Object(ARRAY(matching2)), matching3) → 967_0_main_InvokeMethod(EOS(STATIC_967), java.lang.Object(ARRAY(3)), i140, o217) | &&(&&(&&(<(0, 3), =(matching1, 3)), =(matching2, 3)), =(matching3, 0))
967_0_main_InvokeMethod(EOS(STATIC_967), java.lang.Object(ARRAY(matching1)), i140, o217) → 968_1_main_InvokeMethod(968_0_length_ConstantStackPush(EOS(STATIC_968), o217), java.lang.Object(ARRAY(3)), i140, o217) | =(matching1, 3)
968_1_main_InvokeMethod(884_0_length_Return(EOS(STATIC_884), i126), java.lang.Object(ARRAY(matching1)), i140, o230) → 976_0_length_Return(EOS(STATIC_976), java.lang.Object(ARRAY(3)), i140, o230, i126) | =(matching1, 3)
976_0_length_Return(EOS(STATIC_976), java.lang.Object(ARRAY(matching1)), i140, o230, i126) → 978_0_main_Store(EOS(STATIC_978), java.lang.Object(ARRAY(3)), i140, i126) | =(matching1, 3)
978_0_main_Store(EOS(STATIC_978), java.lang.Object(ARRAY(matching1)), i140, i126) → 980_0_main_ConstantStackPush(EOS(STATIC_980), java.lang.Object(ARRAY(3)), i140, i126) | =(matching1, 3)
980_0_main_ConstantStackPush(EOS(STATIC_980), java.lang.Object(ARRAY(matching1)), i140, i126) → 982_0_main_Store(EOS(STATIC_982), java.lang.Object(ARRAY(3)), i140, i126, 0) | =(matching1, 3)
982_0_main_Store(EOS(STATIC_982), java.lang.Object(ARRAY(matching1)), i140, i126, matching2) → 984_0_main_Load(EOS(STATIC_984), java.lang.Object(ARRAY(3)), i140, i126, 0) | &&(=(matching1, 3), =(matching2, 0))
984_0_main_Load(EOS(STATIC_984), java.lang.Object(ARRAY(matching1)), i140, i126, matching2) → 1053_0_main_Load(EOS(STATIC_1053), java.lang.Object(ARRAY(3)), i140, i126, 0) | &&(=(matching1, 3), =(matching2, 0))
1053_0_main_Load(EOS(STATIC_1053), java.lang.Object(ARRAY(matching1)), i140, i150, i151) → 1140_0_main_Load(EOS(STATIC_1140), java.lang.Object(ARRAY(3)), i140, i150, i151) | =(matching1, 3)
1140_0_main_Load(EOS(STATIC_1140), java.lang.Object(ARRAY(matching1)), i140, i150, i163) → 1228_0_main_Load(EOS(STATIC_1228), java.lang.Object(ARRAY(3)), i140, i150, i163) | =(matching1, 3)
1228_0_main_Load(EOS(STATIC_1228), java.lang.Object(ARRAY(matching1)), i140, i150, i177) → 1339_0_main_Load(EOS(STATIC_1339), java.lang.Object(ARRAY(3)), i140, i150, i177) | =(matching1, 3)
1339_0_main_Load(EOS(STATIC_1339), java.lang.Object(ARRAY(matching1)), i140, i150, i189) → 1352_0_main_Load(EOS(STATIC_1352), java.lang.Object(ARRAY(3)), i140, i150, i189, i189) | =(matching1, 3)
1352_0_main_Load(EOS(STATIC_1352), java.lang.Object(ARRAY(matching1)), i140, i150, i189, i189) → 1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), i140, i150, i189, i189, i150) | =(matching1, 3)
1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(matching1)), i140, i150, i189, i189, i150) → 1382_0_main_GE(EOS(STATIC_1382), java.lang.Object(ARRAY(3)), i140, i150, i189, i189, i150) | =(matching1, 3)
1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(matching1)), i140, i150, i189, i189, i150) → 1383_0_main_GE(EOS(STATIC_1383), java.lang.Object(ARRAY(3)), i140, i150, i189, i189, i150) | =(matching1, 3)
1382_0_main_GE(EOS(STATIC_1382), java.lang.Object(ARRAY(matching1)), i140, i150, i189, i189, i150) → 1396_0_main_Inc(EOS(STATIC_1396), java.lang.Object(ARRAY(3)), i140) | &&(>=(i189, i150), =(matching1, 3))
1396_0_main_Inc(EOS(STATIC_1396), java.lang.Object(ARRAY(matching1)), i140) → 1408_0_main_JMP(EOS(STATIC_1408), java.lang.Object(ARRAY(3)), +(i140, 1)) | &&(>=(i140, 0), =(matching1, 3))
1408_0_main_JMP(EOS(STATIC_1408), java.lang.Object(ARRAY(matching1)), i209) → 1428_0_main_Load(EOS(STATIC_1428), java.lang.Object(ARRAY(3)), i209) | =(matching1, 3)
1428_0_main_Load(EOS(STATIC_1428), java.lang.Object(ARRAY(matching1)), i209) → 946_0_main_Load(EOS(STATIC_946), java.lang.Object(ARRAY(3)), i209) | =(matching1, 3)
946_0_main_Load(EOS(STATIC_946), java.lang.Object(ARRAY(matching1)), i137) → 948_0_main_Load(EOS(STATIC_948), java.lang.Object(ARRAY(3)), i137, i137) | =(matching1, 3)
1383_0_main_GE(EOS(STATIC_1383), java.lang.Object(ARRAY(matching1)), i140, i150, i189, i189, i150) → 1398_0_main_Load(EOS(STATIC_1398), java.lang.Object(ARRAY(3)), i140, i150, i189) | &&(<(i189, i150), =(matching1, 3))
1398_0_main_Load(EOS(STATIC_1398), java.lang.Object(ARRAY(matching1)), i140, i150, i189) → 1410_0_main_ConstantStackPush(EOS(STATIC_1410), java.lang.Object(ARRAY(3)), i140, i150, i189, java.lang.Object(ARRAY(3))) | =(matching1, 3)
1410_0_main_ConstantStackPush(EOS(STATIC_1410), java.lang.Object(ARRAY(matching1)), i140, i150, i189, java.lang.Object(ARRAY(matching2))) → 1429_0_main_ArrayAccess(EOS(STATIC_1429), java.lang.Object(ARRAY(3)), i140, i150, i189, java.lang.Object(ARRAY(3)), 0) | &&(=(matching1, 3), =(matching2, 3))
1429_0_main_ArrayAccess(EOS(STATIC_1429), java.lang.Object(ARRAY(matching1)), i140, i150, i189, java.lang.Object(ARRAY(matching2)), matching3) → 1445_0_main_InvokeMethod(EOS(STATIC_1445), java.lang.Object(ARRAY(3)), i140, i150, i189, o416) | &&(&&(&&(<(0, 3), =(matching1, 3)), =(matching2, 3)), =(matching3, 0))
1445_0_main_InvokeMethod(EOS(STATIC_1445), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o416) → 1454_1_main_InvokeMethod(1454_0_bubble_Load(EOS(STATIC_1454), o416), java.lang.Object(ARRAY(3)), i140, i150, i189, o416) | =(matching1, 3)
1454_1_main_InvokeMethod(1634_0_bubble_Return(EOS(STATIC_1634)), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o416) → 1643_0_bubble_Return(EOS(STATIC_1643), java.lang.Object(ARRAY(3)), i140, i150, i189, o1102) | =(matching1, 3)
1454_1_main_InvokeMethod(1666_0_bubble_Return(EOS(STATIC_1666)), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o416) → 1686_0_bubble_Return(EOS(STATIC_1686), java.lang.Object(ARRAY(3)), i140, i150, i189, o1102) | =(matching1, 3)
1454_1_main_InvokeMethod(1669_0_bubble_Return(EOS(STATIC_1669)), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o416) → 1691_0_bubble_Return(EOS(STATIC_1691), java.lang.Object(ARRAY(3)), i140, i150, i189, java.lang.Object(List(EOC))) | =(matching1, 3)
1643_0_bubble_Return(EOS(STATIC_1643), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o1102) → 1499_0_bubble_Return(EOS(STATIC_1499), java.lang.Object(ARRAY(3)), i140, i150, i189, o1102) | =(matching1, 3)
1499_0_bubble_Return(EOS(STATIC_1499), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o688) → 1511_0_main_Inc(EOS(STATIC_1511), java.lang.Object(ARRAY(3)), i140, i150, i189) | =(matching1, 3)
1511_0_main_Inc(EOS(STATIC_1511), java.lang.Object(ARRAY(matching1)), i140, i150, i189) → 1518_0_main_JMP(EOS(STATIC_1518), java.lang.Object(ARRAY(3)), i140, i150, +(i189, 1)) | &&(>=(i189, 0), =(matching1, 3))
1518_0_main_JMP(EOS(STATIC_1518), java.lang.Object(ARRAY(matching1)), i140, i150, i234) → 1524_0_main_Load(EOS(STATIC_1524), java.lang.Object(ARRAY(3)), i140, i150, i234) | =(matching1, 3)
1524_0_main_Load(EOS(STATIC_1524), java.lang.Object(ARRAY(matching1)), i140, i150, i234) → 1339_0_main_Load(EOS(STATIC_1339), java.lang.Object(ARRAY(3)), i140, i150, i234) | =(matching1, 3)
1686_0_bubble_Return(EOS(STATIC_1686), java.lang.Object(ARRAY(matching1)), i140, i150, i189, o1102) → 1499_0_bubble_Return(EOS(STATIC_1499), java.lang.Object(ARRAY(3)), i140, i150, i189, o1102) | =(matching1, 3)
1691_0_bubble_Return(EOS(STATIC_1691), java.lang.Object(ARRAY(matching1)), i140, i150, i189, java.lang.Object(List(EOC))) → 1499_0_bubble_Return(EOS(STATIC_1499), java.lang.Object(ARRAY(3)), i140, i150, i189, java.lang.Object(List(EOC))) | =(matching1, 3)
R rules:
968_0_length_ConstantStackPush(EOS(STATIC_968), o217) → 971_0_length_ConstantStackPush(EOS(STATIC_971), o217)
971_0_length_ConstantStackPush(EOS(STATIC_971), o217) → 421_0_length_ConstantStackPush(EOS(STATIC_421), o217)
1454_0_bubble_Load(EOS(STATIC_1454), o416) → 1461_0_bubble_Load(EOS(STATIC_1461), o416)
1461_0_bubble_Load(EOS(STATIC_1461), o416) → 1011_0_bubble_Load(EOS(STATIC_1011), o416)
421_0_length_ConstantStackPush(EOS(STATIC_421), o22) → 425_0_length_Store(EOS(STATIC_425), o22, 0)
425_0_length_Store(EOS(STATIC_425), o22, matching1) → 431_0_length_Load(EOS(STATIC_431), o22, 0) | =(matching1, 0)
431_0_length_Load(EOS(STATIC_431), o22, matching1) → 543_0_length_Load(EOS(STATIC_543), o22, 0) | =(matching1, 0)
543_0_length_Load(EOS(STATIC_543), o73, i71) → 700_0_length_Load(EOS(STATIC_700), o73, i71)
700_0_length_Load(EOS(STATIC_700), o126, i99) → 782_0_length_Load(EOS(STATIC_782), o126, i99)
782_0_length_Load(EOS(STATIC_782), o154, i107) → 870_0_length_Load(EOS(STATIC_870), o154, i107)
870_0_length_Load(EOS(STATIC_870), o186, i126) → 874_0_length_NULL(EOS(STATIC_874), o186, i126, o186)
874_0_length_NULL(EOS(STATIC_874), java.lang.Object(o199sub), i126, java.lang.Object(o199sub)) → 876_0_length_NULL(EOS(STATIC_876), java.lang.Object(o199sub), i126, java.lang.Object(o199sub))
874_0_length_NULL(EOS(STATIC_874), NULL, i126, NULL) → 877_0_length_NULL(EOS(STATIC_877), NULL, i126, NULL)
876_0_length_NULL(EOS(STATIC_876), java.lang.Object(o199sub), i126, java.lang.Object(o199sub)) → 879_0_length_Load(EOS(STATIC_879), java.lang.Object(o199sub), i126)
877_0_length_NULL(EOS(STATIC_877), NULL, i126, NULL) → 881_0_length_Load(EOS(STATIC_881), i126)
879_0_length_Load(EOS(STATIC_879), java.lang.Object(o199sub), i126) → 883_0_length_InvokeMethod(EOS(STATIC_883), i126, java.lang.Object(o199sub))
881_0_length_Load(EOS(STATIC_881), i126) → 884_0_length_Return(EOS(STATIC_884), i126)
883_0_length_InvokeMethod(EOS(STATIC_883), i126, java.lang.Object(o199sub)) → 886_0_getTail_Load(EOS(STATIC_886), i126, java.lang.Object(o199sub), java.lang.Object(o199sub))
886_0_getTail_Load(EOS(STATIC_886), i126, java.lang.Object(o199sub), java.lang.Object(o199sub)) → 893_0_getTail_FieldAccess(EOS(STATIC_893), i126, java.lang.Object(o199sub), java.lang.Object(o199sub))
893_0_getTail_FieldAccess(EOS(STATIC_893), i126, java.lang.Object(o199sub), java.lang.Object(o199sub)) → 897_0_getTail_FieldAccess(EOS(STATIC_897), i126, java.lang.Object(o199sub), java.lang.Object(o199sub))
893_0_getTail_FieldAccess(EOS(STATIC_893), i126, java.lang.Object(o199sub), java.lang.Object(o199sub)) → 898_0_getTail_FieldAccess(EOS(STATIC_898), i126, java.lang.Object(o199sub), java.lang.Object(o199sub))
897_0_getTail_FieldAccess(EOS(STATIC_897), i126, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 902_0_getTail_FieldAccess(EOS(STATIC_902), i126, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
898_0_getTail_FieldAccess(EOS(STATIC_898), i126, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 904_0_getTail_FieldAccess(EOS(STATIC_904), i126, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
902_0_getTail_FieldAccess(EOS(STATIC_902), i126, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 907_0_getTail_Return(EOS(STATIC_907), i126, java.lang.Object(List(EOC)), o203)
904_0_getTail_FieldAccess(EOS(STATIC_904), i126, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 909_0_getTail_Return(EOS(STATIC_909), i126, java.lang.Object(List(EOC)), o205)
907_0_getTail_Return(EOS(STATIC_907), i126, java.lang.Object(List(EOC)), o203) → 911_0_length_Store(EOS(STATIC_911), i126, o203)
909_0_getTail_Return(EOS(STATIC_909), i126, java.lang.Object(List(EOC)), o205) → 912_0_length_Store(EOS(STATIC_912), i126, o205)
911_0_length_Store(EOS(STATIC_911), i126, o203) → 916_0_length_Inc(EOS(STATIC_916), o203, i126)
912_0_length_Store(EOS(STATIC_912), i126, o205) → 917_0_length_Inc(EOS(STATIC_917), o205, i126)
916_0_length_Inc(EOS(STATIC_916), o203, i126) → 920_0_length_JMP(EOS(STATIC_920), o203, +(i126, 1)) | >=(i126, 0)
917_0_length_Inc(EOS(STATIC_917), o205, i126) → 921_0_length_JMP(EOS(STATIC_921), o205, +(i126, 1)) | >=(i126, 0)
920_0_length_JMP(EOS(STATIC_920), o203, i130) → 925_0_length_Load(EOS(STATIC_925), o203, i130)
921_0_length_JMP(EOS(STATIC_921), o205, i131) → 926_0_length_Load(EOS(STATIC_926), o205, i131)
925_0_length_Load(EOS(STATIC_925), o203, i130) → 870_0_length_Load(EOS(STATIC_870), o203, i130)
926_0_length_Load(EOS(STATIC_926), o205, i131) → 870_0_length_Load(EOS(STATIC_870), o205, i131)
1011_0_bubble_Load(EOS(STATIC_1011), o230) → 1013_0_bubble_Store(EOS(STATIC_1013), o230)
1013_0_bubble_Store(EOS(STATIC_1013), o230) → 1014_0_bubble_Load(EOS(STATIC_1014), o230)
1014_0_bubble_Load(EOS(STATIC_1014), o230) → 1188_0_bubble_Load(EOS(STATIC_1188), o230)
1188_0_bubble_Load(EOS(STATIC_1188), o303) → 1626_0_bubble_Load(EOS(STATIC_1626), o303)
1626_0_bubble_Load(EOS(STATIC_1626), o1104) → 1629_0_bubble_NULL(EOS(STATIC_1629), o1104, o1104)
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1630_0_bubble_NULL(EOS(STATIC_1630), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1629_0_bubble_NULL(EOS(STATIC_1629), NULL, NULL) → 1631_0_bubble_NULL(EOS(STATIC_1631), NULL, NULL)
1630_0_bubble_NULL(EOS(STATIC_1630), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1633_0_bubble_Load(EOS(STATIC_1633), java.lang.Object(o1109sub))
1631_0_bubble_NULL(EOS(STATIC_1631), NULL, NULL) → 1634_0_bubble_Return(EOS(STATIC_1634))
1633_0_bubble_Load(EOS(STATIC_1633), java.lang.Object(o1109sub)) → 1636_0_bubble_InvokeMethod(EOS(STATIC_1636), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1634_0_bubble_Return(EOS(STATIC_1634)) → 1666_0_bubble_Return(EOS(STATIC_1666))
1636_0_bubble_InvokeMethod(EOS(STATIC_1636), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1638_0_getTail_Load(EOS(STATIC_1638), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1638_0_getTail_Load(EOS(STATIC_1638), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1645_0_getTail_FieldAccess(EOS(STATIC_1645), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1645_0_getTail_FieldAccess(EOS(STATIC_1645), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1647_0_getTail_FieldAccess(EOS(STATIC_1647), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1645_0_getTail_FieldAccess(EOS(STATIC_1645), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub)) → 1648_0_getTail_FieldAccess(EOS(STATIC_1648), java.lang.Object(o1109sub), java.lang.Object(o1109sub), java.lang.Object(o1109sub))
1647_0_getTail_FieldAccess(EOS(STATIC_1647), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1649_0_getTail_FieldAccess(EOS(STATIC_1649), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1648_0_getTail_FieldAccess(EOS(STATIC_1648), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1651_0_getTail_FieldAccess(EOS(STATIC_1651), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1649_0_getTail_FieldAccess(EOS(STATIC_1649), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1652_0_getTail_Return(EOS(STATIC_1652), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), o1116)
1651_0_getTail_FieldAccess(EOS(STATIC_1651), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1654_0_getTail_Return(EOS(STATIC_1654), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), o1118)
1652_0_getTail_Return(EOS(STATIC_1652), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), o1116) → 1656_0_bubble_NULL(EOS(STATIC_1656), java.lang.Object(List(EOC)), o1116)
1654_0_getTail_Return(EOS(STATIC_1654), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), o1118) → 1658_0_bubble_NULL(EOS(STATIC_1658), java.lang.Object(List(EOC)), o1118)
1656_0_bubble_NULL(EOS(STATIC_1656), java.lang.Object(List(EOC)), java.lang.Object(o1126sub)) → 1660_0_bubble_NULL(EOS(STATIC_1660), java.lang.Object(List(EOC)), java.lang.Object(o1126sub))
1656_0_bubble_NULL(EOS(STATIC_1656), java.lang.Object(List(EOC)), NULL) → 1661_0_bubble_NULL(EOS(STATIC_1661), java.lang.Object(List(EOC)), NULL)
1658_0_bubble_NULL(EOS(STATIC_1658), java.lang.Object(List(EOC)), java.lang.Object(o1127sub)) → 1662_0_bubble_NULL(EOS(STATIC_1662), java.lang.Object(List(EOC)), java.lang.Object(o1127sub))
1658_0_bubble_NULL(EOS(STATIC_1658), java.lang.Object(List(EOC)), NULL) → 1663_0_bubble_NULL(EOS(STATIC_1663), java.lang.Object(List(EOC)), NULL)
1660_0_bubble_NULL(EOS(STATIC_1660), java.lang.Object(List(EOC)), java.lang.Object(o1126sub)) → 1665_0_bubble_Load(EOS(STATIC_1665), java.lang.Object(List(EOC)))
1661_0_bubble_NULL(EOS(STATIC_1661), java.lang.Object(List(EOC)), NULL) → 1666_0_bubble_Return(EOS(STATIC_1666))
1662_0_bubble_NULL(EOS(STATIC_1662), java.lang.Object(List(EOC)), java.lang.Object(o1127sub)) → 1668_0_bubble_Load(EOS(STATIC_1668), java.lang.Object(List(EOC)))
1663_0_bubble_NULL(EOS(STATIC_1663), java.lang.Object(List(EOC)), NULL) → 1669_0_bubble_Return(EOS(STATIC_1669))
1665_0_bubble_Load(EOS(STATIC_1665), java.lang.Object(List(EOC))) → 1671_0_bubble_FieldAccess(EOS(STATIC_1671), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1668_0_bubble_Load(EOS(STATIC_1668), java.lang.Object(List(EOC))) → 1674_0_bubble_FieldAccess(EOS(STATIC_1674), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1671_0_bubble_FieldAccess(EOS(STATIC_1671), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1677_0_bubble_Load(EOS(STATIC_1677), java.lang.Object(List(EOC)), i316)
1674_0_bubble_FieldAccess(EOS(STATIC_1674), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1680_0_bubble_Load(EOS(STATIC_1680), java.lang.Object(List(EOC)), i317)
1677_0_bubble_Load(EOS(STATIC_1677), java.lang.Object(List(EOC)), i316) → 1683_0_bubble_InvokeMethod(EOS(STATIC_1683), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1680_0_bubble_Load(EOS(STATIC_1680), java.lang.Object(List(EOC)), i317) → 1688_0_bubble_InvokeMethod(EOS(STATIC_1688), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)))
1683_0_bubble_InvokeMethod(EOS(STATIC_1683), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1693_0_getTail_Load(EOS(STATIC_1693), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1688_0_bubble_InvokeMethod(EOS(STATIC_1688), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC))) → 1694_0_getTail_Load(EOS(STATIC_1694), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1693_0_getTail_Load(EOS(STATIC_1693), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1696_0_getTail_FieldAccess(EOS(STATIC_1696), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1694_0_getTail_Load(EOS(STATIC_1694), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1698_0_getTail_FieldAccess(EOS(STATIC_1698), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1696_0_getTail_FieldAccess(EOS(STATIC_1696), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1700_0_getTail_Return(EOS(STATIC_1700), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(o1126sub))
1698_0_getTail_FieldAccess(EOS(STATIC_1698), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1701_0_getTail_Return(EOS(STATIC_1701), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(o1127sub))
1700_0_getTail_Return(EOS(STATIC_1700), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(o1126sub)) → 1703_0_bubble_FieldAccess(EOS(STATIC_1703), java.lang.Object(List(EOC)), i316, java.lang.Object(o1126sub))
1701_0_getTail_Return(EOS(STATIC_1701), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(o1127sub)) → 1705_0_bubble_FieldAccess(EOS(STATIC_1705), java.lang.Object(List(EOC)), i317, java.lang.Object(o1127sub))
1703_0_bubble_FieldAccess(EOS(STATIC_1703), java.lang.Object(List(EOC)), i316, java.lang.Object(o1126sub)) → 1707_0_bubble_FieldAccess(EOS(STATIC_1707), java.lang.Object(List(EOC)), i316, java.lang.Object(o1126sub))
1703_0_bubble_FieldAccess(EOS(STATIC_1703), java.lang.Object(List(EOC)), i316, java.lang.Object(o1126sub)) → 1708_0_bubble_FieldAccess(EOS(STATIC_1708), java.lang.Object(List(EOC)), i316, java.lang.Object(o1126sub))
1705_0_bubble_FieldAccess(EOS(STATIC_1705), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC))) → 1709_0_bubble_FieldAccess(EOS(STATIC_1709), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)))
1707_0_bubble_FieldAccess(EOS(STATIC_1707), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1711_0_bubble_FieldAccess(EOS(STATIC_1711), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1708_0_bubble_FieldAccess(EOS(STATIC_1708), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1713_0_bubble_FieldAccess(EOS(STATIC_1713), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1709_0_bubble_FieldAccess(EOS(STATIC_1709), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC))) → 1715_0_bubble_LE(EOS(STATIC_1715), java.lang.Object(List(EOC)), i317, i319)
1711_0_bubble_FieldAccess(EOS(STATIC_1711), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1717_0_bubble_LE(EOS(STATIC_1717), java.lang.Object(List(EOC)), i316, i320)
1713_0_bubble_FieldAccess(EOS(STATIC_1713), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1720_0_bubble_LE(EOS(STATIC_1720), java.lang.Object(List(EOC)), i316, i321)
1715_0_bubble_LE(EOS(STATIC_1715), java.lang.Object(List(EOC)), i317, i319) → 1722_0_bubble_LE(EOS(STATIC_1722), java.lang.Object(List(EOC)), i317, i319)
1715_0_bubble_LE(EOS(STATIC_1715), java.lang.Object(List(EOC)), i317, i319) → 1723_0_bubble_LE(EOS(STATIC_1723), java.lang.Object(List(EOC)), i317, i319)
1717_0_bubble_LE(EOS(STATIC_1717), java.lang.Object(List(EOC)), i316, i320) → 1724_0_bubble_LE(EOS(STATIC_1724), java.lang.Object(List(EOC)), i316, i320)
1717_0_bubble_LE(EOS(STATIC_1717), java.lang.Object(List(EOC)), i316, i320) → 1725_0_bubble_LE(EOS(STATIC_1725), java.lang.Object(List(EOC)), i316, i320)
1720_0_bubble_LE(EOS(STATIC_1720), java.lang.Object(List(EOC)), i316, i321) → 1727_0_bubble_LE(EOS(STATIC_1727), java.lang.Object(List(EOC)), i316, i321)
1720_0_bubble_LE(EOS(STATIC_1720), java.lang.Object(List(EOC)), i316, i321) → 1728_0_bubble_LE(EOS(STATIC_1728), java.lang.Object(List(EOC)), i316, i321)
1722_0_bubble_LE(EOS(STATIC_1722), java.lang.Object(List(EOC)), i317, i319) → 1729_0_bubble_Load(EOS(STATIC_1729), java.lang.Object(List(EOC))) | <=(i317, i319)
1723_0_bubble_LE(EOS(STATIC_1723), java.lang.Object(List(EOC)), i317, i319) → 1731_0_bubble_Load(EOS(STATIC_1731), java.lang.Object(List(EOC))) | >(i317, i319)
1724_0_bubble_LE(EOS(STATIC_1724), java.lang.Object(List(EOC)), i316, i320) → 1732_0_bubble_Load(EOS(STATIC_1732), java.lang.Object(List(EOC))) | <=(i316, i320)
1725_0_bubble_LE(EOS(STATIC_1725), java.lang.Object(List(EOC)), i316, i320) → 1734_0_bubble_Load(EOS(STATIC_1734), java.lang.Object(List(EOC))) | >(i316, i320)
1727_0_bubble_LE(EOS(STATIC_1727), java.lang.Object(List(EOC)), i316, i321) → 1736_0_bubble_Load(EOS(STATIC_1736), java.lang.Object(List(EOC))) | <=(i316, i321)
1728_0_bubble_LE(EOS(STATIC_1728), java.lang.Object(List(EOC)), i316, i321) → 1738_0_bubble_Load(EOS(STATIC_1738), java.lang.Object(List(EOC))) | >(i316, i321)
1729_0_bubble_Load(EOS(STATIC_1729), java.lang.Object(List(EOC))) → 1887_0_bubble_Load(EOS(STATIC_1887), java.lang.Object(List(EOC)))
1731_0_bubble_Load(EOS(STATIC_1731), java.lang.Object(List(EOC))) → 1740_0_bubble_FieldAccess(EOS(STATIC_1740), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1732_0_bubble_Load(EOS(STATIC_1732), java.lang.Object(List(EOC))) → 1894_0_bubble_Load(EOS(STATIC_1894), java.lang.Object(List(EOC)))
1734_0_bubble_Load(EOS(STATIC_1734), java.lang.Object(List(EOC))) → 1744_0_bubble_FieldAccess(EOS(STATIC_1744), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1736_0_bubble_Load(EOS(STATIC_1736), java.lang.Object(List(EOC))) → 1898_0_bubble_Load(EOS(STATIC_1898), java.lang.Object(List(EOC)))
1738_0_bubble_Load(EOS(STATIC_1738), java.lang.Object(List(EOC))) → 1747_0_bubble_FieldAccess(EOS(STATIC_1747), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1740_0_bubble_FieldAccess(EOS(STATIC_1740), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1750_0_bubble_Store(EOS(STATIC_1750), java.lang.Object(List(EOC)), i317)
1744_0_bubble_FieldAccess(EOS(STATIC_1744), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1753_0_bubble_Store(EOS(STATIC_1753), java.lang.Object(List(EOC)), i316)
1747_0_bubble_FieldAccess(EOS(STATIC_1747), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1757_0_bubble_Store(EOS(STATIC_1757), java.lang.Object(List(EOC)), i316)
1750_0_bubble_Store(EOS(STATIC_1750), java.lang.Object(List(EOC)), i317) → 1758_0_bubble_Load(EOS(STATIC_1758), java.lang.Object(List(EOC)), i317)
1753_0_bubble_Store(EOS(STATIC_1753), java.lang.Object(List(EOC)), i316) → 1760_0_bubble_Load(EOS(STATIC_1760), java.lang.Object(List(EOC)), i316)
1757_0_bubble_Store(EOS(STATIC_1757), java.lang.Object(List(EOC)), i316) → 1762_0_bubble_Load(EOS(STATIC_1762), java.lang.Object(List(EOC)), i316)
1758_0_bubble_Load(EOS(STATIC_1758), java.lang.Object(List(EOC)), i317) → 1765_0_bubble_Load(EOS(STATIC_1765), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)))
1760_0_bubble_Load(EOS(STATIC_1760), java.lang.Object(List(EOC)), i316) → 1770_0_bubble_Load(EOS(STATIC_1770), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1762_0_bubble_Load(EOS(STATIC_1762), java.lang.Object(List(EOC)), i316) → 1774_0_bubble_Load(EOS(STATIC_1774), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1765_0_bubble_Load(EOS(STATIC_1765), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC))) → 1777_0_bubble_InvokeMethod(EOS(STATIC_1777), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1770_0_bubble_Load(EOS(STATIC_1770), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1782_0_bubble_InvokeMethod(EOS(STATIC_1782), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1774_0_bubble_Load(EOS(STATIC_1774), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1787_0_bubble_InvokeMethod(EOS(STATIC_1787), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1777_0_bubble_InvokeMethod(EOS(STATIC_1777), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1789_0_getTail_Load(EOS(STATIC_1789), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1782_0_bubble_InvokeMethod(EOS(STATIC_1782), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1793_0_getTail_Load(EOS(STATIC_1793), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1787_0_bubble_InvokeMethod(EOS(STATIC_1787), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1796_0_getTail_Load(EOS(STATIC_1796), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1789_0_getTail_Load(EOS(STATIC_1789), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1801_0_getTail_FieldAccess(EOS(STATIC_1801), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1793_0_getTail_Load(EOS(STATIC_1793), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1808_0_getTail_FieldAccess(EOS(STATIC_1808), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1796_0_getTail_Load(EOS(STATIC_1796), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1813_0_getTail_FieldAccess(EOS(STATIC_1813), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1801_0_getTail_FieldAccess(EOS(STATIC_1801), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1816_0_getTail_Return(EOS(STATIC_1816), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1808_0_getTail_FieldAccess(EOS(STATIC_1808), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1819_0_getTail_Return(EOS(STATIC_1819), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1813_0_getTail_FieldAccess(EOS(STATIC_1813), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1822_0_getTail_Return(EOS(STATIC_1822), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1816_0_getTail_Return(EOS(STATIC_1816), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1824_0_bubble_FieldAccess(EOS(STATIC_1824), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1819_0_getTail_Return(EOS(STATIC_1819), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1825_0_bubble_FieldAccess(EOS(STATIC_1825), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1822_0_getTail_Return(EOS(STATIC_1822), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1826_0_bubble_FieldAccess(EOS(STATIC_1826), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1824_0_bubble_FieldAccess(EOS(STATIC_1824), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1828_0_bubble_FieldAccess(EOS(STATIC_1828), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), i319)
1825_0_bubble_FieldAccess(EOS(STATIC_1825), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1829_0_bubble_FieldAccess(EOS(STATIC_1829), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), i320)
1826_0_bubble_FieldAccess(EOS(STATIC_1826), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1831_0_bubble_FieldAccess(EOS(STATIC_1831), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), i321)
1828_0_bubble_FieldAccess(EOS(STATIC_1828), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), i319) → 1832_0_bubble_Load(EOS(STATIC_1832), java.lang.Object(List(EOC)), i317)
1829_0_bubble_FieldAccess(EOS(STATIC_1829), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), i320) → 1834_0_bubble_Load(EOS(STATIC_1834), java.lang.Object(List(EOC)), i316)
1831_0_bubble_FieldAccess(EOS(STATIC_1831), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), i321) → 1835_0_bubble_Load(EOS(STATIC_1835), java.lang.Object(List(EOC)), i316)
1832_0_bubble_Load(EOS(STATIC_1832), java.lang.Object(List(EOC)), i317) → 1837_0_bubble_InvokeMethod(EOS(STATIC_1837), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)))
1834_0_bubble_Load(EOS(STATIC_1834), java.lang.Object(List(EOC)), i316) → 1839_0_bubble_InvokeMethod(EOS(STATIC_1839), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1835_0_bubble_Load(EOS(STATIC_1835), java.lang.Object(List(EOC)), i316) → 1841_0_bubble_InvokeMethod(EOS(STATIC_1841), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1837_0_bubble_InvokeMethod(EOS(STATIC_1837), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC))) → 1842_0_getTail_Load(EOS(STATIC_1842), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1839_0_bubble_InvokeMethod(EOS(STATIC_1839), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1844_0_getTail_Load(EOS(STATIC_1844), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1841_0_bubble_InvokeMethod(EOS(STATIC_1841), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1845_0_getTail_Load(EOS(STATIC_1845), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1842_0_getTail_Load(EOS(STATIC_1842), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1849_0_getTail_FieldAccess(EOS(STATIC_1849), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1844_0_getTail_Load(EOS(STATIC_1844), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1854_0_getTail_FieldAccess(EOS(STATIC_1854), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1845_0_getTail_Load(EOS(STATIC_1845), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1858_0_getTail_FieldAccess(EOS(STATIC_1858), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1849_0_getTail_FieldAccess(EOS(STATIC_1849), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1862_0_getTail_Return(EOS(STATIC_1862), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1854_0_getTail_FieldAccess(EOS(STATIC_1854), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1866_0_getTail_Return(EOS(STATIC_1866), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1858_0_getTail_FieldAccess(EOS(STATIC_1858), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1871_0_getTail_Return(EOS(STATIC_1871), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1862_0_getTail_Return(EOS(STATIC_1862), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1873_0_bubble_Load(EOS(STATIC_1873), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC)))
1866_0_getTail_Return(EOS(STATIC_1866), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1875_0_bubble_Load(EOS(STATIC_1875), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1871_0_getTail_Return(EOS(STATIC_1871), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1878_0_bubble_Load(EOS(STATIC_1878), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC)))
1873_0_bubble_Load(EOS(STATIC_1873), java.lang.Object(List(EOC)), i317, java.lang.Object(List(EOC))) → 1879_0_bubble_FieldAccess(EOS(STATIC_1879), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i317)
1875_0_bubble_Load(EOS(STATIC_1875), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1881_0_bubble_FieldAccess(EOS(STATIC_1881), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i316)
1878_0_bubble_Load(EOS(STATIC_1878), java.lang.Object(List(EOC)), i316, java.lang.Object(List(EOC))) → 1884_0_bubble_FieldAccess(EOS(STATIC_1884), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i316)
1879_0_bubble_FieldAccess(EOS(STATIC_1879), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i317) → 1887_0_bubble_Load(EOS(STATIC_1887), java.lang.Object(List(EOC)))
1881_0_bubble_FieldAccess(EOS(STATIC_1881), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i316) → 1894_0_bubble_Load(EOS(STATIC_1894), java.lang.Object(List(EOC)))
1884_0_bubble_FieldAccess(EOS(STATIC_1884), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i316) → 1898_0_bubble_Load(EOS(STATIC_1898), java.lang.Object(List(EOC)))
1887_0_bubble_Load(EOS(STATIC_1887), java.lang.Object(List(EOC))) → 1901_0_bubble_InvokeMethod(EOS(STATIC_1901), java.lang.Object(List(EOC)))
1894_0_bubble_Load(EOS(STATIC_1894), java.lang.Object(List(EOC))) → 1902_0_bubble_InvokeMethod(EOS(STATIC_1902), java.lang.Object(List(EOC)))
1898_0_bubble_Load(EOS(STATIC_1898), java.lang.Object(List(EOC))) → 1904_0_bubble_InvokeMethod(EOS(STATIC_1904), java.lang.Object(List(EOC)))
1901_0_bubble_InvokeMethod(EOS(STATIC_1901), java.lang.Object(List(EOC))) → 1905_0_getTail_Load(EOS(STATIC_1905), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1902_0_bubble_InvokeMethod(EOS(STATIC_1902), java.lang.Object(List(EOC))) → 1907_0_getTail_Load(EOS(STATIC_1907), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1904_0_bubble_InvokeMethod(EOS(STATIC_1904), java.lang.Object(List(EOC))) → 1908_0_getTail_Load(EOS(STATIC_1908), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1905_0_getTail_Load(EOS(STATIC_1905), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1911_0_getTail_FieldAccess(EOS(STATIC_1911), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1907_0_getTail_Load(EOS(STATIC_1907), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1917_0_getTail_FieldAccess(EOS(STATIC_1917), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1908_0_getTail_Load(EOS(STATIC_1908), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1922_0_getTail_FieldAccess(EOS(STATIC_1922), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1911_0_getTail_FieldAccess(EOS(STATIC_1911), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1925_0_getTail_Return(EOS(STATIC_1925), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1917_0_getTail_FieldAccess(EOS(STATIC_1917), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1928_0_getTail_Return(EOS(STATIC_1928), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1922_0_getTail_FieldAccess(EOS(STATIC_1922), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1933_0_getTail_Return(EOS(STATIC_1933), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
1925_0_getTail_Return(EOS(STATIC_1925), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1934_0_bubble_Store(EOS(STATIC_1934), java.lang.Object(List(EOC)))
1928_0_getTail_Return(EOS(STATIC_1928), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1936_0_bubble_Store(EOS(STATIC_1936), java.lang.Object(List(EOC)))
1933_0_getTail_Return(EOS(STATIC_1933), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1938_0_bubble_Store(EOS(STATIC_1938), java.lang.Object(List(EOC)))
1934_0_bubble_Store(EOS(STATIC_1934), java.lang.Object(List(EOC))) → 1936_0_bubble_Store(EOS(STATIC_1936), java.lang.Object(List(EOC)))
1936_0_bubble_Store(EOS(STATIC_1936), java.lang.Object(List(EOC))) → 1939_0_bubble_JMP(EOS(STATIC_1939), java.lang.Object(List(EOC)))
1938_0_bubble_Store(EOS(STATIC_1938), java.lang.Object(List(EOC))) → 1940_0_bubble_JMP(EOS(STATIC_1940), java.lang.Object(List(EOC)))
1939_0_bubble_JMP(EOS(STATIC_1939), java.lang.Object(List(EOC))) → 1942_0_bubble_Load(EOS(STATIC_1942), java.lang.Object(List(EOC)))
1940_0_bubble_JMP(EOS(STATIC_1940), java.lang.Object(List(EOC))) → 1944_0_bubble_Load(EOS(STATIC_1944), java.lang.Object(List(EOC)))
1942_0_bubble_Load(EOS(STATIC_1942), java.lang.Object(List(EOC))) → 1626_0_bubble_Load(EOS(STATIC_1626), java.lang.Object(List(EOC)))
1944_0_bubble_Load(EOS(STATIC_1944), java.lang.Object(List(EOC))) → 1626_0_bubble_Load(EOS(STATIC_1626), java.lang.Object(List(EOC)))
Combined rules. Obtained 6 conditional rules for P and 8 conditional rules for R.
P rules:
968_1_main_InvokeMethod(884_0_length_Return(EOS(STATIC_884), x0), java.lang.Object(ARRAY(3)), x2, x3) → 1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), x2, x0, 0, 0, x0)
1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), x1, x2, x3, x3, x2) → 968_1_main_InvokeMethod(968_0_length_ConstantStackPush(EOS(STATIC_968), x4), java.lang.Object(ARRAY(3)), +(x1, 1), x4) | &&(&&(>=(x3, x2), >(+(x1, 1), 0)), <(x1, 2))
1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), x1, x2, x3, x3, x2) → 1454_1_main_InvokeMethod(1454_0_bubble_Load(EOS(STATIC_1454), x4), java.lang.Object(ARRAY(3)), x1, x2, x3, x4) | <(x3, x2)
1454_1_main_InvokeMethod(1634_0_bubble_Return(EOS(STATIC_1634)), java.lang.Object(ARRAY(3)), x1, x2, x3, x4) → 1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), x1, x2, +(x3, 1), +(x3, 1), x2) | >(+(x3, 1), 0)
1454_1_main_InvokeMethod(1666_0_bubble_Return(EOS(STATIC_1666)), java.lang.Object(ARRAY(3)), x1, x2, x3, x4) → 1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), x1, x2, +(x3, 1), +(x3, 1), x2) | >(+(x3, 1), 0)
1454_1_main_InvokeMethod(1669_0_bubble_Return(EOS(STATIC_1669)), java.lang.Object(ARRAY(3)), x1, x2, x3, x4) → 1366_0_main_GE(EOS(STATIC_1366), java.lang.Object(ARRAY(3)), x1, x2, +(x3, 1), +(x3, 1), x2) | >(+(x3, 1), 0)
R rules:
968_0_length_ConstantStackPush(EOS(STATIC_968), x0) → 874_0_length_NULL(EOS(STATIC_874), x0, 0, x0)
874_0_length_NULL(EOS(STATIC_874), NULL, x0, NULL) → 884_0_length_Return(EOS(STATIC_884), x0)
874_0_length_NULL(EOS(STATIC_874), java.lang.Object(List(EOC)), x0, java.lang.Object(List(EOC))) → 874_0_length_NULL(EOS(STATIC_874), x1, +(x0, 1), x1) | >(+(x0, 1), 0)
1454_0_bubble_Load(EOS(STATIC_1454), x0) → 1629_0_bubble_NULL(EOS(STATIC_1629), x0, x0)
1629_0_bubble_NULL(EOS(STATIC_1629), NULL, NULL) → 1666_0_bubble_Return(EOS(STATIC_1666))
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1666_0_bubble_Return(EOS(STATIC_1666))
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1669_0_bubble_Return(EOS(STATIC_1669))
1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 1629_0_bubble_NULL(EOS(STATIC_1629), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
Filtered ground terms:
1366_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → 1366_0_main_GE(x3, x4, x5, x6, x7)
ARRAY(x1) → ARRAY
Cond_1454_1_main_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_1454_1_main_InvokeMethod2(x1, x4, x5, x6, x7)
1669_0_bubble_Return(x1) → 1669_0_bubble_Return
1454_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → 1454_1_main_InvokeMethod(x1, x3, x4, x5, x6)
Cond_1454_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_1454_1_main_InvokeMethod1(x1, x4, x5, x6, x7)
1666_0_bubble_Return(x1) → 1666_0_bubble_Return
Cond_1454_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_1454_1_main_InvokeMethod(x1, x4, x5, x6, x7)
1634_0_bubble_Return(x1) → 1634_0_bubble_Return
1454_0_bubble_Load(x1, x2) → 1454_0_bubble_Load(x2)
Cond_1366_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1366_0_main_GE1(x1, x4, x5, x6, x7, x8, x9)
968_1_main_InvokeMethod(x1, x2, x3, x4) → 968_1_main_InvokeMethod(x1, x3, x4)
968_0_length_ConstantStackPush(x1, x2) → 968_0_length_ConstantStackPush(x2)
Cond_1366_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_1366_0_main_GE(x1, x4, x5, x6, x7, x8, x9)
884_0_length_Return(x1, x2) → 884_0_length_Return(x2)
1629_0_bubble_NULL(x1, x2, x3) → 1629_0_bubble_NULL(x2, x3)
List(x1) → List
874_0_length_NULL(x1, x2, x3, x4) → 874_0_length_NULL(x2, x3, x4)
Cond_874_0_length_NULL(x1, x2, x3, x4, x5, x6) → Cond_874_0_length_NULL(x1, x4, x6)
Filtered duplicate args:
1366_0_main_GE(x1, x2, x3, x4, x5) → 1366_0_main_GE(x1, x4, x5)
Cond_1366_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_1366_0_main_GE(x1, x2, x5, x6, x7)
Cond_1366_0_main_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_1366_0_main_GE1(x1, x2, x5, x6, x7)
874_0_length_NULL(x1, x2, x3) → 874_0_length_NULL(x2, x3)
1629_0_bubble_NULL(x1, x2) → 1629_0_bubble_NULL(x2)
Filtered unneeded arguments:
968_1_main_InvokeMethod(x1, x2, x3) → 968_1_main_InvokeMethod(x1, x2)
Cond_1366_0_main_GE(x1, x2, x3, x4, x5) → Cond_1366_0_main_GE(x1, x2, x5)
1454_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 1454_1_main_InvokeMethod(x1, x2, x3, x4)
Cond_1454_1_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_1454_1_main_InvokeMethod(x1, x2, x3, x4)
Cond_1454_1_main_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_1454_1_main_InvokeMethod1(x1, x2, x3, x4)
Cond_1454_1_main_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_1454_1_main_InvokeMethod2(x1, x2, x3, x4)
Combined rules. Obtained 6 conditional rules for P and 8 conditional rules for R.
P rules:
968_1_main_InvokeMethod(884_0_length_Return(x0), x2) → 1366_0_main_GE(x2, 0, x0)
1366_0_main_GE(x1, x3, x2) → 968_1_main_InvokeMethod(968_0_length_ConstantStackPush(x4), +(x1, 1)) | &&(&&(>=(x3, x2), >(x1, -1)), <(x1, 2))
1366_0_main_GE(x1, x3, x2) → 1454_1_main_InvokeMethod(1454_0_bubble_Load(x4), x1, x2, x3) | <(x3, x2)
1454_1_main_InvokeMethod(1634_0_bubble_Return, x1, x2, x3) → 1366_0_main_GE(x1, +(x3, 1), x2) | >(x3, -1)
1454_1_main_InvokeMethod(1666_0_bubble_Return, x1, x2, x3) → 1366_0_main_GE(x1, +(x3, 1), x2) | >(x3, -1)
1454_1_main_InvokeMethod(1669_0_bubble_Return, x1, x2, x3) → 1366_0_main_GE(x1, +(x3, 1), x2) | >(x3, -1)
R rules:
968_0_length_ConstantStackPush(x0) → 874_0_length_NULL(0, x0)
874_0_length_NULL(x0, NULL) → 884_0_length_Return(x0)
874_0_length_NULL(x0, java.lang.Object(List)) → 874_0_length_NULL(+(x0, 1), x1) | >(x0, -1)
1454_0_bubble_Load(x0) → 1629_0_bubble_NULL(x0)
1629_0_bubble_NULL(NULL) → 1666_0_bubble_Return
1629_0_bubble_NULL(java.lang.Object(List)) → 1666_0_bubble_Return
1629_0_bubble_NULL(java.lang.Object(List)) → 1669_0_bubble_Return
1629_0_bubble_NULL(java.lang.Object(List)) → 1629_0_bubble_NULL(java.lang.Object(List))
Performed bisimulation on rules. Used the following equivalence classes: {[List, 1666_0_bubble_Return, 1669_0_bubble_Return, 1634_0_bubble_Return]=List, [Cond_1454_1_main_InvokeMethod_5, Cond_1454_1_main_InvokeMethod1_5, Cond_1454_1_main_InvokeMethod2_5]=Cond_1454_1_main_InvokeMethod_5}
Finished conversion. Obtained 7 rules for P and 8 rules for R. System has predefined symbols.
P rules:
968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0), x2) → 1366_0_MAIN_GE(x2, 0, x0)
1366_0_MAIN_GE(x1, x3, x2) → COND_1366_0_MAIN_GE(&&(&&(>=(x3, x2), >(x1, -1)), <(x1, 2)), x1, x3, x2, x4)
COND_1366_0_MAIN_GE(TRUE, x1, x3, x2, x4) → 968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4), +(x1, 1))
1366_0_MAIN_GE(x1, x3, x2) → COND_1366_0_MAIN_GE1(<(x3, x2), x1, x3, x2, x4)
COND_1366_0_MAIN_GE1(TRUE, x1, x3, x2, x4) → 1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4), x1, x2, x3)
1454_1_MAIN_INVOKEMETHOD(List, x1, x2, x3) → COND_1454_1_MAIN_INVOKEMETHOD(>(x3, -1), List, x1, x2, x3)
COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1, x2, x3) → 1366_0_MAIN_GE(x1, +(x3, 1), x2)
R rules:
968_0_length_ConstantStackPush(x0) → 874_0_length_NULL(0, x0)
874_0_length_NULL(x0, NULL) → 884_0_length_Return(x0)
874_0_length_NULL(x0, java.lang.Object(List)) → Cond_874_0_length_NULL(>(x0, -1), x0, java.lang.Object(List), x1)
Cond_874_0_length_NULL(TRUE, x0, java.lang.Object(List), x1) → 874_0_length_NULL(+(x0, 1), x1)
1454_0_bubble_Load(x0) → 1629_0_bubble_NULL(x0)
1629_0_bubble_NULL(NULL) → List
1629_0_bubble_NULL(java.lang.Object(List)) → List
1629_0_bubble_NULL(java.lang.Object(List)) → 1629_0_bubble_NULL(java.lang.Object(List))
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if (x2[0] →* x1[1]∧0 →* x3[1]∧x0[0] →* x2[1])
(0) -> (3), if (x2[0] →* x1[3]∧0 →* x3[3]∧x0[0] →* x2[3])
(1) -> (2), if (x3[1] >= x2[1] && x1[1] > -1 && x1[1] < 2 ∧x1[1] →* x1[2]∧x3[1] →* x3[2]∧x2[1] →* x2[2]∧x4[1] →* x4[2])
(2) -> (0), if (968_0_length_ConstantStackPush(x4[2]) →* 884_0_length_Return(x0[0])∧x1[2] + 1 →* x2[0])
(3) -> (4), if (x3[3] < x2[3] ∧x1[3] →* x1[4]∧x3[3] →* x3[4]∧x2[3] →* x2[4]∧x4[3] →* x4[4])
(4) -> (5), if (1454_0_bubble_Load(x4[4]) →* List∧x1[4] →* x1[5]∧x2[4] →* x2[5]∧x3[4] →* x3[5])
(5) -> (6), if (x3[5] > -1 ∧x1[5] →* x1[6]∧x2[5] →* x2[6]∧x3[5] →* x3[6])
(6) -> (1), if (x1[6] →* x1[1]∧x3[6] + 1 →* x3[1]∧x2[6] →* x2[1])
(6) -> (3), if (x1[6] →* x1[3]∧x3[6] + 1 →* x3[3]∧x2[6] →* x2[3])
(1) (968_0_length_ConstantStackPush(x4[2])=884_0_length_Return(x0[0])∧+(x1[2], 1)=x2[0]∧x2[0]=x1[1]∧0=x3[1]∧x0[0]=x2[1] ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), x2[0])≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), x2[0])≥1366_0_MAIN_GE(x2[0], 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(2) (0=x0∧874_0_length_NULL(x0, x4[2])=884_0_length_Return(x0[0]) ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(3) (884_0_length_Return(x1)=884_0_length_Return(x0[0])∧0=x1 ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(4) (Cond_874_0_length_NULL(>(x2, -1), x2, java.lang.Object(List), x3)=884_0_length_Return(x0[0])∧0=x2 ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(5) (968_1_MAIN_INVOKEMETHOD(884_0_length_Return(0), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(0), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, 0)∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(6) (Cond_874_0_length_NULL(TRUE, 0, java.lang.Object(List), x3)=884_0_length_Return(x0[0]) ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(7) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(8) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 ≥ 0∧[(-1)bso_58] ≥ 0)
(9) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(10) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 ≥ 0∧[(-1)bso_58] ≥ 0)
(11) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(12) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 ≥ 0∧[(-1)bso_58] ≥ 0)
(13) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
(14) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
(15) (968_0_length_ConstantStackPush(x4[2])=884_0_length_Return(x0[0])∧+(x1[2], 1)=x2[0]∧x2[0]=x1[3]∧0=x3[3]∧x0[0]=x2[3] ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), x2[0])≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), x2[0])≥1366_0_MAIN_GE(x2[0], 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(16) (0=x6∧874_0_length_NULL(x6, x4[2])=884_0_length_Return(x0[0]) ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(17) (884_0_length_Return(x7)=884_0_length_Return(x0[0])∧0=x7 ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(18) (Cond_874_0_length_NULL(>(x8, -1), x8, java.lang.Object(List), x9)=884_0_length_Return(x0[0])∧0=x8 ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(19) (968_1_MAIN_INVOKEMETHOD(884_0_length_Return(0), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(0), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, 0)∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(20) (Cond_874_0_length_NULL(TRUE, 0, java.lang.Object(List), x9)=884_0_length_Return(x0[0]) ⇒ 968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥NonInfC∧968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), +(x1[2], 1))≥1366_0_MAIN_GE(+(x1[2], 1), 0, x0[0])∧(UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥))
(21) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(22) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 ≥ 0∧[(-1)bso_58] ≥ 0)
(23) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(24) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 ≥ 0∧[(-1)bso_58] ≥ 0)
(25) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧[(-1)bso_58] ≥ 0)
(26) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 ≥ 0∧[(-1)bso_58] ≥ 0)
(27) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧[bni_57] = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
(28) ((UIncreasing(1366_0_MAIN_GE(x2[0], 0, x0[0])), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_58] ≥ 0)
(29) (x2[0]=x1[1]∧0=x3[1]∧x0[0]=x2[1]∧&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2))=TRUE∧x1[1]=x1[2]∧x3[1]=x3[2]∧x2[1]=x2[2]∧x4[1]=x4[2] ⇒ 1366_0_MAIN_GE(x1[1], x3[1], x2[1])≥NonInfC∧1366_0_MAIN_GE(x1[1], x3[1], x2[1])≥COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])∧(UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥))
(30) (<(x1[1], 2)=TRUE∧>=(0, x2[1])=TRUE∧>(x1[1], -1)=TRUE ⇒ 1366_0_MAIN_GE(x1[1], 0, x2[1])≥NonInfC∧1366_0_MAIN_GE(x1[1], 0, x2[1])≥COND_1366_0_MAIN_GE(&&(&&(>=(0, x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], 0, x2[1], x4[1])∧(UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥))
(31) ([1] + [-1]x1[1] ≥ 0∧[-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧[(-1)bso_60] ≥ 0)
(32) ([1] + [-1]x1[1] ≥ 0∧[-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧[(-1)bso_60] ≥ 0)
(33) ([1] + [-1]x1[1] ≥ 0∧[-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧[(-1)bso_60] ≥ 0)
(34) ([1] + [-1]x1[1] ≥ 0∧[-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧0 = 0∧[(-1)bso_60] ≥ 0)
(35) ([1] + [-1]x1[1] ≥ 0∧x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧0 = 0∧[(-1)bso_60] ≥ 0)
(36) (x1[6]=x1[1]∧+(x3[6], 1)=x3[1]∧x2[6]=x2[1]∧&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2))=TRUE∧x1[1]=x1[2]∧x3[1]=x3[2]∧x2[1]=x2[2]∧x4[1]=x4[2] ⇒ 1366_0_MAIN_GE(x1[1], x3[1], x2[1])≥NonInfC∧1366_0_MAIN_GE(x1[1], x3[1], x2[1])≥COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])∧(UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥))
(37) (<(x1[1], 2)=TRUE∧>=(+(x3[6], 1), x2[1])=TRUE∧>(x1[1], -1)=TRUE ⇒ 1366_0_MAIN_GE(x1[1], +(x3[6], 1), x2[1])≥NonInfC∧1366_0_MAIN_GE(x1[1], +(x3[6], 1), x2[1])≥COND_1366_0_MAIN_GE(&&(&&(>=(+(x3[6], 1), x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], +(x3[6], 1), x2[1], x4[1])∧(UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥))
(38) ([1] + [-1]x1[1] ≥ 0∧x3[6] + [1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧[(-1)bso_60] ≥ 0)
(39) ([1] + [-1]x1[1] ≥ 0∧x3[6] + [1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧[(-1)bso_60] ≥ 0)
(40) ([1] + [-1]x1[1] ≥ 0∧x3[6] + [1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧[(-1)bso_60] ≥ 0)
(41) ([1] + [-1]x1[1] ≥ 0∧x3[6] + [1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧0 = 0∧[(-1)bso_60] ≥ 0)
(42) ([1] + [-1]x1[1] ≥ 0∧x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧0 = 0∧[(-1)bso_60] ≥ 0)
(43) ([1] + [-1]x1[1] ≥ 0∧x2[1] ≥ 0∧x1[1] ≥ 0∧x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧0 = 0∧[(-1)bso_60] ≥ 0)
(44) ([1] + [-1]x1[1] ≥ 0∧x2[1] ≥ 0∧x1[1] ≥ 0∧x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])), ≥)∧[(-1)bni_59 + (-1)Bound*bni_59] + [(-1)bni_59]x1[1] ≥ 0∧0 = 0∧[(-1)bso_60] ≥ 0)
(45) (&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2))=TRUE∧x1[1]=x1[2]∧x3[1]=x3[2]∧x2[1]=x2[2]∧x4[1]=x4[2]∧968_0_length_ConstantStackPush(x4[2])=884_0_length_Return(x0[0])∧+(x1[2], 1)=x2[0] ⇒ COND_1366_0_MAIN_GE(TRUE, x1[2], x3[2], x2[2], x4[2])≥NonInfC∧COND_1366_0_MAIN_GE(TRUE, x1[2], x3[2], x2[2], x4[2])≥968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))∧(UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥))
(46) (0=x12∧874_0_length_NULL(x12, x4[2])=884_0_length_Return(x0[0])∧<(x1[1], 2)=TRUE∧>=(x3[1], x2[1])=TRUE∧>(x1[1], -1)=TRUE ⇒ COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], x4[2])≥NonInfC∧COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], x4[2])≥968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[1], 1))∧(UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥))
(47) (884_0_length_Return(x13)=884_0_length_Return(x0[0])∧0=x13∧<(x1[1], 2)=TRUE∧>=(x3[1], x2[1])=TRUE∧>(x1[1], -1)=TRUE ⇒ COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], NULL)≥NonInfC∧COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], NULL)≥968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(NULL), +(x1[1], 1))∧(UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥))
(48) (Cond_874_0_length_NULL(>(x14, -1), x14, java.lang.Object(List), x15)=884_0_length_Return(x0[0])∧0=x14∧<(x1[1], 2)=TRUE∧>=(x3[1], x2[1])=TRUE∧>(x1[1], -1)=TRUE ⇒ COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], java.lang.Object(List))≥NonInfC∧COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], java.lang.Object(List))≥968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(java.lang.Object(List)), +(x1[1], 1))∧(UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥))
(49) (<(x1[1], 2)=TRUE∧>=(x3[1], x2[1])=TRUE∧>(x1[1], -1)=TRUE ⇒ COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], NULL)≥NonInfC∧COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], NULL)≥968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(NULL), +(x1[1], 1))∧(UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥))
(50) (<(x1[1], 2)=TRUE∧>=(x3[1], x2[1])=TRUE∧>(x1[1], -1)=TRUE∧Cond_874_0_length_NULL(TRUE, 0, java.lang.Object(List), x15)=884_0_length_Return(x0[0]) ⇒ COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], java.lang.Object(List))≥NonInfC∧COND_1366_0_MAIN_GE(TRUE, x1[1], x3[1], x2[1], java.lang.Object(List))≥968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(java.lang.Object(List)), +(x1[1], 1))∧(UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥))
(51) ([1] + [-1]x1[1] ≥ 0∧x3[1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(52) ([1] + [-1]x1[1] ≥ 0∧x3[1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(53) ([1] + [-1]x1[1] ≥ 0∧x3[1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(54) ([1] + [-1]x1[1] ≥ 0∧x3[1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(55) ([1] + [-1]x1[1] ≥ 0∧x3[1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(56) ([1] + [-1]x1[1] ≥ 0∧x3[1] + [-1]x2[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(57) ([1] + [-1]x1[1] ≥ 0∧x3[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(58) ([1] + [-1]x1[1] ≥ 0∧x3[1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(59) ([1] + [-1]x1[1] ≥ 0∧x3[1] ≥ 0∧x1[1] ≥ 0∧x2[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(60) ([1] + [-1]x1[1] ≥ 0∧x3[1] ≥ 0∧x1[1] ≥ 0∧x2[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(61) ([1] + [-1]x1[1] ≥ 0∧x3[1] ≥ 0∧x1[1] ≥ 0∧x2[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(62) ([1] + [-1]x1[1] ≥ 0∧x3[1] ≥ 0∧x1[1] ≥ 0∧x2[1] ≥ 0 ⇒ (UIncreasing(968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]x1[1] ≥ 0∧[1 + (-1)bso_62] ≥ 0)
(63) (x2[0]=x1[3]∧0=x3[3]∧x0[0]=x2[3]∧<(x3[3], x2[3])=TRUE∧x1[3]=x1[4]∧x3[3]=x3[4]∧x2[3]=x2[4]∧x4[3]=x4[4] ⇒ 1366_0_MAIN_GE(x1[3], x3[3], x2[3])≥NonInfC∧1366_0_MAIN_GE(x1[3], x3[3], x2[3])≥COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])∧(UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥))
(64) (<(0, x2[3])=TRUE ⇒ 1366_0_MAIN_GE(x2[0], 0, x2[3])≥NonInfC∧1366_0_MAIN_GE(x2[0], 0, x2[3])≥COND_1366_0_MAIN_GE1(<(0, x2[3]), x2[0], 0, x2[3], x4[3])∧(UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥))
(65) (x2[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]x2[0] ≥ 0∧[(-1)bso_64] ≥ 0)
(66) (x2[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]x2[0] ≥ 0∧[(-1)bso_64] ≥ 0)
(67) (x2[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]x2[0] ≥ 0∧[(-1)bso_64] ≥ 0)
(68) (x2[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63] = 0∧[(-1)bni_63 + (-1)Bound*bni_63] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_64] ≥ 0)
(69) (x2[3] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63] = 0∧[(-1)bni_63 + (-1)Bound*bni_63] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_64] ≥ 0)
(70) (x1[6]=x1[3]∧+(x3[6], 1)=x3[3]∧x2[6]=x2[3]∧<(x3[3], x2[3])=TRUE∧x1[3]=x1[4]∧x3[3]=x3[4]∧x2[3]=x2[4]∧x4[3]=x4[4] ⇒ 1366_0_MAIN_GE(x1[3], x3[3], x2[3])≥NonInfC∧1366_0_MAIN_GE(x1[3], x3[3], x2[3])≥COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])∧(UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥))
(71) (<(+(x3[6], 1), x2[3])=TRUE ⇒ 1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[3])≥NonInfC∧1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[3])≥COND_1366_0_MAIN_GE1(<(+(x3[6], 1), x2[3]), x1[6], +(x3[6], 1), x2[3], x4[3])∧(UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥))
(72) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]x1[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(73) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]x1[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(74) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]x1[6] ≥ 0∧[(-1)bso_64] ≥ 0)
(75) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63] = 0∧[(-1)bni_63 + (-1)Bound*bni_63] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_64] ≥ 0)
(76) (x2[3] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63] = 0∧[(-1)bni_63 + (-1)Bound*bni_63] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_64] ≥ 0)
(77) (x2[3] ≥ 0∧x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63] = 0∧[(-1)bni_63 + (-1)Bound*bni_63] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_64] ≥ 0)
(78) (x2[3] ≥ 0∧x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-1)bni_63] = 0∧[(-1)bni_63 + (-1)Bound*bni_63] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_64] ≥ 0)
(79) (<(x3[3], x2[3])=TRUE∧x1[3]=x1[4]∧x3[3]=x3[4]∧x2[3]=x2[4]∧x4[3]=x4[4]∧1454_0_bubble_Load(x4[4])=List∧x1[4]=x1[5]∧x2[4]=x2[5]∧x3[4]=x3[5] ⇒ COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4])≥NonInfC∧COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4])≥1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])∧(UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥))
(80) (<(x3[3], x2[3])=TRUE∧1454_0_bubble_Load(x4[4])=List ⇒ COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x4[4])≥NonInfC∧COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x4[4])≥1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[3], x2[3], x3[3])∧(UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥))
(81) (1629_0_bubble_NULL(x18)=List∧<(x3[3], x2[3])=TRUE ⇒ COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x18)≥NonInfC∧COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x18)≥1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x18), x1[3], x2[3], x3[3])∧(UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥))
(82) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]x1[3] ≥ 0∧[(-1)bso_66] ≥ 0)
(83) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]x1[3] ≥ 0∧[(-1)bso_66] ≥ 0)
(84) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]x1[3] ≥ 0∧[(-1)bso_66] ≥ 0)
(85) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧[(-1)bni_65] = 0∧[(-1)bni_65 + (-1)Bound*bni_65] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_66] ≥ 0)
(86) (x2[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧[(-1)bni_65] = 0∧[(-1)bni_65 + (-1)Bound*bni_65] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_66] ≥ 0)
(87) (x2[3] ≥ 0∧x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧[(-1)bni_65] = 0∧[(-1)bni_65 + (-1)Bound*bni_65] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_66] ≥ 0)
(88) (x2[3] ≥ 0∧x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧[(-1)bni_65] = 0∧[(-1)bni_65 + (-1)Bound*bni_65] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_66] ≥ 0)
(89) (>(x3[5], -1)=TRUE∧x1[5]=x1[6]∧x2[5]=x2[6]∧x3[5]=x3[6] ⇒ 1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥NonInfC∧1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])∧(UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥))
(90) (>(x3[5], -1)=TRUE ⇒ 1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥NonInfC∧1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])∧(UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥))
(91) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]x1[5] ≥ 0∧[(-1)bso_68] ≥ 0)
(92) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]x1[5] ≥ 0∧[(-1)bso_68] ≥ 0)
(93) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]x1[5] ≥ 0∧[(-1)bso_68] ≥ 0)
(94) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧0 = 0∧[(-1)bni_67] = 0∧[(-1)bni_67 + (-1)Bound*bni_67] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_68] ≥ 0)
(95) (>(x3[5], -1)=TRUE∧x1[5]=x1[6]∧x2[5]=x2[6]∧x3[5]=x3[6]∧x1[6]=x1[1]∧+(x3[6], 1)=x3[1]∧x2[6]=x2[1] ⇒ COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6])≥NonInfC∧COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6])≥1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])∧(UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥))
(96) (>(x3[5], -1)=TRUE ⇒ COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[5], x2[5], x3[5])≥NonInfC∧COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[5], x2[5], x3[5])≥1366_0_MAIN_GE(x1[5], +(x3[5], 1), x2[5])∧(UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥))
(97) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]x1[5] ≥ 0∧[(-1)bso_70] ≥ 0)
(98) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]x1[5] ≥ 0∧[(-1)bso_70] ≥ 0)
(99) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]x1[5] ≥ 0∧[(-1)bso_70] ≥ 0)
(100) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧0 = 0∧[(-1)bni_69] = 0∧[(-1)bni_69 + (-1)Bound*bni_69] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_70] ≥ 0)
(101) (>(x3[5], -1)=TRUE∧x1[5]=x1[6]∧x2[5]=x2[6]∧x3[5]=x3[6]∧x1[6]=x1[3]∧+(x3[6], 1)=x3[3]∧x2[6]=x2[3] ⇒ COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6])≥NonInfC∧COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6])≥1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])∧(UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥))
(102) (>(x3[5], -1)=TRUE ⇒ COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[5], x2[5], x3[5])≥NonInfC∧COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[5], x2[5], x3[5])≥1366_0_MAIN_GE(x1[5], +(x3[5], 1), x2[5])∧(UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥))
(103) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]x1[5] ≥ 0∧[(-1)bso_70] ≥ 0)
(104) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]x1[5] ≥ 0∧[(-1)bso_70] ≥ 0)
(105) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]x1[5] ≥ 0∧[(-1)bso_70] ≥ 0)
(106) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧0 = 0∧[(-1)bni_69] = 0∧[(-1)bni_69 + (-1)Bound*bni_69] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_70] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = [1]
POL(968_0_length_ConstantStackPush(x1)) = [-1] + [-1]x1
POL(874_0_length_NULL(x1, x2)) = [-1] + [-1]x2
POL(0) = 0
POL(NULL) = [-1]
POL(884_0_length_Return(x1)) = [-1] + [-1]x1
POL(java.lang.Object(x1)) = [-1] + [-1]x1
POL(List) = [-1]
POL(Cond_874_0_length_NULL(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + x2
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(1454_0_bubble_Load(x1)) = 0
POL(1629_0_bubble_NULL(x1)) = [-1] + [-1]x1
POL(968_1_MAIN_INVOKEMETHOD(x1, x2)) = [-1] + [-1]x2
POL(1366_0_MAIN_GE(x1, x2, x3)) = [-1] + [-1]x1
POL(COND_1366_0_MAIN_GE(x1, x2, x3, x4, x5)) = [-1] + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(<(x1, x2)) = [-1]
POL(2) = [2]
POL(COND_1366_0_MAIN_GE1(x1, x2, x3, x4, x5)) = [-1] + [-1]x2
POL(1454_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x2
POL(COND_1454_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + [-1]x3
COND_1366_0_MAIN_GE(TRUE, x1[2], x3[2], x2[2], x4[2]) → 968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))
1366_0_MAIN_GE(x1[1], x3[1], x2[1]) → COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])
COND_1366_0_MAIN_GE(TRUE, x1[2], x3[2], x2[2], x4[2]) → 968_1_MAIN_INVOKEMETHOD(968_0_length_ConstantStackPush(x4[2]), +(x1[2], 1))
968_1_MAIN_INVOKEMETHOD(884_0_length_Return(x0[0]), x2[0]) → 1366_0_MAIN_GE(x2[0], 0, x0[0])
1366_0_MAIN_GE(x1[1], x3[1], x2[1]) → COND_1366_0_MAIN_GE(&&(&&(>=(x3[1], x2[1]), >(x1[1], -1)), <(x1[1], 2)), x1[1], x3[1], x2[1], x4[1])
1366_0_MAIN_GE(x1[3], x3[3], x2[3]) → COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])
COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4]) → 1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])
1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5]) → COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])
COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6]) → 1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1
List1 → 1629_0_bubble_NULL(java.lang.Object(List))1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if (x2[0] →* x1[1]∧0 →* x3[1]∧x0[0] →* x2[1])
(6) -> (1), if (x1[6] →* x1[1]∧x3[6] + 1 →* x3[1]∧x2[6] →* x2[1])
(0) -> (3), if (x2[0] →* x1[3]∧0 →* x3[3]∧x0[0] →* x2[3])
(6) -> (3), if (x1[6] →* x1[3]∧x3[6] + 1 →* x3[3]∧x2[6] →* x2[3])
(3) -> (4), if (x3[3] < x2[3] ∧x1[3] →* x1[4]∧x3[3] →* x3[4]∧x2[3] →* x2[4]∧x4[3] →* x4[4])
(4) -> (5), if (1454_0_bubble_Load(x4[4]) →* List∧x1[4] →* x1[5]∧x2[4] →* x2[5]∧x3[4] →* x3[5])
(5) -> (6), if (x3[5] > -1 ∧x1[5] →* x1[6]∧x2[5] →* x2[6]∧x3[5] →* x3[6])
!= | ~ | 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
(6) -> (3), if (x1[6] →* x1[3]∧x3[6] + 1 →* x3[3]∧x2[6] →* x2[3])
(3) -> (4), if (x3[3] < x2[3] ∧x1[3] →* x1[4]∧x3[3] →* x3[4]∧x2[3] →* x2[4]∧x4[3] →* x4[4])
(4) -> (5), if (1454_0_bubble_Load(x4[4]) →* List∧x1[4] →* x1[5]∧x2[4] →* x2[5]∧x3[4] →* x3[5])
(5) -> (6), if (x3[5] > -1 ∧x1[5] →* x1[6]∧x2[5] →* x2[6]∧x3[5] →* x3[6])
!= | ~ | 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
(6) -> (3), if (x1[6] →* x1[3]∧x3[6] + 1 →* x3[3]∧x2[6] →* x2[3])
(3) -> (4), if (x3[3] < x2[3] ∧x1[3] →* x1[4]∧x3[3] →* x3[4]∧x2[3] →* x2[4]∧x4[3] →* x4[4])
(4) -> (5), if (1454_0_bubble_Load(x4[4]) →* List∧x1[4] →* x1[5]∧x2[4] →* x2[5]∧x3[4] →* x3[5])
(5) -> (6), if (x3[5] > -1 ∧x1[5] →* x1[6]∧x2[5] →* x2[6]∧x3[5] →* x3[6])
(1) (>(x3[5], -1)=TRUE∧x1[5]=x1[6]∧x2[5]=x2[6]∧x3[5]=x3[6]∧x1[6]=x1[3]∧+(x3[6], 1)=x3[3]∧x2[6]=x2[3] ⇒ COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6])≥NonInfC∧COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6])≥1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])∧(UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥))
(2) (>(x3[5], -1)=TRUE ⇒ COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[5], x2[5], x3[5])≥NonInfC∧COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[5], x2[5], x3[5])≥1366_0_MAIN_GE(x1[5], +(x3[5], 1), x2[5])∧(UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥))
(3) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x3[5] + [bni_34]x2[5] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(4) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x3[5] + [bni_34]x2[5] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(5) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x3[5] + [bni_34]x2[5] ≥ 0∧[1 + (-1)bso_35] ≥ 0)
(6) (x3[5] ≥ 0 ⇒ (UIncreasing(1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x3[5] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
(7) (>(x3[5], -1)=TRUE∧x1[5]=x1[6]∧x2[5]=x2[6]∧x3[5]=x3[6] ⇒ 1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥NonInfC∧1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])∧(UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥))
(8) (>(x3[5], -1)=TRUE ⇒ 1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥NonInfC∧1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5])≥COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])∧(UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥))
(9) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x3[5] + [bni_36]x2[5] ≥ 0∧[(-1)bso_37] ≥ 0)
(10) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x3[5] + [bni_36]x2[5] ≥ 0∧[(-1)bso_37] ≥ 0)
(11) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x3[5] + [bni_36]x2[5] ≥ 0∧[(-1)bso_37] ≥ 0)
(12) (x3[5] ≥ 0 ⇒ (UIncreasing(COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])), ≥)∧[bni_36] = 0∧0 = 0∧[(-1)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]x3[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
(13) (<(x3[3], x2[3])=TRUE∧x1[3]=x1[4]∧x3[3]=x3[4]∧x2[3]=x2[4]∧x4[3]=x4[4]∧1454_0_bubble_Load(x4[4])=List∧x1[4]=x1[5]∧x2[4]=x2[5]∧x3[4]=x3[5] ⇒ COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4])≥NonInfC∧COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4])≥1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])∧(UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥))
(14) (<(x3[3], x2[3])=TRUE∧1454_0_bubble_Load(x4[4])=List ⇒ COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x4[4])≥NonInfC∧COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x4[4])≥1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[3], x2[3], x3[3])∧(UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥))
(15) (1629_0_bubble_NULL(x0)=List∧<(x3[3], x2[3])=TRUE ⇒ COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x0)≥NonInfC∧COND_1366_0_MAIN_GE1(TRUE, x1[3], x3[3], x2[3], x0)≥1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x0), x1[3], x2[3], x3[3])∧(UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥))
(16) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x2[3] + [(-1)bni_38]x3[3] ≥ 0∧[(-1)bso_39] ≥ 0)
(17) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x2[3] + [(-1)bni_38]x3[3] ≥ 0∧[(-1)bso_39] ≥ 0)
(18) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x2[3] + [(-1)bni_38]x3[3] ≥ 0∧[(-1)bso_39] ≥ 0)
(19) (x2[3] + [-1] + [-1]x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x2[3] + [(-1)bni_38]x3[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
(20) (x2[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_38] + [bni_38]x2[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
(21) (x2[3] ≥ 0∧x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_38] + [bni_38]x2[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
(22) (x2[3] ≥ 0∧x3[3] ≥ 0 ⇒ (UIncreasing(1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_38] + [bni_38]x2[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
(23) (x1[6]=x1[3]∧+(x3[6], 1)=x3[3]∧x2[6]=x2[3]∧<(x3[3], x2[3])=TRUE∧x1[3]=x1[4]∧x3[3]=x3[4]∧x2[3]=x2[4]∧x4[3]=x4[4] ⇒ 1366_0_MAIN_GE(x1[3], x3[3], x2[3])≥NonInfC∧1366_0_MAIN_GE(x1[3], x3[3], x2[3])≥COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])∧(UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥))
(24) (<(+(x3[6], 1), x2[3])=TRUE ⇒ 1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[3])≥NonInfC∧1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[3])≥COND_1366_0_MAIN_GE1(<(+(x3[6], 1), x2[3]), x1[6], +(x3[6], 1), x2[3], x4[3])∧(UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥))
(25) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-2)bni_40 + (-1)Bound*bni_40] + [bni_40]x2[3] + [(-1)bni_40]x3[6] ≥ 0∧[(-1)bso_41] ≥ 0)
(26) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-2)bni_40 + (-1)Bound*bni_40] + [bni_40]x2[3] + [(-1)bni_40]x3[6] ≥ 0∧[(-1)bso_41] ≥ 0)
(27) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧[(-2)bni_40 + (-1)Bound*bni_40] + [bni_40]x2[3] + [(-1)bni_40]x3[6] ≥ 0∧[(-1)bso_41] ≥ 0)
(28) (x2[3] + [-2] + [-1]x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧0 = 0∧[(-2)bni_40 + (-1)Bound*bni_40] + [bni_40]x2[3] + [(-1)bni_40]x3[6] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
(29) (x2[3] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]x2[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
(30) (x2[3] ≥ 0∧x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]x2[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
(31) (x2[3] ≥ 0∧x3[6] ≥ 0 ⇒ (UIncreasing(COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])), ≥)∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]x2[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(1454_0_bubble_Load(x1)) = [-1] + [-1]x1
POL(1629_0_bubble_NULL(x1)) = [-1] + x1
POL(NULL) = [-1]
POL(List) = [2]
POL(java.lang.Object(x1)) = 0
POL(COND_1454_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [1] + [-1]x5 + x4 + [-1]x2
POL(1366_0_MAIN_GE(x1, x2, x3)) = [-1] + x3 + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(1454_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(>(x1, x2)) = [-1]
POL(-1) = [-1]
POL(COND_1366_0_MAIN_GE1(x1, x2, x3, x4, x5)) = [-1] + x4 + [-1]x3
POL(<(x1, x2)) = [-1]
COND_1454_1_MAIN_INVOKEMETHOD(TRUE, List, x1[6], x2[6], x3[6]) → 1366_0_MAIN_GE(x1[6], +(x3[6], 1), x2[6])
COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4]) → 1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])
1366_0_MAIN_GE(x1[3], x3[3], x2[3]) → COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])
1454_1_MAIN_INVOKEMETHOD(List, x1[5], x2[5], x3[5]) → COND_1454_1_MAIN_INVOKEMETHOD(>(x3[5], -1), List, x1[5], x2[5], x3[5])
COND_1366_0_MAIN_GE1(TRUE, x1[4], x3[4], x2[4], x4[4]) → 1454_1_MAIN_INVOKEMETHOD(1454_0_bubble_Load(x4[4]), x1[4], x2[4], x3[4])
1366_0_MAIN_GE(x1[3], x3[3], x2[3]) → COND_1366_0_MAIN_GE1(<(x3[3], x2[3]), x1[3], x3[3], x2[3], x4[3])
List1 → 1629_0_bubble_NULL(java.lang.Object(List))1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (4), if (x3[3] < x2[3] ∧x1[3] →* x1[4]∧x3[3] →* x3[4]∧x2[3] →* x2[4]∧x4[3] →* x4[4])
(4) -> (5), if (1454_0_bubble_Load(x4[4]) →* List∧x1[4] →* x1[5]∧x2[4] →* x2[5]∧x3[4] →* x3[5])
!= | ~ | 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
(5) -> (6), if (x3[5] > -1 ∧x1[5] →* x1[6]∧x2[5] →* x2[6]∧x3[5] →* x3[6])