Termination proof of /tmp/tmpHlnab0/MainFind.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 2200 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 830 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 290 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 360 ms)

        ↳14 IDP

        ↳15 IDPtoQDPProof (⇒, 20 ms)

        ↳16 QDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QReductionProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 JBCTerminationSCC

        ↳24 SCCToIDPv1Proof (⇒, 1210 ms)

        ↳25 IDP

        ↳26 IDPNonInfProof (⇒, 310 ms)

        ↳27 AND

            ↳28 IDP

                ↳29 IDependencyGraphProof (⇔, 0 ms)

                ↳30 TRUE

            ↳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_14 (Sun Microsystems Inc.) Main-Class: DoublyLinkedList/MainFind

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) {
        DoublyLinkedList current = this.getFirst();
        while (index > 0 && current != null) {
            current = current.next;
        }
        return current;
    }

    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 MainFind {
    public static void main(final String[] args) {
        Random.args = args;
        final DoublyLinkedList list = DoublyLinkedList.createList();
        list.find(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.MainFind.main([Ljava/lang/String;)V: Graph of 305 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.findR(I)LDoublyLinkedList/DoublyLinkedList;: Graph of 88 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.findR(I)LDoublyLinkedList/DoublyLinkedList;
SCC calls the following helper methods: DoublyLinkedList.DoublyLinkedList.findR(I)LDoublyLinkedList/DoublyLinkedList;
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 36 rules for P and 57 rules for R.

P rules:
3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub)) → 3626_0_findR_FieldAccess(EOS(STATIC_3626), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub))
3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub)) → 3627_0_findR_FieldAccess(EOS(STATIC_3627), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub))
3626_0_findR_FieldAccess(EOS(STATIC_3626), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084))) → 3639_0_findR_FieldAccess(EOS(STATIC_3639), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)))
3639_0_findR_FieldAccess(EOS(STATIC_3639), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084))) → 3651_0_findR_Load(EOS(STATIC_3651), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875)
3651_0_findR_Load(EOS(STATIC_3651), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875) → 3666_0_findR_NE(EOS(STATIC_3666), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754)
3666_0_findR_NE(EOS(STATIC_3666), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754) → 3684_0_findR_NE(EOS(STATIC_3684), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754)
3684_0_findR_NE(EOS(STATIC_3684), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754) → 3700_0_findR_Load(EOS(STATIC_3700), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754) | !(=(i1875, i1754))
3700_0_findR_Load(EOS(STATIC_3700), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754) → 3715_0_findR_FieldAccess(EOS(STATIC_3715), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)))
3715_0_findR_FieldAccess(EOS(STATIC_3715), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084))) → 3734_0_findR_NULL(EOS(STATIC_3734), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, o3084)
3734_0_findR_NULL(EOS(STATIC_3734), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754, java.lang.Object(o3181sub)) → 3760_0_findR_NULL(EOS(STATIC_3760), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754, java.lang.Object(o3181sub))
3760_0_findR_NULL(EOS(STATIC_3760), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754, java.lang.Object(o3181sub)) → 3777_0_findR_Load(EOS(STATIC_3777), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754)
3777_0_findR_Load(EOS(STATIC_3777), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754) → 3804_0_findR_FieldAccess(EOS(STATIC_3804), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))))
3804_0_findR_FieldAccess(EOS(STATIC_3804), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub)))) → 3844_0_findR_Load(EOS(STATIC_3844), i1754, java.lang.Object(o3181sub))
3844_0_findR_Load(EOS(STATIC_3844), i1754, java.lang.Object(o3181sub)) → 3864_0_findR_InvokeMethod(EOS(STATIC_3864), java.lang.Object(o3181sub), i1754)
3864_0_findR_InvokeMethod(EOS(STATIC_3864), java.lang.Object(o3181sub), i1754) → 3878_1_findR_InvokeMethod(3878_0_findR_Load(EOS(STATIC_3878), java.lang.Object(o3181sub), i1754), java.lang.Object(o3181sub), i1754)
3878_0_findR_Load(EOS(STATIC_3878), java.lang.Object(o3181sub), i1754) → 3901_0_findR_Load(EOS(STATIC_3901), java.lang.Object(o3181sub), i1754)
3901_0_findR_Load(EOS(STATIC_3901), java.lang.Object(o3181sub), i1754) → 3953_0_findR_Load(EOS(STATIC_3953), java.lang.Object(o3181sub), i1754)
3953_0_findR_Load(EOS(STATIC_3953), java.lang.Object(o3391sub), i1754) → 3996_0_findR_Load(EOS(STATIC_3996), java.lang.Object(o3391sub), i1754)
3996_0_findR_Load(EOS(STATIC_3996), java.lang.Object(o3391sub), i1754) → 3613_0_findR_Load(EOS(STATIC_3613), java.lang.Object(o3391sub), i1754)
3613_0_findR_Load(EOS(STATIC_3613), java.lang.Object(o3057sub), i1754) → 3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub))
3627_0_findR_FieldAccess(EOS(STATIC_3627), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087))) → 3640_0_findR_FieldAccess(EOS(STATIC_3640), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)))
3640_0_findR_FieldAccess(EOS(STATIC_3640), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087))) → 3652_0_findR_Load(EOS(STATIC_3652), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876)
3652_0_findR_Load(EOS(STATIC_3652), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876) → 3671_0_findR_NE(EOS(STATIC_3671), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754)
3671_0_findR_NE(EOS(STATIC_3671), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754) → 3687_0_findR_NE(EOS(STATIC_3687), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754)
3687_0_findR_NE(EOS(STATIC_3687), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754) → 3704_0_findR_Load(EOS(STATIC_3704), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754) | !(=(i1876, i1754))
3704_0_findR_Load(EOS(STATIC_3704), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754) → 3718_0_findR_FieldAccess(EOS(STATIC_3718), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)))
3718_0_findR_FieldAccess(EOS(STATIC_3718), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087))) → 3740_0_findR_NULL(EOS(STATIC_3740), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, o3087)
3740_0_findR_NULL(EOS(STATIC_3740), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754, java.lang.Object(o3182sub)) → 3762_0_findR_NULL(EOS(STATIC_3762), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754, java.lang.Object(o3182sub))
3762_0_findR_NULL(EOS(STATIC_3762), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754, java.lang.Object(o3182sub)) → 3780_0_findR_Load(EOS(STATIC_3780), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754)
3780_0_findR_Load(EOS(STATIC_3780), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754) → 3807_0_findR_FieldAccess(EOS(STATIC_3807), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))))
3807_0_findR_FieldAccess(EOS(STATIC_3807), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub)))) → 3847_0_findR_Load(EOS(STATIC_3847), i1754, java.lang.Object(o3182sub))
3847_0_findR_Load(EOS(STATIC_3847), i1754, java.lang.Object(o3182sub)) → 3866_0_findR_InvokeMethod(EOS(STATIC_3866), java.lang.Object(o3182sub), i1754)
3866_0_findR_InvokeMethod(EOS(STATIC_3866), java.lang.Object(o3182sub), i1754) → 3879_1_findR_InvokeMethod(3879_0_findR_Load(EOS(STATIC_3879), java.lang.Object(o3182sub), i1754), java.lang.Object(o3182sub), i1754)
3879_0_findR_Load(EOS(STATIC_3879), java.lang.Object(o3182sub), i1754) → 3902_0_findR_Load(EOS(STATIC_3902), java.lang.Object(o3182sub), i1754)
3902_0_findR_Load(EOS(STATIC_3902), java.lang.Object(o3182sub), i1754) → 3998_0_findR_Load(EOS(STATIC_3998), java.lang.Object(o3182sub), i1754)
3998_0_findR_Load(EOS(STATIC_3998), java.lang.Object(o3182sub), i1754) → 3613_0_findR_Load(EOS(STATIC_3613), java.lang.Object(o3182sub), i1754)
R rules:
3666_0_findR_NE(EOS(STATIC_3666), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, i1754, i1754) → 3685_0_findR_NE(EOS(STATIC_3685), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, i1754, i1754)
3671_0_findR_NE(EOS(STATIC_3671), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, i1754, i1754) → 3688_0_findR_NE(EOS(STATIC_3688), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, i1754, i1754)
3685_0_findR_NE(EOS(STATIC_3685), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, i1754, i1754) → 3702_0_findR_Load(EOS(STATIC_3702), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754)
3688_0_findR_NE(EOS(STATIC_3688), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, i1754, i1754) → 3705_0_findR_Load(EOS(STATIC_3705), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754)
3702_0_findR_Load(EOS(STATIC_3702), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754) → 3717_0_findR_Return(EOS(STATIC_3717), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)))
3705_0_findR_Load(EOS(STATIC_3705), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754) → 3720_0_findR_Return(EOS(STATIC_3720), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)))
3734_0_findR_NULL(EOS(STATIC_3734), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, NULL)), i1754, NULL) → 3761_0_findR_NULL(EOS(STATIC_3761), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, NULL)), i1754, NULL)
3740_0_findR_NULL(EOS(STATIC_3740), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, NULL)), i1754, NULL) → 3763_0_findR_NULL(EOS(STATIC_3763), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, NULL)), i1754, NULL)
3761_0_findR_NULL(EOS(STATIC_3761), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, NULL)), i1754, NULL) → 3778_0_findR_ConstantStackPush(EOS(STATIC_3778))
3763_0_findR_NULL(EOS(STATIC_3763), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, NULL)), i1754, NULL) → 3782_0_findR_ConstantStackPush(EOS(STATIC_3782))
3778_0_findR_ConstantStackPush(EOS(STATIC_3778)) → 3805_0_findR_Return(EOS(STATIC_3805), NULL)
3782_0_findR_ConstantStackPush(EOS(STATIC_3782)) → 3809_0_findR_Return(EOS(STATIC_3809), NULL)
3878_1_findR_InvokeMethod(3717_0_findR_Return(EOS(STATIC_3717), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070) → 4055_0_findR_Return(EOS(STATIC_4055), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)))
3878_1_findR_InvokeMethod(3720_0_findR_Return(EOS(STATIC_3720), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077) → 4070_0_findR_Return(EOS(STATIC_4070), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)))
3878_1_findR_InvokeMethod(3805_0_findR_Return(EOS(STATIC_3805), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085) → 4073_0_findR_Return(EOS(STATIC_4073), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085, NULL)
3878_1_findR_InvokeMethod(3809_0_findR_Return(EOS(STATIC_3809), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092) → 4080_0_findR_Return(EOS(STATIC_4080), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092, NULL)
3878_1_findR_InvokeMethod(4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2330, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050)))), i2331) → 4319_0_findR_Return(EOS(STATIC_4319), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2330, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050)))), i2331, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050)))
3878_1_findR_InvokeMethod(4225_0_findR_Return(EOS(STATIC_4225), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2341, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2340, NULL)))), i2342) → 4331_0_findR_Return(EOS(STATIC_4331), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2341, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2340, NULL)))), i2342, NULL)
3878_1_findR_InvokeMethod(4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2353, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075)))), i2354) → 4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2353, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075)))), i2354, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075)))
3878_1_findR_InvokeMethod(4232_0_findR_Return(EOS(STATIC_4232), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2364, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2363, NULL)))), i2365) → 4378_0_findR_Return(EOS(STATIC_4378), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2364, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2363, NULL)))), i2365, NULL)
3878_1_findR_InvokeMethod(4446_0_findR_Return(EOS(STATIC_4446), o4199), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583) → 4565_0_findR_Return(EOS(STATIC_4565), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583, o4199)
3878_1_findR_InvokeMethod(4450_0_findR_Return(EOS(STATIC_4450), o4236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4606)))))), i2597) → 4581_0_findR_Return(EOS(STATIC_4581), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4606)))))), i2597, o4236)
3879_1_findR_InvokeMethod(3717_0_findR_Return(EOS(STATIC_3717), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099) → 4082_0_findR_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)))
3879_1_findR_InvokeMethod(3720_0_findR_Return(EOS(STATIC_3720), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106) → 4091_0_findR_Return(EOS(STATIC_4091), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)))
3879_1_findR_InvokeMethod(3805_0_findR_Return(EOS(STATIC_3805), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2112, NULL)), i2113) → 4092_0_findR_Return(EOS(STATIC_4092), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2112, NULL)), i2113, NULL)
3879_1_findR_InvokeMethod(3809_0_findR_Return(EOS(STATIC_3809), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121) → 4096_0_findR_Return(EOS(STATIC_4096), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121, NULL)
3879_1_findR_InvokeMethod(4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2335, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057)))), i2336) → 4320_0_findR_Return(EOS(STATIC_4320), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2335, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057)))), i2336, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057)))
3879_1_findR_InvokeMethod(4225_0_findR_Return(EOS(STATIC_4225), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2347, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2346, NULL)))), i2348) → 4342_0_findR_Return(EOS(STATIC_4342), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2347, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2346, NULL)))), i2348, NULL)
3879_1_findR_InvokeMethod(4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085)))), i2360) → 4372_0_findR_Return(EOS(STATIC_4372), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085)))), i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085)))
3879_1_findR_InvokeMethod(4232_0_findR_Return(EOS(STATIC_4232), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2370, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2369, NULL)))), i2371) → 4383_0_findR_Return(EOS(STATIC_4383), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2370, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2369, NULL)))), i2371, NULL)
3879_1_findR_InvokeMethod(4446_0_findR_Return(EOS(STATIC_4446), o4199), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590) → 4572_0_findR_Return(EOS(STATIC_4572), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590, o4199)
3879_1_findR_InvokeMethod(4450_0_findR_Return(EOS(STATIC_4450), o4236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4616)))))), i2603) → 4588_0_findR_Return(EOS(STATIC_4588), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4616)))))), i2603, o4236)
4055_0_findR_Return(EOS(STATIC_4055), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517))) → 4071_0_findR_Return(EOS(STATIC_4071), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)))
4070_0_findR_Return(EOS(STATIC_4070), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524))) → 4071_0_findR_Return(EOS(STATIC_4071), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)))
4071_0_findR_Return(EOS(STATIC_4071), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630)), i2164, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630)), i2164, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630))) → 4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630)))
4073_0_findR_Return(EOS(STATIC_4073), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085, NULL) → 4081_0_findR_Return(EOS(STATIC_4081), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085, NULL)
4080_0_findR_Return(EOS(STATIC_4080), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092, NULL) → 4081_0_findR_Return(EOS(STATIC_4081), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092, NULL)
4081_0_findR_Return(EOS(STATIC_4081), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2170, NULL)), i2171, NULL) → 4225_0_findR_Return(EOS(STATIC_4225), NULL)
4082_0_findR_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550))) → 4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)))
4091_0_findR_Return(EOS(STATIC_4091), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558))) → 4082_0_findR_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)))
4092_0_findR_Return(EOS(STATIC_4092), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2112, NULL)), i2113, NULL) → 4232_0_findR_Return(EOS(STATIC_4232), NULL)
4096_0_findR_Return(EOS(STATIC_4096), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121, NULL) → 4092_0_findR_Return(EOS(STATIC_4092), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121, NULL)
4319_0_findR_Return(EOS(STATIC_4319), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2330, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050)))), i2331, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050))) → 4332_0_findR_Return(EOS(STATIC_4332), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2330, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050)))), i2331, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2331, o4050)))
4320_0_findR_Return(EOS(STATIC_4320), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2335, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057)))), i2336, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057))) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2335, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057)))), i2336, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2336, o4057)))
4331_0_findR_Return(EOS(STATIC_4331), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2341, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2340, NULL)))), i2342, NULL) → 4332_0_findR_Return(EOS(STATIC_4332), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2341, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2340, NULL)))), i2342, NULL)
4332_0_findR_Return(EOS(STATIC_4332), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2417, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2416, o4166)))), i2418, o4172) → 4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2417, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2416, o4166)))), i2418, o4172)
4342_0_findR_Return(EOS(STATIC_4342), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2347, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2346, NULL)))), i2348, NULL) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2347, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2346, NULL)))), i2348, NULL)
4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2422, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2421, o4193)))), i2423, o4199) → 4446_0_findR_Return(EOS(STATIC_4446), o4199)
4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2353, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075)))), i2354, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075))) → 4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2353, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075)))), i2354, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2354, o4075)))
4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2433, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2432, o4230)))), i2434, o4236) → 4450_0_findR_Return(EOS(STATIC_4450), o4236)
4372_0_findR_Return(EOS(STATIC_4372), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085)))), i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085))) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085)))), i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, o4085)))
4378_0_findR_Return(EOS(STATIC_4378), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2364, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2363, NULL)))), i2365, NULL) → 4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2364, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2363, NULL)))), i2365, NULL)
4383_0_findR_Return(EOS(STATIC_4383), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2370, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2369, NULL)))), i2371, NULL) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2370, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2369, NULL)))), i2371, NULL)
4565_0_findR_Return(EOS(STATIC_4565), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583, o4199) → 4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583, o4199)
4572_0_findR_Return(EOS(STATIC_4572), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590, o4199) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590, o4199)
4581_0_findR_Return(EOS(STATIC_4581), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4606)))))), i2597, o4236) → 4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4606)))))), i2597, o4236)
4588_0_findR_Return(EOS(STATIC_4588), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4616)))))), i2603, o4236) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4616)))))), i2603, o4236)

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

