Termination proof of /tmp/tmp929XV3/MainGet.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1990 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 660 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 190 ms)

        ↳9 AND

            ↳10 IDP

                ↳11 IDependencyGraphProof (⇔, 0 ms)

                ↳12 TRUE

            ↳13 IDP

                ↳14 IDependencyGraphProof (⇔, 0 ms)

                ↳15 TRUE

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 540 ms)

        ↳18 IDP

        ↳19 IDPtoQDPProof (⇒, 10 ms)

        ↳20 QDP

        ↳21 UsableRulesProof (⇔, 0 ms)

        ↳22 QDP

        ↳23 QReductionProof (⇔, 0 ms)

        ↳24 QDP

        ↳25 QDPSizeChangeProof (⇔, 0 ms)

        ↳26 YES

    ↳27 JBCTerminationSCC

        ↳28 SCCToIDPv1Proof (⇒, 1230 ms)

        ↳29 IDP

        ↳30 IDPNonInfProof (⇒, 130 ms)

        ↳31 IDP

        ↳32 IDependencyGraphProof (⇔, 0 ms)

        ↳33 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: DoublyLinkedList/MainGet

package DoublyLinkedList;

/**
 * A linked list with pointers to the previous and next elements
 * @author cotto
 */
public class DoublyLinkedList {
    public int value;
    public DoublyLinkedList prev;
    public DoublyLinkedList next;

    public DoublyLinkedList(final int v) {
        this.value = v;
    }

    public DoublyLinkedList getFirst() {
        if (this.prev == null) {
            return this;
        }
        return this.prev.getFirst();
    }

    public void move(final int relativePosition) {
        if (relativePosition == 0) {
            return;
        }
        if (relativePosition > 0 && this.next != null) {
            final DoublyLinkedList temp = this.next;
            if (this.prev != null) {
                this.prev.next = temp;
            }
            temp.prev = this.prev;
            this.next = temp.next;
            temp.next = this;
            this.prev = temp;
            move(relativePosition - 1);
        }
        if (relativePosition < 0 && this.prev != null) {
            final DoublyLinkedList temp = this.prev;
            if (this.next != null) {
                this.next.prev = temp;
            }
            temp.next = this.next;
            this.prev = temp.prev;
            temp.prev = this;
            this.next = temp;
            move(relativePosition - 1);
        }
    }

    public DoublyLinkedList get(final int index) {
        return this.getFirst().getR(index);
    }

    private DoublyLinkedList getR(final int index) {
      if (index == 0 || this.next == null) {
        return this;
      }
      return this.next.getR(index - 1);
    }

    public DoublyLinkedList find(final int v) {
        final DoublyLinkedList first = this.getFirst();
        return first.findR(v);
    }

    private DoublyLinkedList findR(final int v) {
        if (this.value == v) {
            return this;
        }
        if (this.next != null) {
            return this.next.findR(v);
        }
        return null;
    }

    public void delete(final int v) {
        final DoublyLinkedList elem = find(v);
        if (elem != null) {
            if (elem.prev != null) {
                elem.prev.next = elem.next;
            }
            if (elem.next != null) {
                elem.next.prev = elem.prev;
            }
        }
    }

    public DoublyLinkedList copy() {
        final DoublyLinkedList first = this.getFirst();
        return first.copyR(null);
    }

    private DoublyLinkedList copyR(final DoublyLinkedList p) {
        final DoublyLinkedList copy = new DoublyLinkedList(this.value);
        copy.prev = p;
        if (p != null) {
            p.next = copy;
        }
        if (this.next != null) {
            this.next.copyR(copy);
        }
        return copy;
    }

    static DoublyLinkedList createList() {
        final int count = Random.random();
        DoublyLinkedList cur = null;
        for (int i = 0; i < count; i++) {
            final DoublyLinkedList old = cur;
            cur = new DoublyLinkedList(Random.random());
            cur.prev = old;
            if (old != null) {
              old.next = cur;
            }
        }

        return cur;
    }
}


package DoublyLinkedList;

/**
 *
 * @author cotto
 */
