Termination proof of /tmp/tmpdZu8hK/MainDelete.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 3560 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 980 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 320 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 480 ms)

        ↳14 IDP

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

        ↳25 IDP

        ↳26 IDPNonInfProof (⇒, 350 ms)

        ↳27 AND

            ↳28 IDP

                ↳29 IDependencyGraphProof (⇔, 0 ms)

                ↳30 TRUE

            ↳31 IDP

                ↳32 IDependencyGraphProof (⇔, 0 ms)

                ↳33 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_14 (Sun Microsystems Inc.) Main-Class: DoublyLinkedList/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:
3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(o3926sub), i2306, java.lang.Object(o3926sub)) → 3976_0_findR_FieldAccess(EOS(STATIC_3976), java.lang.Object(o3926sub), i2306, java.lang.Object(o3926sub))
3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(o3926sub), i2306, java.lang.Object(o3926sub)) → 3977_0_findR_FieldAccess(EOS(STATIC_3977), java.lang.Object(o3926sub), i2306, java.lang.Object(o3926sub))
3976_0_findR_FieldAccess(EOS(STATIC_3976), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955))) → 3991_0_findR_FieldAccess(EOS(STATIC_3991), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)))
3991_0_findR_FieldAccess(EOS(STATIC_3991), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955))) → 4004_0_findR_Load(EOS(STATIC_4004), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, i2389)
4004_0_findR_Load(EOS(STATIC_4004), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, i2389) → 4021_0_findR_NE(EOS(STATIC_4021), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, i2389, i2306)
4021_0_findR_NE(EOS(STATIC_4021), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, i2389, i2306) → 4043_0_findR_NE(EOS(STATIC_4043), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, i2389, i2306)
4043_0_findR_NE(EOS(STATIC_4043), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, i2389, i2306) → 4060_0_findR_Load(EOS(STATIC_4060), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306) | !(=(i2389, i2306))
4060_0_findR_Load(EOS(STATIC_4060), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306) → 4076_0_findR_FieldAccess(EOS(STATIC_4076), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)))
4076_0_findR_FieldAccess(EOS(STATIC_4076), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955))) → 4096_0_findR_NULL(EOS(STATIC_4096), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, o3955)), i2306, o3955)
4096_0_findR_NULL(EOS(STATIC_4096), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub))), i2306, java.lang.Object(o4060sub)) → 4120_0_findR_NULL(EOS(STATIC_4120), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub))), i2306, java.lang.Object(o4060sub))
4120_0_findR_NULL(EOS(STATIC_4120), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub))), i2306, java.lang.Object(o4060sub)) → 4138_0_findR_Load(EOS(STATIC_4138), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub))), i2306)
4138_0_findR_Load(EOS(STATIC_4138), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub))), i2306) → 4167_0_findR_FieldAccess(EOS(STATIC_4167), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub))))
4167_0_findR_FieldAccess(EOS(STATIC_4167), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, java.lang.Object(o4060sub)))) → 4202_0_findR_Load(EOS(STATIC_4202), i2306, java.lang.Object(o4060sub))
4202_0_findR_Load(EOS(STATIC_4202), i2306, java.lang.Object(o4060sub)) → 4221_0_findR_InvokeMethod(EOS(STATIC_4221), java.lang.Object(o4060sub), i2306)
4221_0_findR_InvokeMethod(EOS(STATIC_4221), java.lang.Object(o4060sub), i2306) → 4239_1_findR_InvokeMethod(4239_0_findR_Load(EOS(STATIC_4239), java.lang.Object(o4060sub), i2306), java.lang.Object(o4060sub), i2306)
4239_0_findR_Load(EOS(STATIC_4239), java.lang.Object(o4060sub), i2306) → 4260_0_findR_Load(EOS(STATIC_4260), java.lang.Object(o4060sub), i2306)
4260_0_findR_Load(EOS(STATIC_4260), java.lang.Object(o4060sub), i2306) → 4284_0_findR_Load(EOS(STATIC_4284), java.lang.Object(o4060sub), i2306)
4284_0_findR_Load(EOS(STATIC_4284), java.lang.Object(o4227sub), i2306) → 4300_0_findR_Load(EOS(STATIC_4300), java.lang.Object(o4227sub), i2306)
4300_0_findR_Load(EOS(STATIC_4300), java.lang.Object(o4227sub), i2306) → 3956_0_findR_Load(EOS(STATIC_3956), java.lang.Object(o4227sub), i2306)
3956_0_findR_Load(EOS(STATIC_3956), java.lang.Object(o3926sub), i2306) → 3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(o3926sub), i2306, java.lang.Object(o3926sub))
3977_0_findR_FieldAccess(EOS(STATIC_3977), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958))) → 3992_0_findR_FieldAccess(EOS(STATIC_3992), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)))
3992_0_findR_FieldAccess(EOS(STATIC_3992), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958))) → 4005_0_findR_Load(EOS(STATIC_4005), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, i2390)
4005_0_findR_Load(EOS(STATIC_4005), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, i2390) → 4026_0_findR_NE(EOS(STATIC_4026), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, i2390, i2306)
4026_0_findR_NE(EOS(STATIC_4026), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, i2390, i2306) → 4045_0_findR_NE(EOS(STATIC_4045), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, i2390, i2306)
4045_0_findR_NE(EOS(STATIC_4045), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, i2390, i2306) → 4063_0_findR_Load(EOS(STATIC_4063), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306) | !(=(i2390, i2306))
4063_0_findR_Load(EOS(STATIC_4063), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306) → 4079_0_findR_FieldAccess(EOS(STATIC_4079), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)))
4079_0_findR_FieldAccess(EOS(STATIC_4079), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958))) → 4102_0_findR_NULL(EOS(STATIC_4102), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, o3958)), i2306, o3958)
4102_0_findR_NULL(EOS(STATIC_4102), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub))), i2306, java.lang.Object(o4061sub)) → 4122_0_findR_NULL(EOS(STATIC_4122), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub))), i2306, java.lang.Object(o4061sub))
4122_0_findR_NULL(EOS(STATIC_4122), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub))), i2306, java.lang.Object(o4061sub)) → 4140_0_findR_Load(EOS(STATIC_4140), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub))), i2306)
4140_0_findR_Load(EOS(STATIC_4140), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub))), i2306) → 4169_0_findR_FieldAccess(EOS(STATIC_4169), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub))))
4169_0_findR_FieldAccess(EOS(STATIC_4169), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, java.lang.Object(o4061sub)))) → 4205_0_findR_Load(EOS(STATIC_4205), i2306, java.lang.Object(o4061sub))
4205_0_findR_Load(EOS(STATIC_4205), i2306, java.lang.Object(o4061sub)) → 4223_0_findR_InvokeMethod(EOS(STATIC_4223), java.lang.Object(o4061sub), i2306)
4223_0_findR_InvokeMethod(EOS(STATIC_4223), java.lang.Object(o4061sub), i2306) → 4240_1_findR_InvokeMethod(4240_0_findR_Load(EOS(STATIC_4240), java.lang.Object(o4061sub), i2306), java.lang.Object(o4061sub), i2306)
4240_0_findR_Load(EOS(STATIC_4240), java.lang.Object(o4061sub), i2306) → 4261_0_findR_Load(EOS(STATIC_4261), java.lang.Object(o4061sub), i2306)
4261_0_findR_Load(EOS(STATIC_4261), java.lang.Object(o4061sub), i2306) → 4303_0_findR_Load(EOS(STATIC_4303), java.lang.Object(o4061sub), i2306)
4303_0_findR_Load(EOS(STATIC_4303), java.lang.Object(o4061sub), i2306) → 3956_0_findR_Load(EOS(STATIC_3956), java.lang.Object(o4061sub), i2306)
R rules:
4021_0_findR_NE(EOS(STATIC_4021), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)), i2306, i2306, i2306) → 4044_0_findR_NE(EOS(STATIC_4044), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)), i2306, i2306, i2306)
4026_0_findR_NE(EOS(STATIC_4026), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)), i2306, i2306, i2306) → 4046_0_findR_NE(EOS(STATIC_4046), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)), i2306, i2306, i2306)
4044_0_findR_NE(EOS(STATIC_4044), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)), i2306, i2306, i2306) → 4061_0_findR_Load(EOS(STATIC_4061), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)), i2306)
4046_0_findR_NE(EOS(STATIC_4046), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)), i2306, i2306, i2306) → 4064_0_findR_Load(EOS(STATIC_4064), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)), i2306)
4061_0_findR_Load(EOS(STATIC_4061), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)), i2306) → 4078_0_findR_Return(EOS(STATIC_4078), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3955)))
4064_0_findR_Load(EOS(STATIC_4064), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)), i2306) → 4081_0_findR_Return(EOS(STATIC_4081), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)), i2306, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2306, o3958)))
4096_0_findR_NULL(EOS(STATIC_4096), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, NULL)), i2306, NULL) → 4121_0_findR_NULL(EOS(STATIC_4121), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, NULL)), i2306, NULL)
4102_0_findR_NULL(EOS(STATIC_4102), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, NULL)), i2306, NULL) → 4123_0_findR_NULL(EOS(STATIC_4123), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, NULL)), i2306, NULL)
4121_0_findR_NULL(EOS(STATIC_4121), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2389, NULL)), i2306, NULL) → 4139_0_findR_ConstantStackPush(EOS(STATIC_4139))
4123_0_findR_NULL(EOS(STATIC_4123), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2390, NULL)), i2306, NULL) → 4142_0_findR_ConstantStackPush(EOS(STATIC_4142))
4139_0_findR_ConstantStackPush(EOS(STATIC_4139)) → 4168_0_findR_Return(EOS(STATIC_4168), NULL)
4142_0_findR_ConstantStackPush(EOS(STATIC_4142)) → 4171_0_findR_Return(EOS(STATIC_4171), NULL)
4239_1_findR_InvokeMethod(4078_0_findR_Return(EOS(STATIC_4078), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540) → 4347_0_findR_Return(EOS(STATIC_4347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)))
4239_1_findR_InvokeMethod(4081_0_findR_Return(EOS(STATIC_4081), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547) → 4363_0_findR_Return(EOS(STATIC_4363), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)))
4239_1_findR_InvokeMethod(4168_0_findR_Return(EOS(STATIC_4168), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2554, NULL)), i2555) → 4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2554, NULL)), i2555, NULL)
4239_1_findR_InvokeMethod(4171_0_findR_Return(EOS(STATIC_4171), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2561, NULL)), i2562) → 4373_0_findR_Return(EOS(STATIC_4373), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2561, NULL)), i2562, NULL)
4239_1_findR_InvokeMethod(4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451)))), i2642) → 4487_0_findR_Return(EOS(STATIC_4487), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451)))), i2642, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451)))
4239_1_findR_InvokeMethod(4409_0_findR_Return(EOS(STATIC_4409), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2652, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, NULL)))), i2653) → 4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2652, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, NULL)))), i2653, NULL)
4239_1_findR_InvokeMethod(4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476)))), i2663) → 4548_0_findR_Return(EOS(STATIC_4548), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476)))), i2663, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476)))
4239_1_findR_InvokeMethod(4417_0_findR_Return(EOS(STATIC_4417), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2673, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, NULL)))), i2674) → 4568_0_findR_Return(EOS(STATIC_4568), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2673, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, NULL)))), i2674, NULL)
4239_1_findR_InvokeMethod(4599_0_findR_Return(EOS(STATIC_4599), o4555), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2784, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2783, o4846)))))), i2786) → 4684_0_findR_Return(EOS(STATIC_4684), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2784, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2783, o4846)))))), i2786, o4555)
4239_1_findR_InvokeMethod(4604_0_findR_Return(EOS(STATIC_4604), o4594), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2798, o4863)))))), i2801) → 4708_0_findR_Return(EOS(STATIC_4708), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2798, o4863)))))), i2801, o4594)
4240_1_findR_InvokeMethod(4078_0_findR_Return(EOS(STATIC_4078), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)), i2569, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)), i2569) → 4375_0_findR_Return(EOS(STATIC_4375), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)), i2569, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)), i2569, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)))
4240_1_findR_InvokeMethod(4081_0_findR_Return(EOS(STATIC_4081), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576) → 4384_0_findR_Return(EOS(STATIC_4384), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)))
4240_1_findR_InvokeMethod(4168_0_findR_Return(EOS(STATIC_4168), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, NULL)), i2583) → 4385_0_findR_Return(EOS(STATIC_4385), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, NULL)), i2583, NULL)
4240_1_findR_InvokeMethod(4171_0_findR_Return(EOS(STATIC_4171), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2590, NULL)), i2591) → 4389_0_findR_Return(EOS(STATIC_4389), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2590, NULL)), i2591, NULL)
4240_1_findR_InvokeMethod(4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458)))), i2647) → 4488_0_findR_Return(EOS(STATIC_4488), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458)))), i2647, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458)))
4240_1_findR_InvokeMethod(4409_0_findR_Return(EOS(STATIC_4409), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2657, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, NULL)))), i2658) → 4516_0_findR_Return(EOS(STATIC_4516), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2657, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, NULL)))), i2658, NULL)
4240_1_findR_InvokeMethod(4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486)))), i2669) → 4559_0_findR_Return(EOS(STATIC_4559), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486)))), i2669, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486)))
4240_1_findR_InvokeMethod(4417_0_findR_Return(EOS(STATIC_4417), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2680, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2679, NULL)))), i2681) → 4575_0_findR_Return(EOS(STATIC_4575), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2680, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2679, NULL)))), i2681, NULL)
4240_1_findR_InvokeMethod(4599_0_findR_Return(EOS(STATIC_4599), o4555), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2792, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2791, o4855)))))), i2794) → 4694_0_findR_Return(EOS(STATIC_4694), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2792, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2791, o4855)))))), i2794, o4555)
4240_1_findR_InvokeMethod(4604_0_findR_Return(EOS(STATIC_4604), o4594), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2806, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2805, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2804, o4872)))))), i2807) → 4719_0_findR_Return(EOS(STATIC_4719), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2806, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2805, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2804, o4872)))))), i2807, o4594)
4347_0_findR_Return(EOS(STATIC_4347), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262))) → 4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)), i2540, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2540, o4262)))
4363_0_findR_Return(EOS(STATIC_4363), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269))) → 4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)), i2547, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2547, o4269)))
4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, o4331)), i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, o4331)), i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, o4331))) → 4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, o4331)))
4365_0_findR_Return(EOS(STATIC_4365), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2554, NULL)), i2555, NULL) → 4374_0_findR_Return(EOS(STATIC_4374), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2554, NULL)), i2555, NULL)
4373_0_findR_Return(EOS(STATIC_4373), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2561, NULL)), i2562, NULL) → 4374_0_findR_Return(EOS(STATIC_4374), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2561, NULL)), i2562, NULL)
4374_0_findR_Return(EOS(STATIC_4374), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2607, NULL)), i2608, NULL) → 4409_0_findR_Return(EOS(STATIC_4409), NULL)
4375_0_findR_Return(EOS(STATIC_4375), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)), i2569, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)), i2569, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295))) → 4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2569, o4295)))
4384_0_findR_Return(EOS(STATIC_4384), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303))) → 4375_0_findR_Return(EOS(STATIC_4375), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)), i2576, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2576, o4303)))
4385_0_findR_Return(EOS(STATIC_4385), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, NULL)), i2583, NULL) → 4417_0_findR_Return(EOS(STATIC_4417), NULL)
4389_0_findR_Return(EOS(STATIC_4389), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2590, NULL)), i2591, NULL) → 4385_0_findR_Return(EOS(STATIC_4385), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2590, NULL)), i2591, NULL)
4487_0_findR_Return(EOS(STATIC_4487), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451)))), i2642, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451))) → 4502_0_findR_Return(EOS(STATIC_4502), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2641, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451)))), i2642, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2642, o4451)))
4488_0_findR_Return(EOS(STATIC_4488), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458)))), i2647, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458))) → 4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2646, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458)))), i2647, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2647, o4458)))
4501_0_findR_Return(EOS(STATIC_4501), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2652, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, NULL)))), i2653, NULL) → 4502_0_findR_Return(EOS(STATIC_4502), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2652, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2651, NULL)))), i2653, NULL)
4502_0_findR_Return(EOS(STATIC_4502), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2687, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2686, o4522)))), i2688, o4528) → 4549_0_findR_Return(EOS(STATIC_4549), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2687, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2686, o4522)))), i2688, o4528)
4516_0_findR_Return(EOS(STATIC_4516), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2657, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, NULL)))), i2658, NULL) → 4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2657, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2656, NULL)))), i2658, NULL)
4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2692, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2691, o4549)))), i2693, o4555) → 4599_0_findR_Return(EOS(STATIC_4599), o4555)
4548_0_findR_Return(EOS(STATIC_4548), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476)))), i2663, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476))) → 4549_0_findR_Return(EOS(STATIC_4549), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2662, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476)))), i2663, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2663, o4476)))
4549_0_findR_Return(EOS(STATIC_4549), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2704, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2703, o4588)))), i2705, o4594) → 4604_0_findR_Return(EOS(STATIC_4604), o4594)
4559_0_findR_Return(EOS(STATIC_4559), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486)))), i2669, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486))) → 4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2668, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486)))), i2669, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2669, o4486)))
4568_0_findR_Return(EOS(STATIC_4568), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2673, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, NULL)))), i2674, NULL) → 4549_0_findR_Return(EOS(STATIC_4549), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2673, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2672, NULL)))), i2674, NULL)
4575_0_findR_Return(EOS(STATIC_4575), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2680, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2679, NULL)))), i2681, NULL) → 4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2680, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2679, NULL)))), i2681, NULL)
4684_0_findR_Return(EOS(STATIC_4684), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2784, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2783, o4846)))))), i2786, o4555) → 4549_0_findR_Return(EOS(STATIC_4549), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2784, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2783, o4846)))))), i2786, o4555)
4694_0_findR_Return(EOS(STATIC_4694), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2792, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2791, o4855)))))), i2794, o4555) → 4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2793, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2792, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2791, o4855)))))), i2794, o4555)
4708_0_findR_Return(EOS(STATIC_4708), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2798, o4863)))))), i2801, o4594) → 4549_0_findR_Return(EOS(STATIC_4549), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2800, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2799, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2798, o4863)))))), i2801, o4594)
4719_0_findR_Return(EOS(STATIC_4719), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2806, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2805, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2804, o4872)))))), i2807, o4594) → 4517_0_findR_Return(EOS(STATIC_4517), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2806, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2805, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2804, o4872)))))), i2807, o4594)

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

