Termination proof of /tmp/tmpVzIYcN/MainDelete.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 3310 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 910 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 270 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 450 ms)

        ↳14 IDP

        ↳15 IDPtoQDPProof (⇒, 10 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 (⇒, 1050 ms)

        ↳25 IDP

        ↳26 IDPNonInfProof (⇒, 230 ms)

        ↳27 IDP

        ↳28 IDependencyGraphProof (⇔, 0 ms)

        ↳29 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/MainDelete

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 MainDelete {
    public static void main(final String[] args) {
        Random.args = args;
        final DoublyLinkedList list = DoublyLinkedList.createList();
        list.delete(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.MainDelete.main([Ljava/lang/String;)V: Graph of 822 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:
3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(o3926sub), i2303, java.lang.Object(o3926sub)) → 3939_0_findR_FieldAccess(EOS(STATIC_3939), java.lang.Object(o3926sub), i2303, java.lang.Object(o3926sub))
3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(o3926sub), i2303, java.lang.Object(o3926sub)) → 3940_0_findR_FieldAccess(EOS(STATIC_3940), java.lang.Object(o3926sub), i2303, java.lang.Object(o3926sub))
3939_0_findR_FieldAccess(EOS(STATIC_3939), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955))) → 3953_0_findR_FieldAccess(EOS(STATIC_3953), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)))
3953_0_findR_FieldAccess(EOS(STATIC_3953), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955))) → 3966_0_findR_Load(EOS(STATIC_3966), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, i2389)
3966_0_findR_Load(EOS(STATIC_3966), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, i2389) → 3984_0_findR_NE(EOS(STATIC_3984), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, i2389, i2303)
3984_0_findR_NE(EOS(STATIC_3984), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, i2389, i2303) → 4006_0_findR_NE(EOS(STATIC_4006), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, i2389, i2303)
4006_0_findR_NE(EOS(STATIC_4006), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, i2389, i2303) → 4023_0_findR_Load(EOS(STATIC_4023), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303) | !(=(i2389, i2303))
4023_0_findR_Load(EOS(STATIC_4023), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303) → 4039_0_findR_FieldAccess(EOS(STATIC_4039), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)))
4039_0_findR_FieldAccess(EOS(STATIC_4039), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955))) → 4059_0_findR_NULL(EOS(STATIC_4059), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2303, o3955)
4059_0_findR_NULL(EOS(STATIC_4059), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub))), i2303, java.lang.Object(o4057sub)) → 4082_0_findR_NULL(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub))), i2303, java.lang.Object(o4057sub))
4082_0_findR_NULL(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub))), i2303, java.lang.Object(o4057sub)) → 4099_0_findR_Load(EOS(STATIC_4099), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub))), i2303)
4099_0_findR_Load(EOS(STATIC_4099), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub))), i2303) → 4127_0_findR_FieldAccess(EOS(STATIC_4127), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub))))
4127_0_findR_FieldAccess(EOS(STATIC_4127), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4057sub)))) → 4166_0_findR_Load(EOS(STATIC_4166), i2303, java.lang.Object(o4057sub))
4166_0_findR_Load(EOS(STATIC_4166), i2303, java.lang.Object(o4057sub)) → 4186_0_findR_InvokeMethod(EOS(STATIC_4186), java.lang.Object(o4057sub), i2303)
4186_0_findR_InvokeMethod(EOS(STATIC_4186), java.lang.Object(o4057sub), i2303) → 4203_1_findR_InvokeMethod(4203_0_findR_Load(EOS(STATIC_4203), java.lang.Object(o4057sub), i2303), java.lang.Object(o4057sub), i2303)
4203_0_findR_Load(EOS(STATIC_4203), java.lang.Object(o4057sub), i2303) → 4225_0_findR_Load(EOS(STATIC_4225), java.lang.Object(o4057sub), i2303)
4225_0_findR_Load(EOS(STATIC_4225), java.lang.Object(o4057sub), i2303) → 4249_0_findR_Load(EOS(STATIC_4249), java.lang.Object(o4057sub), i2303)
4249_0_findR_Load(EOS(STATIC_4249), java.lang.Object(o4225sub), i2303) → 4265_0_findR_Load(EOS(STATIC_4265), java.lang.Object(o4225sub), i2303)
4265_0_findR_Load(EOS(STATIC_4265), java.lang.Object(o4225sub), i2303) → 3918_0_findR_Load(EOS(STATIC_3918), java.lang.Object(o4225sub), i2303)
3918_0_findR_Load(EOS(STATIC_3918), java.lang.Object(o3926sub), i2303) → 3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(o3926sub), i2303, java.lang.Object(o3926sub))
3940_0_findR_FieldAccess(EOS(STATIC_3940), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958))) → 3954_0_findR_FieldAccess(EOS(STATIC_3954), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)))
3954_0_findR_FieldAccess(EOS(STATIC_3954), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958))) → 3968_0_findR_Load(EOS(STATIC_3968), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, i2390)
3968_0_findR_Load(EOS(STATIC_3968), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, i2390) → 3988_0_findR_NE(EOS(STATIC_3988), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, i2390, i2303)
3988_0_findR_NE(EOS(STATIC_3988), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, i2390, i2303) → 4008_0_findR_NE(EOS(STATIC_4008), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, i2390, i2303)
4008_0_findR_NE(EOS(STATIC_4008), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, i2390, i2303) → 4026_0_findR_Load(EOS(STATIC_4026), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303) | !(=(i2390, i2303))
4026_0_findR_Load(EOS(STATIC_4026), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303) → 4042_0_findR_FieldAccess(EOS(STATIC_4042), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)))
4042_0_findR_FieldAccess(EOS(STATIC_4042), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958))) → 4065_0_findR_NULL(EOS(STATIC_4065), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2303, o3958)
4065_0_findR_NULL(EOS(STATIC_4065), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub))), i2303, java.lang.Object(o4058sub)) → 4084_0_findR_NULL(EOS(STATIC_4084), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub))), i2303, java.lang.Object(o4058sub))
4084_0_findR_NULL(EOS(STATIC_4084), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub))), i2303, java.lang.Object(o4058sub)) → 4102_0_findR_Load(EOS(STATIC_4102), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub))), i2303)
4102_0_findR_Load(EOS(STATIC_4102), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub))), i2303) → 4130_0_findR_FieldAccess(EOS(STATIC_4130), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub))))
4130_0_findR_FieldAccess(EOS(STATIC_4130), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4058sub)))) → 4169_0_findR_Load(EOS(STATIC_4169), i2303, java.lang.Object(o4058sub))
4169_0_findR_Load(EOS(STATIC_4169), i2303, java.lang.Object(o4058sub)) → 4187_0_findR_InvokeMethod(EOS(STATIC_4187), java.lang.Object(o4058sub), i2303)
4187_0_findR_InvokeMethod(EOS(STATIC_4187), java.lang.Object(o4058sub), i2303) → 4204_1_findR_InvokeMethod(4204_0_findR_Load(EOS(STATIC_4204), java.lang.Object(o4058sub), i2303), java.lang.Object(o4058sub), i2303)
4204_0_findR_Load(EOS(STATIC_4204), java.lang.Object(o4058sub), i2303) → 4226_0_findR_Load(EOS(STATIC_4226), java.lang.Object(o4058sub), i2303)
4226_0_findR_Load(EOS(STATIC_4226), java.lang.Object(o4058sub), i2303) → 4267_0_findR_Load(EOS(STATIC_4267), java.lang.Object(o4058sub), i2303)
4267_0_findR_Load(EOS(STATIC_4267), java.lang.Object(o4058sub), i2303) → 3918_0_findR_Load(EOS(STATIC_3918), java.lang.Object(o4058sub), i2303)
R rules:
3984_0_findR_NE(EOS(STATIC_3984), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)), i2303, i2303, i2303) → 4007_0_findR_NE(EOS(STATIC_4007), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)), i2303, i2303, i2303)
3988_0_findR_NE(EOS(STATIC_3988), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)), i2303, i2303, i2303) → 4009_0_findR_NE(EOS(STATIC_4009), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)), i2303, i2303, i2303)
4007_0_findR_NE(EOS(STATIC_4007), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)), i2303, i2303, i2303) → 4024_0_findR_Load(EOS(STATIC_4024), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)), i2303)
4009_0_findR_NE(EOS(STATIC_4009), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)), i2303, i2303, i2303) → 4027_0_findR_Load(EOS(STATIC_4027), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)), i2303)
4024_0_findR_Load(EOS(STATIC_4024), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)), i2303) → 4041_0_findR_Return(EOS(STATIC_4041), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3955)))
4027_0_findR_Load(EOS(STATIC_4027), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)), i2303) → 4044_0_findR_Return(EOS(STATIC_4044), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)), i2303, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2303, o3958)))
4059_0_findR_NULL(EOS(STATIC_4059), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, NULL)), i2303, NULL) → 4083_0_findR_NULL(EOS(STATIC_4083), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, NULL)), i2303, NULL)
4065_0_findR_NULL(EOS(STATIC_4065), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, NULL)), i2303, NULL) → 4085_0_findR_NULL(EOS(STATIC_4085), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, NULL)), i2303, NULL)
4083_0_findR_NULL(EOS(STATIC_4083), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, NULL)), i2303, NULL) → 4100_0_findR_ConstantStackPush(EOS(STATIC_4100))
4085_0_findR_NULL(EOS(STATIC_4085), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, NULL)), i2303, NULL) → 4103_0_findR_ConstantStackPush(EOS(STATIC_4103))
4100_0_findR_ConstantStackPush(EOS(STATIC_4100)) → 4129_0_findR_Return(EOS(STATIC_4129), NULL)
4103_0_findR_ConstantStackPush(EOS(STATIC_4103)) → 4132_0_findR_Return(EOS(STATIC_4132), NULL)
4203_1_findR_InvokeMethod(4041_0_findR_Return(EOS(STATIC_4041), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536) → 4317_0_findR_Return(EOS(STATIC_4317), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)))
4203_1_findR_InvokeMethod(4044_0_findR_Return(EOS(STATIC_4044), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544) → 4334_0_findR_Return(EOS(STATIC_4334), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)))
4203_1_findR_InvokeMethod(4129_0_findR_Return(EOS(STATIC_4129), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2551, NULL)), i2552) → 4336_0_findR_Return(EOS(STATIC_4336), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2551, NULL)), i2552, NULL)
4203_1_findR_InvokeMethod(4132_0_findR_Return(EOS(STATIC_4132), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2558, NULL)), i2559) → 4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2558, NULL)), i2559, NULL)
4203_1_findR_InvokeMethod(4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2640, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449)))), i2641) → 4464_0_findR_Return(EOS(STATIC_4464), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2640, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449)))), i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449)))
4203_1_findR_InvokeMethod(4379_0_findR_Return(EOS(STATIC_4379), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2650, NULL)))), i2652) → 4484_0_findR_Return(EOS(STATIC_4484), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2650, NULL)))), i2652, NULL)
4203_1_findR_InvokeMethod(4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2661, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474)))), i2662) → 4530_0_findR_Return(EOS(STATIC_4530), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2661, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474)))), i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474)))
4203_1_findR_InvokeMethod(4385_0_findR_Return(EOS(STATIC_4385), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2671, NULL)))), i2673) → 4550_0_findR_Return(EOS(STATIC_4550), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2671, NULL)))), i2673, NULL)
4203_1_findR_InvokeMethod(4581_0_findR_Return(EOS(STATIC_4581), o4553), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2780, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2779, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2778, o4844)))))), i2781) → 4660_0_findR_Return(EOS(STATIC_4660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2780, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2779, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2778, o4844)))))), i2781, o4553)
4203_1_findR_InvokeMethod(4586_0_findR_Return(EOS(STATIC_4586), o4590), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2795, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2794, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, o4861)))))), i2796) → 4684_0_findR_Return(EOS(STATIC_4684), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2795, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2794, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, o4861)))))), i2796, o4590)
4204_1_findR_InvokeMethod(4041_0_findR_Return(EOS(STATIC_4041), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)), i2567, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)), i2567) → 4345_0_findR_Return(EOS(STATIC_4345), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)), i2567, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)), i2567, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)))
4204_1_findR_InvokeMethod(4044_0_findR_Return(EOS(STATIC_4044), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574) → 4355_0_findR_Return(EOS(STATIC_4355), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)))
4204_1_findR_InvokeMethod(4129_0_findR_Return(EOS(STATIC_4129), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, NULL)), i2581) → 4356_0_findR_Return(EOS(STATIC_4356), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, NULL)), i2581, NULL)
4204_1_findR_InvokeMethod(4132_0_findR_Return(EOS(STATIC_4132), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, NULL)), i2590) → 4360_0_findR_Return(EOS(STATIC_4360), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, NULL)), i2590, NULL)
4204_1_findR_InvokeMethod(4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2645, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456)))), i2646) → 4465_0_findR_Return(EOS(STATIC_4465), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2645, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456)))), i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456)))
4204_1_findR_InvokeMethod(4379_0_findR_Return(EOS(STATIC_4379), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2655, NULL)))), i2657) → 4500_0_findR_Return(EOS(STATIC_4500), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2655, NULL)))), i2657, NULL)
4204_1_findR_InvokeMethod(4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2667, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484)))), i2668) → 4542_0_findR_Return(EOS(STATIC_4542), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2667, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484)))), i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484)))
4204_1_findR_InvokeMethod(4385_0_findR_Return(EOS(STATIC_4385), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2678, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2677, NULL)))), i2679) → 4557_0_findR_Return(EOS(STATIC_4557), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2678, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2677, NULL)))), i2679, NULL)
4204_1_findR_InvokeMethod(4581_0_findR_Return(EOS(STATIC_4581), o4553), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2788, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2787, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2786, o4853)))))), i2789) → 4670_0_findR_Return(EOS(STATIC_4670), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2788, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2787, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2786, o4853)))))), i2789, o4553)
4204_1_findR_InvokeMethod(4586_0_findR_Return(EOS(STATIC_4586), o4590), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2801, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, o4870)))))), i2802) → 4695_0_findR_Return(EOS(STATIC_4695), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2801, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, o4870)))))), i2802, o4590)
4317_0_findR_Return(EOS(STATIC_4317), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260))) → 4335_0_findR_Return(EOS(STATIC_4335), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)), i2536, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2536, o4260)))
4334_0_findR_Return(EOS(STATIC_4334), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267))) → 4335_0_findR_Return(EOS(STATIC_4335), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)), i2544, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2544, o4267)))
4335_0_findR_Return(EOS(STATIC_4335), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4329)), i2600, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4329)), i2600, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4329))) → 4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4329)))
4336_0_findR_Return(EOS(STATIC_4336), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2551, NULL)), i2552, NULL) → 4344_0_findR_Return(EOS(STATIC_4344), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2551, NULL)), i2552, NULL)
4343_0_findR_Return(EOS(STATIC_4343), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2558, NULL)), i2559, NULL) → 4344_0_findR_Return(EOS(STATIC_4344), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2558, NULL)), i2559, NULL)
4344_0_findR_Return(EOS(STATIC_4344), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2606, NULL)), i2607, NULL) → 4379_0_findR_Return(EOS(STATIC_4379), NULL)
4345_0_findR_Return(EOS(STATIC_4345), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)), i2567, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)), i2567, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293))) → 4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2567, o4293)))
4355_0_findR_Return(EOS(STATIC_4355), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301))) → 4345_0_findR_Return(EOS(STATIC_4345), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)), i2574, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2574, o4301)))
4356_0_findR_Return(EOS(STATIC_4356), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, NULL)), i2581, NULL) → 4385_0_findR_Return(EOS(STATIC_4385), NULL)
4360_0_findR_Return(EOS(STATIC_4360), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, NULL)), i2590, NULL) → 4356_0_findR_Return(EOS(STATIC_4356), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, NULL)), i2590, NULL)
4464_0_findR_Return(EOS(STATIC_4464), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2640, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449)))), i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449))) → 4485_0_findR_Return(EOS(STATIC_4485), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2640, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449)))), i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, o4449)))
4465_0_findR_Return(EOS(STATIC_4465), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2645, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456)))), i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456))) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2645, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456)))), i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, o4456)))
4484_0_findR_Return(EOS(STATIC_4484), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2650, NULL)))), i2652, NULL) → 4485_0_findR_Return(EOS(STATIC_4485), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2650, NULL)))), i2652, NULL)
4485_0_findR_Return(EOS(STATIC_4485), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2685, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2684, o4520)))), i2686, o4526) → 4531_0_findR_Return(EOS(STATIC_4531), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2685, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2684, o4520)))), i2686, o4526)
4500_0_findR_Return(EOS(STATIC_4500), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2655, NULL)))), i2657, NULL) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2655, NULL)))), i2657, NULL)
4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2691, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2690, o4547)))), i2692, o4553) → 4581_0_findR_Return(EOS(STATIC_4581), o4553)
4530_0_findR_Return(EOS(STATIC_4530), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2661, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474)))), i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474))) → 4531_0_findR_Return(EOS(STATIC_4531), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2661, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474)))), i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, o4474)))
4531_0_findR_Return(EOS(STATIC_4531), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2702, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2701, o4584)))), i2703, o4590) → 4586_0_findR_Return(EOS(STATIC_4586), o4590)
4542_0_findR_Return(EOS(STATIC_4542), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2667, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484)))), i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484))) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2667, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484)))), i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, o4484)))
4550_0_findR_Return(EOS(STATIC_4550), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2671, NULL)))), i2673, NULL) → 4531_0_findR_Return(EOS(STATIC_4531), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2671, NULL)))), i2673, NULL)
4557_0_findR_Return(EOS(STATIC_4557), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2678, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2677, NULL)))), i2679, NULL) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2678, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2677, NULL)))), i2679, NULL)
4660_0_findR_Return(EOS(STATIC_4660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2780, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2779, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2778, o4844)))))), i2781, o4553) → 4531_0_findR_Return(EOS(STATIC_4531), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2780, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2779, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2778, o4844)))))), i2781, o4553)
4670_0_findR_Return(EOS(STATIC_4670), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2788, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2787, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2786, o4853)))))), i2789, o4553) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2788, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2787, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2786, o4853)))))), i2789, o4553)
4684_0_findR_Return(EOS(STATIC_4684), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2795, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2794, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, o4861)))))), i2796, o4590) → 4531_0_findR_Return(EOS(STATIC_4531), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2795, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2794, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, o4861)))))), i2796, o4590)
4695_0_findR_Return(EOS(STATIC_4695), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2801, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, o4870)))))), i2802, o4590) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2801, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, o4870)))))), i2802, o4590)

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