public class MainGet {
    public static void main(final String[] args) {
        Random.args = args;
        final DoublyLinkedList list = DoublyLinkedList.createList();
        list.get(Random.random());
    }
}


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

    public static int random() {
        if (args.length <= index) {
            return 0;
        }
        final String string = args[index];
        index++;
        if (string == null) {
            return 0;
        }
        return string.length();
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
DoublyLinkedList.MainGet.main([Ljava/lang/String;)V: Graph of 261 nodes with 0 SCCs.

DoublyLinkedList.DoublyLinkedList.createList()LDoublyLinkedList/DoublyLinkedList;: Graph of 166 nodes with 1 SCC.

DoublyLinkedList.DoublyLinkedList.getFirst()LDoublyLinkedList/DoublyLinkedList;: Graph of 56 nodes with 0 SCCs.

DoublyLinkedList.DoublyLinkedList.getR(I)LDoublyLinkedList/DoublyLinkedList;: Graph of 72 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DoublyLinkedList.DoublyLinkedList.getR(I)LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods: DoublyLinkedList.DoublyLinkedList.getR(I)LDoublyLinkedList/DoublyLinkedList;
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 33 rules for P and 43 rules for R.

P rules:
3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(o2058sub), i1415, i1415) → 3230_0_getR_EQ(EOS(STATIC_3230), java.lang.Object(o2058sub), i1415, i1415)
3230_0_getR_EQ(EOS(STATIC_3230), java.lang.Object(o2058sub), i1415, i1415) → 3237_0_getR_Load(EOS(STATIC_3237), java.lang.Object(o2058sub), i1415) | >(i1415, 0)
3237_0_getR_Load(EOS(STATIC_3237), java.lang.Object(o2058sub), i1415) → 3247_0_getR_FieldAccess(EOS(STATIC_3247), java.lang.Object(o2058sub), i1415, java.lang.Object(o2058sub))
3247_0_getR_FieldAccess(EOS(STATIC_3247), java.lang.Object(o2058sub), i1415, java.lang.Object(o2058sub)) → 3262_0_getR_FieldAccess(EOS(STATIC_3262), java.lang.Object(o2058sub), i1415, java.lang.Object(o2058sub))
3247_0_getR_FieldAccess(EOS(STATIC_3247), java.lang.Object(o2058sub), i1415, java.lang.Object(o2058sub)) → 3263_0_getR_FieldAccess(EOS(STATIC_3263), java.lang.Object(o2058sub), i1415, java.lang.Object(o2058sub))
3262_0_getR_FieldAccess(EOS(STATIC_3262), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096))) → 3277_0_getR_FieldAccess(EOS(STATIC_3277), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)))
3277_0_getR_FieldAccess(EOS(STATIC_3277), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096))) → 3291_0_getR_NONNULL(EOS(STATIC_3291), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2096)), i1415, o2096)
3291_0_getR_NONNULL(EOS(STATIC_3291), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1415, java.lang.Object(o2132sub)) → 3311_0_getR_NONNULL(EOS(STATIC_3311), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1415, java.lang.Object(o2132sub))
3311_0_getR_NONNULL(EOS(STATIC_3311), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1415, java.lang.Object(o2132sub)) → 3326_0_getR_Load(EOS(STATIC_3326), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1415)
3326_0_getR_Load(EOS(STATIC_3326), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))), i1415) → 3342_0_getR_FieldAccess(EOS(STATIC_3342), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub))))
3342_0_getR_FieldAccess(EOS(STATIC_3342), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2132sub)))) → 3361_0_getR_Load(EOS(STATIC_3361), i1415, java.lang.Object(o2132sub))
3361_0_getR_Load(EOS(STATIC_3361), i1415, java.lang.Object(o2132sub)) → 3379_0_getR_ConstantStackPush(EOS(STATIC_3379), java.lang.Object(o2132sub), i1415)
3379_0_getR_ConstantStackPush(EOS(STATIC_3379), java.lang.Object(o2132sub), i1415) → 3391_0_getR_IntArithmetic(EOS(STATIC_3391), java.lang.Object(o2132sub), i1415, 1)
3391_0_getR_IntArithmetic(EOS(STATIC_3391), java.lang.Object(o2132sub), i1415, matching1) → 3417_0_getR_InvokeMethod(EOS(STATIC_3417), java.lang.Object(o2132sub), -(i1415, 1)) | &&(>(i1415, 0), =(matching1, 1))
3417_0_getR_InvokeMethod(EOS(STATIC_3417), java.lang.Object(o2132sub), i1491) → 3459_1_getR_InvokeMethod(3459_0_getR_Load(EOS(STATIC_3459), java.lang.Object(o2132sub), i1491), java.lang.Object(o2132sub), i1491)
3459_0_getR_Load(EOS(STATIC_3459), java.lang.Object(o2132sub), i1491) → 3477_0_getR_Load(EOS(STATIC_3477), java.lang.Object(o2132sub), i1491)
3477_0_getR_Load(EOS(STATIC_3477), java.lang.Object(o2132sub), i1491) → 3497_0_getR_Load(EOS(STATIC_3497), java.lang.Object(o2132sub), i1491)
3497_0_getR_Load(EOS(STATIC_3497), java.lang.Object(o2281sub), i1491) → 3525_0_getR_Load(EOS(STATIC_3525), java.lang.Object(o2281sub), i1491)
3525_0_getR_Load(EOS(STATIC_3525), java.lang.Object(o2281sub), i1491) → 3213_0_getR_Load(EOS(STATIC_3213), java.lang.Object(o2281sub), i1491)
3213_0_getR_Load(EOS(STATIC_3213), java.lang.Object(o2058sub), i1409) → 3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(o2058sub), i1409, i1409)
3263_0_getR_FieldAccess(EOS(STATIC_3263), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099))) → 3278_0_getR_FieldAccess(EOS(STATIC_3278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)))
3278_0_getR_FieldAccess(EOS(STATIC_3278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099))) → 3297_0_getR_NONNULL(EOS(STATIC_3297), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2099)), i1415, o2099)
3297_0_getR_NONNULL(EOS(STATIC_3297), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1415, java.lang.Object(o2133sub)) → 3313_0_getR_NONNULL(EOS(STATIC_3313), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1415, java.lang.Object(o2133sub))
3313_0_getR_NONNULL(EOS(STATIC_3313), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1415, java.lang.Object(o2133sub)) → 3329_0_getR_Load(EOS(STATIC_3329), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1415)
3329_0_getR_Load(EOS(STATIC_3329), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))), i1415) → 3345_0_getR_FieldAccess(EOS(STATIC_3345), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub))))
3345_0_getR_FieldAccess(EOS(STATIC_3345), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2133sub)))) → 3364_0_getR_Load(EOS(STATIC_3364), i1415, java.lang.Object(o2133sub))
3364_0_getR_Load(EOS(STATIC_3364), i1415, java.lang.Object(o2133sub)) → 3380_0_getR_ConstantStackPush(EOS(STATIC_3380), java.lang.Object(o2133sub), i1415)
3380_0_getR_ConstantStackPush(EOS(STATIC_3380), java.lang.Object(o2133sub), i1415) → 3392_0_getR_IntArithmetic(EOS(STATIC_3392), java.lang.Object(o2133sub), i1415, 1)
3392_0_getR_IntArithmetic(EOS(STATIC_3392), java.lang.Object(o2133sub), i1415, matching1) → 3419_0_getR_InvokeMethod(EOS(STATIC_3419), java.lang.Object(o2133sub), -(i1415, 1)) | &&(>(i1415, 0), =(matching1, 1))
3419_0_getR_InvokeMethod(EOS(STATIC_3419), java.lang.Object(o2133sub), i1492) → 3460_1_getR_InvokeMethod(3460_0_getR_Load(EOS(STATIC_3460), java.lang.Object(o2133sub), i1492), java.lang.Object(o2133sub), i1492)
3460_0_getR_Load(EOS(STATIC_3460), java.lang.Object(o2133sub), i1492) → 3479_0_getR_Load(EOS(STATIC_3479), java.lang.Object(o2133sub), i1492)
3479_0_getR_Load(EOS(STATIC_3479), java.lang.Object(o2133sub), i1492) → 3528_0_getR_Load(EOS(STATIC_3528), java.lang.Object(o2133sub), i1492)
3528_0_getR_Load(EOS(STATIC_3528), java.lang.Object(o2133sub), i1492) → 3213_0_getR_Load(EOS(STATIC_3213), java.lang.Object(o2133sub), i1492)
R rules:
3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(o2058sub), matching1, matching2) → 3231_0_getR_EQ(EOS(STATIC_3231), java.lang.Object(o2058sub), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
3231_0_getR_EQ(EOS(STATIC_3231), java.lang.Object(o2058sub), matching1, matching2) → 3238_0_getR_Load(EOS(STATIC_3238), java.lang.Object(o2058sub), 0) | &&(=(matching1, 0), =(matching2, 0))
3238_0_getR_Load(EOS(STATIC_3238), java.lang.Object(o2058sub), matching1) → 3249_0_getR_Return(EOS(STATIC_3249), java.lang.Object(o2058sub), 0, java.lang.Object(o2058sub)) | =(matching1, 0)
3291_0_getR_NONNULL(EOS(STATIC_3291), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, NULL) → 3312_0_getR_NONNULL(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, NULL)
3297_0_getR_NONNULL(EOS(STATIC_3297), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, NULL) → 3314_0_getR_NONNULL(EOS(STATIC_3314), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, NULL)
3312_0_getR_NONNULL(EOS(STATIC_3312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, NULL) → 3327_0_getR_Load(EOS(STATIC_3327), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415)
3314_0_getR_NONNULL(EOS(STATIC_3314), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, NULL) → 3331_0_getR_Load(EOS(STATIC_3331), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415)
3327_0_getR_Load(EOS(STATIC_3327), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415) → 3343_0_getR_Return(EOS(STATIC_3343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3331_0_getR_Load(EOS(STATIC_3331), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415) → 3347_0_getR_Return(EOS(STATIC_3347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1415, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(EOS(STATIC_3249), java.lang.Object(o2389sub), matching1, java.lang.Object(o2389sub)), java.lang.Object(o2389sub), matching2) → 3633_0_getR_Return(EOS(STATIC_3633), java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub)) | &&(=(matching1, 0), =(matching2, 0))
3459_1_getR_InvokeMethod(3343_0_getR_Return(EOS(STATIC_3343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585) → 3642_0_getR_Return(EOS(STATIC_3642), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3459_1_getR_InvokeMethod(3347_0_getR_Return(EOS(STATIC_3347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592) → 3659_0_getR_Return(EOS(STATIC_3659), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3459_1_getR_InvokeMethod(3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(o2874sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2874sub))), i1825) → 3938_0_getR_Return(EOS(STATIC_3938), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2874sub))), i1825)
3459_1_getR_InvokeMethod(3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(o2883sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2883sub))), i1835) → 3954_0_getR_Return(EOS(STATIC_3954), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2883sub))), i1835)
3459_1_getR_InvokeMethod(4219_0_getR_Return(EOS(STATIC_4219)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3442sub))))), i2113) → 4278_0_getR_Return(EOS(STATIC_4278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3442sub))))), i2113)
3459_1_getR_InvokeMethod(4223_0_getR_Return(EOS(STATIC_4223)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3459sub))))), i2127) → 4294_0_getR_Return(EOS(STATIC_4294), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3459sub))))), i2127)
3460_1_getR_InvokeMethod(3249_0_getR_Return(EOS(STATIC_3249), java.lang.Object(o2413sub), matching1, java.lang.Object(o2413sub)), java.lang.Object(o2413sub), matching2) → 3662_0_getR_Return(EOS(STATIC_3662), java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub)) | &&(=(matching1, 0), =(matching2, 0))
3460_1_getR_InvokeMethod(3343_0_getR_Return(EOS(STATIC_3343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606) → 3673_0_getR_Return(EOS(STATIC_3673), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3460_1_getR_InvokeMethod(3347_0_getR_Return(EOS(STATIC_3347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614) → 3680_0_getR_Return(EOS(STATIC_3680), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3460_1_getR_InvokeMethod(3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(o2879sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2879sub))), i1830) → 3939_0_getR_Return(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2879sub))), i1830)
3460_1_getR_InvokeMethod(3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(o2888sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2888sub))), i1841) → 3964_0_getR_Return(EOS(STATIC_3964), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2888sub))), i1841)
3460_1_getR_InvokeMethod(4219_0_getR_Return(EOS(STATIC_4219)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3449sub))))), i2119) → 4285_0_getR_Return(EOS(STATIC_4285), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3449sub))))), i2119)
3460_1_getR_InvokeMethod(4223_0_getR_Return(EOS(STATIC_4223)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3466sub))))), i2134) → 4301_0_getR_Return(EOS(STATIC_4301), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3466sub))))), i2134)
3633_0_getR_Return(EOS(STATIC_3633), java.lang.Object(o2389sub), matching1, java.lang.Object(o2389sub), matching2, java.lang.Object(o2389sub)) → 3643_0_getR_Return(EOS(STATIC_3643), java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub), 0, java.lang.Object(o2389sub)) | &&(=(matching1, 0), =(matching2, 0))
3642_0_getR_Return(EOS(STATIC_3642), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3643_0_getR_Return(EOS(STATIC_3643), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1585, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3643_0_getR_Return(EOS(STATIC_3643), java.lang.Object(o2525sub), i1651, java.lang.Object(o2525sub), i1651, java.lang.Object(o2525sub)) → 3660_0_getR_Return(EOS(STATIC_3660), java.lang.Object(o2525sub), i1651, java.lang.Object(o2525sub), i1651, java.lang.Object(o2525sub))
3659_0_getR_Return(EOS(STATIC_3659), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3660_0_getR_Return(EOS(STATIC_3660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1592, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3660_0_getR_Return(EOS(STATIC_3660), java.lang.Object(o2539sub), i1656, java.lang.Object(o2539sub), i1656, java.lang.Object(o2539sub)) → 3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(o2539sub))
3662_0_getR_Return(EOS(STATIC_3662), java.lang.Object(o2413sub), matching1, java.lang.Object(o2413sub), matching2, java.lang.Object(o2413sub)) → 3674_0_getR_Return(EOS(STATIC_3674), java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub), 0, java.lang.Object(o2413sub)) | &&(=(matching1, 0), =(matching2, 0))
3673_0_getR_Return(EOS(STATIC_3673), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3674_0_getR_Return(EOS(STATIC_3674), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1606, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3674_0_getR_Return(EOS(STATIC_3674), java.lang.Object(o2558sub), i1665, java.lang.Object(o2558sub), i1665, java.lang.Object(o2558sub)) → 3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(o2558sub))
3680_0_getR_Return(EOS(STATIC_3680), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3674_0_getR_Return(EOS(STATIC_3674), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), i1614, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3938_0_getR_Return(EOS(STATIC_3938), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2874sub))), i1825) → 3955_0_getR_Return(EOS(STATIC_3955), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2874sub))), i1825)
3939_0_getR_Return(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2879sub))), i1830) → 4189_0_getR_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2879sub))), i1830)
3954_0_getR_Return(EOS(STATIC_3954), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2883sub))), i1835) → 3955_0_getR_Return(EOS(STATIC_3955), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2883sub))), i1835)
3955_0_getR_Return(EOS(STATIC_3955), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3000sub))), i1879) → 4173_0_getR_Return(EOS(STATIC_4173), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3000sub))), i1879)
3964_0_getR_Return(EOS(STATIC_3964), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2888sub))), i1841) → 3939_0_getR_Return(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2888sub))), i1841)
4173_0_getR_Return(EOS(STATIC_4173), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3276sub))), i2043) → 4219_0_getR_Return(EOS(STATIC_4219))
4189_0_getR_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3324sub))), i2068) → 4223_0_getR_Return(EOS(STATIC_4223))
4278_0_getR_Return(EOS(STATIC_4278), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3442sub))))), i2113) → 4173_0_getR_Return(EOS(STATIC_4173), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3442sub))))), i2113)
4285_0_getR_Return(EOS(STATIC_4285), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3449sub))))), i2119) → 4189_0_getR_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3449sub))))), i2119)
4294_0_getR_Return(EOS(STATIC_4294), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3459sub))))), i2127) → 4173_0_getR_Return(EOS(STATIC_4173), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3459sub))))), i2127)
4301_0_getR_Return(EOS(STATIC_4301), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3466sub))))), i2134) → 4189_0_getR_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3466sub))))), i2134)