P rules:
3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 4239_1_findR_InvokeMethod(3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 4240_1_findR_InvokeMethod(3966_0_findR_FieldAccess(EOS(STATIC_3966), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
4240_1_findR_InvokeMethod(4078_0_findR_Return(EOS(STATIC_4078), 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) → 4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4240_1_findR_InvokeMethod(4081_0_findR_Return(EOS(STATIC_4081), 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) → 4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return(EOS(STATIC_4168), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4417_0_findR_Return(EOS(STATIC_4417), NULL)
4240_1_findR_InvokeMethod(4171_0_findR_Return(EOS(STATIC_4171), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4417_0_findR_Return(EOS(STATIC_4417), NULL)
4239_1_findR_InvokeMethod(4078_0_findR_Return(EOS(STATIC_4078), 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) → 4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4239_1_findR_InvokeMethod(4081_0_findR_Return(EOS(STATIC_4081), 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) → 4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4239_1_findR_InvokeMethod(4168_0_findR_Return(EOS(STATIC_4168), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4409_0_findR_Return(EOS(STATIC_4409), NULL)
4239_1_findR_InvokeMethod(4171_0_findR_Return(EOS(STATIC_4171), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4409_0_findR_Return(EOS(STATIC_4409), NULL)
4240_1_findR_InvokeMethod(4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4599_0_findR_Return(EOS(STATIC_4599), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4240_1_findR_InvokeMethod(4409_0_findR_Return(EOS(STATIC_4409), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4599_0_findR_Return(EOS(STATIC_4599), NULL)
4240_1_findR_InvokeMethod(4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4599_0_findR_Return(EOS(STATIC_4599), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4240_1_findR_InvokeMethod(4417_0_findR_Return(EOS(STATIC_4417), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4599_0_findR_Return(EOS(STATIC_4599), NULL)
4240_1_findR_InvokeMethod(4599_0_findR_Return(EOS(STATIC_4599), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4599_0_findR_Return(EOS(STATIC_4599), x0)
4240_1_findR_InvokeMethod(4604_0_findR_Return(EOS(STATIC_4604), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4599_0_findR_Return(EOS(STATIC_4599), x0)
4239_1_findR_InvokeMethod(4413_0_findR_Return(EOS(STATIC_4413), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4604_0_findR_Return(EOS(STATIC_4604), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4239_1_findR_InvokeMethod(4417_0_findR_Return(EOS(STATIC_4417), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4604_0_findR_Return(EOS(STATIC_4604), NULL)
4239_1_findR_InvokeMethod(4599_0_findR_Return(EOS(STATIC_4599), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4604_0_findR_Return(EOS(STATIC_4604), x0)
4239_1_findR_InvokeMethod(4604_0_findR_Return(EOS(STATIC_4604), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4604_0_findR_Return(EOS(STATIC_4604), x0)
4239_1_findR_InvokeMethod(4408_0_findR_Return(EOS(STATIC_4408), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4604_0_findR_Return(EOS(STATIC_4604), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
4239_1_findR_InvokeMethod(4409_0_findR_Return(EOS(STATIC_4409), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4604_0_findR_Return(EOS(STATIC_4604), NULL)

Filtered ground terms:

3966_0_findR_FieldAccess(x1, x2, x3, x4) → 3966_0_findR_FieldAccess(x2, x3, x4)
Cond_3966_0_findR_FieldAccess1(x1, x2, x3, x4, x5) → Cond_3966_0_findR_FieldAccess1(x1, x3, x4, x5)
DoublyLinkedList.DoublyLinkedList(x1, x2, x3) → DoublyLinkedList.DoublyLinkedList(x2, x3)
Cond_3966_0_findR_FieldAccess(x1, x2, x3, x4, x5) → Cond_3966_0_findR_FieldAccess(x1, x3, x4, x5)
4604_0_findR_Return(x1, x2) → 4604_0_findR_Return(x2)
4409_0_findR_Return(x1, x2) → 4409_0_findR_Return
4408_0_findR_Return(x1, x2) → 4408_0_findR_Return(x2)
4599_0_findR_Return(x1, x2) → 4599_0_findR_Return(x2)
4417_0_findR_Return(x1, x2) → 4417_0_findR_Return
4413_0_findR_Return(x1, x2) → 4413_0_findR_Return(x2)
4171_0_findR_Return(x1, x2) → 4171_0_findR_Return
4168_0_findR_Return(x1, x2) → 4168_0_findR_Return
4081_0_findR_Return(x1, x2, x3, x4) → 4081_0_findR_Return(x2, x3, x4)
4078_0_findR_Return(x1, x2, x3, x4) → 4078_0_findR_Return(x2, x3, x4)

Filtered duplicate args:

3966_0_findR_FieldAccess(x1, x2, x3) → 3966_0_findR_FieldAccess(x2, x3)
Cond_3966_0_findR_FieldAccess(x1, x2, x3, x4) → Cond_3966_0_findR_FieldAccess(x1, x3, x4)
Cond_3966_0_findR_FieldAccess1(x1, x2, x3, x4) → Cond_3966_0_findR_FieldAccess1(x1, x3, x4)
4078_0_findR_Return(x1, x2, x3) → 4078_0_findR_Return(x3)
4081_0_findR_Return(x1, x2, x3) → 4081_0_findR_Return(x3)

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

P rules:
3966_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 4239_1_findR_InvokeMethod(3966_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3966_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 4240_1_findR_InvokeMethod(3966_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4413_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4081_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4413_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4417_0_findR_Return
4240_1_findR_InvokeMethod(4171_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4417_0_findR_Return
4239_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4408_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4239_1_findR_InvokeMethod(4081_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4408_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4239_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4409_0_findR_Return
4239_1_findR_InvokeMethod(4171_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4409_0_findR_Return
4240_1_findR_InvokeMethod(4408_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4599_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4409_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4599_0_findR_Return(NULL)
4240_1_findR_InvokeMethod(4413_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4599_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4417_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4599_0_findR_Return(NULL)
4240_1_findR_InvokeMethod(4599_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4599_0_findR_Return(x0)
4240_1_findR_InvokeMethod(4604_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4599_0_findR_Return(x0)
4239_1_findR_InvokeMethod(4413_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4604_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4239_1_findR_InvokeMethod(4417_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4604_0_findR_Return(NULL)
4239_1_findR_InvokeMethod(4599_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4604_0_findR_Return(x0)
4239_1_findR_InvokeMethod(4604_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4604_0_findR_Return(x0)
4239_1_findR_InvokeMethod(4408_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4604_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4239_1_findR_InvokeMethod(4409_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4604_0_findR_Return(NULL)

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_3966_0_findR_FieldAccess_3, Cond_3966_0_findR_FieldAccess1_3]=Cond_3966_0_findR_FieldAccess_3, [4240_1_findR_InvokeMethod_3, 4239_1_findR_InvokeMethod_3]=4240_1_findR_InvokeMethod_3, [4078_0_findR_Return_1, 4413_0_findR_Return_1, 4081_0_findR_Return_1, 4408_0_findR_Return_1]=4078_0_findR_Return_1, [4599_0_findR_Return_1, 4604_0_findR_Return_1]=4599_0_findR_Return_1, [4168_0_findR_Return, 4417_0_findR_Return, 4171_0_findR_Return, 4409_0_findR_Return]=4168_0_findR_Return}

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

P rules:
3966_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3966_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
COND_3966_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3966_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
R rules:
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4168_0_findR_Return
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4599_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4599_0_findR_Return(NULL)
4240_1_findR_InvokeMethod(4599_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4599_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:
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4168_0_findR_Return
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4599_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4599_0_findR_Return(NULL)
4240_1_findR_InvokeMethod(4599_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4599_0_findR_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3966_0_FINDR_FIELDACCESS(!(x0[0] = x2[0]), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
(1): COND_3966_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3966_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:
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
4240_1_findR_InvokeMethod(4599_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@1e70f0ed 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 3966_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3966_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 3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3966_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3966_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3966_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]))) ⇒ 3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3966_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(U^Increasing(COND_3966_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 ⇒ 3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3966_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(U^Increasing(COND_3966_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_3966_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_3966_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_3966_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_3966_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_3966_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3966_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1)) the following chains were created:

We consider the chain 3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3966_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3966_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3966_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1])), 3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3966_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_3966_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥NonInfC∧COND_3966_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥3966_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))∧(U^Increasing(3966_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_3966_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_3966_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))))))≥3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))))∧(U^Increasing(3966_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(3966_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(3966_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(3966_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(3966_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.

3966_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3966_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
- (0 ≥ 0 ⇒ (U^Increasing(COND_3966_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_3966_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3966_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
- (0 ≥ 0 ⇒ (U^Increasing(3966_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(4240_1_findR_InvokeMethod(x₁, x₂, x₃)) = 0
POL(4078_0_findR_Return(x₁)) = 0
POL(java.lang.Object(x₁)) = [1] + [2]x₁
POL(DoublyLinkedList.DoublyLinkedList(x₁, x₂)) = [2]x₂
POL(4168_0_findR_Return) = 0
POL(NULL) = 0
POL(4599_0_findR_Return(x₁)) = 0
POL(3966_0_FINDR_FIELDACCESS(x₁, x₂)) = [1] + x₂ + [2]x₁
POL(COND_3966_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_>:

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

The following pairs are in P_bound:

3966_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3966_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
COND_3966_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3966_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:
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4168_0_findR_Return
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4599_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4599_0_findR_Return(NULL)
4240_1_findR_InvokeMethod(4599_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4599_0_findR_Return(x0)

The integer pair graph is empty.

The set Q consists of the following terms:
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
4240_1_findR_InvokeMethod(4078_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
4240_1_findR_InvokeMethod(4168_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
4240_1_findR_InvokeMethod(4599_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:
4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(o4221sub), java.lang.Object(o4221sub)) → 4307_0_getFirst_FieldAccess(EOS(STATIC_4307), java.lang.Object(o4221sub), java.lang.Object(o4221sub))
4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(o4221sub), java.lang.Object(o4221sub)) → 4308_0_getFirst_FieldAccess(EOS(STATIC_4308), java.lang.Object(o4221sub), java.lang.Object(o4221sub))
4307_0_getFirst_FieldAccess(EOS(STATIC_4307), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321))) → 4334_0_getFirst_FieldAccess(EOS(STATIC_4334), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321)))
4334_0_getFirst_FieldAccess(EOS(STATIC_4334), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321))) → 4395_0_getFirst_NONNULL(EOS(STATIC_4395), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4321)), o4321)
4395_0_getFirst_NONNULL(EOS(STATIC_4395), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub))), java.lang.Object(o4426sub)) → 4423_0_getFirst_NONNULL(EOS(STATIC_4423), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub))), java.lang.Object(o4426sub))
4423_0_getFirst_NONNULL(EOS(STATIC_4423), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub))), java.lang.Object(o4426sub)) → 4446_0_getFirst_Load(EOS(STATIC_4446), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub))))
4446_0_getFirst_Load(EOS(STATIC_4446), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub)))) → 4478_0_getFirst_FieldAccess(EOS(STATIC_4478), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub))))
4478_0_getFirst_FieldAccess(EOS(STATIC_4478), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4426sub)))) → 4584_0_getFirst_InvokeMethod(EOS(STATIC_4584), java.lang.Object(o4426sub))
4584_0_getFirst_InvokeMethod(EOS(STATIC_4584), java.lang.Object(o4426sub)) → 4610_1_getFirst_InvokeMethod(4610_0_getFirst_Load(EOS(STATIC_4610), java.lang.Object(o4426sub)), java.lang.Object(o4426sub))
4610_0_getFirst_Load(EOS(STATIC_4610), java.lang.Object(o4426sub)) → 4627_0_getFirst_Load(EOS(STATIC_4627), java.lang.Object(o4426sub))
4627_0_getFirst_Load(EOS(STATIC_4627), java.lang.Object(o4426sub)) → 4666_0_getFirst_Load(EOS(STATIC_4666), java.lang.Object(o4426sub))
4666_0_getFirst_Load(EOS(STATIC_4666), java.lang.Object(o4882sub)) → 4728_0_getFirst_Load(EOS(STATIC_4728), java.lang.Object(o4882sub))
4728_0_getFirst_Load(EOS(STATIC_4728), java.lang.Object(o4882sub)) → 4271_0_getFirst_Load(EOS(STATIC_4271), java.lang.Object(o4882sub))
4271_0_getFirst_Load(EOS(STATIC_4271), java.lang.Object(o4221sub)) → 4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(o4221sub), java.lang.Object(o4221sub))
4308_0_getFirst_FieldAccess(EOS(STATIC_4308), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324))) → 4335_0_getFirst_FieldAccess(EOS(STATIC_4335), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324)))
4335_0_getFirst_FieldAccess(EOS(STATIC_4335), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324))) → 4400_0_getFirst_NONNULL(EOS(STATIC_4400), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4324)), o4324)
4400_0_getFirst_NONNULL(EOS(STATIC_4400), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub))), java.lang.Object(o4427sub)) → 4425_0_getFirst_NONNULL(EOS(STATIC_4425), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub))), java.lang.Object(o4427sub))
4425_0_getFirst_NONNULL(EOS(STATIC_4425), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub))), java.lang.Object(o4427sub)) → 4449_0_getFirst_Load(EOS(STATIC_4449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub))))
4449_0_getFirst_Load(EOS(STATIC_4449), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub)))) → 4480_0_getFirst_FieldAccess(EOS(STATIC_4480), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub))))
4480_0_getFirst_FieldAccess(EOS(STATIC_4480), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o4427sub)))) → 4586_0_getFirst_InvokeMethod(EOS(STATIC_4586), java.lang.Object(o4427sub))
4586_0_getFirst_InvokeMethod(EOS(STATIC_4586), java.lang.Object(o4427sub)) → 4613_1_getFirst_InvokeMethod(4613_0_getFirst_Load(EOS(STATIC_4613), java.lang.Object(o4427sub)), java.lang.Object(o4427sub))
4613_0_getFirst_Load(EOS(STATIC_4613), java.lang.Object(o4427sub)) → 4630_0_getFirst_Load(EOS(STATIC_4630), java.lang.Object(o4427sub))
4630_0_getFirst_Load(EOS(STATIC_4630), java.lang.Object(o4427sub)) → 4731_0_getFirst_Load(EOS(STATIC_4731), java.lang.Object(o4427sub))
4731_0_getFirst_Load(EOS(STATIC_4731), java.lang.Object(o4427sub)) → 4271_0_getFirst_Load(EOS(STATIC_4271), java.lang.Object(o4427sub))
R rules:
4395_0_getFirst_NONNULL(EOS(STATIC_4395), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4424_0_getFirst_NONNULL(EOS(STATIC_4424), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
4400_0_getFirst_NONNULL(EOS(STATIC_4400), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4426_0_getFirst_NONNULL(EOS(STATIC_4426), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
4424_0_getFirst_NONNULL(EOS(STATIC_4424), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4447_0_getFirst_Load(EOS(STATIC_4447), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4426_0_getFirst_NONNULL(EOS(STATIC_4426), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 4450_0_getFirst_Load(EOS(STATIC_4450), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4447_0_getFirst_Load(EOS(STATIC_4447), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4479_0_getFirst_Return(EOS(STATIC_4479), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4450_0_getFirst_Load(EOS(STATIC_4450), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4482_0_getFirst_Return(EOS(STATIC_4482), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(4479_0_getFirst_Return(EOS(STATIC_4479), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4766_0_getFirst_Return(EOS(STATIC_4766), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(4482_0_getFirst_Return(EOS(STATIC_4482), 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)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, 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)))
4610_1_getFirst_InvokeMethod(4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4874_0_getFirst_Return(EOS(STATIC_4874), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(o5559sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5882))))))) → 5319_0_getFirst_Return(EOS(STATIC_5319), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5882)))))), java.lang.Object(o5559sub))
4610_1_getFirst_InvokeMethod(5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(o5649sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5924))))))) → 5375_0_getFirst_Return(EOS(STATIC_5375), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5924)))))), java.lang.Object(o5649sub))
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return(EOS(STATIC_4479), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4782_0_getFirst_Return(EOS(STATIC_4782), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(4482_0_getFirst_Return(EOS(STATIC_4482), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4789_0_getFirst_Return(EOS(STATIC_4789), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4847_0_getFirst_Return(EOS(STATIC_4847), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4881_0_getFirst_Return(EOS(STATIC_4881), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(o5559sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5892))))))) → 5327_0_getFirst_Return(EOS(STATIC_5327), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5892)))))), java.lang.Object(o5559sub))
4613_1_getFirst_InvokeMethod(5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(o5649sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5933))))))) → 5384_0_getFirst_Return(EOS(STATIC_5384), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5933)))))), java.lang.Object(o5649sub))
4766_0_getFirst_Return(EOS(STATIC_4766), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4780_0_getFirst_Return(EOS(STATIC_4780), 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)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4780_0_getFirst_Return(EOS(STATIC_4780), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4780_0_getFirst_Return(EOS(STATIC_4780), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4782_0_getFirst_Return(EOS(STATIC_4782), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4789_0_getFirst_Return(EOS(STATIC_4789), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4782_0_getFirst_Return(EOS(STATIC_4782), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), 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))) → 4875_0_getFirst_Return(EOS(STATIC_4875), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4847_0_getFirst_Return(EOS(STATIC_4847), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 5125_0_getFirst_Return(EOS(STATIC_5125), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4874_0_getFirst_Return(EOS(STATIC_4874), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4875_0_getFirst_Return(EOS(STATIC_4875), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4875_0_getFirst_Return(EOS(STATIC_4875), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 5107_0_getFirst_Return(EOS(STATIC_5107), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4881_0_getFirst_Return(EOS(STATIC_4881), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4847_0_getFirst_Return(EOS(STATIC_4847), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
5107_0_getFirst_Return(EOS(STATIC_5107), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5491)))), java.lang.Object(o5494sub)) → 5204_0_getFirst_Return(EOS(STATIC_5204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5491)))), java.lang.Object(o5494sub))
5125_0_getFirst_Return(EOS(STATIC_5125), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5556)))), java.lang.Object(o5559sub)) → 5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(o5559sub))
5204_0_getFirst_Return(EOS(STATIC_5204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5646)))), java.lang.Object(o5649sub)) → 5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(o5649sub))
5319_0_getFirst_Return(EOS(STATIC_5319), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5882)))))), java.lang.Object(o5559sub)) → 5204_0_getFirst_Return(EOS(STATIC_5204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5882)))))), java.lang.Object(o5559sub))
5327_0_getFirst_Return(EOS(STATIC_5327), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5892)))))), java.lang.Object(o5559sub)) → 5125_0_getFirst_Return(EOS(STATIC_5125), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5892)))))), java.lang.Object(o5559sub))
5375_0_getFirst_Return(EOS(STATIC_5375), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5924)))))), java.lang.Object(o5649sub)) → 5204_0_getFirst_Return(EOS(STATIC_5204), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5924)))))), java.lang.Object(o5649sub))
5384_0_getFirst_Return(EOS(STATIC_5384), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5933)))))), java.lang.Object(o5649sub)) → 5125_0_getFirst_Return(EOS(STATIC_5125), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o5933)))))), java.lang.Object(o5649sub))

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