P rules:
3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 4203_1_findR_InvokeMethod(3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 4204_1_findR_InvokeMethod(3928_0_findR_FieldAccess(EOS(STATIC_3928), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
4204_1_findR_InvokeMethod(4041_0_findR_Return(EOS(STATIC_4041), 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) → 4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4204_1_findR_InvokeMethod(4044_0_findR_Return(EOS(STATIC_4044), 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) → 4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return(EOS(STATIC_4129), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4385_0_findR_Return(EOS(STATIC_4385), NULL)
4204_1_findR_InvokeMethod(4132_0_findR_Return(EOS(STATIC_4132), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4385_0_findR_Return(EOS(STATIC_4385), NULL)
4203_1_findR_InvokeMethod(4041_0_findR_Return(EOS(STATIC_4041), 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) → 4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4203_1_findR_InvokeMethod(4044_0_findR_Return(EOS(STATIC_4044), 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) → 4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4203_1_findR_InvokeMethod(4129_0_findR_Return(EOS(STATIC_4129), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4379_0_findR_Return(EOS(STATIC_4379), NULL)
4203_1_findR_InvokeMethod(4132_0_findR_Return(EOS(STATIC_4132), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4379_0_findR_Return(EOS(STATIC_4379), NULL)
4204_1_findR_InvokeMethod(4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4581_0_findR_Return(EOS(STATIC_4581), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4204_1_findR_InvokeMethod(4379_0_findR_Return(EOS(STATIC_4379), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4581_0_findR_Return(EOS(STATIC_4581), NULL)
4204_1_findR_InvokeMethod(4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4581_0_findR_Return(EOS(STATIC_4581), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4204_1_findR_InvokeMethod(4385_0_findR_Return(EOS(STATIC_4385), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4581_0_findR_Return(EOS(STATIC_4581), NULL)
4204_1_findR_InvokeMethod(4581_0_findR_Return(EOS(STATIC_4581), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4581_0_findR_Return(EOS(STATIC_4581), x0)
4204_1_findR_InvokeMethod(4586_0_findR_Return(EOS(STATIC_4586), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4581_0_findR_Return(EOS(STATIC_4581), x0)
4203_1_findR_InvokeMethod(4382_0_findR_Return(EOS(STATIC_4382), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4586_0_findR_Return(EOS(STATIC_4586), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4203_1_findR_InvokeMethod(4385_0_findR_Return(EOS(STATIC_4385), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4586_0_findR_Return(EOS(STATIC_4586), NULL)
4203_1_findR_InvokeMethod(4581_0_findR_Return(EOS(STATIC_4581), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4586_0_findR_Return(EOS(STATIC_4586), x0)
4203_1_findR_InvokeMethod(4586_0_findR_Return(EOS(STATIC_4586), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4586_0_findR_Return(EOS(STATIC_4586), x0)
4203_1_findR_InvokeMethod(4377_0_findR_Return(EOS(STATIC_4377), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4586_0_findR_Return(EOS(STATIC_4586), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4203_1_findR_InvokeMethod(4379_0_findR_Return(EOS(STATIC_4379), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4586_0_findR_Return(EOS(STATIC_4586), NULL)

Filtered ground terms:

3928_0_findR_FieldAccess(x1, x2, x3, x4) → 3928_0_findR_FieldAccess(x2, x3, x4)
Cond_3928_0_findR_FieldAccess1(x1, x2, x3, x4, x5) → Cond_3928_0_findR_FieldAccess1(x1, x3, x4, x5)
DoublyLinkedList.DoublyLinkedList(x1, x2, x3) → DoublyLinkedList.DoublyLinkedList(x2, x3)
Cond_3928_0_findR_FieldAccess(x1, x2, x3, x4, x5) → Cond_3928_0_findR_FieldAccess(x1, x3, x4, x5)
4586_0_findR_Return(x1, x2) → 4586_0_findR_Return(x2)
4379_0_findR_Return(x1, x2) → 4379_0_findR_Return
4377_0_findR_Return(x1, x2) → 4377_0_findR_Return(x2)
4581_0_findR_Return(x1, x2) → 4581_0_findR_Return(x2)
4385_0_findR_Return(x1, x2) → 4385_0_findR_Return
4382_0_findR_Return(x1, x2) → 4382_0_findR_Return(x2)
4132_0_findR_Return(x1, x2) → 4132_0_findR_Return
4129_0_findR_Return(x1, x2) → 4129_0_findR_Return
4044_0_findR_Return(x1, x2, x3, x4) → 4044_0_findR_Return(x2, x3, x4)
4041_0_findR_Return(x1, x2, x3, x4) → 4041_0_findR_Return(x2, x3, x4)

Filtered duplicate args:

3928_0_findR_FieldAccess(x1, x2, x3) → 3928_0_findR_FieldAccess(x2, x3)
Cond_3928_0_findR_FieldAccess(x1, x2, x3, x4) → Cond_3928_0_findR_FieldAccess(x1, x3, x4)
Cond_3928_0_findR_FieldAccess1(x1, x2, x3, x4) → Cond_3928_0_findR_FieldAccess1(x1, x3, x4)
4041_0_findR_Return(x1, x2, x3) → 4041_0_findR_Return(x3)
4044_0_findR_Return(x1, x2, x3) → 4044_0_findR_Return(x3)

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

P rules:
3928_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 4203_1_findR_InvokeMethod(3928_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3928_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 4204_1_findR_InvokeMethod(3928_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4382_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4044_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4382_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4385_0_findR_Return
4204_1_findR_InvokeMethod(4132_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4385_0_findR_Return
4203_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4377_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4203_1_findR_InvokeMethod(4044_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4377_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4203_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4379_0_findR_Return
4203_1_findR_InvokeMethod(4132_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4379_0_findR_Return
4204_1_findR_InvokeMethod(4377_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4581_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4379_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4581_0_findR_Return(NULL)
4204_1_findR_InvokeMethod(4382_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4581_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4385_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4581_0_findR_Return(NULL)
4204_1_findR_InvokeMethod(4581_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4581_0_findR_Return(x0)
4204_1_findR_InvokeMethod(4586_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4581_0_findR_Return(x0)
4203_1_findR_InvokeMethod(4382_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4586_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4203_1_findR_InvokeMethod(4385_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4586_0_findR_Return(NULL)
4203_1_findR_InvokeMethod(4581_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4586_0_findR_Return(x0)
4203_1_findR_InvokeMethod(4586_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4586_0_findR_Return(x0)
4203_1_findR_InvokeMethod(4377_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4586_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4203_1_findR_InvokeMethod(4379_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4586_0_findR_Return(NULL)

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_3928_0_findR_FieldAccess_3, Cond_3928_0_findR_FieldAccess1_3]=Cond_3928_0_findR_FieldAccess_3, [4204_1_findR_InvokeMethod_3, 4203_1_findR_InvokeMethod_3]=4204_1_findR_InvokeMethod_3, [4041_0_findR_Return_1, 4382_0_findR_Return_1, 4044_0_findR_Return_1, 4377_0_findR_Return_1]=4041_0_findR_Return_1, [4581_0_findR_Return_1, 4586_0_findR_Return_1]=4581_0_findR_Return_1, [4129_0_findR_Return, 4385_0_findR_Return, 4132_0_findR_Return, 4379_0_findR_Return]=4129_0_findR_Return}

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

P rules:
3928_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3928_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
COND_3928_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3928_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
R rules:
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4129_0_findR_Return
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4581_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4581_0_findR_Return(NULL)
4204_1_findR_InvokeMethod(4581_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4581_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:
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4129_0_findR_Return
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4581_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4581_0_findR_Return(NULL)
4204_1_findR_InvokeMethod(4581_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4581_0_findR_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3928_0_FINDR_FIELDACCESS(!(x0[0] = x2[0]), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
(1): COND_3928_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3928_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:
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
4204_1_findR_InvokeMethod(4581_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@5756231e 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 3928_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3928_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 3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3928_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3928_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3928_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]))) ⇒ 3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3928_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(U^Increasing(COND_3928_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 ⇒ 3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3928_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(U^Increasing(COND_3928_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_3928_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_3928_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_3928_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_3928_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_3928_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3928_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1)) the following chains were created:

We consider the chain 3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3928_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3928_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3928_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1])), 3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3928_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_3928_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥NonInfC∧COND_3928_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥3928_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))∧(U^Increasing(3928_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_3928_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_3928_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))))))≥3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))))∧(U^Increasing(3928_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(3928_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(3928_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(3928_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(3928_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.

3928_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3928_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
- (0 ≥ 0 ⇒ (U^Increasing(COND_3928_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_3928_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3928_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
- (0 ≥ 0 ⇒ (U^Increasing(3928_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(4204_1_findR_InvokeMethod(x₁, x₂, x₃)) = 0
POL(4041_0_findR_Return(x₁)) = 0
POL(java.lang.Object(x₁)) = [1] + [2]x₁
POL(DoublyLinkedList.DoublyLinkedList(x₁, x₂)) = [2]x₂
POL(4129_0_findR_Return) = 0
POL(NULL) = 0
POL(4581_0_findR_Return(x₁)) = 0
POL(3928_0_FINDR_FIELDACCESS(x₁, x₂)) = [1] + x₂ + [2]x₁
POL(COND_3928_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_>:

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

The following pairs are in P_bound:

3928_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3928_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
COND_3928_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3928_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:
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4129_0_findR_Return
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4581_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4581_0_findR_Return(NULL)
4204_1_findR_InvokeMethod(4581_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4581_0_findR_Return(x0)

The integer pair graph is empty.

The set Q consists of the following terms:
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
4204_1_findR_InvokeMethod(4041_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
4204_1_findR_InvokeMethod(4129_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
4204_1_findR_InvokeMethod(4581_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:
4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(o4219sub), java.lang.Object(o4219sub)) → 4272_0_getFirst_FieldAccess(EOS(STATIC_4272), java.lang.Object(o4219sub), java.lang.Object(o4219sub))
4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(o4219sub), java.lang.Object(o4219sub)) → 4273_0_getFirst_FieldAccess(EOS(STATIC_4273), java.lang.Object(o4219sub), java.lang.Object(o4219sub))
4272_0_getFirst_FieldAccess(EOS(STATIC_4272), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319))) → 4304_0_getFirst_FieldAccess(EOS(STATIC_4304), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319)))
4304_0_getFirst_FieldAccess(EOS(STATIC_4304), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319))) → 4365_0_getFirst_NONNULL(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4319)), o4319)
4365_0_getFirst_NONNULL(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub))), java.lang.Object(o4424sub)) → 4391_0_getFirst_NONNULL(EOS(STATIC_4391), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub))), java.lang.Object(o4424sub))
4391_0_getFirst_NONNULL(EOS(STATIC_4391), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub))), java.lang.Object(o4424sub)) → 4416_0_getFirst_Load(EOS(STATIC_4416), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub))))
4416_0_getFirst_Load(EOS(STATIC_4416), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub)))) → 4454_0_getFirst_FieldAccess(EOS(STATIC_4454), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub))))
4454_0_getFirst_FieldAccess(EOS(STATIC_4454), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4424sub)))) → 4566_0_getFirst_InvokeMethod(EOS(STATIC_4566), java.lang.Object(o4424sub))
4566_0_getFirst_InvokeMethod(EOS(STATIC_4566), java.lang.Object(o4424sub)) → 4592_1_getFirst_InvokeMethod(4592_0_getFirst_Load(EOS(STATIC_4592), java.lang.Object(o4424sub)), java.lang.Object(o4424sub))
4592_0_getFirst_Load(EOS(STATIC_4592), java.lang.Object(o4424sub)) → 4608_0_getFirst_Load(EOS(STATIC_4608), java.lang.Object(o4424sub))
4608_0_getFirst_Load(EOS(STATIC_4608), java.lang.Object(o4424sub)) → 4642_0_getFirst_Load(EOS(STATIC_4642), java.lang.Object(o4424sub))
4642_0_getFirst_Load(EOS(STATIC_4642), java.lang.Object(o4880sub)) → 4704_0_getFirst_Load(EOS(STATIC_4704), java.lang.Object(o4880sub))
4704_0_getFirst_Load(EOS(STATIC_4704), java.lang.Object(o4880sub)) → 4236_0_getFirst_Load(EOS(STATIC_4236), java.lang.Object(o4880sub))
4236_0_getFirst_Load(EOS(STATIC_4236), java.lang.Object(o4219sub)) → 4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(o4219sub), java.lang.Object(o4219sub))
4273_0_getFirst_FieldAccess(EOS(STATIC_4273), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322))) → 4305_0_getFirst_FieldAccess(EOS(STATIC_4305), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322)))
4305_0_getFirst_FieldAccess(EOS(STATIC_4305), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322))) → 4370_0_getFirst_NONNULL(EOS(STATIC_4370), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4322)), o4322)
4370_0_getFirst_NONNULL(EOS(STATIC_4370), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub))), java.lang.Object(o4425sub)) → 4393_0_getFirst_NONNULL(EOS(STATIC_4393), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub))), java.lang.Object(o4425sub))
4393_0_getFirst_NONNULL(EOS(STATIC_4393), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub))), java.lang.Object(o4425sub)) → 4418_0_getFirst_Load(EOS(STATIC_4418), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub))))
4418_0_getFirst_Load(EOS(STATIC_4418), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub)))) → 4457_0_getFirst_FieldAccess(EOS(STATIC_4457), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub))))
4457_0_getFirst_FieldAccess(EOS(STATIC_4457), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4425sub)))) → 4569_0_getFirst_InvokeMethod(EOS(STATIC_4569), java.lang.Object(o4425sub))
4569_0_getFirst_InvokeMethod(EOS(STATIC_4569), java.lang.Object(o4425sub)) → 4594_1_getFirst_InvokeMethod(4594_0_getFirst_Load(EOS(STATIC_4594), java.lang.Object(o4425sub)), java.lang.Object(o4425sub))
4594_0_getFirst_Load(EOS(STATIC_4594), java.lang.Object(o4425sub)) → 4611_0_getFirst_Load(EOS(STATIC_4611), java.lang.Object(o4425sub))
4611_0_getFirst_Load(EOS(STATIC_4611), java.lang.Object(o4425sub)) → 4706_0_getFirst_Load(EOS(STATIC_4706), java.lang.Object(o4425sub))
4706_0_getFirst_Load(EOS(STATIC_4706), java.lang.Object(o4425sub)) → 4236_0_getFirst_Load(EOS(STATIC_4236), java.lang.Object(o4425sub))
R rules:
4365_0_getFirst_NONNULL(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4392_0_getFirst_NONNULL(EOS(STATIC_4392), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
4370_0_getFirst_NONNULL(EOS(STATIC_4370), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4395_0_getFirst_NONNULL(EOS(STATIC_4395), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
4392_0_getFirst_NONNULL(EOS(STATIC_4392), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4417_0_getFirst_Load(EOS(STATIC_4417), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4395_0_getFirst_NONNULL(EOS(STATIC_4395), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4420_0_getFirst_Load(EOS(STATIC_4420), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4417_0_getFirst_Load(EOS(STATIC_4417), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4455_0_getFirst_Return(EOS(STATIC_4455), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4420_0_getFirst_Load(EOS(STATIC_4420), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4458_0_getFirst_Return(EOS(STATIC_4458), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4455_0_getFirst_Return(EOS(STATIC_4455), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4739_0_getFirst_Return(EOS(STATIC_4739), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4458_0_getFirst_Return(EOS(STATIC_4458), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4755_0_getFirst_Return(EOS(STATIC_4755), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4821_0_getFirst_Return(EOS(STATIC_4821), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4845_0_getFirst_Return(EOS(STATIC_4845), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(o5557sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5880))))))) → 5277_0_getFirst_Return(EOS(STATIC_5277), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5880)))))), java.lang.Object(o5557sub))
4592_1_getFirst_InvokeMethod(5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(o5647sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5920))))))) → 5338_0_getFirst_Return(EOS(STATIC_5338), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5920)))))), java.lang.Object(o5647sub))
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return(EOS(STATIC_4455), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4758_0_getFirst_Return(EOS(STATIC_4758), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(4458_0_getFirst_Return(EOS(STATIC_4458), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4765_0_getFirst_Return(EOS(STATIC_4765), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4823_0_getFirst_Return(EOS(STATIC_4823), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4852_0_getFirst_Return(EOS(STATIC_4852), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(o5557sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5889))))))) → 5286_0_getFirst_Return(EOS(STATIC_5286), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5889)))))), java.lang.Object(o5557sub))
4594_1_getFirst_InvokeMethod(5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(o5647sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5929))))))) → 5346_0_getFirst_Return(EOS(STATIC_5346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5929)))))), java.lang.Object(o5647sub))
4739_0_getFirst_Return(EOS(STATIC_4739), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4756_0_getFirst_Return(EOS(STATIC_4756), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4755_0_getFirst_Return(EOS(STATIC_4755), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4756_0_getFirst_Return(EOS(STATIC_4756), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4756_0_getFirst_Return(EOS(STATIC_4756), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4758_0_getFirst_Return(EOS(STATIC_4758), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4765_0_getFirst_Return(EOS(STATIC_4765), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4758_0_getFirst_Return(EOS(STATIC_4758), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4821_0_getFirst_Return(EOS(STATIC_4821), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4846_0_getFirst_Return(EOS(STATIC_4846), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4823_0_getFirst_Return(EOS(STATIC_4823), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 5087_0_getFirst_Return(EOS(STATIC_5087), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4845_0_getFirst_Return(EOS(STATIC_4845), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4846_0_getFirst_Return(EOS(STATIC_4846), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4846_0_getFirst_Return(EOS(STATIC_4846), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 5071_0_getFirst_Return(EOS(STATIC_5071), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4852_0_getFirst_Return(EOS(STATIC_4852), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4823_0_getFirst_Return(EOS(STATIC_4823), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
5071_0_getFirst_Return(EOS(STATIC_5071), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5489)))), java.lang.Object(o5492sub)) → 5156_0_getFirst_Return(EOS(STATIC_5156), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5489)))), java.lang.Object(o5492sub))
5087_0_getFirst_Return(EOS(STATIC_5087), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5554)))), java.lang.Object(o5557sub)) → 5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(o5557sub))
5156_0_getFirst_Return(EOS(STATIC_5156), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5644)))), java.lang.Object(o5647sub)) → 5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(o5647sub))
5277_0_getFirst_Return(EOS(STATIC_5277), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5880)))))), java.lang.Object(o5557sub)) → 5156_0_getFirst_Return(EOS(STATIC_5156), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5880)))))), java.lang.Object(o5557sub))
5286_0_getFirst_Return(EOS(STATIC_5286), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5889)))))), java.lang.Object(o5557sub)) → 5087_0_getFirst_Return(EOS(STATIC_5087), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5889)))))), java.lang.Object(o5557sub))
5338_0_getFirst_Return(EOS(STATIC_5338), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5920)))))), java.lang.Object(o5647sub)) → 5156_0_getFirst_Return(EOS(STATIC_5156), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5920)))))), java.lang.Object(o5647sub))
5346_0_getFirst_Return(EOS(STATIC_5346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5929)))))), java.lang.Object(o5647sub)) → 5087_0_getFirst_Return(EOS(STATIC_5087), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5929)))))), java.lang.Object(o5647sub))

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