Combined rules. Obtained 2 conditional rules for P and 15 conditional rules for R.

P rules:
3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1, x1) → 3459_1_getR_InvokeMethod(3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(x0), -(x1, 1), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1, x1) → 3460_1_getR_InvokeMethod(3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(x0), -(x1, 1), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
R rules:
3223_0_getR_EQ(EOS(STATIC_3223), java.lang.Object(x0), 0, 0) → 3249_0_getR_Return(EOS(STATIC_3249), java.lang.Object(x0), 0, java.lang.Object(x0))
3459_1_getR_InvokeMethod(3347_0_getR_Return(EOS(STATIC_3347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(EOS(STATIC_3249), java.lang.Object(x0), 0, java.lang.Object(x0)), java.lang.Object(x0), 0) → 3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(x0))
3459_1_getR_InvokeMethod(3343_0_getR_Return(EOS(STATIC_3343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3460_1_getR_InvokeMethod(3249_0_getR_Return(EOS(STATIC_3249), java.lang.Object(x0), 0, java.lang.Object(x0)), java.lang.Object(x0), 0) → 3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(x0))
3460_1_getR_InvokeMethod(3343_0_getR_Return(EOS(STATIC_3343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3460_1_getR_InvokeMethod(3347_0_getR_Return(EOS(STATIC_3347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), x0) → 3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3460_1_getR_InvokeMethod(3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4223_0_getR_Return(EOS(STATIC_4223))
3460_1_getR_InvokeMethod(3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4223_0_getR_Return(EOS(STATIC_4223))
3460_1_getR_InvokeMethod(4219_0_getR_Return(EOS(STATIC_4219)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4223_0_getR_Return(EOS(STATIC_4223))
3460_1_getR_InvokeMethod(4223_0_getR_Return(EOS(STATIC_4223)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4223_0_getR_Return(EOS(STATIC_4223))
3459_1_getR_InvokeMethod(4219_0_getR_Return(EOS(STATIC_4219)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4219_0_getR_Return(EOS(STATIC_4219))
3459_1_getR_InvokeMethod(4223_0_getR_Return(EOS(STATIC_4223)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))))), x1) → 4219_0_getR_Return(EOS(STATIC_4219))
3459_1_getR_InvokeMethod(3701_0_getR_Return(EOS(STATIC_3701), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4219_0_getR_Return(EOS(STATIC_4219))
3459_1_getR_InvokeMethod(3704_0_getR_Return(EOS(STATIC_3704), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), x1) → 4219_0_getR_Return(EOS(STATIC_4219))

Filtered ground terms:

3223_0_getR_EQ(x1, x2, x3, x4) → 3223_0_getR_EQ(x2, x3, x4)
Cond_3223_0_getR_EQ1(x1, x2, x3, x4, x5) → Cond_3223_0_getR_EQ1(x1, x3, x4, x5)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
Cond_3223_0_getR_EQ(x1, x2, x3, x4, x5) → Cond_3223_0_getR_EQ(x1, x3, x4, x5)
4219_0_getR_Return(x1) → 4219_0_getR_Return
3704_0_getR_Return(x1, x2) → 3704_0_getR_Return(x2)
3701_0_getR_Return(x1, x2) → 3701_0_getR_Return(x2)
4223_0_getR_Return(x1) → 4223_0_getR_Return
3347_0_getR_Return(x1, x2, x3, x4) → 3347_0_getR_Return(x3)
3343_0_getR_Return(x1, x2, x3, x4) → 3343_0_getR_Return(x3)
3249_0_getR_Return(x1, x2, x3, x4) → 3249_0_getR_Return(x2, x4)

Filtered duplicate args:

3223_0_getR_EQ(x1, x2, x3) → 3223_0_getR_EQ(x1, x3)
Cond_3223_0_getR_EQ(x1, x2, x3, x4) → Cond_3223_0_getR_EQ(x1, x2, x4)
Cond_3223_0_getR_EQ1(x1, x2, x3, x4) → Cond_3223_0_getR_EQ1(x1, x2, x4)
3249_0_getR_Return(x1, x2) → 3249_0_getR_Return(x2)

Combined rules. Obtained 2 conditional rules for P and 15 conditional rules for R.

P rules:
3223_0_getR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3459_1_getR_InvokeMethod(3223_0_getR_EQ(java.lang.Object(x0), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
3223_0_getR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3460_1_getR_InvokeMethod(3223_0_getR_EQ(java.lang.Object(x0), -(x1, 1)), java.lang.Object(x0), -(x1, 1)) | >(x1, 0)
R rules:
3223_0_getR_EQ(java.lang.Object(x0), 0) → 3249_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3701_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3701_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3343_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3701_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3460_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3704_0_getR_Return(java.lang.Object(x0))
3460_1_getR_InvokeMethod(3343_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3704_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3460_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3704_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3460_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4223_0_getR_Return
3460_1_getR_InvokeMethod(3704_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4223_0_getR_Return
3460_1_getR_InvokeMethod(4219_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4223_0_getR_Return
3460_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4223_0_getR_Return
3459_1_getR_InvokeMethod(4219_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4219_0_getR_Return
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4219_0_getR_Return
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4219_0_getR_Return
3459_1_getR_InvokeMethod(3704_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4219_0_getR_Return

Performed bisimulation on rules. Used the following equivalence classes: {[3701_0_getR_Return_1, 3704_0_getR_Return_1]=3701_0_getR_Return_1, [3347_0_getR_Return_1, 3343_0_getR_Return_1]=3347_0_getR_Return_1, [3459_1_getR_InvokeMethod_3, 3460_1_getR_InvokeMethod_3]=3459_1_getR_InvokeMethod_3, [Cond_3223_0_getR_EQ_3, Cond_3223_0_getR_EQ1_3]=Cond_3223_0_getR_EQ_3, [4223_0_getR_Return, 4219_0_getR_Return]=4223_0_getR_Return}

Finished conversion. Obtained 2 rules for P and 5 rules for R. System has predefined symbols.

P rules:
3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → COND_3223_0_GETR_EQ(>(x1, 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3223_0_GETR_EQ(java.lang.Object(x0), -(x1, 1))
R rules:
3223_0_getR_EQ(java.lang.Object(x0), 0) → 3249_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3701_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3701_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4223_0_getR_Return
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4223_0_getR_Return

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3223_0_getR_EQ(java.lang.Object(x0), 0) → 3249_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3701_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3701_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4223_0_getR_Return
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4223_0_getR_Return

The integer pair graph contains the following rules and edges:
(0): 3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3223_0_GETR_EQ(x1[0] > 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])
(1): COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3223_0_GETR_EQ(java.lang.Object(x0[1]), x1[1] - 1)

(0) -> (1), if (x1[0] > 0 ∧java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))) →^* java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1])))∧x1[0] →^* x1[1])

(1) -> (0), if (java.lang.Object(x0[1]) →^* java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))∧x1[1] - 1 →^* x1[0])

The set Q consists of the following terms:
3223_0_getR_EQ(java.lang.Object(x0), 0)
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0)
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0)
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1)

(8) IDPNonInfProof (SOUND transformation)

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

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

For Pair 3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → COND_3223_0_GETR_EQ(>(x1, 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) the following chains were created:

We consider the chain 3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]), COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1)) which results in the following constraint:
(1)    (>(x1[0], 0)=TRUE∧java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))=java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1])))∧x1[0]=x1[1] ⇒ 3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥NonInfC∧3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])∧(U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (>(x1[0], 0)=TRUE ⇒ 3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥NonInfC∧3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])≥COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])∧(U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17 + (2)bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

For Pair COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3223_0_GETR_EQ(java.lang.Object(x0), -(x1, 1)) the following chains were created:

We consider the chain COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1)) which results in the following constraint:
(7)    (COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1])≥NonInfC∧COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1])≥3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))∧(U^Increasing(3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧0 = 0∧[2 + (-1)bso_20] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → COND_3223_0_GETR_EQ(>(x1, 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
- (x1[0] ≥ 0 ⇒ (U^Increasing(COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])), ≥)∧[(-1)Bound*bni_17 + (2)bni_17] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)
COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 3223_0_GETR_EQ(java.lang.Object(x0), -(x1, 1))
- ((U^Increasing(3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))), ≥)∧[bni_19] = 0∧0 = 0∧[2 + (-1)bso_20] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(3223_0_getR_EQ(x₁, x₂)) = [-1]
POL(java.lang.Object(x₁)) = [-1]
POL(0) = 0
POL(3249_0_getR_Return(x₁)) = [-1]
POL(3459_1_getR_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(3347_0_getR_Return(x₁)) = [-1]
POL(DoublyLinkedList.DoublyLinkedList(x₁)) = [-1]
POL(NULL) = [-1]
POL(3701_0_getR_Return(x₁)) = [-1]
POL(4223_0_getR_Return) = [-1]
POL(3223_0_GETR_EQ(x₁, x₂)) = [2]x₂
POL(COND_3223_0_GETR_EQ(x₁, x₂, x₃)) = [2]x₃
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(1) = [1]

The following pairs are in P_>:

COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3223_0_GETR_EQ(java.lang.Object(x0[1]), -(x1[1], 1))

The following pairs are in P_bound:

3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])