P rules:
4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 4610_1_getFirst_InvokeMethod(4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 4613_1_getFirst_InvokeMethod(4289_0_getFirst_FieldAccess(EOS(STATIC_4289), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return(EOS(STATIC_4479), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(4482_0_getFirst_Return(EOS(STATIC_4482), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(4479_0_getFirst_Return(EOS(STATIC_4479), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(4482_0_getFirst_Return(EOS(STATIC_4482), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4613_1_getFirst_InvokeMethod(5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(x0))
4613_1_getFirst_InvokeMethod(5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(x0))
4610_1_getFirst_InvokeMethod(5233_0_getFirst_Return(EOS(STATIC_5233), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(x0))
4610_1_getFirst_InvokeMethod(5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(x0))
4610_1_getFirst_InvokeMethod(4799_0_getFirst_Return(EOS(STATIC_4799), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4610_1_getFirst_InvokeMethod(4801_0_getFirst_Return(EOS(STATIC_4801), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 5242_0_getFirst_Return(EOS(STATIC_5242), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))

Filtered ground terms:

4289_0_getFirst_FieldAccess(x1, x2, x3) → 4289_0_getFirst_FieldAccess(x2, x3)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
5242_0_getFirst_Return(x1, x2) → 5242_0_getFirst_Return(x2)
4801_0_getFirst_Return(x1, x2) → 4801_0_getFirst_Return
4799_0_getFirst_Return(x1, x2) → 4799_0_getFirst_Return
5233_0_getFirst_Return(x1, x2) → 5233_0_getFirst_Return(x2)
4482_0_getFirst_Return(x1, x2, x3) → 4482_0_getFirst_Return
4479_0_getFirst_Return(x1, x2, x3) → 4479_0_getFirst_Return

Filtered duplicate args:

4289_0_getFirst_FieldAccess(x1, x2) → 4289_0_getFirst_FieldAccess(x2)

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

P rules:
4289_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 4610_1_getFirst_InvokeMethod(4289_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
4289_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 4613_1_getFirst_InvokeMethod(4289_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4801_0_getFirst_Return
4613_1_getFirst_InvokeMethod(4482_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4801_0_getFirst_Return
4610_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4799_0_getFirst_Return
4610_1_getFirst_InvokeMethod(4482_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4799_0_getFirst_Return
4613_1_getFirst_InvokeMethod(4799_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(4801_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(5233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5233_0_getFirst_Return(java.lang.Object(x0))
4613_1_getFirst_InvokeMethod(5242_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5233_0_getFirst_Return(java.lang.Object(x0))
4610_1_getFirst_InvokeMethod(5233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5242_0_getFirst_Return(java.lang.Object(x0))
4610_1_getFirst_InvokeMethod(5242_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5242_0_getFirst_Return(java.lang.Object(x0))
4610_1_getFirst_InvokeMethod(4799_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5242_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4610_1_getFirst_InvokeMethod(4801_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5242_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))

Performed bisimulation on rules. Used the following equivalence classes: {[4613_1_getFirst_InvokeMethod_2, 4610_1_getFirst_InvokeMethod_2]=4613_1_getFirst_InvokeMethod_2, [4479_0_getFirst_Return, 4801_0_getFirst_Return, 4482_0_getFirst_Return, 4799_0_getFirst_Return]=4479_0_getFirst_Return, [5233_0_getFirst_Return_1, 5242_0_getFirst_Return_1]=5233_0_getFirst_Return_1}

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

P rules:
4289_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 4289_0_GETFIRST_FIELDACCESS(java.lang.Object(x0))
R rules:
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4479_0_getFirst_Return
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(5233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5233_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:
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4479_0_getFirst_Return
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(5233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5233_0_getFirst_Return(java.lang.Object(x0))

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

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

The TRS R consists of the following rules:

4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 4479_0_getFirst_Return
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 5233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(5233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 5233_0_getFirst_Return(java.lang.Object(x0))

The set Q consists of the following terms:

4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
4613_1_getFirst_InvokeMethod(5233_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:

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

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

4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
4613_1_getFirst_InvokeMethod(5233_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].

4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
4613_1_getFirst_InvokeMethod(4479_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
4613_1_getFirst_InvokeMethod(5233_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:

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

4289_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 4289_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:
3766_0_createList_Load(EOS(STATIC_3766(i2326)), i193, o3755, i2327, i2327) → 3774_0_createList_GE(EOS(STATIC_3774(i2326)), i193, o3755, i2327, i2327, i193)
3774_0_createList_GE(EOS(STATIC_3774(i2326)), i193, o3755, i2327, i2327, i193) → 3788_0_createList_GE(EOS(STATIC_3788(i2326)), i193, o3755, i2327, i2327, i193)
3788_0_createList_GE(EOS(STATIC_3788(i2326)), i193, o3755, i2327, i2327, i193) → 3804_0_createList_Load(EOS(STATIC_3804(i2326)), i193, o3755, i2327) | <(i2327, i193)
3804_0_createList_Load(EOS(STATIC_3804(i2326)), i193, o3755, i2327) → 3815_0_createList_Store(EOS(STATIC_3815(i2326)), i193, i2327, o3755)
3815_0_createList_Store(EOS(STATIC_3815(i2326)), i193, i2327, o3755) → 3827_0_createList_New(EOS(STATIC_3827(i2326)), i193, i2327, o3755)
3827_0_createList_New(EOS(STATIC_3827(i2326)), i193, i2327, o3755) → 3841_0_createList_Duplicate(EOS(STATIC_3841(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3841_0_createList_Duplicate(EOS(STATIC_3841(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3864_0_createList_InvokeMethod(EOS(STATIC_3864(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3864_0_createList_InvokeMethod(EOS(STATIC_3864(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3875_0_random_FieldAccess(EOS(STATIC_3875(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3875_0_random_FieldAccess(EOS(STATIC_3875(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3896_0_random_ArrayLength(EOS(STATIC_3896(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)))
3896_0_random_ArrayLength(EOS(STATIC_3896(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191))) → 3903_0_random_FieldAccess(EOS(STATIC_3903(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191) | >=(i191, 0)
3903_0_random_FieldAccess(EOS(STATIC_3903(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191) → 3909_0_random_GT(EOS(STATIC_3909(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326)
3909_0_random_GT(EOS(STATIC_3909(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326) → 3921_0_random_GT(EOS(STATIC_3921(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326)
3909_0_random_GT(EOS(STATIC_3909(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326) → 3922_0_random_GT(EOS(STATIC_3922(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326)
3921_0_random_GT(EOS(STATIC_3921(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326) → 3933_0_random_FieldAccess(EOS(STATIC_3933(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | >(i191, i2326)
3933_0_random_FieldAccess(EOS(STATIC_3933(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3947_0_random_FieldAccess(EOS(STATIC_3947(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)))
3947_0_random_FieldAccess(EOS(STATIC_3947(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191))) → 3960_0_random_ArrayAccess(EOS(STATIC_3960(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i2326)
3960_0_random_ArrayAccess(EOS(STATIC_3960(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i2326) → 3970_0_random_ArrayAccess(EOS(STATIC_3970(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i2326)
3970_0_random_ArrayAccess(EOS(STATIC_3970(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i2326) → 3981_0_random_Store(EOS(STATIC_3981(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) | <(i2326, i191)
3981_0_random_Store(EOS(STATIC_3981(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) → 3996_0_random_FieldAccess(EOS(STATIC_3996(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937)
3996_0_random_FieldAccess(EOS(STATIC_3996(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) → 4011_0_random_ConstantStackPush(EOS(STATIC_4011(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2326)
4011_0_random_ConstantStackPush(EOS(STATIC_4011(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2326) → 4033_0_random_IntArithmetic(EOS(STATIC_4033(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2326, 1)
4033_0_random_IntArithmetic(EOS(STATIC_4033(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2326, matching1) → 4052_0_random_FieldAccess(EOS(STATIC_4052(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, +(i2326, 1)) | &&(>=(i2326, 0), =(matching1, 1))
4052_0_random_FieldAccess(EOS(STATIC_4052(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, i2409) → 4070_0_random_Load(EOS(STATIC_4070(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937)
4070_0_random_Load(EOS(STATIC_4070(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937) → 4089_0_random_NONNULL(EOS(STATIC_4089(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3937, o3937)
4089_0_random_NONNULL(EOS(STATIC_4089(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub), java.lang.Object(o4055sub)) → 4110_0_random_NONNULL(EOS(STATIC_4110(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub), java.lang.Object(o4055sub))
4089_0_random_NONNULL(EOS(STATIC_4089(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 4111_0_random_NONNULL(EOS(STATIC_4111(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL)
4110_0_random_NONNULL(EOS(STATIC_4110(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub), java.lang.Object(o4055sub)) → 4127_0_random_Load(EOS(STATIC_4127(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub))
4127_0_random_Load(EOS(STATIC_4127(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub)) → 4150_0_random_InvokeMethod(EOS(STATIC_4150(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub))
4150_0_random_InvokeMethod(EOS(STATIC_4150(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub)) → 4178_0_length_Load(EOS(STATIC_4178(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub), java.lang.Object(o4055sub))
4178_0_length_Load(EOS(STATIC_4178(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub), java.lang.Object(o4055sub)) → 4231_0_length_FieldAccess(EOS(STATIC_4231(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o4055sub), java.lang.Object(o4055sub))
4231_0_length_FieldAccess(EOS(STATIC_4231(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2489)), java.lang.Object(java.lang.String(o4184sub, i2489))) → 4249_0_length_FieldAccess(EOS(STATIC_4249(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2489)), java.lang.Object(java.lang.String(o4184sub, i2489))) | &&(>=(i2489, 0), >=(i2490, 0))
4249_0_length_FieldAccess(EOS(STATIC_4249(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2489)), java.lang.Object(java.lang.String(o4184sub, i2489))) → 4273_0_length_Return(EOS(STATIC_4273(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2489)), i2489)
4273_0_length_Return(EOS(STATIC_4273(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o4184sub, i2489)), i2489) → 4292_0_random_Return(EOS(STATIC_4292(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489)
4292_0_random_Return(EOS(STATIC_4292(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489) → 4312_0_createList_InvokeMethod(EOS(STATIC_4312(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489)
4312_0_createList_InvokeMethod(EOS(STATIC_4312(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489) → 4338_0_<init>_Load(EOS(STATIC_4338(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489)
4338_0_<init>_Load(EOS(STATIC_4338(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489) → 4429_0_<init>_InvokeMethod(EOS(STATIC_4429(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4429_0_<init>_InvokeMethod(EOS(STATIC_4429(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4453_0_<init>_Load(EOS(STATIC_4453(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489)
4453_0_<init>_Load(EOS(STATIC_4453(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489) → 4485_0_<init>_Load(EOS(STATIC_4485(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4485_0_<init>_Load(EOS(STATIC_4485(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4590_0_<init>_FieldAccess(EOS(STATIC_4590(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489)
4590_0_<init>_FieldAccess(EOS(STATIC_4590(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489) → 4617_0_<init>_Return(EOS(STATIC_4617(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489)
4617_0_<init>_Return(EOS(STATIC_4617(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2489) → 4642_0_createList_Store(EOS(STATIC_4642(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4642_0_createList_Store(EOS(STATIC_4642(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4670_0_createList_Load(EOS(STATIC_4670(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755)
4670_0_createList_Load(EOS(STATIC_4670(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755) → 4735_0_createList_Load(EOS(STATIC_4735(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4735_0_createList_Load(EOS(STATIC_4735(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4758_0_createList_FieldAccess(EOS(STATIC_4758(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755)
4758_0_createList_FieldAccess(EOS(STATIC_4758(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755) → 4791_0_createList_Load(EOS(STATIC_4791(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755)
4791_0_createList_Load(EOS(STATIC_4791(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755) → 4803_0_createList_NULL(EOS(STATIC_4803(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, o3755)
4803_0_createList_NULL(EOS(STATIC_4803(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub), java.lang.Object(o5032sub)) → 4814_0_createList_NULL(EOS(STATIC_4814(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub), java.lang.Object(o5032sub))
4803_0_createList_NULL(EOS(STATIC_4803(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, NULL, NULL) → 4815_0_createList_NULL(EOS(STATIC_4815(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, NULL, NULL)
4814_0_createList_NULL(EOS(STATIC_4814(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub), java.lang.Object(o5032sub)) → 4835_0_createList_Load(EOS(STATIC_4835(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub))
4835_0_createList_Load(EOS(STATIC_4835(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub)) → 4883_0_createList_Load(EOS(STATIC_4883(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub))
4883_0_createList_Load(EOS(STATIC_4883(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub)) → 4923_0_createList_FieldAccess(EOS(STATIC_4923(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o5032sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4923_0_createList_FieldAccess(EOS(STATIC_4923(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 5026_0_createList_FieldAccess(EOS(STATIC_5026(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
5026_0_createList_FieldAccess(EOS(STATIC_5026(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 5057_0_createList_Inc(EOS(STATIC_5057(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327)
5057_0_createList_Inc(EOS(STATIC_5057(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327) → 5225_0_createList_JMP(EOS(STATIC_5225(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2327, 1))
5225_0_createList_JMP(EOS(STATIC_5225(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3236) → 5246_0_createList_Load(EOS(STATIC_5246(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3236)
5246_0_createList_Load(EOS(STATIC_5246(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3236) → 3754_0_createList_Load(EOS(STATIC_3754(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i3236)
3754_0_createList_Load(EOS(STATIC_3754(i2326)), i193, o3755, i2327) → 3766_0_createList_Load(EOS(STATIC_3766(i2326)), i193, o3755, i2327, i2327)
4815_0_createList_NULL(EOS(STATIC_4815(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, NULL, NULL) → 4837_0_createList_Inc(EOS(STATIC_4837(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327)
4837_0_createList_Inc(EOS(STATIC_4837(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327) → 4884_0_createList_JMP(EOS(STATIC_4884(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2327, 1))
4884_0_createList_JMP(EOS(STATIC_4884(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2927) → 4925_0_createList_Load(EOS(STATIC_4925(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2927)
4925_0_createList_Load(EOS(STATIC_4925(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2927) → 3754_0_createList_Load(EOS(STATIC_3754(i2409)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2927)
4111_0_random_NONNULL(EOS(STATIC_4111(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 4129_0_random_ConstantStackPush(EOS(STATIC_4129(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL)
4129_0_random_ConstantStackPush(EOS(STATIC_4129(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL) → 4152_0_random_Return(EOS(STATIC_4152(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, 0)
4152_0_random_Return(EOS(STATIC_4152(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, matching1) → 4179_0_createList_InvokeMethod(EOS(STATIC_4179(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
4179_0_createList_InvokeMethod(EOS(STATIC_4179(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 4312_0_createList_InvokeMethod(EOS(STATIC_4312(i2409)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3922_0_random_GT(EOS(STATIC_3922(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i2326) → 3935_0_random_ConstantStackPush(EOS(STATIC_3935(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | <=(i191, i2326)
3935_0_random_ConstantStackPush(EOS(STATIC_3935(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3949_0_random_Return(EOS(STATIC_3949(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0)
3949_0_random_Return(EOS(STATIC_3949(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3961_0_createList_InvokeMethod(EOS(STATIC_3961(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3961_0_createList_InvokeMethod(EOS(STATIC_3961(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3972_0_<init>_Load(EOS(STATIC_3972(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3972_0_<init>_Load(EOS(STATIC_3972(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3998_0_<init>_InvokeMethod(EOS(STATIC_3998(i2326)), i193, i2327, 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))
3998_0_<init>_InvokeMethod(EOS(STATIC_3998(i2326)), i193, i2327, 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))) → 4014_0_<init>_Load(EOS(STATIC_4014(i2326)), i193, i2327, 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))
4014_0_<init>_Load(EOS(STATIC_4014(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 4036_0_<init>_Load(EOS(STATIC_4036(i2326)), i193, i2327, 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))
4036_0_<init>_Load(EOS(STATIC_4036(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4053_0_<init>_FieldAccess(EOS(STATIC_4053(i2326)), i193, i2327, 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))
4053_0_<init>_FieldAccess(EOS(STATIC_4053(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 4072_0_<init>_Return(EOS(STATIC_4072(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
4072_0_<init>_Return(EOS(STATIC_4072(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 4091_0_createList_Store(EOS(STATIC_4091(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | =(matching1, 0)
4091_0_createList_Store(EOS(STATIC_4091(i2326)), i193, i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4112_0_createList_Load(EOS(STATIC_4112(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755)
4112_0_createList_Load(EOS(STATIC_4112(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755) → 4131_0_createList_Load(EOS(STATIC_4131(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4131_0_createList_Load(EOS(STATIC_4131(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4154_0_createList_FieldAccess(EOS(STATIC_4154(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755)
4154_0_createList_FieldAccess(EOS(STATIC_4154(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3755) → 4181_0_createList_Load(EOS(STATIC_4181(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755)
4181_0_createList_Load(EOS(STATIC_4181(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755) → 4216_0_createList_NULL(EOS(STATIC_4216(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, o3755, o3755)
4216_0_createList_NULL(EOS(STATIC_4216(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub), java.lang.Object(o4180sub)) → 4234_0_createList_NULL(EOS(STATIC_4234(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub), java.lang.Object(o4180sub))
4216_0_createList_NULL(EOS(STATIC_4216(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, NULL, NULL) → 4235_0_createList_NULL(EOS(STATIC_4235(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, NULL, NULL)
4234_0_createList_NULL(EOS(STATIC_4234(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub), java.lang.Object(o4180sub)) → 4252_0_createList_Load(EOS(STATIC_4252(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub))
4252_0_createList_Load(EOS(STATIC_4252(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub)) → 4277_0_createList_Load(EOS(STATIC_4277(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub))
4277_0_createList_Load(EOS(STATIC_4277(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub)) → 4296_0_createList_FieldAccess(EOS(STATIC_4296(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(o4180sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4296_0_createList_FieldAccess(EOS(STATIC_4296(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4314_0_createList_FieldAccess(EOS(STATIC_4314(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4314_0_createList_FieldAccess(EOS(STATIC_4314(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4346_0_createList_Inc(EOS(STATIC_4346(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327)
4346_0_createList_Inc(EOS(STATIC_4346(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327) → 4406_0_createList_JMP(EOS(STATIC_4406(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2327, 1))
4406_0_createList_JMP(EOS(STATIC_4406(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2624) → 4435_0_createList_Load(EOS(STATIC_4435(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2624)
4435_0_createList_Load(EOS(STATIC_4435(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2624) → 3754_0_createList_Load(EOS(STATIC_3754(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2624)
4235_0_createList_NULL(EOS(STATIC_4235(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327, NULL, NULL) → 4253_0_createList_Inc(EOS(STATIC_4253(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327)
4253_0_createList_Inc(EOS(STATIC_4253(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2327) → 4278_0_createList_JMP(EOS(STATIC_4278(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i2327, 1))
4278_0_createList_JMP(EOS(STATIC_4278(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2523) → 4298_0_createList_Load(EOS(STATIC_4298(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2523)
4298_0_createList_Load(EOS(STATIC_4298(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2523) → 3754_0_createList_Load(EOS(STATIC_3754(i2326)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2523)
R rules:

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

P rules:
3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, x2, x3, x3) → 4803_0_createList_NULL(EOS(STATIC_4803(+(x0, 1))), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x3, x2, x2) | &&(<(x3, x1), >(+(x0, 1), 0))
4803_0_createList_NULL(EOS(STATIC_4803(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
4803_0_createList_NULL(EOS(STATIC_4803(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, NULL, NULL) → 3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, x2) → 3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, NULL, x2, x2) → 3766_0_createList_Load(EOS(STATIC_3766(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_3766_0_createList_Load2(x1, x2, x3, x4, x5, x6) → Cond_3766_0_createList_Load2(x1, x2, x3, x5, x6)
Cond_3766_0_createList_Load1(x1, x2, x3, x4, x5, x6) → Cond_3766_0_createList_Load1(x1, x2, x3, x5, x6)
4803_0_createList_NULL(x1, x2, x3, x4, x5, x6) → 4803_0_createList_NULL(x1, x2, x4, x5, x6)

Filtered duplicate args:

3766_0_createList_Load(x1, x2, x3, x4, x5) → 3766_0_createList_Load(x1, x2, x3, x5)
Cond_3766_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_3766_0_createList_Load(x1, x2, x3, x4, x6)
4803_0_createList_NULL(x1, x2, x3, x4, x5) → 4803_0_createList_NULL(x1, x2, x3, x5)
Cond_3766_0_createList_Load1(x1, x2, x3, x4, x5) → Cond_3766_0_createList_Load1(x1, x2, x3, x5)
Cond_3766_0_createList_Load2(x1, x2, x3, x4, x5) → Cond_3766_0_createList_Load2(x1, x2, x3, x5)

Filtered all non-integer terms:

4803_0_createList_NULL(x1, x2, x3, x4) → 4803_0_createList_NULL(x1, x2, x3)
3766_0_createList_Load(x1, x2, x3, x4) → 3766_0_createList_Load(x1, x2, x4)

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

P rules:
3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, x2) → 3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, +(x2, 1)) | <(x2, x1)
3766_0_createList_Load(EOS(STATIC_3766(x0)), x1, x2) → 3766_0_createList_Load(EOS(STATIC_3766(+(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:
3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, x2) → COND_3766_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3766(x0)), x1, x2)
COND_3766_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3766(x0)), x1, x2) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, +(x2, 1))
3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, x2) → COND_3766_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3766(x0)), x1, x2)
COND_3766_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3766(x0)), x1, x2) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(+(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): 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[0])), x1[0], x2[0]) → COND_3766_0_CREATELIST_LOAD(x2[0] < x1[0], EOS(STATIC_3766(x0[0])), x1[0], x2[0])
(1): COND_3766_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3766(x0[1])), x1[1], x2[1]) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[1])), x1[1], x2[1] + 1)
(2): 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[2])), x1[2], x2[2]) → COND_3766_0_CREATELIST_LOAD1(x2[2] < x1[2] && x0[2] > -1, EOS(STATIC_3766(x0[2])), x1[2], x2[2])
(3): COND_3766_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3766(x0[3])), x1[3], x2[3]) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[3] + 1)), x1[3], x2[3] + 1)

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

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

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

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

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

(3) -> (2), if (EOS(STATIC_3766(x0[3] + 1)) →^* EOS(STATIC_3766(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@580a657c 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 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, x2) → COND_3766_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3766(x0)), x1, x2) the following chains were created:

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

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

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

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

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

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

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

For Pair COND_3766_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3766(x0)), x1, x2) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, +(x2, 1)) the following chains were created:

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

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

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

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

For Pair 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, x2) → COND_3766_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3766(x0)), x1, x2) the following chains were created:

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

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

3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, x2) → COND_3766_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3766(x0)), x1, x2)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3766_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3766(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[(-1)bso_13] ≥ 0)
- (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (U^Increasing(COND_3766_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3766(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[(-1)bso_13] ≥ 0)
COND_3766_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3766(x0)), x1, x2) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, +(x2, 1))
- ((U^Increasing(3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0)), x1, x2) → COND_3766_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3766(x0)), x1, x2)
- (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(COND_3766_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3766(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_3766_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3766(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
COND_3766_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3766(x0)), x1, x2) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(+(x0, 1))), x1, +(x2, 1))
- ((U^Increasing(3766_0_CREATELIST_LOAD(EOS(STATIC_3766(+(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(3766_0_CREATELIST_LOAD(x₁, x₂, x₃)) = [-1]x₃ + x₂
POL(EOS(x₁)) = x₁
POL(STATIC_3766(x₁)) = x₁
POL(COND_3766_0_CREATELIST_LOAD(x₁, x₂, x₃, x₄)) = [-1]x₄ + x₃
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_3766_0_CREATELIST_LOAD1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₃
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]

The following pairs are in P_>:

COND_3766_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3766(x0[1])), x1[1], x2[1]) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[1])), x1[1], +(x2[1], 1))
3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[2])), x1[2], x2[2]) → COND_3766_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3766(x0[2])), x1[2], x2[2])

The following pairs are in P_bound:

3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[0])), x1[0], x2[0]) → COND_3766_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3766(x0[0])), x1[0], x2[0])
3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[2])), x1[2], x2[2]) → COND_3766_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3766(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[0])), x1[0], x2[0]) → COND_3766_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3766(x0[0])), x1[0], x2[0])
COND_3766_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3766(x0[3])), x1[3], x2[3]) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(+(x0[3], 1))), x1[3], +(x2[3], 1))

There are no usable rules.

(27) Complex Obligation (AND)

(28) Obligation:

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

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

The following domains are used:

Integer

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

The set Q is empty.

(29) IDependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

(31) Obligation:

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

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_3766_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3766(x0[1])), x1[1], x2[1]) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[1])), x1[1], x2[1] + 1)
(3): COND_3766_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3766(x0[3])), x1[3], x2[3]) → 3766_0_CREATELIST_LOAD(EOS(STATIC_3766(x0[3] + 1)), x1[3], x2[3] + 1)

The set Q is empty.

(32) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPtoQDPProof (SOUND transformation)

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) QReductionProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) SCCToIDPv1Proof (SOUND transformation)

(25) Obligation:

(26) IDPNonInfProof (SOUND transformation)

(27) Complex Obligation (AND)

(28) Obligation:

(29) IDependencyGraphProof (EQUIVALENT transformation)

(30) TRUE

(31) Obligation:

(32) IDependencyGraphProof (EQUIVALENT transformation)

(33) TRUE