P rules:
4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 4592_1_getFirst_InvokeMethod(4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 4594_1_getFirst_InvokeMethod(4254_0_getFirst_FieldAccess(EOS(STATIC_4254), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return(EOS(STATIC_4455), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(4458_0_getFirst_Return(EOS(STATIC_4458), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4455_0_getFirst_Return(EOS(STATIC_4455), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4458_0_getFirst_Return(EOS(STATIC_4458), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4594_1_getFirst_InvokeMethod(5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(x0))
4594_1_getFirst_InvokeMethod(5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(x0))
4592_1_getFirst_InvokeMethod(5186_0_getFirst_Return(EOS(STATIC_5186), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(x0))
4592_1_getFirst_InvokeMethod(5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(x0))
4592_1_getFirst_InvokeMethod(4774_0_getFirst_Return(EOS(STATIC_4774), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4592_1_getFirst_InvokeMethod(4779_0_getFirst_Return(EOS(STATIC_4779), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5198_0_getFirst_Return(EOS(STATIC_5198), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))

Filtered ground terms:

4254_0_getFirst_FieldAccess(x1, x2, x3) → 4254_0_getFirst_FieldAccess(x2, x3)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
5198_0_getFirst_Return(x1, x2) → 5198_0_getFirst_Return(x2)
4779_0_getFirst_Return(x1, x2) → 4779_0_getFirst_Return
4774_0_getFirst_Return(x1, x2) → 4774_0_getFirst_Return
5186_0_getFirst_Return(x1, x2) → 5186_0_getFirst_Return(x2)
4458_0_getFirst_Return(x1, x2, x3) → 4458_0_getFirst_Return
4455_0_getFirst_Return(x1, x2, x3) → 4455_0_getFirst_Return

Filtered duplicate args:

4254_0_getFirst_FieldAccess(x1, x2) → 4254_0_getFirst_FieldAccess(x2)

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

P rules:
4254_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 4592_1_getFirst_InvokeMethod(4254_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
4254_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 4594_1_getFirst_InvokeMethod(4254_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4779_0_getFirst_Return
4594_1_getFirst_InvokeMethod(4458_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4779_0_getFirst_Return
4592_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4774_0_getFirst_Return
4592_1_getFirst_InvokeMethod(4458_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4774_0_getFirst_Return
4594_1_getFirst_InvokeMethod(4774_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5186_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(4779_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5186_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(5186_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5186_0_getFirst_Return(java.lang.Object(x0))
4594_1_getFirst_InvokeMethod(5198_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5186_0_getFirst_Return(java.lang.Object(x0))
4592_1_getFirst_InvokeMethod(5186_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5198_0_getFirst_Return(java.lang.Object(x0))
4592_1_getFirst_InvokeMethod(5198_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5198_0_getFirst_Return(java.lang.Object(x0))
4592_1_getFirst_InvokeMethod(4774_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5198_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4592_1_getFirst_InvokeMethod(4779_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5198_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))

Performed bisimulation on rules. Used the following equivalence classes: {[4594_1_getFirst_InvokeMethod_2, 4592_1_getFirst_InvokeMethod_2]=4594_1_getFirst_InvokeMethod_2, [4455_0_getFirst_Return, 4779_0_getFirst_Return, 4458_0_getFirst_Return, 4774_0_getFirst_Return]=4455_0_getFirst_Return, [5186_0_getFirst_Return_1, 5198_0_getFirst_Return_1]=5186_0_getFirst_Return_1}

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

P rules:
4254_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 4254_0_GETFIRST_FIELDACCESS(java.lang.Object(x0))
R rules:
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4455_0_getFirst_Return
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5186_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(5186_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5186_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:
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4455_0_getFirst_Return
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5186_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(5186_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5186_0_getFirst_Return(java.lang.Object(x0))

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

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

The TRS R consists of the following rules:

4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4455_0_getFirst_Return
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5186_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(5186_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5186_0_getFirst_Return(java.lang.Object(x0))

The set Q consists of the following terms:

4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
4594_1_getFirst_InvokeMethod(5186_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:

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

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

4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
4594_1_getFirst_InvokeMethod(5186_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].

4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4594_1_getFirst_InvokeMethod(4455_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
4594_1_getFirst_InvokeMethod(5186_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:

4254_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 4254_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:

4254_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 4254_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:
3737_0_createList_Load(EOS(STATIC_3737(i2325)), i191, o3755, i2326, i2326) → 3746_0_createList_GE(EOS(STATIC_3746(i2325)), i191, o3755, i2326, i2326, i191)
3746_0_createList_GE(EOS(STATIC_3746(i2325)), i191, o3755, i2326, i2326, i191) → 3760_0_createList_GE(EOS(STATIC_3760(i2325)), i191, o3755, i2326, i2326, i191)
3760_0_createList_GE(EOS(STATIC_3760(i2325)), i191, o3755, i2326, i2326, i191) → 3774_0_createList_Load(EOS(STATIC_3774(i2325)), i191, o3755, i2326) | <(i2326, i191)
3774_0_createList_Load(EOS(STATIC_3774(i2325)), i191, o3755, i2326) → 3787_0_createList_Store(EOS(STATIC_3787(i2325)), i191, i2326, o3755)
3787_0_createList_Store(EOS(STATIC_3787(i2325)), i191, i2326, o3755) → 3799_0_createList_New(EOS(STATIC_3799(i2325)), i191, i2326, o3755)
3799_0_createList_New(EOS(STATIC_3799(i2325)), i191, i2326, o3755) → 3810_0_createList_Duplicate(EOS(STATIC_3810(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3810_0_createList_Duplicate(EOS(STATIC_3810(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3831_0_createList_InvokeMethod(EOS(STATIC_3831(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3831_0_createList_InvokeMethod(EOS(STATIC_3831(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3842_0_random_FieldAccess(EOS(STATIC_3842(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3842_0_random_FieldAccess(EOS(STATIC_3842(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3862_0_random_ArrayLength(EOS(STATIC_3862(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189)))
3862_0_random_ArrayLength(EOS(STATIC_3862(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189))) → 3868_0_random_FieldAccess(EOS(STATIC_3868(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189) | >=(i189, 0)
3868_0_random_FieldAccess(EOS(STATIC_3868(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189) → 3874_0_random_GT(EOS(STATIC_3874(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325)
3874_0_random_GT(EOS(STATIC_3874(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325) → 3884_0_random_GT(EOS(STATIC_3884(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325)
3874_0_random_GT(EOS(STATIC_3874(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325) → 3885_0_random_GT(EOS(STATIC_3885(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325)
3884_0_random_GT(EOS(STATIC_3884(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325) → 3896_0_random_FieldAccess(EOS(STATIC_3896(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | >(i189, i2325)
3896_0_random_FieldAccess(EOS(STATIC_3896(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3910_0_random_FieldAccess(EOS(STATIC_3910(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189)))
3910_0_random_FieldAccess(EOS(STATIC_3910(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189))) → 3922_0_random_ArrayAccess(EOS(STATIC_3922(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189)), i2325)
3922_0_random_ArrayAccess(EOS(STATIC_3922(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189)), i2325) → 3932_0_random_ArrayAccess(EOS(STATIC_3932(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189)), i2325)
3932_0_random_ArrayAccess(EOS(STATIC_3932(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i189)), i2325) → 3944_0_random_Store(EOS(STATIC_3944(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) | <(i2325, i189)
3944_0_random_Store(EOS(STATIC_3944(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) → 3959_0_random_FieldAccess(EOS(STATIC_3959(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937)
3959_0_random_FieldAccess(EOS(STATIC_3959(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) → 3974_0_random_ConstantStackPush(EOS(STATIC_3974(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2325)
3974_0_random_ConstantStackPush(EOS(STATIC_3974(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2325) → 3996_0_random_IntArithmetic(EOS(STATIC_3996(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2325, 1)
3996_0_random_IntArithmetic(EOS(STATIC_3996(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2325, matching1) → 4015_0_random_FieldAccess(EOS(STATIC_4015(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, +(i2325, 1)) | &&(>=(i2325, 0), =(matching1, 1))
4015_0_random_FieldAccess(EOS(STATIC_4015(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2408) → 4033_0_random_Load(EOS(STATIC_4033(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937)
4033_0_random_Load(EOS(STATIC_4033(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) → 4052_0_random_NONNULL(EOS(STATIC_4052(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, o3937)
4052_0_random_NONNULL(EOS(STATIC_4052(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub), java.lang.Object(o4052sub)) → 4072_0_random_NONNULL(EOS(STATIC_4072(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub), java.lang.Object(o4052sub))
4052_0_random_NONNULL(EOS(STATIC_4052(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 4073_0_random_NONNULL(EOS(STATIC_4073(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL)
4072_0_random_NONNULL(EOS(STATIC_4072(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub), java.lang.Object(o4052sub)) → 4089_0_random_Load(EOS(STATIC_4089(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub))
4089_0_random_Load(EOS(STATIC_4089(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub)) → 4111_0_random_InvokeMethod(EOS(STATIC_4111(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub))
4111_0_random_InvokeMethod(EOS(STATIC_4111(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub)) → 4138_0_length_Load(EOS(STATIC_4138(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub), java.lang.Object(o4052sub))
4138_0_length_Load(EOS(STATIC_4138(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub), java.lang.Object(o4052sub)) → 4196_0_length_FieldAccess(EOS(STATIC_4196(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4052sub), java.lang.Object(o4052sub))
4196_0_length_FieldAccess(EOS(STATIC_4196(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2486)), java.lang.Object(java.lang.String(o4184sub, i2486))) → 4213_0_length_FieldAccess(EOS(STATIC_4213(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2486)), java.lang.Object(java.lang.String(o4184sub, i2486))) | &&(>=(i2486, 0), >=(i2487, 0))
4213_0_length_FieldAccess(EOS(STATIC_4213(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2486)), java.lang.Object(java.lang.String(o4184sub, i2486))) → 4237_0_length_Return(EOS(STATIC_4237(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2486)), i2486)
4237_0_length_Return(EOS(STATIC_4237(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2486)), i2486) → 4256_0_random_Return(EOS(STATIC_4256(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486)
4256_0_random_Return(EOS(STATIC_4256(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486) → 4277_0_createList_InvokeMethod(EOS(STATIC_4277(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486)
4277_0_createList_InvokeMethod(EOS(STATIC_4277(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486) → 4308_0_<init>_Load(EOS(STATIC_4308(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486)
4308_0_<init>_Load(EOS(STATIC_4308(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486) → 4398_0_<init>_InvokeMethod(EOS(STATIC_4398(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4398_0_<init>_InvokeMethod(EOS(STATIC_4398(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4423_0_<init>_Load(EOS(STATIC_4423(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486)
4423_0_<init>_Load(EOS(STATIC_4423(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486) → 4461_0_<init>_Load(EOS(STATIC_4461(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4461_0_<init>_Load(EOS(STATIC_4461(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4573_0_<init>_FieldAccess(EOS(STATIC_4573(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486)
4573_0_<init>_FieldAccess(EOS(STATIC_4573(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486) → 4598_0_<init>_Return(EOS(STATIC_4598(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486)
4598_0_<init>_Return(EOS(STATIC_4598(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2486) → 4620_0_createList_Store(EOS(STATIC_4620(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4620_0_createList_Store(EOS(STATIC_4620(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4646_0_createList_Load(EOS(STATIC_4646(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755)
4646_0_createList_Load(EOS(STATIC_4646(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755) → 4710_0_createList_Load(EOS(STATIC_4710(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4710_0_createList_Load(EOS(STATIC_4710(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4731_0_createList_FieldAccess(EOS(STATIC_4731(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755)
4731_0_createList_FieldAccess(EOS(STATIC_4731(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755) → 4767_0_createList_Load(EOS(STATIC_4767(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755)
4767_0_createList_Load(EOS(STATIC_4767(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755) → 4780_0_createList_NULL(EOS(STATIC_4780(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, o3755)
4780_0_createList_NULL(EOS(STATIC_4780(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub), java.lang.Object(o5030sub)) → 4791_0_createList_NULL(EOS(STATIC_4791(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub), java.lang.Object(o5030sub))
4780_0_createList_NULL(EOS(STATIC_4780(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, NULL, NULL) → 4792_0_createList_NULL(EOS(STATIC_4792(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, NULL, NULL)
4791_0_createList_NULL(EOS(STATIC_4791(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub), java.lang.Object(o5030sub)) → 4812_0_createList_Load(EOS(STATIC_4812(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub))
4812_0_createList_Load(EOS(STATIC_4812(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub)) → 4854_0_createList_Load(EOS(STATIC_4854(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub))
4854_0_createList_Load(EOS(STATIC_4854(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub)) → 4891_0_createList_FieldAccess(EOS(STATIC_4891(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o5030sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4891_0_createList_FieldAccess(EOS(STATIC_4891(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4995_0_createList_FieldAccess(EOS(STATIC_4995(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4995_0_createList_FieldAccess(EOS(STATIC_4995(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 5023_0_createList_Inc(EOS(STATIC_5023(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326)
5023_0_createList_Inc(EOS(STATIC_5023(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326) → 5178_0_createList_JMP(EOS(STATIC_5178(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2326, 1))
5178_0_createList_JMP(EOS(STATIC_5178(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3235) → 5201_0_createList_Load(EOS(STATIC_5201(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3235)
5201_0_createList_Load(EOS(STATIC_5201(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3235) → 3724_0_createList_Load(EOS(STATIC_3724(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3235)
3724_0_createList_Load(EOS(STATIC_3724(i2325)), i191, o3755, i2326) → 3737_0_createList_Load(EOS(STATIC_3737(i2325)), i191, o3755, i2326, i2326)
4792_0_createList_NULL(EOS(STATIC_4792(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, NULL, NULL) → 4813_0_createList_Inc(EOS(STATIC_4813(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326)
4813_0_createList_Inc(EOS(STATIC_4813(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326) → 4855_0_createList_JMP(EOS(STATIC_4855(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2326, 1))
4855_0_createList_JMP(EOS(STATIC_4855(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2926) → 4893_0_createList_Load(EOS(STATIC_4893(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2926)
4893_0_createList_Load(EOS(STATIC_4893(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2926) → 3724_0_createList_Load(EOS(STATIC_3724(i2408)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2926)
4073_0_random_NONNULL(EOS(STATIC_4073(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 4091_0_random_ConstantStackPush(EOS(STATIC_4091(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL)
4091_0_random_ConstantStackPush(EOS(STATIC_4091(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL) → 4113_0_random_Return(EOS(STATIC_4113(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, 0)
4113_0_random_Return(EOS(STATIC_4113(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, matching1) → 4140_0_createList_InvokeMethod(EOS(STATIC_4140(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
4140_0_createList_InvokeMethod(EOS(STATIC_4140(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 4277_0_createList_InvokeMethod(EOS(STATIC_4277(i2408)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3885_0_random_GT(EOS(STATIC_3885(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i189, i2325) → 3898_0_random_ConstantStackPush(EOS(STATIC_3898(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | <=(i189, i2325)
3898_0_random_ConstantStackPush(EOS(STATIC_3898(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3912_0_random_Return(EOS(STATIC_3912(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0)
3912_0_random_Return(EOS(STATIC_3912(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3924_0_createList_InvokeMethod(EOS(STATIC_3924(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3924_0_createList_InvokeMethod(EOS(STATIC_3924(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3934_0_<init>_Load(EOS(STATIC_3934(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3934_0_<init>_Load(EOS(STATIC_3934(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3960_0_<init>_InvokeMethod(EOS(STATIC_3960(i2325)), i191, i2326, o3755, 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))
3960_0_<init>_InvokeMethod(EOS(STATIC_3960(i2325)), i191, i2326, o3755, 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))) → 3977_0_<init>_Load(EOS(STATIC_3977(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3977_0_<init>_Load(EOS(STATIC_3977(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3998_0_<init>_Load(EOS(STATIC_3998(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3998_0_<init>_Load(EOS(STATIC_3998(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4016_0_<init>_FieldAccess(EOS(STATIC_4016(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
4016_0_<init>_FieldAccess(EOS(STATIC_4016(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 4035_0_<init>_Return(EOS(STATIC_4035(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
4035_0_<init>_Return(EOS(STATIC_4035(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 4055_0_createList_Store(EOS(STATIC_4055(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | =(matching1, 0)
4055_0_createList_Store(EOS(STATIC_4055(i2325)), i191, i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4075_0_createList_Load(EOS(STATIC_4075(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755)
4075_0_createList_Load(EOS(STATIC_4075(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755) → 4093_0_createList_Load(EOS(STATIC_4093(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4093_0_createList_Load(EOS(STATIC_4093(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4115_0_createList_FieldAccess(EOS(STATIC_4115(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755)
4115_0_createList_FieldAccess(EOS(STATIC_4115(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755) → 4142_0_createList_Load(EOS(STATIC_4142(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755)
4142_0_createList_Load(EOS(STATIC_4142(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755) → 4179_0_createList_NULL(EOS(STATIC_4179(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, o3755, o3755)
4179_0_createList_NULL(EOS(STATIC_4179(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub), java.lang.Object(o4180sub)) → 4198_0_createList_NULL(EOS(STATIC_4198(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub), java.lang.Object(o4180sub))
4179_0_createList_NULL(EOS(STATIC_4179(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, NULL, NULL) → 4199_0_createList_NULL(EOS(STATIC_4199(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, NULL, NULL)
4198_0_createList_NULL(EOS(STATIC_4198(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub), java.lang.Object(o4180sub)) → 4216_0_createList_Load(EOS(STATIC_4216(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub))
4216_0_createList_Load(EOS(STATIC_4216(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub)) → 4242_0_createList_Load(EOS(STATIC_4242(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub))
4242_0_createList_Load(EOS(STATIC_4242(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub)) → 4261_0_createList_FieldAccess(EOS(STATIC_4261(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(o4180sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4261_0_createList_FieldAccess(EOS(STATIC_4261(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4279_0_createList_FieldAccess(EOS(STATIC_4279(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4279_0_createList_FieldAccess(EOS(STATIC_4279(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4316_0_createList_Inc(EOS(STATIC_4316(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326)
4316_0_createList_Inc(EOS(STATIC_4316(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326) → 4376_0_createList_JMP(EOS(STATIC_4376(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2326, 1))
4376_0_createList_JMP(EOS(STATIC_4376(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2623) → 4404_0_createList_Load(EOS(STATIC_4404(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2623)
4404_0_createList_Load(EOS(STATIC_4404(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2623) → 3724_0_createList_Load(EOS(STATIC_3724(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2623)
4199_0_createList_NULL(EOS(STATIC_4199(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326, NULL, NULL) → 4217_0_createList_Inc(EOS(STATIC_4217(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326)
4217_0_createList_Inc(EOS(STATIC_4217(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2326) → 4243_0_createList_JMP(EOS(STATIC_4243(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2326, 1))
4243_0_createList_JMP(EOS(STATIC_4243(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2517) → 4262_0_createList_Load(EOS(STATIC_4262(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2517)
4262_0_createList_Load(EOS(STATIC_4262(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2517) → 3724_0_createList_Load(EOS(STATIC_3724(i2325)), i191, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2517)
R rules:

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

P rules:
3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, x2, x3, x3) → 4780_0_createList_NULL(EOS(STATIC_4780(+(x0, 1))), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x3, x2, x2) | &&(<(x3, x1), >(+(x0, 1), 0))
4780_0_createList_NULL(EOS(STATIC_4780(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
4780_0_createList_NULL(EOS(STATIC_4780(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, NULL, NULL) → 3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, x2) → 3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, NULL, x2, x2) → 3737_0_createList_Load(EOS(STATIC_3737(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_3737_0_createList_Load2(x1, x2, x3, x4, x5, x6) → Cond_3737_0_createList_Load2(x1, x2, x3, x5, x6)
Cond_3737_0_createList_Load1(x1, x2, x3, x4, x5, x6) → Cond_3737_0_createList_Load1(x1, x2, x3, x5, x6)
4780_0_createList_NULL(x1, x2, x3, x4, x5, x6) → 4780_0_createList_NULL(x1, x2, x4, x5, x6)

Filtered duplicate args:

3737_0_createList_Load(x1, x2, x3, x4, x5) → 3737_0_createList_Load(x1, x2, x3, x5)
Cond_3737_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_3737_0_createList_Load(x1, x2, x3, x4, x6)
4780_0_createList_NULL(x1, x2, x3, x4, x5) → 4780_0_createList_NULL(x1, x2, x3, x5)
Cond_3737_0_createList_Load1(x1, x2, x3, x4, x5) → Cond_3737_0_createList_Load1(x1, x2, x3, x5)
Cond_3737_0_createList_Load2(x1, x2, x3, x4, x5) → Cond_3737_0_createList_Load2(x1, x2, x3, x5)

Filtered all non-integer terms:

4780_0_createList_NULL(x1, x2, x3, x4) → 4780_0_createList_NULL(x1, x2, x3)
3737_0_createList_Load(x1, x2, x3, x4) → 3737_0_createList_Load(x1, x2, x4)

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

P rules:
3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, x2) → 3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, +(x2, 1)) | <(x2, x1)
3737_0_createList_Load(EOS(STATIC_3737(x0)), x1, x2) → 3737_0_createList_Load(EOS(STATIC_3737(+(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:
3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0)), x1, x2) → COND_3737_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3737(x0)), x1, x2)
COND_3737_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3737(x0)), x1, x2) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0)), x1, +(x2, 1))
3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0)), x1, x2) → COND_3737_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3737(x0)), x1, x2)
COND_3737_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3737(x0)), x1, x2) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(+(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): 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[0])), x1[0], x2[0]) → COND_3737_0_CREATELIST_LOAD(x2[0] < x1[0], EOS(STATIC_3737(x0[0])), x1[0], x2[0])
(1): COND_3737_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3737(x0[1])), x1[1], x2[1]) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[1])), x1[1], x2[1] + 1)
(2): 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[2])), x1[2], x2[2]) → COND_3737_0_CREATELIST_LOAD1(x2[2] < x1[2] && x0[2] > -1, EOS(STATIC_3737(x0[2])), x1[2], x2[2])
(3): COND_3737_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3737(x0[3])), x1[3], x2[3]) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[3] + 1)), x1[3], x2[3] + 1)

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

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

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

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

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

(3) -> (2), if (EOS(STATIC_3737(x0[3] + 1)) →^* EOS(STATIC_3737(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@604f05f8 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 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0)), x1, x2) → COND_3737_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3737(x0)), x1, x2) the following chains were created:

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

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

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

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

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

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

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

For Pair COND_3737_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3737(x0)), x1, x2) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0)), x1, +(x2, 1)) the following chains were created:

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

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

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

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

For Pair 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0)), x1, x2) → COND_3737_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3737(x0)), x1, x2) the following chains were created:

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

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

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

3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[0])), x1[0], x2[0]) → COND_3737_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3737(x0[0])), x1[0], x2[0])
3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[2])), x1[2], x2[2]) → COND_3737_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3737(x0[2])), x1[2], x2[2])

The following pairs are in P_bound:

3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[0])), x1[0], x2[0]) → COND_3737_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3737(x0[0])), x1[0], x2[0])
3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[2])), x1[2], x2[2]) → COND_3737_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3737(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

COND_3737_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3737(x0[1])), x1[1], x2[1]) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[1])), x1[1], +(x2[1], 1))
COND_3737_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3737(x0[3])), x1[3], x2[3]) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(+(x0[3], 1))), x1[3], +(x2[3], 1))

There are no usable rules.

(27) 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_3737_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3737(x0[1])), x1[1], x2[1]) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[1])), x1[1], x2[1] + 1)
(3): COND_3737_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3737(x0[3])), x1[3], x2[3]) → 3737_0_CREATELIST_LOAD(EOS(STATIC_3737(x0[3] + 1)), x1[3], x2[3] + 1)

The set Q is empty.

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

(28) IDependencyGraphProof (EQUIVALENT transformation)

(29) TRUE