The following pairs are in P_≥:

3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3223_0_GETR_EQ(>(x1[0], 0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])

There are no usable rules.

(9) Complex Obligation (AND)

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3223_0_getR_EQ(java.lang.Object(x0), 0) → 3249_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3701_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3701_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4223_0_getR_Return
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4223_0_getR_Return

The integer pair graph contains the following rules and edges:
(0): 3223_0_GETR_EQ(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0]) → COND_3223_0_GETR_EQ(x1[0] > 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]))), x1[0])

The set Q consists of the following terms:
3223_0_getR_EQ(java.lang.Object(x0), 0)
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0)
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0)
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1)

(11) IDependencyGraphProof (EQUIVALENT transformation)

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

(12) TRUE

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3223_0_getR_EQ(java.lang.Object(x0), 0) → 3249_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0) → 3701_0_getR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0) → 3701_0_getR_Return(java.lang.Object(x0))
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1) → 4223_0_getR_Return
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1) → 4223_0_getR_Return

The integer pair graph contains the following rules and edges:
(1): COND_3223_0_GETR_EQ(TRUE, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[1]))), x1[1]) → 3223_0_GETR_EQ(java.lang.Object(x0[1]), x1[1] - 1)

The set Q consists of the following terms:
3223_0_getR_EQ(java.lang.Object(x0), 0)
3459_1_getR_InvokeMethod(3347_0_getR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)), x0)
3459_1_getR_InvokeMethod(3249_0_getR_Return(java.lang.Object(x0)), java.lang.Object(x0), 0)
3459_1_getR_InvokeMethod(3701_0_getR_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))), x1)
3459_1_getR_InvokeMethod(4223_0_getR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0))))), x1)

(14) IDependencyGraphProof (EQUIVALENT transformation)

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

(15) TRUE

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DoublyLinkedList.DoublyLinkedList.getFirst()LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods: DoublyLinkedList.DoublyLinkedList.getFirst()LDoublyLinkedList/DoublyLinkedList;
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 24 rules for P and 35 rules for R.