P rules:
3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 3878_1_findR_InvokeMethod(3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 3879_1_findR_InvokeMethod(3619_0_findR_FieldAccess(EOS(STATIC_3619), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
3879_1_findR_InvokeMethod(3717_0_findR_Return(EOS(STATIC_3717), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0) → 4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3879_1_findR_InvokeMethod(3720_0_findR_Return(EOS(STATIC_3720), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0) → 4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return(EOS(STATIC_3805), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4232_0_findR_Return(EOS(STATIC_4232), NULL)
3879_1_findR_InvokeMethod(3809_0_findR_Return(EOS(STATIC_3809), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4232_0_findR_Return(EOS(STATIC_4232), NULL)
3878_1_findR_InvokeMethod(3717_0_findR_Return(EOS(STATIC_3717), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0) → 4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3878_1_findR_InvokeMethod(3720_0_findR_Return(EOS(STATIC_3720), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)), x0) → 4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3878_1_findR_InvokeMethod(3805_0_findR_Return(EOS(STATIC_3805), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4225_0_findR_Return(EOS(STATIC_4225), NULL)
3878_1_findR_InvokeMethod(3809_0_findR_Return(EOS(STATIC_3809), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4225_0_findR_Return(EOS(STATIC_4225), NULL)
3879_1_findR_InvokeMethod(4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4446_0_findR_Return(EOS(STATIC_4446), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3879_1_findR_InvokeMethod(4225_0_findR_Return(EOS(STATIC_4225), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4446_0_findR_Return(EOS(STATIC_4446), NULL)
3879_1_findR_InvokeMethod(4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4446_0_findR_Return(EOS(STATIC_4446), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3879_1_findR_InvokeMethod(4232_0_findR_Return(EOS(STATIC_4232), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4446_0_findR_Return(EOS(STATIC_4446), NULL)
3879_1_findR_InvokeMethod(4446_0_findR_Return(EOS(STATIC_4446), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4446_0_findR_Return(EOS(STATIC_4446), x0)
3879_1_findR_InvokeMethod(4450_0_findR_Return(EOS(STATIC_4450), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4446_0_findR_Return(EOS(STATIC_4446), x0)
3878_1_findR_InvokeMethod(4229_0_findR_Return(EOS(STATIC_4229), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4450_0_findR_Return(EOS(STATIC_4450), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3878_1_findR_InvokeMethod(4232_0_findR_Return(EOS(STATIC_4232), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4450_0_findR_Return(EOS(STATIC_4450), NULL)
3878_1_findR_InvokeMethod(4446_0_findR_Return(EOS(STATIC_4446), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4450_0_findR_Return(EOS(STATIC_4450), x0)
3878_1_findR_InvokeMethod(4450_0_findR_Return(EOS(STATIC_4450), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4450_0_findR_Return(EOS(STATIC_4450), x0)
3878_1_findR_InvokeMethod(4224_0_findR_Return(EOS(STATIC_4224), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4450_0_findR_Return(EOS(STATIC_4450), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3878_1_findR_InvokeMethod(4225_0_findR_Return(EOS(STATIC_4225), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4450_0_findR_Return(EOS(STATIC_4450), NULL)

Filtered ground terms:

3619_0_findR_FieldAccess(x1, x2, x3, x4) → 3619_0_findR_FieldAccess(x2, x3, x4)
Cond_3619_0_findR_FieldAccess1(x1, x2, x3, x4, x5) → Cond_3619_0_findR_FieldAccess1(x1, x3, x4, x5)
DoublyLinkedList.DoublyLinkedList(x1, x2, x3) → DoublyLinkedList.DoublyLinkedList(x2, x3)
Cond_3619_0_findR_FieldAccess(x1, x2, x3, x4, x5) → Cond_3619_0_findR_FieldAccess(x1, x3, x4, x5)
4450_0_findR_Return(x1, x2) → 4450_0_findR_Return(x2)
4225_0_findR_Return(x1, x2) → 4225_0_findR_Return
4224_0_findR_Return(x1, x2) → 4224_0_findR_Return(x2)
4446_0_findR_Return(x1, x2) → 4446_0_findR_Return(x2)
4232_0_findR_Return(x1, x2) → 4232_0_findR_Return
4229_0_findR_Return(x1, x2) → 4229_0_findR_Return(x2)
3809_0_findR_Return(x1, x2) → 3809_0_findR_Return
3805_0_findR_Return(x1, x2) → 3805_0_findR_Return
3720_0_findR_Return(x1, x2, x3, x4) → 3720_0_findR_Return(x2, x3, x4)
3717_0_findR_Return(x1, x2, x3, x4) → 3717_0_findR_Return(x2, x3, x4)

Filtered duplicate args:

3619_0_findR_FieldAccess(x1, x2, x3) → 3619_0_findR_FieldAccess(x2, x3)
Cond_3619_0_findR_FieldAccess(x1, x2, x3, x4) → Cond_3619_0_findR_FieldAccess(x1, x3, x4)
Cond_3619_0_findR_FieldAccess1(x1, x2, x3, x4) → Cond_3619_0_findR_FieldAccess1(x1, x3, x4)
3717_0_findR_Return(x1, x2, x3) → 3717_0_findR_Return(x3)
3720_0_findR_Return(x1, x2, x3) → 3720_0_findR_Return(x3)

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

P rules:
3619_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3878_1_findR_InvokeMethod(3619_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3619_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3879_1_findR_InvokeMethod(3619_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4229_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3720_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4229_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4232_0_findR_Return
3879_1_findR_InvokeMethod(3809_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4232_0_findR_Return
3878_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4224_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3878_1_findR_InvokeMethod(3720_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4224_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3878_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4225_0_findR_Return
3878_1_findR_InvokeMethod(3809_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4225_0_findR_Return
3879_1_findR_InvokeMethod(4224_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4446_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(4225_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4446_0_findR_Return(NULL)
3879_1_findR_InvokeMethod(4229_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4446_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(4232_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4446_0_findR_Return(NULL)
3879_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4446_0_findR_Return(x0)
3879_1_findR_InvokeMethod(4450_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4446_0_findR_Return(x0)
3878_1_findR_InvokeMethod(4229_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4450_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3878_1_findR_InvokeMethod(4232_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4450_0_findR_Return(NULL)
3878_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4450_0_findR_Return(x0)
3878_1_findR_InvokeMethod(4450_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4450_0_findR_Return(x0)
3878_1_findR_InvokeMethod(4224_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4450_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3878_1_findR_InvokeMethod(4225_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4450_0_findR_Return(NULL)

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_3619_0_findR_FieldAccess_3, Cond_3619_0_findR_FieldAccess1_3]=Cond_3619_0_findR_FieldAccess_3, [3879_1_findR_InvokeMethod_3, 3878_1_findR_InvokeMethod_3]=3879_1_findR_InvokeMethod_3, [3717_0_findR_Return_1, 4229_0_findR_Return_1, 3720_0_findR_Return_1, 4224_0_findR_Return_1]=3717_0_findR_Return_1, [4446_0_findR_Return_1, 4450_0_findR_Return_1]=4446_0_findR_Return_1, [3805_0_findR_Return, 4232_0_findR_Return, 3809_0_findR_Return, 4225_0_findR_Return]=3805_0_findR_Return}

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

P rules:
3619_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
COND_3619_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3619_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
R rules:
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 3805_0_findR_Return
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4446_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4446_0_findR_Return(NULL)
3879_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4446_0_findR_Return(x0)

(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:

Boolean, Integer

The ITRS R consists of the following rules:
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 3805_0_findR_Return
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4446_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4446_0_findR_Return(NULL)
3879_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4446_0_findR_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3619_0_FINDR_FIELDACCESS(!(x0[0] = x2[0]), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
(1): COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))

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

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

The set Q consists of the following terms:
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
3879_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5)

(8) IDPNonInfProof (SOUND transformation)

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

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 3619_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) the following chains were created:

We consider the chain 3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1])) which results in the following constraint:
(1)    (!(=(x0[0], x2[0]))=TRUE∧x2[0]=x2[1]∧java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))=java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))) ⇒ 3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(U^Increasing(COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))), ≥))

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

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (0 ≥ 0 ⇒ (U^Increasing(COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))), ≥)∧[(6)bni_23 + (-1)Bound*bni_23] + [(8)bni_23]x1[0] + [(2)bni_23]x2[0] ≥ 0∧[2 + (-1)bso_24] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (0 ≥ 0 ⇒ (U^Increasing(COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))), ≥)∧[(6)bni_23 + (-1)Bound*bni_23] + [(8)bni_23]x1[0] + [(2)bni_23]x2[0] ≥ 0∧[2 + (-1)bso_24] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (0 ≥ 0 ⇒ (U^Increasing(COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))), ≥)∧[(6)bni_23 + (-1)Bound*bni_23] + [(8)bni_23]x1[0] + [(2)bni_23]x2[0] ≥ 0∧[2 + (-1)bso_24] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))), ≥)∧[(8)bni_23] ≥ 0∧0 ≥ 0∧[(2)bni_23] ≥ 0∧[(6)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[2 + (-1)bso_24] ≥ 0)

For Pair COND_3619_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3619_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1)) the following chains were created:

We consider the chain 3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1])), 3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) which results in the following constraint:
(7)    (!(=(x0[0], x2[0]))=TRUE∧x2[0]=x2[1]∧java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))=java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))∧x2[1]=x2[0]1∧java.lang.Object(x1[1])=java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))) ⇒ COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥NonInfC∧COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))∧(U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥))

We simplified constraint (7) using rules (I), (II), (III), (IV) which results in the following new constraint:
(8)    (!(=(x0[0], x2[0]))=TRUE ⇒ COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))))))≥NonInfC∧COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))))))≥3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))))∧(U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥)∧[(20)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x1[0]1 + [(2)bni_25]x2[0] ≥ 0∧[14 + (-1)bso_26] + [24]x1[0]1 ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥)∧[(20)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x1[0]1 + [(2)bni_25]x2[0] ≥ 0∧[14 + (-1)bso_26] + [24]x1[0]1 ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥)∧[(20)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x1[0]1 + [(2)bni_25]x2[0] ≥ 0∧[14 + (-1)bso_26] + [24]x1[0]1 ≥ 0)

We simplified constraint (11) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥)∧[(32)bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(2)bni_25] ≥ 0∧[(20)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[14 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

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

3619_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
- (0 ≥ 0 ⇒ (U^Increasing(COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))), ≥)∧[(8)bni_23] ≥ 0∧0 ≥ 0∧[(2)bni_23] ≥ 0∧[(6)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[2 + (-1)bso_24] ≥ 0)
COND_3619_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3619_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
- (0 ≥ 0 ⇒ (U^Increasing(3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))), ≥)∧[(32)bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(2)bni_25] ≥ 0∧[(20)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[14 + (-1)bso_26] ≥ 0∧[1] ≥ 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 with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(3879_1_findR_InvokeMethod(x₁, x₂, x₃)) = 0
POL(3717_0_findR_Return(x₁)) = 0
POL(java.lang.Object(x₁)) = [1] + [2]x₁
POL(DoublyLinkedList.DoublyLinkedList(x₁, x₂)) = [2]x₂
POL(3805_0_findR_Return) = 0
POL(NULL) = 0
POL(4446_0_findR_Return(x₁)) = 0
POL(3619_0_FINDR_FIELDACCESS(x₁, x₂)) = [1] + x₂ + [2]x₁
POL(COND_3619_0_FINDR_FIELDACCESS(x₁, x₂, x₃)) = [-1] + x₃ + [2]x₂ + [-1]x₁
POL(!(x₁)) = 0
POL(=(x₁, x₂)) = 0

The following pairs are in P_>:

3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))