P rules:
3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(o2064sub), java.lang.Object(o2064sub)) → 3235_0_getFirst_FieldAccess(EOS(STATIC_3235), java.lang.Object(o2064sub), java.lang.Object(o2064sub))
3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(o2064sub), java.lang.Object(o2064sub)) → 3236_0_getFirst_FieldAccess(EOS(STATIC_3236), java.lang.Object(o2064sub), java.lang.Object(o2064sub))
3235_0_getFirst_FieldAccess(EOS(STATIC_3235), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071))) → 3244_0_getFirst_FieldAccess(EOS(STATIC_3244), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)))
3244_0_getFirst_FieldAccess(EOS(STATIC_3244), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071))) → 3255_0_getFirst_NONNULL(EOS(STATIC_3255), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2071)), o2071)
3255_0_getFirst_NONNULL(EOS(STATIC_3255), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))), java.lang.Object(o2092sub)) → 3271_0_getFirst_NONNULL(EOS(STATIC_3271), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))), java.lang.Object(o2092sub))
3271_0_getFirst_NONNULL(EOS(STATIC_3271), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))), java.lang.Object(o2092sub)) → 3285_0_getFirst_Load(EOS(STATIC_3285), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))))
3285_0_getFirst_Load(EOS(STATIC_3285), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub)))) → 3305_0_getFirst_FieldAccess(EOS(STATIC_3305), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub))))
3305_0_getFirst_FieldAccess(EOS(STATIC_3305), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2092sub)))) → 3322_0_getFirst_InvokeMethod(EOS(STATIC_3322), java.lang.Object(o2092sub))
3322_0_getFirst_InvokeMethod(EOS(STATIC_3322), java.lang.Object(o2092sub)) → 3339_1_getFirst_InvokeMethod(3339_0_getFirst_Load(EOS(STATIC_3339), java.lang.Object(o2092sub)), java.lang.Object(o2092sub))
3339_0_getFirst_Load(EOS(STATIC_3339), java.lang.Object(o2092sub)) → 3358_0_getFirst_Load(EOS(STATIC_3358), java.lang.Object(o2092sub))
3358_0_getFirst_Load(EOS(STATIC_3358), java.lang.Object(o2092sub)) → 3378_0_getFirst_Load(EOS(STATIC_3378), java.lang.Object(o2092sub))
3378_0_getFirst_Load(EOS(STATIC_3378), java.lang.Object(o2175sub)) → 3388_0_getFirst_Load(EOS(STATIC_3388), java.lang.Object(o2175sub))
3388_0_getFirst_Load(EOS(STATIC_3388), java.lang.Object(o2175sub)) → 3221_0_getFirst_Load(EOS(STATIC_3221), java.lang.Object(o2175sub))
3221_0_getFirst_Load(EOS(STATIC_3221), java.lang.Object(o2064sub)) → 3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(o2064sub), java.lang.Object(o2064sub))
3236_0_getFirst_FieldAccess(EOS(STATIC_3236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074))) → 3245_0_getFirst_FieldAccess(EOS(STATIC_3245), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)))
3245_0_getFirst_FieldAccess(EOS(STATIC_3245), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074))) → 3260_0_getFirst_NONNULL(EOS(STATIC_3260), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2074)), o2074)
3260_0_getFirst_NONNULL(EOS(STATIC_3260), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))), java.lang.Object(o2093sub)) → 3274_0_getFirst_NONNULL(EOS(STATIC_3274), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))), java.lang.Object(o2093sub))
3274_0_getFirst_NONNULL(EOS(STATIC_3274), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))), java.lang.Object(o2093sub)) → 3287_0_getFirst_Load(EOS(STATIC_3287), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))))
3287_0_getFirst_Load(EOS(STATIC_3287), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub)))) → 3307_0_getFirst_FieldAccess(EOS(STATIC_3307), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub))))
3307_0_getFirst_FieldAccess(EOS(STATIC_3307), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o2093sub)))) → 3324_0_getFirst_InvokeMethod(EOS(STATIC_3324), java.lang.Object(o2093sub))
3324_0_getFirst_InvokeMethod(EOS(STATIC_3324), java.lang.Object(o2093sub)) → 3340_1_getFirst_InvokeMethod(3340_0_getFirst_Load(EOS(STATIC_3340), java.lang.Object(o2093sub)), java.lang.Object(o2093sub))
3340_0_getFirst_Load(EOS(STATIC_3340), java.lang.Object(o2093sub)) → 3359_0_getFirst_Load(EOS(STATIC_3359), java.lang.Object(o2093sub))
3359_0_getFirst_Load(EOS(STATIC_3359), java.lang.Object(o2093sub)) → 3389_0_getFirst_Load(EOS(STATIC_3389), java.lang.Object(o2093sub))
3389_0_getFirst_Load(EOS(STATIC_3389), java.lang.Object(o2093sub)) → 3221_0_getFirst_Load(EOS(STATIC_3221), java.lang.Object(o2093sub))
R rules:
3255_0_getFirst_NONNULL(EOS(STATIC_3255), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3272_0_getFirst_NONNULL(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3260_0_getFirst_NONNULL(EOS(STATIC_3260), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3275_0_getFirst_NONNULL(EOS(STATIC_3275), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3272_0_getFirst_NONNULL(EOS(STATIC_3272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3286_0_getFirst_Load(EOS(STATIC_3286), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3275_0_getFirst_NONNULL(EOS(STATIC_3275), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3289_0_getFirst_Load(EOS(STATIC_3289), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3286_0_getFirst_Load(EOS(STATIC_3286), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3306_0_getFirst_Return(EOS(STATIC_3306), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3289_0_getFirst_Load(EOS(STATIC_3289), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3309_0_getFirst_Return(EOS(STATIC_3309), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3306_0_getFirst_Return(EOS(STATIC_3306), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3432_0_getFirst_Return(EOS(STATIC_3432), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3309_0_getFirst_Return(EOS(STATIC_3309), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3447_0_getFirst_Return(EOS(STATIC_3447), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3550_0_getFirst_Return(EOS(STATIC_3550), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3569_0_getFirst_Return(EOS(STATIC_3569), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(o2742sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103))))))) → 4061_0_getFirst_Return(EOS(STATIC_4061), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103)))))), java.lang.Object(o2742sub))
3339_1_getFirst_InvokeMethod(3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(o2816sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3129))))))) → 4104_0_getFirst_Return(EOS(STATIC_4104), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3129)))))), java.lang.Object(o2816sub))
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return(EOS(STATIC_3306), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3309_0_getFirst_Return(EOS(STATIC_3309), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3457_0_getFirst_Return(EOS(STATIC_3457), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3552_0_getFirst_Return(EOS(STATIC_3552), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3579_0_getFirst_Return(EOS(STATIC_3579), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(o2742sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112))))))) → 4073_0_getFirst_Return(EOS(STATIC_4073), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112)))))), java.lang.Object(o2742sub))
3340_1_getFirst_InvokeMethod(3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(o2816sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3138))))))) → 4116_0_getFirst_Return(EOS(STATIC_4116), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3138)))))), java.lang.Object(o2816sub))
3432_0_getFirst_Return(EOS(STATIC_3432), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3448_0_getFirst_Return(EOS(STATIC_3448), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3447_0_getFirst_Return(EOS(STATIC_3447), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3448_0_getFirst_Return(EOS(STATIC_3448), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3448_0_getFirst_Return(EOS(STATIC_3448), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3457_0_getFirst_Return(EOS(STATIC_3457), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3449_0_getFirst_Return(EOS(STATIC_3449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3550_0_getFirst_Return(EOS(STATIC_3550), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3570_0_getFirst_Return(EOS(STATIC_3570), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3552_0_getFirst_Return(EOS(STATIC_3552), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3818_0_getFirst_Return(EOS(STATIC_3818), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3569_0_getFirst_Return(EOS(STATIC_3569), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3570_0_getFirst_Return(EOS(STATIC_3570), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3570_0_getFirst_Return(EOS(STATIC_3570), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3786_0_getFirst_Return(EOS(STATIC_3786), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3579_0_getFirst_Return(EOS(STATIC_3579), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3552_0_getFirst_Return(EOS(STATIC_3552), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3786_0_getFirst_Return(EOS(STATIC_3786), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2671)))), java.lang.Object(o2674sub)) → 3877_0_getFirst_Return(EOS(STATIC_3877), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2671)))), java.lang.Object(o2674sub))
3818_0_getFirst_Return(EOS(STATIC_3818), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2739)))), java.lang.Object(o2742sub)) → 3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(o2742sub))
3877_0_getFirst_Return(EOS(STATIC_3877), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o2813)))), java.lang.Object(o2816sub)) → 3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(o2816sub))
4061_0_getFirst_Return(EOS(STATIC_4061), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103)))))), java.lang.Object(o2742sub)) → 3877_0_getFirst_Return(EOS(STATIC_3877), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3103)))))), java.lang.Object(o2742sub))
4073_0_getFirst_Return(EOS(STATIC_4073), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112)))))), java.lang.Object(o2742sub)) → 3818_0_getFirst_Return(EOS(STATIC_3818), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3112)))))), java.lang.Object(o2742sub))
4104_0_getFirst_Return(EOS(STATIC_4104), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3129)))))), java.lang.Object(o2816sub)) → 3877_0_getFirst_Return(EOS(STATIC_3877), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3129)))))), java.lang.Object(o2816sub))
4116_0_getFirst_Return(EOS(STATIC_4116), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3138)))))), java.lang.Object(o2816sub)) → 3818_0_getFirst_Return(EOS(STATIC_3818), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3138)))))), java.lang.Object(o2816sub))

Combined rules. Obtained 2 conditional rules for P and 12 conditional rules for R.