The following pairs are in P_bound:

3619_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3619_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
COND_3619_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3619_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))

The following pairs are in P_≥:
none

At least the following rules have been oriented under context sensitive arithmetic replacement:

FALSE¹ → !(TRUE)¹
TRUE¹ → !(FALSE)¹

(9) Obligation:

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

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

The following domains are used:
none

The ITRS R consists of the following rules:
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 3805_0_findR_Return
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4446_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4446_0_findR_Return(NULL)
3879_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4446_0_findR_Return(x0)

The integer pair graph is empty.

The set Q consists of the following terms:
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
3879_1_findR_InvokeMethod(3717_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
3879_1_findR_InvokeMethod(3805_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
3879_1_findR_InvokeMethod(4446_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5)

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

(11) TRUE

(12) 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

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 24 rules for P and 35 rules for R.

P rules:
3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(o3047sub), java.lang.Object(o3047sub)) → 3616_0_getFirst_FieldAccess(EOS(STATIC_3616), java.lang.Object(o3047sub), java.lang.Object(o3047sub))
3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(o3047sub), java.lang.Object(o3047sub)) → 3617_0_getFirst_FieldAccess(EOS(STATIC_3617), java.lang.Object(o3047sub), java.lang.Object(o3047sub))
3616_0_getFirst_FieldAccess(EOS(STATIC_3616), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063))) → 3624_0_getFirst_FieldAccess(EOS(STATIC_3624), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)))
3624_0_getFirst_FieldAccess(EOS(STATIC_3624), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063))) → 3633_0_getFirst_NONNULL(EOS(STATIC_3633), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), o3063)
3633_0_getFirst_NONNULL(EOS(STATIC_3633), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))), java.lang.Object(o3090sub)) → 3646_0_getFirst_NONNULL(EOS(STATIC_3646), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))), java.lang.Object(o3090sub))
3646_0_getFirst_NONNULL(EOS(STATIC_3646), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))), java.lang.Object(o3090sub)) → 3659_0_getFirst_Load(EOS(STATIC_3659), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))))
3659_0_getFirst_Load(EOS(STATIC_3659), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub)))) → 3678_0_getFirst_FieldAccess(EOS(STATIC_3678), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))))
3678_0_getFirst_FieldAccess(EOS(STATIC_3678), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub)))) → 3695_0_getFirst_InvokeMethod(EOS(STATIC_3695), java.lang.Object(o3090sub))
3695_0_getFirst_InvokeMethod(EOS(STATIC_3695), java.lang.Object(o3090sub)) → 3713_1_getFirst_InvokeMethod(3713_0_getFirst_Load(EOS(STATIC_3713), java.lang.Object(o3090sub)), java.lang.Object(o3090sub))
3713_0_getFirst_Load(EOS(STATIC_3713), java.lang.Object(o3090sub)) → 3730_0_getFirst_Load(EOS(STATIC_3730), java.lang.Object(o3090sub))
3730_0_getFirst_Load(EOS(STATIC_3730), java.lang.Object(o3090sub)) → 3758_0_getFirst_Load(EOS(STATIC_3758), java.lang.Object(o3090sub))
3758_0_getFirst_Load(EOS(STATIC_3758), java.lang.Object(o3177sub)) → 3773_0_getFirst_Load(EOS(STATIC_3773), java.lang.Object(o3177sub))
3773_0_getFirst_Load(EOS(STATIC_3773), java.lang.Object(o3177sub)) → 3599_0_getFirst_Load(EOS(STATIC_3599), java.lang.Object(o3177sub))
3599_0_getFirst_Load(EOS(STATIC_3599), java.lang.Object(o3047sub)) → 3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(o3047sub), java.lang.Object(o3047sub))
3617_0_getFirst_FieldAccess(EOS(STATIC_3617), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066))) → 3625_0_getFirst_FieldAccess(EOS(STATIC_3625), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)))
3625_0_getFirst_FieldAccess(EOS(STATIC_3625), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066))) → 3637_0_getFirst_NONNULL(EOS(STATIC_3637), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), o3066)
3637_0_getFirst_NONNULL(EOS(STATIC_3637), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))), java.lang.Object(o3091sub)) → 3648_0_getFirst_NONNULL(EOS(STATIC_3648), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))), java.lang.Object(o3091sub))
3648_0_getFirst_NONNULL(EOS(STATIC_3648), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))), java.lang.Object(o3091sub)) → 3662_0_getFirst_Load(EOS(STATIC_3662), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))))
3662_0_getFirst_Load(EOS(STATIC_3662), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub)))) → 3681_0_getFirst_FieldAccess(EOS(STATIC_3681), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))))
3681_0_getFirst_FieldAccess(EOS(STATIC_3681), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub)))) → 3698_0_getFirst_InvokeMethod(EOS(STATIC_3698), java.lang.Object(o3091sub))
3698_0_getFirst_InvokeMethod(EOS(STATIC_3698), java.lang.Object(o3091sub)) → 3714_1_getFirst_InvokeMethod(3714_0_getFirst_Load(EOS(STATIC_3714), java.lang.Object(o3091sub)), java.lang.Object(o3091sub))
3714_0_getFirst_Load(EOS(STATIC_3714), java.lang.Object(o3091sub)) → 3732_0_getFirst_Load(EOS(STATIC_3732), java.lang.Object(o3091sub))
3732_0_getFirst_Load(EOS(STATIC_3732), java.lang.Object(o3091sub)) → 3776_0_getFirst_Load(EOS(STATIC_3776), java.lang.Object(o3091sub))
3776_0_getFirst_Load(EOS(STATIC_3776), java.lang.Object(o3091sub)) → 3599_0_getFirst_Load(EOS(STATIC_3599), java.lang.Object(o3091sub))
R rules:
3633_0_getFirst_NONNULL(EOS(STATIC_3633), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3647_0_getFirst_NONNULL(EOS(STATIC_3647), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3637_0_getFirst_NONNULL(EOS(STATIC_3637), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3649_0_getFirst_NONNULL(EOS(STATIC_3649), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3647_0_getFirst_NONNULL(EOS(STATIC_3647), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3661_0_getFirst_Load(EOS(STATIC_3661), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3649_0_getFirst_NONNULL(EOS(STATIC_3649), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3664_0_getFirst_Load(EOS(STATIC_3664), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3661_0_getFirst_Load(EOS(STATIC_3661), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3679_0_getFirst_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3664_0_getFirst_Load(EOS(STATIC_3664), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3683_0_getFirst_Return(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3679_0_getFirst_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3821_0_getFirst_Return(EOS(STATIC_3821), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3683_0_getFirst_Return(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3834_0_getFirst_Return(EOS(STATIC_3834), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3938_0_getFirst_Return(EOS(STATIC_3938), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(o3763sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115))))))) → 4399_0_getFirst_Return(EOS(STATIC_4399), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115)))))), java.lang.Object(o3763sub))
3713_1_getFirst_InvokeMethod(4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(o3840sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144))))))) → 4427_0_getFirst_Return(EOS(STATIC_4427), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144)))))), java.lang.Object(o3840sub))
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(3683_0_getFirst_Return(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3843_0_getFirst_Return(EOS(STATIC_3843), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3922_0_getFirst_Return(EOS(STATIC_3922), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3947_0_getFirst_Return(EOS(STATIC_3947), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(o3763sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124))))))) → 4406_0_getFirst_Return(EOS(STATIC_4406), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124)))))), java.lang.Object(o3763sub))
3714_1_getFirst_InvokeMethod(4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(o3840sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153))))))) → 4433_0_getFirst_Return(EOS(STATIC_4433), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153)))))), java.lang.Object(o3840sub))
3821_0_getFirst_Return(EOS(STATIC_3821), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3835_0_getFirst_Return(EOS(STATIC_3835), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3834_0_getFirst_Return(EOS(STATIC_3834), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3835_0_getFirst_Return(EOS(STATIC_3835), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3835_0_getFirst_Return(EOS(STATIC_3835), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3843_0_getFirst_Return(EOS(STATIC_3843), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3921_0_getFirst_Return(EOS(STATIC_3921), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3939_0_getFirst_Return(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3922_0_getFirst_Return(EOS(STATIC_3922), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4157_0_getFirst_Return(EOS(STATIC_4157), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3938_0_getFirst_Return(EOS(STATIC_3938), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3939_0_getFirst_Return(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3939_0_getFirst_Return(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4135_0_getFirst_Return(EOS(STATIC_4135), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3947_0_getFirst_Return(EOS(STATIC_3947), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3922_0_getFirst_Return(EOS(STATIC_3922), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4135_0_getFirst_Return(EOS(STATIC_4135), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3695)))), java.lang.Object(o3698sub)) → 4204_0_getFirst_Return(EOS(STATIC_4204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3695)))), java.lang.Object(o3698sub))
4157_0_getFirst_Return(EOS(STATIC_4157), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3760)))), java.lang.Object(o3763sub)) → 4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(o3763sub))
4204_0_getFirst_Return(EOS(STATIC_4204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3837)))), java.lang.Object(o3840sub)) → 4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(o3840sub))
4399_0_getFirst_Return(EOS(STATIC_4399), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115)))))), java.lang.Object(o3763sub)) → 4204_0_getFirst_Return(EOS(STATIC_4204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115)))))), java.lang.Object(o3763sub))
4406_0_getFirst_Return(EOS(STATIC_4406), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124)))))), java.lang.Object(o3763sub)) → 4157_0_getFirst_Return(EOS(STATIC_4157), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124)))))), java.lang.Object(o3763sub))
4427_0_getFirst_Return(EOS(STATIC_4427), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144)))))), java.lang.Object(o3840sub)) → 4204_0_getFirst_Return(EOS(STATIC_4204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144)))))), java.lang.Object(o3840sub))
4433_0_getFirst_Return(EOS(STATIC_4433), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153)))))), java.lang.Object(o3840sub)) → 4157_0_getFirst_Return(EOS(STATIC_4157), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153)))))), java.lang.Object(o3840sub))

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