P rules:
3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3339_1_getFirst_InvokeMethod(3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3340_1_getFirst_InvokeMethod(3228_0_getFirst_FieldAccess(EOS(STATIC_3228), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return(EOS(STATIC_3306), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3309_0_getFirst_Return(EOS(STATIC_3309), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3306_0_getFirst_Return(EOS(STATIC_3306), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3309_0_getFirst_Return(EOS(STATIC_3309), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(x0))
3340_1_getFirst_InvokeMethod(3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(x0))
3339_1_getFirst_InvokeMethod(3927_0_getFirst_Return(EOS(STATIC_3927), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(x0))
3339_1_getFirst_InvokeMethod(3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(x0))
3339_1_getFirst_InvokeMethod(3471_0_getFirst_Return(EOS(STATIC_3471), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3339_1_getFirst_InvokeMethod(3475_0_getFirst_Return(EOS(STATIC_3475), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3937_0_getFirst_Return(EOS(STATIC_3937), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))

Filtered ground terms:

3228_0_getFirst_FieldAccess(x1, x2, x3) → 3228_0_getFirst_FieldAccess(x2, x3)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
3937_0_getFirst_Return(x1, x2) → 3937_0_getFirst_Return(x2)
3475_0_getFirst_Return(x1, x2) → 3475_0_getFirst_Return
3471_0_getFirst_Return(x1, x2) → 3471_0_getFirst_Return
3927_0_getFirst_Return(x1, x2) → 3927_0_getFirst_Return(x2)
3309_0_getFirst_Return(x1, x2, x3) → 3309_0_getFirst_Return
3306_0_getFirst_Return(x1, x2, x3) → 3306_0_getFirst_Return

Filtered duplicate args:

3228_0_getFirst_FieldAccess(x1, x2) → 3228_0_getFirst_FieldAccess(x2)

Combined rules. Obtained 2 conditional rules for P and 12 conditional rules for R.

P rules:
3228_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3339_1_getFirst_InvokeMethod(3228_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
3228_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3340_1_getFirst_InvokeMethod(3228_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3475_0_getFirst_Return
3340_1_getFirst_InvokeMethod(3309_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3475_0_getFirst_Return
3339_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3471_0_getFirst_Return
3339_1_getFirst_InvokeMethod(3309_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3471_0_getFirst_Return
3340_1_getFirst_InvokeMethod(3471_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3927_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3475_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3927_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3927_0_getFirst_Return(java.lang.Object(x0))
3340_1_getFirst_InvokeMethod(3937_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3927_0_getFirst_Return(java.lang.Object(x0))
3339_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3937_0_getFirst_Return(java.lang.Object(x0))
3339_1_getFirst_InvokeMethod(3937_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3937_0_getFirst_Return(java.lang.Object(x0))
3339_1_getFirst_InvokeMethod(3471_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3937_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3339_1_getFirst_InvokeMethod(3475_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3937_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))

Performed bisimulation on rules. Used the following equivalence classes: {[3340_1_getFirst_InvokeMethod_2, 3339_1_getFirst_InvokeMethod_2]=3340_1_getFirst_InvokeMethod_2, [3306_0_getFirst_Return, 3475_0_getFirst_Return, 3309_0_getFirst_Return, 3471_0_getFirst_Return]=3306_0_getFirst_Return, [3927_0_getFirst_Return_1, 3937_0_getFirst_Return_1]=3927_0_getFirst_Return_1}

Finished conversion. Obtained 1 rules for P and 3 rules for R. System has no predefined symbols.

P rules:
3228_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(x0))
R rules:
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3306_0_getFirst_Return
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3927_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3927_0_getFirst_Return(java.lang.Object(x0))

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3306_0_getFirst_Return
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3927_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3927_0_getFirst_Return(java.lang.Object(x0))

The integer pair graph contains the following rules and edges:
(0): 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

(0) -> (0), if (java.lang.Object(x0[0]) →^* java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0]'))))

The set Q consists of the following terms:
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

(19) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3228_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

The TRS R consists of the following rules:

3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3306_0_getFirst_Return
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 3927_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 3927_0_getFirst_Return(java.lang.Object(x0))

The set Q consists of the following terms:

3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

We have to consider all minimal (P,Q,R)-chains.

(21) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3228_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

R is empty.
The set Q consists of the following terms:

3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

We have to consider all minimal (P,Q,R)-chains.

(23) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3340_1_getFirst_InvokeMethod(3306_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3340_1_getFirst_InvokeMethod(3927_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3228_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

3228_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3228_0_GETFIRST_FIELDACCESS(java.lang.Object(x0[0]))
The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DoublyLinkedList.DoublyLinkedList.createList()LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(28) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 94 rules for P and 0 rules for R.

P rules:
3067_0_createList_Load(EOS(STATIC_3067(i1339)), i190, o1932, i1340, i1340) → 3082_0_createList_GE(EOS(STATIC_3082(i1339)), i190, o1932, i1340, i1340, i190)
3082_0_createList_GE(EOS(STATIC_3082(i1339)), i190, o1932, i1340, i1340, i190) → 3100_0_createList_GE(EOS(STATIC_3100(i1339)), i190, o1932, i1340, i1340, i190)
3100_0_createList_GE(EOS(STATIC_3100(i1339)), i190, o1932, i1340, i1340, i190) → 3118_0_createList_Load(EOS(STATIC_3118(i1339)), i190, o1932, i1340) | <(i1340, i190)
3118_0_createList_Load(EOS(STATIC_3118(i1339)), i190, o1932, i1340) → 3140_0_createList_Store(EOS(STATIC_3140(i1339)), i190, i1340, o1932)
3140_0_createList_Store(EOS(STATIC_3140(i1339)), i190, i1340, o1932) → 3153_0_createList_New(EOS(STATIC_3153(i1339)), i190, i1340, o1932)
3153_0_createList_New(EOS(STATIC_3153(i1339)), i190, i1340, o1932) → 3164_0_createList_Duplicate(EOS(STATIC_3164(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3164_0_createList_Duplicate(EOS(STATIC_3164(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3183_0_createList_InvokeMethod(EOS(STATIC_3183(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3183_0_createList_InvokeMethod(EOS(STATIC_3183(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3193_0_random_FieldAccess(EOS(STATIC_3193(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3193_0_random_FieldAccess(EOS(STATIC_3193(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3216_0_random_ArrayLength(EOS(STATIC_3216(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)))
3216_0_random_ArrayLength(EOS(STATIC_3216(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188))) → 3226_0_random_FieldAccess(EOS(STATIC_3226(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188) | >=(i188, 0)
3226_0_random_FieldAccess(EOS(STATIC_3226(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188) → 3233_0_random_GT(EOS(STATIC_3233(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339)
3233_0_random_GT(EOS(STATIC_3233(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3241_0_random_GT(EOS(STATIC_3241(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339)
3233_0_random_GT(EOS(STATIC_3233(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3242_0_random_GT(EOS(STATIC_3242(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339)
3241_0_random_GT(EOS(STATIC_3241(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3252_0_random_FieldAccess(EOS(STATIC_3252(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | >(i188, i1339)
3252_0_random_FieldAccess(EOS(STATIC_3252(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3268_0_random_FieldAccess(EOS(STATIC_3268(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)))
3268_0_random_FieldAccess(EOS(STATIC_3268(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188))) → 3283_0_random_ArrayAccess(EOS(STATIC_3283(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339)
3283_0_random_ArrayAccess(EOS(STATIC_3283(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339) → 3301_0_random_ArrayAccess(EOS(STATIC_3301(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339)
3301_0_random_ArrayAccess(EOS(STATIC_3301(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i188)), i1339) → 3319_0_random_Store(EOS(STATIC_3319(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) | <(i1339, i188)
3319_0_random_Store(EOS(STATIC_3319(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) → 3336_0_random_FieldAccess(EOS(STATIC_3336(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134)
3336_0_random_FieldAccess(EOS(STATIC_3336(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) → 3354_0_random_ConstantStackPush(EOS(STATIC_3354(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339)
3354_0_random_ConstantStackPush(EOS(STATIC_3354(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339) → 3371_0_random_IntArithmetic(EOS(STATIC_3371(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339, 1)
3371_0_random_IntArithmetic(EOS(STATIC_3371(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1339, matching1) → 3385_0_random_FieldAccess(EOS(STATIC_3385(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, +(i1339, 1)) | &&(>=(i1339, 0), =(matching1, 1))
3385_0_random_FieldAccess(EOS(STATIC_3385(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, i1462) → 3398_0_random_Load(EOS(STATIC_3398(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134)
3398_0_random_Load(EOS(STATIC_3398(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134) → 3428_0_random_NONNULL(EOS(STATIC_3428(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2134, o2134)
3428_0_random_NONNULL(EOS(STATIC_3428(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub), java.lang.Object(o2271sub)) → 3467_0_random_NONNULL(EOS(STATIC_3467(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub), java.lang.Object(o2271sub))
3428_0_random_NONNULL(EOS(STATIC_3428(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3468_0_random_NONNULL(EOS(STATIC_3468(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL)
3467_0_random_NONNULL(EOS(STATIC_3467(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub), java.lang.Object(o2271sub)) → 3484_0_random_Load(EOS(STATIC_3484(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub))
3484_0_random_Load(EOS(STATIC_3484(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub)) → 3508_0_random_InvokeMethod(EOS(STATIC_3508(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub))
3508_0_random_InvokeMethod(EOS(STATIC_3508(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub)) → 3546_0_length_Load(EOS(STATIC_3546(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub), java.lang.Object(o2271sub))
3546_0_length_Load(EOS(STATIC_3546(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub), java.lang.Object(o2271sub)) → 3693_0_length_FieldAccess(EOS(STATIC_3693(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o2271sub), java.lang.Object(o2271sub))
3693_0_length_FieldAccess(EOS(STATIC_3693(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), java.lang.Object(java.lang.String(o2607sub, i1698))) → 3714_0_length_FieldAccess(EOS(STATIC_3714(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), java.lang.Object(java.lang.String(o2607sub, i1698))) | &&(>=(i1698, 0), >=(i1699, 0))
3714_0_length_FieldAccess(EOS(STATIC_3714(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), java.lang.Object(java.lang.String(o2607sub, i1698))) → 3744_0_length_Return(EOS(STATIC_3744(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), i1698)
3744_0_length_Return(EOS(STATIC_3744(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o2607sub, i1698)), i1698) → 3913_0_random_Return(EOS(STATIC_3913(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
3913_0_random_Return(EOS(STATIC_3913(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 3972_0_createList_InvokeMethod(EOS(STATIC_3972(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
3972_0_createList_InvokeMethod(EOS(STATIC_3972(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4001_0_<init>_Load(EOS(STATIC_4001(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4001_0_<init>_Load(EOS(STATIC_4001(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4147_0_<init>_InvokeMethod(EOS(STATIC_4147(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4147_0_<init>_InvokeMethod(EOS(STATIC_4147(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4214_0_<init>_Load(EOS(STATIC_4214(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4214_0_<init>_Load(EOS(STATIC_4214(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4234_0_<init>_Load(EOS(STATIC_4234(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4234_0_<init>_Load(EOS(STATIC_4234(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4248_0_<init>_FieldAccess(EOS(STATIC_4248(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4248_0_<init>_FieldAccess(EOS(STATIC_4248(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4268_0_<init>_Return(EOS(STATIC_4268(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698)
4268_0_<init>_Return(EOS(STATIC_4268(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1698) → 4310_0_createList_Store(EOS(STATIC_4310(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4310_0_createList_Store(EOS(STATIC_4310(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4322_0_createList_Load(EOS(STATIC_4322(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
4322_0_createList_Load(EOS(STATIC_4322(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 4334_0_createList_Load(EOS(STATIC_4334(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4334_0_createList_Load(EOS(STATIC_4334(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4350_0_createList_FieldAccess(EOS(STATIC_4350(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932)
4350_0_createList_FieldAccess(EOS(STATIC_4350(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932) → 4368_0_createList_Load(EOS(STATIC_4368(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
4368_0_createList_Load(EOS(STATIC_4368(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 4387_0_createList_NULL(EOS(STATIC_4387(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, o1932)
4387_0_createList_NULL(EOS(STATIC_4387(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(o3666sub)) → 4434_0_createList_NULL(EOS(STATIC_4434(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(o3666sub))
4387_0_createList_NULL(EOS(STATIC_4387(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 4436_0_createList_NULL(EOS(STATIC_4436(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL)
4434_0_createList_NULL(EOS(STATIC_4434(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(o3666sub)) → 4451_0_createList_Load(EOS(STATIC_4451(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub))
4451_0_createList_Load(EOS(STATIC_4451(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub)) → 4463_0_createList_Load(EOS(STATIC_4463(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub))
4463_0_createList_Load(EOS(STATIC_4463(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub)) → 4471_0_createList_FieldAccess(EOS(STATIC_4471(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o3666sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4471_0_createList_FieldAccess(EOS(STATIC_4471(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4480_0_createList_FieldAccess(EOS(STATIC_4480(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4480_0_createList_FieldAccess(EOS(STATIC_4480(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4490_0_createList_Inc(EOS(STATIC_4490(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
4490_0_createList_Inc(EOS(STATIC_4490(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 4502_0_createList_JMP(EOS(STATIC_4502(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
4502_0_createList_JMP(EOS(STATIC_4502(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2280) → 4524_0_createList_Load(EOS(STATIC_4524(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2280)
4524_0_createList_Load(EOS(STATIC_4524(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2280) → 3053_0_createList_Load(EOS(STATIC_3053(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2280)
3053_0_createList_Load(EOS(STATIC_3053(i1339)), i190, o1932, i1340) → 3067_0_createList_Load(EOS(STATIC_3067(i1339)), i190, o1932, i1340, i1340)
4436_0_createList_NULL(EOS(STATIC_4436(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 4453_0_createList_Inc(EOS(STATIC_4453(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
4453_0_createList_Inc(EOS(STATIC_4453(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 4465_0_createList_JMP(EOS(STATIC_4465(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
4465_0_createList_JMP(EOS(STATIC_4465(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264) → 4473_0_createList_Load(EOS(STATIC_4473(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264)
4473_0_createList_Load(EOS(STATIC_4473(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264) → 3053_0_createList_Load(EOS(STATIC_3053(i1462)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2264)
3468_0_random_NONNULL(EOS(STATIC_3468(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3485_0_random_ConstantStackPush(EOS(STATIC_3485(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL)
3485_0_random_ConstantStackPush(EOS(STATIC_3485(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL) → 3510_0_random_Return(EOS(STATIC_3510(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, 0)
3510_0_random_Return(EOS(STATIC_3510(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, matching1) → 3547_0_createList_InvokeMethod(EOS(STATIC_3547(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3547_0_createList_InvokeMethod(EOS(STATIC_3547(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3972_0_createList_InvokeMethod(EOS(STATIC_3972(i1462)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3242_0_random_GT(EOS(STATIC_3242(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i188, i1339) → 3253_0_random_ConstantStackPush(EOS(STATIC_3253(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | <=(i188, i1339)
3253_0_random_ConstantStackPush(EOS(STATIC_3253(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3270_0_random_Return(EOS(STATIC_3270(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0)
3270_0_random_Return(EOS(STATIC_3270(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3284_0_createList_InvokeMethod(EOS(STATIC_3284(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3284_0_createList_InvokeMethod(EOS(STATIC_3284(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3304_0_<init>_Load(EOS(STATIC_3304(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3304_0_<init>_Load(EOS(STATIC_3304(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3338_0_<init>_InvokeMethod(EOS(STATIC_3338(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3338_0_<init>_InvokeMethod(EOS(STATIC_3338(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3357_0_<init>_Load(EOS(STATIC_3357(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3357_0_<init>_Load(EOS(STATIC_3357(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3374_0_<init>_Load(EOS(STATIC_3374(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3374_0_<init>_Load(EOS(STATIC_3374(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3386_0_<init>_FieldAccess(EOS(STATIC_3386(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3386_0_<init>_FieldAccess(EOS(STATIC_3386(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3401_0_<init>_Return(EOS(STATIC_3401(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3401_0_<init>_Return(EOS(STATIC_3401(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3431_0_createList_Store(EOS(STATIC_3431(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | =(matching1, 0)
3431_0_createList_Store(EOS(STATIC_3431(i1339)), i190, i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3469_0_createList_Load(EOS(STATIC_3469(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
3469_0_createList_Load(EOS(STATIC_3469(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 3488_0_createList_Load(EOS(STATIC_3488(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3488_0_createList_Load(EOS(STATIC_3488(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3512_0_createList_FieldAccess(EOS(STATIC_3512(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932)
3512_0_createList_FieldAccess(EOS(STATIC_3512(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o1932) → 3549_0_createList_Load(EOS(STATIC_3549(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932)
3549_0_createList_Load(EOS(STATIC_3549(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932) → 3620_0_createList_NULL(EOS(STATIC_3620(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, o1932, o1932)
3620_0_createList_NULL(EOS(STATIC_3620(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(o2591sub)) → 3696_0_createList_NULL(EOS(STATIC_3696(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(o2591sub))
3620_0_createList_NULL(EOS(STATIC_3620(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 3697_0_createList_NULL(EOS(STATIC_3697(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL)
3696_0_createList_NULL(EOS(STATIC_3696(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(o2591sub)) → 3717_0_createList_Load(EOS(STATIC_3717(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub))
3717_0_createList_Load(EOS(STATIC_3717(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub)) → 3748_0_createList_Load(EOS(STATIC_3748(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub))
3748_0_createList_Load(EOS(STATIC_3748(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub)) → 3917_0_createList_FieldAccess(EOS(STATIC_3917(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(o2591sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3917_0_createList_FieldAccess(EOS(STATIC_3917(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3975_0_createList_FieldAccess(EOS(STATIC_3975(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3975_0_createList_FieldAccess(EOS(STATIC_3975(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4009_0_createList_Inc(EOS(STATIC_4009(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
4009_0_createList_Inc(EOS(STATIC_4009(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 4048_0_createList_JMP(EOS(STATIC_4048(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
4048_0_createList_JMP(EOS(STATIC_4048(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975) → 4152_0_createList_Load(EOS(STATIC_4152(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975)
4152_0_createList_Load(EOS(STATIC_4152(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975) → 3053_0_createList_Load(EOS(STATIC_3053(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1975)
3697_0_createList_NULL(EOS(STATIC_3697(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340, NULL, NULL) → 3718_0_createList_Inc(EOS(STATIC_3718(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340)
3718_0_createList_Inc(EOS(STATIC_3718(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1340) → 3749_0_createList_JMP(EOS(STATIC_3749(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1340, 1))
3749_0_createList_JMP(EOS(STATIC_3749(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1738) → 3919_0_createList_Load(EOS(STATIC_3919(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1738)
3919_0_createList_Load(EOS(STATIC_3919(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1738) → 3053_0_createList_Load(EOS(STATIC_3053(i1339)), i190, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1738)
R rules:

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

P rules:
3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, x2, x3, x3) → 4387_0_createList_NULL(EOS(STATIC_4387(+(x0, 1))), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x3, x2, x2) | &&(<(x3, x1), >(+(x0, 1), 0))
4387_0_createList_NULL(EOS(STATIC_4387(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
4387_0_createList_NULL(EOS(STATIC_4387(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, NULL, NULL) → 3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, x2) → 3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, NULL, x2, x2) → 3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
R rules:

Filtered ground terms:

DoublyLinkedList.DoublyLinkedList(x1) → DoublyLinkedList.DoublyLinkedList
java.lang.Object(x1) → java.lang.Object
Cond_3067_0_createList_Load2(x1, x2, x3, x4, x5, x6) → Cond_3067_0_createList_Load2(x1, x2, x3, x5, x6)
Cond_3067_0_createList_Load1(x1, x2, x3, x4, x5, x6) → Cond_3067_0_createList_Load1(x1, x2, x3, x5, x6)
4387_0_createList_NULL(x1, x2, x3, x4, x5, x6) → 4387_0_createList_NULL(x1, x2, x4, x5, x6)

Filtered duplicate args:

3067_0_createList_Load(x1, x2, x3, x4, x5) → 3067_0_createList_Load(x1, x2, x3, x5)
Cond_3067_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_3067_0_createList_Load(x1, x2, x3, x4, x6)
4387_0_createList_NULL(x1, x2, x3, x4, x5) → 4387_0_createList_NULL(x1, x2, x3, x5)
Cond_3067_0_createList_Load1(x1, x2, x3, x4, x5) → Cond_3067_0_createList_Load1(x1, x2, x3, x5)
Cond_3067_0_createList_Load2(x1, x2, x3, x4, x5) → Cond_3067_0_createList_Load2(x1, x2, x3, x5)

Filtered all non-integer terms:

4387_0_createList_NULL(x1, x2, x3, x4) → 4387_0_createList_NULL(x1, x2, x3)
3067_0_createList_Load(x1, x2, x3, x4) → 3067_0_createList_Load(x1, x2, x4)

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

P rules:
3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, x2) → 3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, +(x2, 1)) | <(x2, x1)
3067_0_createList_Load(EOS(STATIC_3067(x0)), x1, x2) → 3067_0_createList_Load(EOS(STATIC_3067(+(x0, 1))), x1, +(x2, 1)) | &&(<(x2, x1), >(x0, -1))
R rules:

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

P rules:
3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, x2) → COND_3067_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3067(x0)), x1, x2)
COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0)), x1, x2) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, +(x2, 1))
3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, x2) → COND_3067_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3067(x0)), x1, x2)
COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0)), x1, x2) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0, 1))), x1, +(x2, 1))
R rules:

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0]) → COND_3067_0_CREATELIST_LOAD(x2[0] < x1[0], EOS(STATIC_3067(x0[0])), x1[0], x2[0])
(1): COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], x2[1] + 1)
(2): 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2]) → COND_3067_0_CREATELIST_LOAD1(x2[2] < x1[2] && x0[2] > -1, EOS(STATIC_3067(x0[2])), x1[2], x2[2])
(3): COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[3] + 1)), x1[3], x2[3] + 1)

(0) -> (1), if (x2[0] < x1[0] ∧EOS(STATIC_3067(x0[0])) →^* EOS(STATIC_3067(x0[1]))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

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

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

(2) -> (3), if (x2[2] < x1[2] && x0[2] > -1 ∧EOS(STATIC_3067(x0[2])) →^* EOS(STATIC_3067(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

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

(3) -> (2), if (EOS(STATIC_3067(x0[3] + 1)) →^* EOS(STATIC_3067(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

The set Q is empty.

(30) IDPNonInfProof (SOUND transformation)

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

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

For Pair 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, x2) → COND_3067_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3067(x0)), x1, x2) the following chains were created:

We consider the chain 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0]) → COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0]), COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:
(1)    (<(x2[0], x1[0])=TRUE∧EOS(STATIC_3067(x0[0]))=EOS(STATIC_3067(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0])≥NonInfC∧3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0])≥COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (<(x2[0], x1[0])=TRUE ⇒ 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0])≥NonInfC∧3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0])≥COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(8)    (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

(9)    (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

For Pair COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0)), x1, x2) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:
(10)    (COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1])≥NonInfC∧COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1])≥3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))∧(U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))), ≥))

We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(11)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(12)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(13)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(14)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

For Pair 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, x2) → COND_3067_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3067(x0)), x1, x2) the following chains were created:

We consider the chain 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2]) → COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2]), COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:
(15)    (&&(<(x2[2], x1[2]), >(x0[2], -1))=TRUE∧EOS(STATIC_3067(x0[2]))=EOS(STATIC_3067(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2])≥NonInfC∧3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2])≥COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (15) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(16)    (<(x2[2], x1[2])=TRUE∧>(x0[2], -1)=TRUE ⇒ 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2])≥NonInfC∧3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2])≥COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(17)    (x1[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[2] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    (x1[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[2] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    (x1[2] + [-1] + [-1]x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[2] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(20)    (x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(21)    (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

(22)    (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

For Pair COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0)), x1, x2) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0, 1))), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:
(23)    (COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3])≥3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))∧(U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(26)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(27)    ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, x2) → COND_3067_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3067(x0)), x1, x2)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0)), x1, x2) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, +(x2, 1))
- ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)
3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0)), x1, x2) → COND_3067_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3067(x0)), x1, x2)
- (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
- (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0)), x1, x2) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0, 1))), x1, +(x2, 1))
- ((U^Increasing(3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(3067_0_CREATELIST_LOAD(x₁, x₂, x₃)) = [-1]x₃ + x₂
POL(EOS(x₁)) = x₁
POL(STATIC_3067(x₁)) = x₁
POL(COND_3067_0_CREATELIST_LOAD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₃
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_3067_0_CREATELIST_LOAD1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₃
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]

The following pairs are in P_>:

3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0]) → COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])
3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2]) → COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])

The following pairs are in P_bound:

3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[0])), x1[0], x2[0]) → COND_3067_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3067(x0[0])), x1[0], x2[0])
3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[2])), x1[2], x2[2]) → COND_3067_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3067(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], +(x2[1], 1))
COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(+(x0[3], 1))), x1[3], +(x2[3], 1))

There are no usable rules.

(31) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_3067_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3067(x0[1])), x1[1], x2[1]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[1])), x1[1], x2[1] + 1)
(3): COND_3067_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3067(x0[3])), x1[3], x2[3]) → 3067_0_CREATELIST_LOAD(EOS(STATIC_3067(x0[3] + 1)), x1[3], x2[3] + 1)

The set Q is empty.

(32) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Complex Obligation (AND)

(10) Obligation:

(11) IDependencyGraphProof (EQUIVALENT transformation)

(12) TRUE

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPtoQDPProof (SOUND transformation)

(20) Obligation:

(21) UsableRulesProof (EQUIVALENT transformation)

(22) Obligation:

(23) QReductionProof (EQUIVALENT transformation)

(24) Obligation:

(25) QDPSizeChangeProof (EQUIVALENT transformation)

(26) YES

(27) Obligation:

(28) SCCToIDPv1Proof (SOUND transformation)

(29) Obligation:

(30) IDPNonInfProof (SOUND transformation)

(31) Obligation:

(32) IDependencyGraphProof (EQUIVALENT transformation)

(33) TRUE