P rules:
3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3713_1_getFirst_InvokeMethod(3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3714_1_getFirst_InvokeMethod(3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(3683_0_getFirst_Return(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3679_0_getFirst_Return(EOS(STATIC_3679), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3683_0_getFirst_Return(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(x0))
3714_1_getFirst_InvokeMethod(4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(x0))
3713_1_getFirst_InvokeMethod(4249_0_getFirst_Return(EOS(STATIC_4249), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(x0))
3713_1_getFirst_InvokeMethod(4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(x0))
3713_1_getFirst_InvokeMethod(3859_0_getFirst_Return(EOS(STATIC_3859), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3713_1_getFirst_InvokeMethod(3863_0_getFirst_Return(EOS(STATIC_3863), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4255_0_getFirst_Return(EOS(STATIC_4255), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))

Filtered ground terms:

3607_0_getFirst_FieldAccess(x1, x2, x3) → 3607_0_getFirst_FieldAccess(x2, x3)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
4255_0_getFirst_Return(x1, x2) → 4255_0_getFirst_Return(x2)
3863_0_getFirst_Return(x1, x2) → 3863_0_getFirst_Return
3859_0_getFirst_Return(x1, x2) → 3859_0_getFirst_Return
4249_0_getFirst_Return(x1, x2) → 4249_0_getFirst_Return(x2)
3683_0_getFirst_Return(x1, x2, x3) → 3683_0_getFirst_Return
3679_0_getFirst_Return(x1, x2, x3) → 3679_0_getFirst_Return

Filtered duplicate args:

3607_0_getFirst_FieldAccess(x1, x2) → 3607_0_getFirst_FieldAccess(x2)

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

P rules:
3607_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3713_1_getFirst_InvokeMethod(3607_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
3607_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3714_1_getFirst_InvokeMethod(3607_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3863_0_getFirst_Return
3714_1_getFirst_InvokeMethod(3683_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3863_0_getFirst_Return
3713_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3859_0_getFirst_Return
3713_1_getFirst_InvokeMethod(3683_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3859_0_getFirst_Return
3714_1_getFirst_InvokeMethod(3859_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4249_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(3863_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4249_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4249_0_getFirst_Return(java.lang.Object(x0))
3714_1_getFirst_InvokeMethod(4255_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4249_0_getFirst_Return(java.lang.Object(x0))
3713_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4255_0_getFirst_Return(java.lang.Object(x0))
3713_1_getFirst_InvokeMethod(4255_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4255_0_getFirst_Return(java.lang.Object(x0))
3713_1_getFirst_InvokeMethod(3859_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4255_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3713_1_getFirst_InvokeMethod(3863_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4255_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))

Performed bisimulation on rules. Used the following equivalence classes: {[3714_1_getFirst_InvokeMethod_2, 3713_1_getFirst_InvokeMethod_2]=3714_1_getFirst_InvokeMethod_2, [3679_0_getFirst_Return, 3863_0_getFirst_Return, 3683_0_getFirst_Return, 3859_0_getFirst_Return]=3679_0_getFirst_Return, [4249_0_getFirst_Return_1, 4255_0_getFirst_Return_1]=4249_0_getFirst_Return_1}

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

P rules:
3607_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3607_0_GETFIRST_FIELDACCESS(java.lang.Object(x0))
R rules:
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3679_0_getFirst_Return
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4249_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4249_0_getFirst_Return(java.lang.Object(x0))

(14) 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:
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3679_0_getFirst_Return
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4249_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4249_0_getFirst_Return(java.lang.Object(x0))

The integer pair graph contains the following rules and edges:
(0): 3607_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3607_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:
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

(15) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(16) Obligation:

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

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

The TRS R consists of the following rules:

3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3679_0_getFirst_Return
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4249_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4249_0_getFirst_Return(java.lang.Object(x0))

The set Q consists of the following terms:

3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3714_1_getFirst_InvokeMethod(4249_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.

(17) 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.

(18) Obligation:

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

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

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

3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3714_1_getFirst_InvokeMethod(4249_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.

(19) 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].

3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3714_1_getFirst_InvokeMethod(3679_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3714_1_getFirst_InvokeMethod(4249_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1)))))))

(20) Obligation:

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

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

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

(21) 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:

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

(22) YES

(23) 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

(24) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 94 rules for P and 0 rules for R.

P rules:
3423_0_createList_Load(EOS(STATIC_3423(i1784)), i189, o2894, i1785, i1785) → 3436_0_createList_GE(EOS(STATIC_3436(i1784)), i189, o2894, i1785, i1785, i189)
3436_0_createList_GE(EOS(STATIC_3436(i1784)), i189, o2894, i1785, i1785, i189) → 3453_0_createList_GE(EOS(STATIC_3453(i1784)), i189, o2894, i1785, i1785, i189)
3453_0_createList_GE(EOS(STATIC_3453(i1784)), i189, o2894, i1785, i1785, i189) → 3473_0_createList_Load(EOS(STATIC_3473(i1784)), i189, o2894, i1785) | <(i1785, i189)
3473_0_createList_Load(EOS(STATIC_3473(i1784)), i189, o2894, i1785) → 3504_0_createList_Store(EOS(STATIC_3504(i1784)), i189, i1785, o2894)
3504_0_createList_Store(EOS(STATIC_3504(i1784)), i189, i1785, o2894) → 3527_0_createList_New(EOS(STATIC_3527(i1784)), i189, i1785, o2894)
3527_0_createList_New(EOS(STATIC_3527(i1784)), i189, i1785, o2894) → 3543_0_createList_Duplicate(EOS(STATIC_3543(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3543_0_createList_Duplicate(EOS(STATIC_3543(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3569_0_createList_InvokeMethod(EOS(STATIC_3569(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3569_0_createList_InvokeMethod(EOS(STATIC_3569(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3577_0_random_FieldAccess(EOS(STATIC_3577(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3577_0_random_FieldAccess(EOS(STATIC_3577(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3595_0_random_ArrayLength(EOS(STATIC_3595(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187)))
3595_0_random_ArrayLength(EOS(STATIC_3595(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187))) → 3606_0_random_FieldAccess(EOS(STATIC_3606(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187) | >=(i187, 0)
3606_0_random_FieldAccess(EOS(STATIC_3606(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187) → 3615_0_random_GT(EOS(STATIC_3615(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784)
3615_0_random_GT(EOS(STATIC_3615(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784) → 3622_0_random_GT(EOS(STATIC_3622(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784)
3615_0_random_GT(EOS(STATIC_3615(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784) → 3623_0_random_GT(EOS(STATIC_3623(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784)
3622_0_random_GT(EOS(STATIC_3622(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784) → 3630_0_random_FieldAccess(EOS(STATIC_3630(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | >(i187, i1784)
3630_0_random_FieldAccess(EOS(STATIC_3630(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3643_0_random_FieldAccess(EOS(STATIC_3643(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187)))
3643_0_random_FieldAccess(EOS(STATIC_3643(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187))) → 3657_0_random_ArrayAccess(EOS(STATIC_3657(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187)), i1784)
3657_0_random_ArrayAccess(EOS(STATIC_3657(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187)), i1784) → 3674_0_random_ArrayAccess(EOS(STATIC_3674(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187)), i1784)
3674_0_random_ArrayAccess(EOS(STATIC_3674(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i187)), i1784) → 3692_0_random_Store(EOS(STATIC_3692(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) | <(i1784, i187)
3692_0_random_Store(EOS(STATIC_3692(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) → 3710_0_random_FieldAccess(EOS(STATIC_3710(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127)
3710_0_random_FieldAccess(EOS(STATIC_3710(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) → 3726_0_random_ConstantStackPush(EOS(STATIC_3726(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784)
3726_0_random_ConstantStackPush(EOS(STATIC_3726(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784) → 3749_0_random_IntArithmetic(EOS(STATIC_3749(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784, 1)
3749_0_random_IntArithmetic(EOS(STATIC_3749(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784, matching1) → 3769_0_random_FieldAccess(EOS(STATIC_3769(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, +(i1784, 1)) | &&(>=(i1784, 0), =(matching1, 1))
3769_0_random_FieldAccess(EOS(STATIC_3769(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1907) → 3787_0_random_Load(EOS(STATIC_3787(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127)
3787_0_random_Load(EOS(STATIC_3787(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) → 3817_0_random_NONNULL(EOS(STATIC_3817(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, o3127)
3817_0_random_NONNULL(EOS(STATIC_3817(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub), java.lang.Object(o3285sub)) → 3855_0_random_NONNULL(EOS(STATIC_3855(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub), java.lang.Object(o3285sub))
3817_0_random_NONNULL(EOS(STATIC_3817(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3856_0_random_NONNULL(EOS(STATIC_3856(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL)
3855_0_random_NONNULL(EOS(STATIC_3855(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub), java.lang.Object(o3285sub)) → 3870_0_random_Load(EOS(STATIC_3870(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub))
3870_0_random_Load(EOS(STATIC_3870(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub)) → 3889_0_random_InvokeMethod(EOS(STATIC_3889(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub))
3889_0_random_InvokeMethod(EOS(STATIC_3889(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub)) → 3917_0_length_Load(EOS(STATIC_3917(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub), java.lang.Object(o3285sub))
3917_0_length_Load(EOS(STATIC_3917(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub), java.lang.Object(o3285sub)) → 4008_0_length_FieldAccess(EOS(STATIC_4008(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3285sub), java.lang.Object(o3285sub))
4008_0_length_FieldAccess(EOS(STATIC_4008(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), java.lang.Object(java.lang.String(o3578sub, i2130))) → 4039_0_length_FieldAccess(EOS(STATIC_4039(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), java.lang.Object(java.lang.String(o3578sub, i2130))) | &&(>=(i2130, 0), >=(i2131, 0))
4039_0_length_FieldAccess(EOS(STATIC_4039(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), java.lang.Object(java.lang.String(o3578sub, i2130))) → 4105_0_length_Return(EOS(STATIC_4105(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), i2130)
4105_0_length_Return(EOS(STATIC_4105(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), i2130) → 4239_0_random_Return(EOS(STATIC_4239(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4239_0_random_Return(EOS(STATIC_4239(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4268_0_createList_InvokeMethod(EOS(STATIC_4268(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4268_0_createList_InvokeMethod(EOS(STATIC_4268(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4295_0_<init>_Load(EOS(STATIC_4295(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4295_0_<init>_Load(EOS(STATIC_4295(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4460_0_<init>_InvokeMethod(EOS(STATIC_4460(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4460_0_<init>_InvokeMethod(EOS(STATIC_4460(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4495_0_<init>_Load(EOS(STATIC_4495(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4495_0_<init>_Load(EOS(STATIC_4495(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4554_0_<init>_Load(EOS(STATIC_4554(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4554_0_<init>_Load(EOS(STATIC_4554(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4603_0_<init>_FieldAccess(EOS(STATIC_4603(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4603_0_<init>_FieldAccess(EOS(STATIC_4603(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4618_0_<init>_Return(EOS(STATIC_4618(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4618_0_<init>_Return(EOS(STATIC_4618(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4630_0_createList_Store(EOS(STATIC_4630(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4630_0_createList_Store(EOS(STATIC_4630(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4642_0_createList_Load(EOS(STATIC_4642(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
4642_0_createList_Load(EOS(STATIC_4642(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 4652_0_createList_Load(EOS(STATIC_4652(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4652_0_createList_Load(EOS(STATIC_4652(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4662_0_createList_FieldAccess(EOS(STATIC_4662(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894)
4662_0_createList_FieldAccess(EOS(STATIC_4662(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894) → 4673_0_createList_Load(EOS(STATIC_4673(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
4673_0_createList_Load(EOS(STATIC_4673(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 4701_0_createList_NULL(EOS(STATIC_4701(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, o2894)
4701_0_createList_NULL(EOS(STATIC_4701(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(o5022sub)) → 4777_0_createList_NULL(EOS(STATIC_4777(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(o5022sub))
4701_0_createList_NULL(EOS(STATIC_4701(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4778_0_createList_NULL(EOS(STATIC_4778(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL)
4777_0_createList_NULL(EOS(STATIC_4777(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(o5022sub)) → 4810_0_createList_Load(EOS(STATIC_4810(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub))
4810_0_createList_Load(EOS(STATIC_4810(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub)) → 4823_0_createList_Load(EOS(STATIC_4823(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub))
4823_0_createList_Load(EOS(STATIC_4823(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub)) → 4833_0_createList_FieldAccess(EOS(STATIC_4833(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4833_0_createList_FieldAccess(EOS(STATIC_4833(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4842_0_createList_FieldAccess(EOS(STATIC_4842(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4842_0_createList_FieldAccess(EOS(STATIC_4842(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4851_0_createList_Inc(EOS(STATIC_4851(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4851_0_createList_Inc(EOS(STATIC_4851(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4857_0_createList_JMP(EOS(STATIC_4857(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4857_0_createList_JMP(EOS(STATIC_4857(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930) → 4864_0_createList_Load(EOS(STATIC_4864(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930)
4864_0_createList_Load(EOS(STATIC_4864(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930) → 3408_0_createList_Load(EOS(STATIC_3408(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930)
3408_0_createList_Load(EOS(STATIC_3408(i1784)), i189, o2894, i1785) → 3423_0_createList_Load(EOS(STATIC_3423(i1784)), i189, o2894, i1785, i1785)
4778_0_createList_NULL(EOS(STATIC_4778(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4812_0_createList_Inc(EOS(STATIC_4812(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4812_0_createList_Inc(EOS(STATIC_4812(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4824_0_createList_JMP(EOS(STATIC_4824(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4824_0_createList_JMP(EOS(STATIC_4824(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2912) → 4835_0_createList_Load(EOS(STATIC_4835(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2912)
4835_0_createList_Load(EOS(STATIC_4835(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2912) → 3408_0_createList_Load(EOS(STATIC_3408(i1907)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2912)
3856_0_random_NONNULL(EOS(STATIC_3856(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3872_0_random_ConstantStackPush(EOS(STATIC_3872(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL)
3872_0_random_ConstantStackPush(EOS(STATIC_3872(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL) → 3890_0_random_Return(EOS(STATIC_3890(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, 0)
3890_0_random_Return(EOS(STATIC_3890(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, matching1) → 3918_0_createList_InvokeMethod(EOS(STATIC_3918(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3918_0_createList_InvokeMethod(EOS(STATIC_3918(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 4268_0_createList_InvokeMethod(EOS(STATIC_4268(i1907)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3623_0_random_GT(EOS(STATIC_3623(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i187, i1784) → 3631_0_random_ConstantStackPush(EOS(STATIC_3631(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | <=(i187, i1784)
3631_0_random_ConstantStackPush(EOS(STATIC_3631(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3644_0_random_Return(EOS(STATIC_3644(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0)
3644_0_random_Return(EOS(STATIC_3644(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3658_0_createList_InvokeMethod(EOS(STATIC_3658(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3658_0_createList_InvokeMethod(EOS(STATIC_3658(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3677_0_<init>_Load(EOS(STATIC_3677(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3677_0_<init>_Load(EOS(STATIC_3677(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3711_0_<init>_InvokeMethod(EOS(STATIC_3711(i1784)), i189, i1785, o2894, 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))
3711_0_<init>_InvokeMethod(EOS(STATIC_3711(i1784)), i189, i1785, o2894, 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))) → 3729_0_<init>_Load(EOS(STATIC_3729(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3729_0_<init>_Load(EOS(STATIC_3729(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3752_0_<init>_Load(EOS(STATIC_3752(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3752_0_<init>_Load(EOS(STATIC_3752(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3771_0_<init>_FieldAccess(EOS(STATIC_3771(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3771_0_<init>_FieldAccess(EOS(STATIC_3771(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3790_0_<init>_Return(EOS(STATIC_3790(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3790_0_<init>_Return(EOS(STATIC_3790(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3820_0_createList_Store(EOS(STATIC_3820(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | =(matching1, 0)
3820_0_createList_Store(EOS(STATIC_3820(i1784)), i189, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3858_0_createList_Load(EOS(STATIC_3858(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
3858_0_createList_Load(EOS(STATIC_3858(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 3874_0_createList_Load(EOS(STATIC_3874(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3874_0_createList_Load(EOS(STATIC_3874(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3893_0_createList_FieldAccess(EOS(STATIC_3893(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894)
3893_0_createList_FieldAccess(EOS(STATIC_3893(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894) → 3920_0_createList_Load(EOS(STATIC_3920(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
3920_0_createList_Load(EOS(STATIC_3920(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 3976_0_createList_NULL(EOS(STATIC_3976(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, o2894)
3976_0_createList_NULL(EOS(STATIC_3976(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(o3506sub)) → 4010_0_createList_NULL(EOS(STATIC_4010(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(o3506sub))
3976_0_createList_NULL(EOS(STATIC_3976(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4011_0_createList_NULL(EOS(STATIC_4011(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL)
4010_0_createList_NULL(EOS(STATIC_4010(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(o3506sub)) → 4042_0_createList_Load(EOS(STATIC_4042(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub))
4042_0_createList_Load(EOS(STATIC_4042(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub)) → 4109_0_createList_Load(EOS(STATIC_4109(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub))
4109_0_createList_Load(EOS(STATIC_4109(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub)) → 4243_0_createList_FieldAccess(EOS(STATIC_4243(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4243_0_createList_FieldAccess(EOS(STATIC_4243(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4270_0_createList_FieldAccess(EOS(STATIC_4270(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4270_0_createList_FieldAccess(EOS(STATIC_4270(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4302_0_createList_Inc(EOS(STATIC_4302(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4302_0_createList_Inc(EOS(STATIC_4302(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4392_0_createList_JMP(EOS(STATIC_4392(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4392_0_createList_JMP(EOS(STATIC_4392(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469) → 4465_0_createList_Load(EOS(STATIC_4465(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469)
4465_0_createList_Load(EOS(STATIC_4465(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469) → 3408_0_createList_Load(EOS(STATIC_3408(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469)
4011_0_createList_NULL(EOS(STATIC_4011(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4043_0_createList_Inc(EOS(STATIC_4043(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4043_0_createList_Inc(EOS(STATIC_4043(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4110_0_createList_JMP(EOS(STATIC_4110(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4110_0_createList_JMP(EOS(STATIC_4110(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195) → 4245_0_createList_Load(EOS(STATIC_4245(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195)
4245_0_createList_Load(EOS(STATIC_4245(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195) → 3408_0_createList_Load(EOS(STATIC_3408(i1784)), i189, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195)
R rules:

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

P rules:
3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, x2, x3, x3) → 4701_0_createList_NULL(EOS(STATIC_4701(+(x0, 1))), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x3, x2, x2) | &&(<(x3, x1), >(+(x0, 1), 0))
4701_0_createList_NULL(EOS(STATIC_4701(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
4701_0_createList_NULL(EOS(STATIC_4701(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, NULL, NULL) → 3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, x2) → 3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, NULL, x2, x2) → 3423_0_createList_Load(EOS(STATIC_3423(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_3423_0_createList_Load2(x1, x2, x3, x4, x5, x6) → Cond_3423_0_createList_Load2(x1, x2, x3, x5, x6)
Cond_3423_0_createList_Load1(x1, x2, x3, x4, x5, x6) → Cond_3423_0_createList_Load1(x1, x2, x3, x5, x6)
4701_0_createList_NULL(x1, x2, x3, x4, x5, x6) → 4701_0_createList_NULL(x1, x2, x4, x5, x6)

Filtered duplicate args:

3423_0_createList_Load(x1, x2, x3, x4, x5) → 3423_0_createList_Load(x1, x2, x3, x5)
Cond_3423_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_3423_0_createList_Load(x1, x2, x3, x4, x6)
4701_0_createList_NULL(x1, x2, x3, x4, x5) → 4701_0_createList_NULL(x1, x2, x3, x5)
Cond_3423_0_createList_Load1(x1, x2, x3, x4, x5) → Cond_3423_0_createList_Load1(x1, x2, x3, x5)
Cond_3423_0_createList_Load2(x1, x2, x3, x4, x5) → Cond_3423_0_createList_Load2(x1, x2, x3, x5)

Filtered all non-integer terms:

4701_0_createList_NULL(x1, x2, x3, x4) → 4701_0_createList_NULL(x1, x2, x3)
3423_0_createList_Load(x1, x2, x3, x4) → 3423_0_createList_Load(x1, x2, x4)

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

P rules:
3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, x2) → 3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, +(x2, 1)) | <(x2, x1)
3423_0_createList_Load(EOS(STATIC_3423(x0)), x1, x2) → 3423_0_createList_Load(EOS(STATIC_3423(+(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:
3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, x2) → COND_3423_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3423(x0)), x1, x2)
COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0)), x1, x2) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, +(x2, 1))
3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, x2) → COND_3423_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3423(x0)), x1, x2)
COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0)), x1, x2) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(x0, 1))), x1, +(x2, 1))
R rules:

(25) 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): 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0]) → COND_3423_0_CREATELIST_LOAD(x2[0] < x1[0], EOS(STATIC_3423(x0[0])), x1[0], x2[0])
(1): COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], x2[1] + 1)
(2): 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2]) → COND_3423_0_CREATELIST_LOAD1(x2[2] < x1[2] && x0[2] > -1, EOS(STATIC_3423(x0[2])), x1[2], x2[2])
(3): COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[3] + 1)), x1[3], x2[3] + 1)

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

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

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

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

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

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

The set Q is empty.

(26) 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@6c745bc0 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 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, x2) → COND_3423_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3423(x0)), x1, x2) the following chains were created:

We consider the chain 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0]) → COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0]), COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:
(1)    (<(x2[0], x1[0])=TRUE∧EOS(STATIC_3423(x0[0]))=EOS(STATIC_3423(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0])≥NonInfC∧3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0])≥COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(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 ⇒ 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0])≥NonInfC∧3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0])≥COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[(-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_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[(-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_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[(-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_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(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)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_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[(-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_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[(-1)bso_13] ≥ 0)

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

For Pair COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0)), x1, x2) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:
(10)    (COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1])≥NonInfC∧COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1])≥3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], +(x2[1], 1))∧(U^Increasing(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(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(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[1 + (-1)bso_15] ≥ 0)

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

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

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

For Pair 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, x2) → COND_3423_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3423(x0)), x1, x2) the following chains were created:

We consider the chain 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2]) → COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(x0[2])), x1[2], x2[2]), COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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_3423(x0[2]))=EOS(STATIC_3423(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2])≥NonInfC∧3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2])≥COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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 ⇒ 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2])≥NonInfC∧3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2])≥COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0)), x1, x2) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(x0, 1))), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:
(23)    (COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3])≥3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(x0[3], 1))), x1[3], +(x2[3], 1))∧(U^Increasing(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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.

3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, x2) → COND_3423_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3423(x0)), x1, x2)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[(-1)bso_13] ≥ 0)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[(-1)bso_13] ≥ 0)
COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0)), x1, x2) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, +(x2, 1))
- ((U^Increasing(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0)), x1, x2) → COND_3423_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3423(x0)), x1, x2)
- (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(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_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0)), x1, x2) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(x0, 1))), x1, +(x2, 1))
- ((U^Increasing(3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(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(3423_0_CREATELIST_LOAD(x₁, x₂, x₃)) = [-1]x₃ + x₂
POL(EOS(x₁)) = x₁
POL(STATIC_3423(x₁)) = x₁
POL(COND_3423_0_CREATELIST_LOAD(x₁, x₂, x₃, x₄)) = [-1]x₄ + x₃
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_3423_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_>:

COND_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], +(x2[1], 1))
3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2]) → COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(x0[2])), x1[2], x2[2])

The following pairs are in P_bound:

3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0]) → COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])
3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[2])), x1[2], x2[2]) → COND_3423_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3423(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[0])), x1[0], x2[0]) → COND_3423_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3423(x0[0])), x1[0], x2[0])
COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(+(x0[3], 1))), x1[3], +(x2[3], 1))

There are no usable rules.

(27) Complex Obligation (AND)

(28) 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

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

The set Q is empty.

(29) IDependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

(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_3423_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3423(x0[1])), x1[1], x2[1]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(x0[1])), x1[1], x2[1] + 1)
(3): COND_3423_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3423(x0[3])), x1[3], x2[3]) → 3423_0_CREATELIST_LOAD(EOS(STATIC_3423(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) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPtoQDPProof (SOUND transformation)

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) QReductionProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) SCCToIDPv1Proof (SOUND transformation)

(25) Obligation:

(26) IDPNonInfProof (SOUND transformation)

(27) Complex Obligation (AND)

(28) Obligation:

(29) IDependencyGraphProof (EQUIVALENT transformation)

(30) TRUE

(31) Obligation:

(32) IDependencyGraphProof (EQUIVALENT transformation)

(33) TRUE