(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_14 (Sun Microsystems Inc.) Main-Class: DoublyLinkedList/MainFind
package DoublyLinkedList;

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

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

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

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

public DoublyLinkedList get(final int index) {
DoublyLinkedList current = this.getFirst();
while (index > 0 && current != null) {
current = current.next;
}
return current;
}

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

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

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

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

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

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

return cur;
}
}


package DoublyLinkedList;

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


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

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


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

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

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

DoublyLinkedList.DoublyLinkedList.findR(I)LDoublyLinkedList/DoublyLinkedList;: Graph of 88 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

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

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 36 rules for P and 57 rules for R.


P rules:
3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub)) → 3608_0_findR_FieldAccess(EOS(STATIC_3608), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub))
3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub)) → 3609_0_findR_FieldAccess(EOS(STATIC_3609), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub))
3608_0_findR_FieldAccess(EOS(STATIC_3608), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084))) → 3620_0_findR_FieldAccess(EOS(STATIC_3620), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)))
3620_0_findR_FieldAccess(EOS(STATIC_3620), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084))) → 3632_0_findR_Load(EOS(STATIC_3632), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875)
3632_0_findR_Load(EOS(STATIC_3632), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875) → 3646_0_findR_NE(EOS(STATIC_3646), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754)
3646_0_findR_NE(EOS(STATIC_3646), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754) → 3665_0_findR_NE(EOS(STATIC_3665), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754)
3665_0_findR_NE(EOS(STATIC_3665), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, i1875, i1754) → 3680_0_findR_Load(EOS(STATIC_3680), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754) | !(=(i1875, i1754))
3680_0_findR_Load(EOS(STATIC_3680), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754) → 3694_0_findR_FieldAccess(EOS(STATIC_3694), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)))
3694_0_findR_FieldAccess(EOS(STATIC_3694), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084))) → 3712_0_findR_NULL(EOS(STATIC_3712), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, o3084)), i1754, o3084)
3712_0_findR_NULL(EOS(STATIC_3712), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754, java.lang.Object(o3181sub)) → 3738_0_findR_NULL(EOS(STATIC_3738), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754, java.lang.Object(o3181sub))
3738_0_findR_NULL(EOS(STATIC_3738), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754, java.lang.Object(o3181sub)) → 3755_0_findR_Load(EOS(STATIC_3755), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754)
3755_0_findR_Load(EOS(STATIC_3755), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))), i1754) → 3781_0_findR_FieldAccess(EOS(STATIC_3781), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub))))
3781_0_findR_FieldAccess(EOS(STATIC_3781), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, java.lang.Object(o3181sub)))) → 3821_0_findR_Load(EOS(STATIC_3821), i1754, java.lang.Object(o3181sub))
3821_0_findR_Load(EOS(STATIC_3821), i1754, java.lang.Object(o3181sub)) → 3841_0_findR_InvokeMethod(EOS(STATIC_3841), java.lang.Object(o3181sub), i1754)
3841_0_findR_InvokeMethod(EOS(STATIC_3841), java.lang.Object(o3181sub), i1754) → 3855_1_findR_InvokeMethod(3855_0_findR_Load(EOS(STATIC_3855), java.lang.Object(o3181sub), i1754), java.lang.Object(o3181sub), i1754)
3855_0_findR_Load(EOS(STATIC_3855), java.lang.Object(o3181sub), i1754) → 3883_0_findR_Load(EOS(STATIC_3883), java.lang.Object(o3181sub), i1754)
3883_0_findR_Load(EOS(STATIC_3883), java.lang.Object(o3181sub), i1754) → 3939_0_findR_Load(EOS(STATIC_3939), java.lang.Object(o3181sub), i1754)
3939_0_findR_Load(EOS(STATIC_3939), java.lang.Object(o3391sub), i1754) → 3982_0_findR_Load(EOS(STATIC_3982), java.lang.Object(o3391sub), i1754)
3982_0_findR_Load(EOS(STATIC_3982), java.lang.Object(o3391sub), i1754) → 3595_0_findR_Load(EOS(STATIC_3595), java.lang.Object(o3391sub), i1754)
3595_0_findR_Load(EOS(STATIC_3595), java.lang.Object(o3057sub), i1754) → 3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(o3057sub), i1754, java.lang.Object(o3057sub))
3609_0_findR_FieldAccess(EOS(STATIC_3609), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087))) → 3621_0_findR_FieldAccess(EOS(STATIC_3621), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)))
3621_0_findR_FieldAccess(EOS(STATIC_3621), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087))) → 3633_0_findR_Load(EOS(STATIC_3633), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876)
3633_0_findR_Load(EOS(STATIC_3633), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876) → 3652_0_findR_NE(EOS(STATIC_3652), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754)
3652_0_findR_NE(EOS(STATIC_3652), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754) → 3667_0_findR_NE(EOS(STATIC_3667), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754)
3667_0_findR_NE(EOS(STATIC_3667), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, i1876, i1754) → 3683_0_findR_Load(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754) | !(=(i1876, i1754))
3683_0_findR_Load(EOS(STATIC_3683), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754) → 3697_0_findR_FieldAccess(EOS(STATIC_3697), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)))
3697_0_findR_FieldAccess(EOS(STATIC_3697), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087))) → 3719_0_findR_NULL(EOS(STATIC_3719), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, o3087)), i1754, o3087)
3719_0_findR_NULL(EOS(STATIC_3719), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754, java.lang.Object(o3182sub)) → 3741_0_findR_NULL(EOS(STATIC_3741), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754, java.lang.Object(o3182sub))
3741_0_findR_NULL(EOS(STATIC_3741), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754, java.lang.Object(o3182sub)) → 3758_0_findR_Load(EOS(STATIC_3758), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754)
3758_0_findR_Load(EOS(STATIC_3758), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))), i1754) → 3784_0_findR_FieldAccess(EOS(STATIC_3784), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub))))
3784_0_findR_FieldAccess(EOS(STATIC_3784), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, java.lang.Object(o3182sub)))) → 3825_0_findR_Load(EOS(STATIC_3825), i1754, java.lang.Object(o3182sub))
3825_0_findR_Load(EOS(STATIC_3825), i1754, java.lang.Object(o3182sub)) → 3843_0_findR_InvokeMethod(EOS(STATIC_3843), java.lang.Object(o3182sub), i1754)
3843_0_findR_InvokeMethod(EOS(STATIC_3843), java.lang.Object(o3182sub), i1754) → 3856_1_findR_InvokeMethod(3856_0_findR_Load(EOS(STATIC_3856), java.lang.Object(o3182sub), i1754), java.lang.Object(o3182sub), i1754)
3856_0_findR_Load(EOS(STATIC_3856), java.lang.Object(o3182sub), i1754) → 3885_0_findR_Load(EOS(STATIC_3885), java.lang.Object(o3182sub), i1754)
3885_0_findR_Load(EOS(STATIC_3885), java.lang.Object(o3182sub), i1754) → 3984_0_findR_Load(EOS(STATIC_3984), java.lang.Object(o3182sub), i1754)
3984_0_findR_Load(EOS(STATIC_3984), java.lang.Object(o3182sub), i1754) → 3595_0_findR_Load(EOS(STATIC_3595), java.lang.Object(o3182sub), i1754)
R rules:
3646_0_findR_NE(EOS(STATIC_3646), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, i1754, i1754) → 3666_0_findR_NE(EOS(STATIC_3666), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, i1754, i1754)
3652_0_findR_NE(EOS(STATIC_3652), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, i1754, i1754) → 3668_0_findR_NE(EOS(STATIC_3668), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, i1754, i1754)
3666_0_findR_NE(EOS(STATIC_3666), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, i1754, i1754) → 3681_0_findR_Load(EOS(STATIC_3681), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754)
3668_0_findR_NE(EOS(STATIC_3668), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, i1754, i1754) → 3685_0_findR_Load(EOS(STATIC_3685), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754)
3681_0_findR_Load(EOS(STATIC_3681), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754) → 3696_0_findR_Return(EOS(STATIC_3696), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3084)))
3685_0_findR_Load(EOS(STATIC_3685), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754) → 3699_0_findR_Return(EOS(STATIC_3699), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)), i1754, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1754, o3087)))
3712_0_findR_NULL(EOS(STATIC_3712), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, NULL)), i1754, NULL) → 3739_0_findR_NULL(EOS(STATIC_3739), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, NULL)), i1754, NULL)
3719_0_findR_NULL(EOS(STATIC_3719), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, NULL)), i1754, NULL) → 3742_0_findR_NULL(EOS(STATIC_3742), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, NULL)), i1754, NULL)
3739_0_findR_NULL(EOS(STATIC_3739), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1875, NULL)), i1754, NULL) → 3756_0_findR_ConstantStackPush(EOS(STATIC_3756))
3742_0_findR_NULL(EOS(STATIC_3742), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i1876, NULL)), i1754, NULL) → 3760_0_findR_ConstantStackPush(EOS(STATIC_3760))
3756_0_findR_ConstantStackPush(EOS(STATIC_3756)) → 3782_0_findR_Return(EOS(STATIC_3782), NULL)
3760_0_findR_ConstantStackPush(EOS(STATIC_3760)) → 3785_0_findR_Return(EOS(STATIC_3785), NULL)
3855_1_findR_InvokeMethod(3696_0_findR_Return(EOS(STATIC_3696), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070) → 4043_0_findR_Return(EOS(STATIC_4043), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)))
3855_1_findR_InvokeMethod(3699_0_findR_Return(EOS(STATIC_3699), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077) → 4058_0_findR_Return(EOS(STATIC_4058), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)))
3855_1_findR_InvokeMethod(3782_0_findR_Return(EOS(STATIC_3782), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085) → 4060_0_findR_Return(EOS(STATIC_4060), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085, NULL)
3855_1_findR_InvokeMethod(3785_0_findR_Return(EOS(STATIC_3785), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092) → 4067_0_findR_Return(EOS(STATIC_4067), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092, NULL)
3855_1_findR_InvokeMethod(4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050)))), i2327) → 4302_0_findR_Return(EOS(STATIC_4302), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050)))), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050)))
3855_1_findR_InvokeMethod(4210_0_findR_Return(EOS(STATIC_4210), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2338, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2337, NULL)))), i2339) → 4312_0_findR_Return(EOS(STATIC_4312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2338, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2337, NULL)))), i2339, NULL)
3855_1_findR_InvokeMethod(4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2349, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075)))), i2350) → 4345_0_findR_Return(EOS(STATIC_4345), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2349, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075)))), i2350, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075)))
3855_1_findR_InvokeMethod(4216_0_findR_Return(EOS(STATIC_4216), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, NULL)))), i2361) → 4358_0_findR_Return(EOS(STATIC_4358), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, NULL)))), i2361, NULL)
3855_1_findR_InvokeMethod(4425_0_findR_Return(EOS(STATIC_4425), o4199), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583) → 4538_0_findR_Return(EOS(STATIC_4538), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583, o4199)
3855_1_findR_InvokeMethod(4429_0_findR_Return(EOS(STATIC_4429), o4236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4605)))))), i2597) → 4552_0_findR_Return(EOS(STATIC_4552), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4605)))))), i2597, o4236)
3856_1_findR_InvokeMethod(3696_0_findR_Return(EOS(STATIC_3696), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099) → 4069_0_findR_Return(EOS(STATIC_4069), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)))
3856_1_findR_InvokeMethod(3699_0_findR_Return(EOS(STATIC_3699), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106) → 4077_0_findR_Return(EOS(STATIC_4077), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)))
3856_1_findR_InvokeMethod(3782_0_findR_Return(EOS(STATIC_3782), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2112, NULL)), i2113) → 4078_0_findR_Return(EOS(STATIC_4078), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2112, NULL)), i2113, NULL)
3856_1_findR_InvokeMethod(3785_0_findR_Return(EOS(STATIC_3785), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121) → 4082_0_findR_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121, NULL)
3856_1_findR_InvokeMethod(4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2332, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057)))), i2333) → 4303_0_findR_Return(EOS(STATIC_4303), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2332, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057)))), i2333, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057)))
3856_1_findR_InvokeMethod(4210_0_findR_Return(EOS(STATIC_4210), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2343, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2342, NULL)))), i2344) → 4323_0_findR_Return(EOS(STATIC_4323), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2343, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2342, NULL)))), i2344, NULL)
3856_1_findR_InvokeMethod(4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2355, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085)))), i2356) → 4353_0_findR_Return(EOS(STATIC_4353), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2355, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085)))), i2356, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085)))
3856_1_findR_InvokeMethod(4216_0_findR_Return(EOS(STATIC_4216), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2366, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2365, NULL)))), i2367) → 4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2366, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2365, NULL)))), i2367, NULL)
3856_1_findR_InvokeMethod(4425_0_findR_Return(EOS(STATIC_4425), o4199), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590) → 4544_0_findR_Return(EOS(STATIC_4544), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590, o4199)
3856_1_findR_InvokeMethod(4429_0_findR_Return(EOS(STATIC_4429), o4236), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4614)))))), i2603) → 4558_0_findR_Return(EOS(STATIC_4558), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4614)))))), i2603, o4236)
4043_0_findR_Return(EOS(STATIC_4043), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517))) → 4059_0_findR_Return(EOS(STATIC_4059), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)), i2070, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2070, o3517)))
4058_0_findR_Return(EOS(STATIC_4058), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524))) → 4059_0_findR_Return(EOS(STATIC_4059), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)), i2077, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2077, o3524)))
4059_0_findR_Return(EOS(STATIC_4059), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630)), i2164, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630)), i2164, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630))) → 4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2164, o3630)))
4060_0_findR_Return(EOS(STATIC_4060), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085, NULL) → 4068_0_findR_Return(EOS(STATIC_4068), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2084, NULL)), i2085, NULL)
4067_0_findR_Return(EOS(STATIC_4067), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092, NULL) → 4068_0_findR_Return(EOS(STATIC_4068), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2091, NULL)), i2092, NULL)
4068_0_findR_Return(EOS(STATIC_4068), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2170, NULL)), i2171, NULL) → 4210_0_findR_Return(EOS(STATIC_4210), NULL)
4069_0_findR_Return(EOS(STATIC_4069), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)), i2099, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550))) → 4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2099, o3550)))
4077_0_findR_Return(EOS(STATIC_4077), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558))) → 4069_0_findR_Return(EOS(STATIC_4069), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)), i2106, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2106, o3558)))
4078_0_findR_Return(EOS(STATIC_4078), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2112, NULL)), i2113, NULL) → 4216_0_findR_Return(EOS(STATIC_4216), NULL)
4082_0_findR_Return(EOS(STATIC_4082), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121, NULL) → 4078_0_findR_Return(EOS(STATIC_4078), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2120, NULL)), i2121, NULL)
4302_0_findR_Return(EOS(STATIC_4302), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050)))), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050))) → 4313_0_findR_Return(EOS(STATIC_4313), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2326, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050)))), i2327, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2327, o4050)))
4303_0_findR_Return(EOS(STATIC_4303), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2332, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057)))), i2333, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057))) → 4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2332, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057)))), i2333, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2333, o4057)))
4312_0_findR_Return(EOS(STATIC_4312), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2338, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2337, NULL)))), i2339, NULL) → 4313_0_findR_Return(EOS(STATIC_4313), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2338, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2337, NULL)))), i2339, NULL)
4313_0_findR_Return(EOS(STATIC_4313), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2416, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2415, o4166)))), i2417, o4172) → 4346_0_findR_Return(EOS(STATIC_4346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2416, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2415, o4166)))), i2417, o4172)
4323_0_findR_Return(EOS(STATIC_4323), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2343, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2342, NULL)))), i2344, NULL) → 4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2343, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2342, NULL)))), i2344, NULL)
4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2422, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2421, o4193)))), i2423, o4199) → 4425_0_findR_Return(EOS(STATIC_4425), o4199)
4345_0_findR_Return(EOS(STATIC_4345), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2349, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075)))), i2350, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075))) → 4346_0_findR_Return(EOS(STATIC_4346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2349, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075)))), i2350, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2350, o4075)))
4346_0_findR_Return(EOS(STATIC_4346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2433, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2432, o4230)))), i2434, o4236) → 4429_0_findR_Return(EOS(STATIC_4429), o4236)
4353_0_findR_Return(EOS(STATIC_4353), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2355, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085)))), i2356, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085))) → 4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2355, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085)))), i2356, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2356, o4085)))
4358_0_findR_Return(EOS(STATIC_4358), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, NULL)))), i2361, NULL) → 4346_0_findR_Return(EOS(STATIC_4346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2360, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2359, NULL)))), i2361, NULL)
4364_0_findR_Return(EOS(STATIC_4364), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2366, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2365, NULL)))), i2367, NULL) → 4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2366, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2365, NULL)))), i2367, NULL)
4538_0_findR_Return(EOS(STATIC_4538), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583, o4199) → 4346_0_findR_Return(EOS(STATIC_4346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2582, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2581, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2580, o4588)))))), i2583, o4199)
4544_0_findR_Return(EOS(STATIC_4544), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590, o4199) → 4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2589, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2588, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2587, o4597)))))), i2590, o4199)
4552_0_findR_Return(EOS(STATIC_4552), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4605)))))), i2597, o4236) → 4346_0_findR_Return(EOS(STATIC_4346), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2596, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2595, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2594, o4605)))))), i2597, o4236)
4558_0_findR_Return(EOS(STATIC_4558), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4614)))))), i2603, o4236) → 4324_0_findR_Return(EOS(STATIC_4324), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2602, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2601, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, i2600, o4614)))))), i2603, o4236)

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


P rules:
3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 3855_1_findR_InvokeMethod(3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1))), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(x1)))) → 3856_1_findR_InvokeMethod(3602_0_findR_FieldAccess(EOS(STATIC_3602), java.lang.Object(x1), x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
3856_1_findR_InvokeMethod(3696_0_findR_Return(EOS(STATIC_3696), 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) → 4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3856_1_findR_InvokeMethod(3699_0_findR_Return(EOS(STATIC_3699), 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) → 4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return(EOS(STATIC_3782), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4216_0_findR_Return(EOS(STATIC_4216), NULL)
3856_1_findR_InvokeMethod(3785_0_findR_Return(EOS(STATIC_3785), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4216_0_findR_Return(EOS(STATIC_4216), NULL)
3855_1_findR_InvokeMethod(3696_0_findR_Return(EOS(STATIC_3696), 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) → 4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3855_1_findR_InvokeMethod(3699_0_findR_Return(EOS(STATIC_3699), 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) → 4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3855_1_findR_InvokeMethod(3782_0_findR_Return(EOS(STATIC_3782), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4210_0_findR_Return(EOS(STATIC_4210), NULL)
3855_1_findR_InvokeMethod(3785_0_findR_Return(EOS(STATIC_3785), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, NULL)), x1) → 4210_0_findR_Return(EOS(STATIC_4210), NULL)
3856_1_findR_InvokeMethod(4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4425_0_findR_Return(EOS(STATIC_4425), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3856_1_findR_InvokeMethod(4210_0_findR_Return(EOS(STATIC_4210), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4425_0_findR_Return(EOS(STATIC_4425), NULL)
3856_1_findR_InvokeMethod(4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4425_0_findR_Return(EOS(STATIC_4425), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3856_1_findR_InvokeMethod(4216_0_findR_Return(EOS(STATIC_4216), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4425_0_findR_Return(EOS(STATIC_4425), NULL)
3856_1_findR_InvokeMethod(4425_0_findR_Return(EOS(STATIC_4425), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4425_0_findR_Return(EOS(STATIC_4425), x0)
3856_1_findR_InvokeMethod(4429_0_findR_Return(EOS(STATIC_4429), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4425_0_findR_Return(EOS(STATIC_4425), x0)
3855_1_findR_InvokeMethod(4213_0_findR_Return(EOS(STATIC_4213), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4429_0_findR_Return(EOS(STATIC_4429), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3855_1_findR_InvokeMethod(4216_0_findR_Return(EOS(STATIC_4216), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4429_0_findR_Return(EOS(STATIC_4429), NULL)
3855_1_findR_InvokeMethod(4425_0_findR_Return(EOS(STATIC_4425), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4429_0_findR_Return(EOS(STATIC_4429), x0)
3855_1_findR_InvokeMethod(4429_0_findR_Return(EOS(STATIC_4429), x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x3, x4)))))), x5) → 4429_0_findR_Return(EOS(STATIC_4429), x0)
3855_1_findR_InvokeMethod(4208_0_findR_Return(EOS(STATIC_4208), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))), x0) → 4429_0_findR_Return(EOS(STATIC_4429), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, x1)))
3855_1_findR_InvokeMethod(4210_0_findR_Return(EOS(STATIC_4210), NULL), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1, NULL)))), x2) → 4429_0_findR_Return(EOS(STATIC_4429), NULL)

Filtered ground terms:



3602_0_findR_FieldAccess(x1, x2, x3, x4) → 3602_0_findR_FieldAccess(x2, x3, x4)
Cond_3602_0_findR_FieldAccess1(x1, x2, x3, x4, x5) → Cond_3602_0_findR_FieldAccess1(x1, x3, x4, x5)
DoublyLinkedList.DoublyLinkedList(x1, x2, x3) → DoublyLinkedList.DoublyLinkedList(x2, x3)
Cond_3602_0_findR_FieldAccess(x1, x2, x3, x4, x5) → Cond_3602_0_findR_FieldAccess(x1, x3, x4, x5)
4429_0_findR_Return(x1, x2) → 4429_0_findR_Return(x2)
4210_0_findR_Return(x1, x2) → 4210_0_findR_Return
4208_0_findR_Return(x1, x2) → 4208_0_findR_Return(x2)
4425_0_findR_Return(x1, x2) → 4425_0_findR_Return(x2)
4216_0_findR_Return(x1, x2) → 4216_0_findR_Return
4213_0_findR_Return(x1, x2) → 4213_0_findR_Return(x2)
3785_0_findR_Return(x1, x2) → 3785_0_findR_Return
3782_0_findR_Return(x1, x2) → 3782_0_findR_Return
3699_0_findR_Return(x1, x2, x3, x4) → 3699_0_findR_Return(x2, x3, x4)
3696_0_findR_Return(x1, x2, x3, x4) → 3696_0_findR_Return(x2, x3, x4)

Filtered duplicate args:



3602_0_findR_FieldAccess(x1, x2, x3) → 3602_0_findR_FieldAccess(x2, x3)
Cond_3602_0_findR_FieldAccess(x1, x2, x3, x4) → Cond_3602_0_findR_FieldAccess(x1, x3, x4)
Cond_3602_0_findR_FieldAccess1(x1, x2, x3, x4) → Cond_3602_0_findR_FieldAccess1(x1, x3, x4)
3696_0_findR_Return(x1, x2, x3) → 3696_0_findR_Return(x3)
3699_0_findR_Return(x1, x2, x3) → 3699_0_findR_Return(x3)

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


P rules:
3602_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3855_1_findR_InvokeMethod(3602_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
3602_0_findR_FieldAccess(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3856_1_findR_InvokeMethod(3602_0_findR_FieldAccess(x2, java.lang.Object(x1)), java.lang.Object(x1), x2) | !(=(x0, x2))
R rules:
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4213_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3699_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4213_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4216_0_findR_Return
3856_1_findR_InvokeMethod(3785_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4216_0_findR_Return
3855_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4208_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3855_1_findR_InvokeMethod(3699_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 4208_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3855_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4210_0_findR_Return
3855_1_findR_InvokeMethod(3785_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 4210_0_findR_Return
3856_1_findR_InvokeMethod(4208_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4425_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(4210_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4425_0_findR_Return(NULL)
3856_1_findR_InvokeMethod(4213_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4425_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(4216_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4425_0_findR_Return(NULL)
3856_1_findR_InvokeMethod(4425_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4425_0_findR_Return(x0)
3856_1_findR_InvokeMethod(4429_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4425_0_findR_Return(x0)
3855_1_findR_InvokeMethod(4213_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4429_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3855_1_findR_InvokeMethod(4216_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4429_0_findR_Return(NULL)
3855_1_findR_InvokeMethod(4425_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4429_0_findR_Return(x0)
3855_1_findR_InvokeMethod(4429_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4429_0_findR_Return(x0)
3855_1_findR_InvokeMethod(4208_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4429_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3855_1_findR_InvokeMethod(4210_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4429_0_findR_Return(NULL)

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_3602_0_findR_FieldAccess_3, Cond_3602_0_findR_FieldAccess1_3]=Cond_3602_0_findR_FieldAccess_3, [3856_1_findR_InvokeMethod_3, 3855_1_findR_InvokeMethod_3]=3856_1_findR_InvokeMethod_3, [3696_0_findR_Return_1, 4213_0_findR_Return_1, 3699_0_findR_Return_1, 4208_0_findR_Return_1]=3696_0_findR_Return_1, [4425_0_findR_Return_1, 4429_0_findR_Return_1]=4425_0_findR_Return_1, [3782_0_findR_Return, 4216_0_findR_Return, 3785_0_findR_Return, 4210_0_findR_Return]=3782_0_findR_Return}


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


P rules:
3602_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3602_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
COND_3602_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3602_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
R rules:
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 3782_0_findR_Return
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4425_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4425_0_findR_Return(NULL)
3856_1_findR_InvokeMethod(4425_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4425_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:
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 3782_0_findR_Return
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4425_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4425_0_findR_Return(NULL)
3856_1_findR_InvokeMethod(4425_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4425_0_findR_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3602_0_FINDR_FIELDACCESS(!(x0[0] = x2[0]), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
(1): COND_3602_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3602_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:
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
3856_1_findR_InvokeMethod(4425_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@147976eb 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 3602_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3602_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 3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3602_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3602_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3602_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1])) which results in the following constraint:

    (1)    (!(=(x0[0], x2[0]))=TRUEx2[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]))) ⇒ 3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3602_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(UIncreasing(COND_3602_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]))=TRUE3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥NonInfC∧3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))≥COND_3602_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))∧(UIncreasing(COND_3602_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 ⇒ (UIncreasing(COND_3602_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 ⇒ (UIncreasing(COND_3602_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 ⇒ (UIncreasing(COND_3602_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 ⇒ (UIncreasing(COND_3602_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_3602_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3602_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1)) the following chains were created:
  • We consider the chain 3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3602_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))), COND_3602_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3602_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1])), 3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3602_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]))=TRUEx2[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]1java.lang.Object(x1[1])=java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))) ⇒ COND_3602_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥NonInfC∧COND_3602_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1]))))≥3602_0_FINDR_FIELDACCESS(x2[1], java.lang.Object(x1[1]))∧(UIncreasing(3602_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]))=TRUECOND_3602_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_3602_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))))))≥3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0]1, java.lang.Object(x1[0]1))))∧(UIncreasing(3602_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 ⇒ (UIncreasing(3602_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 ⇒ (UIncreasing(3602_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 ⇒ (UIncreasing(3602_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 ⇒ (UIncreasing(3602_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.
  • 3602_0_FINDR_FIELDACCESS(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → COND_3602_0_FINDR_FIELDACCESS(!(=(x0, x2)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1))))
    • (0 ≥ 0 ⇒ (UIncreasing(COND_3602_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_3602_0_FINDR_FIELDACCESS(TRUE, x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(x1)))) → 3602_0_FINDR_FIELDACCESS(x2, java.lang.Object(x1))
    • (0 ≥ 0 ⇒ (UIncreasing(3602_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 Pbound 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 Pbound.
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(3856_1_findR_InvokeMethod(x1, x2, x3)) = 0   
POL(3696_0_findR_Return(x1)) = 0   
POL(java.lang.Object(x1)) = [1] + [2]x1   
POL(DoublyLinkedList.DoublyLinkedList(x1, x2)) = [2]x2   
POL(3782_0_findR_Return) = 0   
POL(NULL) = 0   
POL(4425_0_findR_Return(x1)) = 0   
POL(3602_0_FINDR_FIELDACCESS(x1, x2)) = [1] + x2 + [2]x1   
POL(COND_3602_0_FINDR_FIELDACCESS(x1, x2, x3)) = [-1] + x3 + [2]x2 + [-1]x1   
POL(!(x1)) = 0   
POL(=(x1, x2)) = 0   

The following pairs are in P>:

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

The following pairs are in Pbound:

3602_0_FINDR_FIELDACCESS(x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0])))) → COND_3602_0_FINDR_FIELDACCESS(!(=(x0[0], x2[0])), x2[0], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[0], java.lang.Object(x1[0]))))
COND_3602_0_FINDR_FIELDACCESS(TRUE, x2[1], java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0[1], java.lang.Object(x1[1])))) → 3602_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:

FALSE1!(TRUE)1
TRUE1!(FALSE)1

(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:
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0) → 3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1) → 3782_0_findR_Return
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0) → 4425_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2) → 4425_0_findR_Return(NULL)
3856_1_findR_InvokeMethod(4425_0_findR_Return(x0), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x3, x4)))))), x5) → 4425_0_findR_Return(x0)

The integer pair graph is empty.

The set Q consists of the following terms:
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)), x0)
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, NULL)), x1)
3856_1_findR_InvokeMethod(3696_0_findR_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, x1)))), x0)
3856_1_findR_InvokeMethod(3782_0_findR_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1, NULL)))), x2)
3856_1_findR_InvokeMethod(4425_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:
3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(o3047sub), java.lang.Object(o3047sub)) → 3599_0_getFirst_FieldAccess(EOS(STATIC_3599), java.lang.Object(o3047sub), java.lang.Object(o3047sub))
3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(o3047sub), java.lang.Object(o3047sub)) → 3600_0_getFirst_FieldAccess(EOS(STATIC_3600), java.lang.Object(o3047sub), java.lang.Object(o3047sub))
3599_0_getFirst_FieldAccess(EOS(STATIC_3599), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063))) → 3606_0_getFirst_FieldAccess(EOS(STATIC_3606), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)))
3606_0_getFirst_FieldAccess(EOS(STATIC_3606), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063))) → 3615_0_getFirst_NONNULL(EOS(STATIC_3615), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3063)), o3063)
3615_0_getFirst_NONNULL(EOS(STATIC_3615), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))), java.lang.Object(o3090sub)) → 3627_0_getFirst_NONNULL(EOS(STATIC_3627), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))), java.lang.Object(o3090sub))
3627_0_getFirst_NONNULL(EOS(STATIC_3627), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))), java.lang.Object(o3090sub)) → 3639_0_getFirst_Load(EOS(STATIC_3639), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))))
3639_0_getFirst_Load(EOS(STATIC_3639), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub)))) → 3659_0_getFirst_FieldAccess(EOS(STATIC_3659), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub))))
3659_0_getFirst_FieldAccess(EOS(STATIC_3659), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3090sub)))) → 3675_0_getFirst_InvokeMethod(EOS(STATIC_3675), java.lang.Object(o3090sub))
3675_0_getFirst_InvokeMethod(EOS(STATIC_3675), java.lang.Object(o3090sub)) → 3692_1_getFirst_InvokeMethod(3692_0_getFirst_Load(EOS(STATIC_3692), java.lang.Object(o3090sub)), java.lang.Object(o3090sub))
3692_0_getFirst_Load(EOS(STATIC_3692), java.lang.Object(o3090sub)) → 3709_0_getFirst_Load(EOS(STATIC_3709), java.lang.Object(o3090sub))
3709_0_getFirst_Load(EOS(STATIC_3709), java.lang.Object(o3090sub)) → 3736_0_getFirst_Load(EOS(STATIC_3736), java.lang.Object(o3090sub))
3736_0_getFirst_Load(EOS(STATIC_3736), java.lang.Object(o3177sub)) → 3751_0_getFirst_Load(EOS(STATIC_3751), java.lang.Object(o3177sub))
3751_0_getFirst_Load(EOS(STATIC_3751), java.lang.Object(o3177sub)) → 3581_0_getFirst_Load(EOS(STATIC_3581), java.lang.Object(o3177sub))
3581_0_getFirst_Load(EOS(STATIC_3581), java.lang.Object(o3047sub)) → 3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(o3047sub), java.lang.Object(o3047sub))
3600_0_getFirst_FieldAccess(EOS(STATIC_3600), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066))) → 3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)))
3607_0_getFirst_FieldAccess(EOS(STATIC_3607), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066))) → 3618_0_getFirst_NONNULL(EOS(STATIC_3618), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3066)), o3066)
3618_0_getFirst_NONNULL(EOS(STATIC_3618), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))), java.lang.Object(o3091sub)) → 3629_0_getFirst_NONNULL(EOS(STATIC_3629), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))), java.lang.Object(o3091sub))
3629_0_getFirst_NONNULL(EOS(STATIC_3629), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))), java.lang.Object(o3091sub)) → 3642_0_getFirst_Load(EOS(STATIC_3642), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))))
3642_0_getFirst_Load(EOS(STATIC_3642), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub)))) → 3661_0_getFirst_FieldAccess(EOS(STATIC_3661), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub))))
3661_0_getFirst_FieldAccess(EOS(STATIC_3661), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(o3091sub)))) → 3677_0_getFirst_InvokeMethod(EOS(STATIC_3677), java.lang.Object(o3091sub))
3677_0_getFirst_InvokeMethod(EOS(STATIC_3677), java.lang.Object(o3091sub)) → 3693_1_getFirst_InvokeMethod(3693_0_getFirst_Load(EOS(STATIC_3693), java.lang.Object(o3091sub)), java.lang.Object(o3091sub))
3693_0_getFirst_Load(EOS(STATIC_3693), java.lang.Object(o3091sub)) → 3711_0_getFirst_Load(EOS(STATIC_3711), java.lang.Object(o3091sub))
3711_0_getFirst_Load(EOS(STATIC_3711), java.lang.Object(o3091sub)) → 3754_0_getFirst_Load(EOS(STATIC_3754), java.lang.Object(o3091sub))
3754_0_getFirst_Load(EOS(STATIC_3754), java.lang.Object(o3091sub)) → 3581_0_getFirst_Load(EOS(STATIC_3581), java.lang.Object(o3091sub))
R rules:
3615_0_getFirst_NONNULL(EOS(STATIC_3615), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3628_0_getFirst_NONNULL(EOS(STATIC_3628), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3618_0_getFirst_NONNULL(EOS(STATIC_3618), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3630_0_getFirst_NONNULL(EOS(STATIC_3630), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL)
3628_0_getFirst_NONNULL(EOS(STATIC_3628), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3640_0_getFirst_Load(EOS(STATIC_3640), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3630_0_getFirst_NONNULL(EOS(STATIC_3630), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), NULL) → 3644_0_getFirst_Load(EOS(STATIC_3644), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3640_0_getFirst_Load(EOS(STATIC_3640), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3660_0_getFirst_Return(EOS(STATIC_3660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3644_0_getFirst_Load(EOS(STATIC_3644), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3663_0_getFirst_Return(EOS(STATIC_3663), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3660_0_getFirst_Return(EOS(STATIC_3660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3797_0_getFirst_Return(EOS(STATIC_3797), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3663_0_getFirst_Return(EOS(STATIC_3663), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3811_0_getFirst_Return(EOS(STATIC_3811), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3907_0_getFirst_Return(EOS(STATIC_3907), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3924_0_getFirst_Return(EOS(STATIC_3924), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(o3763sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115))))))) → 4380_0_getFirst_Return(EOS(STATIC_4380), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115)))))), java.lang.Object(o3763sub))
3692_1_getFirst_InvokeMethod(4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(o3838sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144))))))) → 4405_0_getFirst_Return(EOS(STATIC_4405), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144)))))), java.lang.Object(o3838sub))
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return(EOS(STATIC_3660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3813_0_getFirst_Return(EOS(STATIC_3813), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(3663_0_getFirst_Return(EOS(STATIC_3663), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3820_0_getFirst_Return(EOS(STATIC_3820), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3908_0_getFirst_Return(EOS(STATIC_3908), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 3934_0_getFirst_Return(EOS(STATIC_3934), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(o3763sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124))))))) → 4387_0_getFirst_Return(EOS(STATIC_4387), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124)))))), java.lang.Object(o3763sub))
3693_1_getFirst_InvokeMethod(4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(o3838sub)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153))))))) → 4412_0_getFirst_Return(EOS(STATIC_4412), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153)))))), java.lang.Object(o3838sub))
3797_0_getFirst_Return(EOS(STATIC_3797), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3812_0_getFirst_Return(EOS(STATIC_3812), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3811_0_getFirst_Return(EOS(STATIC_3811), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3812_0_getFirst_Return(EOS(STATIC_3812), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3812_0_getFirst_Return(EOS(STATIC_3812), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3813_0_getFirst_Return(EOS(STATIC_3813), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3820_0_getFirst_Return(EOS(STATIC_3820), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3813_0_getFirst_Return(EOS(STATIC_3813), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3907_0_getFirst_Return(EOS(STATIC_3907), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3925_0_getFirst_Return(EOS(STATIC_3925), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3908_0_getFirst_Return(EOS(STATIC_3908), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4143_0_getFirst_Return(EOS(STATIC_4143), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3924_0_getFirst_Return(EOS(STATIC_3924), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3925_0_getFirst_Return(EOS(STATIC_3925), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3925_0_getFirst_Return(EOS(STATIC_3925), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 4121_0_getFirst_Return(EOS(STATIC_4121), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3934_0_getFirst_Return(EOS(STATIC_3934), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3908_0_getFirst_Return(EOS(STATIC_3908), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
4121_0_getFirst_Return(EOS(STATIC_4121), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3695)))), java.lang.Object(o3698sub)) → 4189_0_getFirst_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3695)))), java.lang.Object(o3698sub))
4143_0_getFirst_Return(EOS(STATIC_4143), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3760)))), java.lang.Object(o3763sub)) → 4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(o3763sub))
4189_0_getFirst_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o3835)))), java.lang.Object(o3838sub)) → 4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(o3838sub))
4380_0_getFirst_Return(EOS(STATIC_4380), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115)))))), java.lang.Object(o3763sub)) → 4189_0_getFirst_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4115)))))), java.lang.Object(o3763sub))
4387_0_getFirst_Return(EOS(STATIC_4387), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124)))))), java.lang.Object(o3763sub)) → 4143_0_getFirst_Return(EOS(STATIC_4143), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4124)))))), java.lang.Object(o3763sub))
4405_0_getFirst_Return(EOS(STATIC_4405), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144)))))), java.lang.Object(o3838sub)) → 4189_0_getFirst_Return(EOS(STATIC_4189), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4144)))))), java.lang.Object(o3838sub))
4412_0_getFirst_Return(EOS(STATIC_4412), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153)))))), java.lang.Object(o3838sub)) → 4143_0_getFirst_Return(EOS(STATIC_4143), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, o4153)))))), java.lang.Object(o3838sub))

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


P rules:
3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3692_1_getFirst_InvokeMethod(3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(x0)))) → 3693_1_getFirst_InvokeMethod(3591_0_getFirst_FieldAccess(EOS(STATIC_3591), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return(EOS(STATIC_3660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(3663_0_getFirst_Return(EOS(STATIC_3663), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3660_0_getFirst_Return(EOS(STATIC_3660), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3663_0_getFirst_Return(EOS(STATIC_3663), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))) → 3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3693_1_getFirst_InvokeMethod(4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(x0))
3693_1_getFirst_InvokeMethod(4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(x0))
3692_1_getFirst_InvokeMethod(4233_0_getFirst_Return(EOS(STATIC_4233), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(x0))
3692_1_getFirst_InvokeMethod(4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, x1))))))) → 4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(x0))
3692_1_getFirst_InvokeMethod(3836_0_getFirst_Return(EOS(STATIC_3836), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))
3692_1_getFirst_InvokeMethod(3840_0_getFirst_Return(EOS(STATIC_3840), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL))))) → 4239_0_getFirst_Return(EOS(STATIC_4239), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC, NULL)))

Filtered ground terms:



3591_0_getFirst_FieldAccess(x1, x2, x3) → 3591_0_getFirst_FieldAccess(x2, x3)
DoublyLinkedList.DoublyLinkedList(x1, x2) → DoublyLinkedList.DoublyLinkedList(x2)
4239_0_getFirst_Return(x1, x2) → 4239_0_getFirst_Return(x2)
3840_0_getFirst_Return(x1, x2) → 3840_0_getFirst_Return
3836_0_getFirst_Return(x1, x2) → 3836_0_getFirst_Return
4233_0_getFirst_Return(x1, x2) → 4233_0_getFirst_Return(x2)
3663_0_getFirst_Return(x1, x2, x3) → 3663_0_getFirst_Return
3660_0_getFirst_Return(x1, x2, x3) → 3660_0_getFirst_Return

Filtered duplicate args:



3591_0_getFirst_FieldAccess(x1, x2) → 3591_0_getFirst_FieldAccess(x2)

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


P rules:
3591_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3692_1_getFirst_InvokeMethod(3591_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
3591_0_getFirst_FieldAccess(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3693_1_getFirst_InvokeMethod(3591_0_getFirst_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3840_0_getFirst_Return
3693_1_getFirst_InvokeMethod(3663_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3840_0_getFirst_Return
3692_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3836_0_getFirst_Return
3692_1_getFirst_InvokeMethod(3663_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3836_0_getFirst_Return
3693_1_getFirst_InvokeMethod(3836_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(3840_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(4233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4233_0_getFirst_Return(java.lang.Object(x0))
3693_1_getFirst_InvokeMethod(4239_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4233_0_getFirst_Return(java.lang.Object(x0))
3692_1_getFirst_InvokeMethod(4233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4239_0_getFirst_Return(java.lang.Object(x0))
3692_1_getFirst_InvokeMethod(4239_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4239_0_getFirst_Return(java.lang.Object(x0))
3692_1_getFirst_InvokeMethod(3836_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4239_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3692_1_getFirst_InvokeMethod(3840_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4239_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))

Performed bisimulation on rules. Used the following equivalence classes: {[3693_1_getFirst_InvokeMethod_2, 3692_1_getFirst_InvokeMethod_2]=3693_1_getFirst_InvokeMethod_2, [3660_0_getFirst_Return, 3840_0_getFirst_Return, 3663_0_getFirst_Return, 3836_0_getFirst_Return]=3660_0_getFirst_Return, [4233_0_getFirst_Return_1, 4239_0_getFirst_Return_1]=4233_0_getFirst_Return_1}


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


P rules:
3591_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0)))) → 3591_0_GETFIRST_FIELDACCESS(java.lang.Object(x0))
R rules:
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3660_0_getFirst_Return
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(4233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4233_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:
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3660_0_getFirst_Return
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(4233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4233_0_getFirst_Return(java.lang.Object(x0))

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

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

The TRS R consists of the following rules:

3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))) → 3660_0_getFirst_Return
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL))))) → 4233_0_getFirst_Return(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(4233_0_getFirst_Return(java.lang.Object(x0)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(x1))))))) → 4233_0_getFirst_Return(java.lang.Object(x0))

The set Q consists of the following terms:

3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3693_1_getFirst_InvokeMethod(4233_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:

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

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

3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3693_1_getFirst_InvokeMethod(4233_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].

3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))
3693_1_getFirst_InvokeMethod(3660_0_getFirst_Return, java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(DoublyLinkedList.DoublyLinkedList(NULL)))))
3693_1_getFirst_InvokeMethod(4233_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:

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

  • 3591_0_GETFIRST_FIELDACCESS(java.lang.Object(DoublyLinkedList.DoublyLinkedList(java.lang.Object(x0[0])))) → 3591_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:
3404_0_createList_Load(EOS(STATIC_3404(i1784)), i193, o2894, i1785, i1785) → 3417_0_createList_GE(EOS(STATIC_3417(i1784)), i193, o2894, i1785, i1785, i193)
3417_0_createList_GE(EOS(STATIC_3417(i1784)), i193, o2894, i1785, i1785, i193) → 3433_0_createList_GE(EOS(STATIC_3433(i1784)), i193, o2894, i1785, i1785, i193)
3433_0_createList_GE(EOS(STATIC_3433(i1784)), i193, o2894, i1785, i1785, i193) → 3453_0_createList_Load(EOS(STATIC_3453(i1784)), i193, o2894, i1785) | <(i1785, i193)
3453_0_createList_Load(EOS(STATIC_3453(i1784)), i193, o2894, i1785) → 3483_0_createList_Store(EOS(STATIC_3483(i1784)), i193, i1785, o2894)
3483_0_createList_Store(EOS(STATIC_3483(i1784)), i193, i1785, o2894) → 3506_0_createList_New(EOS(STATIC_3506(i1784)), i193, i1785, o2894)
3506_0_createList_New(EOS(STATIC_3506(i1784)), i193, i1785, o2894) → 3521_0_createList_Duplicate(EOS(STATIC_3521(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3521_0_createList_Duplicate(EOS(STATIC_3521(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3546_0_createList_InvokeMethod(EOS(STATIC_3546(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3546_0_createList_InvokeMethod(EOS(STATIC_3546(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3554_0_random_FieldAccess(EOS(STATIC_3554(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3554_0_random_FieldAccess(EOS(STATIC_3554(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3576_0_random_ArrayLength(EOS(STATIC_3576(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)))
3576_0_random_ArrayLength(EOS(STATIC_3576(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191))) → 3589_0_random_FieldAccess(EOS(STATIC_3589(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191) | >=(i191, 0)
3589_0_random_FieldAccess(EOS(STATIC_3589(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191) → 3597_0_random_GT(EOS(STATIC_3597(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784)
3597_0_random_GT(EOS(STATIC_3597(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784) → 3604_0_random_GT(EOS(STATIC_3604(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784)
3597_0_random_GT(EOS(STATIC_3597(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784) → 3605_0_random_GT(EOS(STATIC_3605(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784)
3604_0_random_GT(EOS(STATIC_3604(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784) → 3612_0_random_FieldAccess(EOS(STATIC_3612(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | >(i191, i1784)
3612_0_random_FieldAccess(EOS(STATIC_3612(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3624_0_random_FieldAccess(EOS(STATIC_3624(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)))
3624_0_random_FieldAccess(EOS(STATIC_3624(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191))) → 3636_0_random_ArrayAccess(EOS(STATIC_3636(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i1784)
3636_0_random_ArrayAccess(EOS(STATIC_3636(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i1784) → 3656_0_random_ArrayAccess(EOS(STATIC_3656(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i1784)
3656_0_random_ArrayAccess(EOS(STATIC_3656(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(ARRAY(i191)), i1784) → 3673_0_random_Store(EOS(STATIC_3673(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) | <(i1784, i191)
3673_0_random_Store(EOS(STATIC_3673(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) → 3689_0_random_FieldAccess(EOS(STATIC_3689(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127)
3689_0_random_FieldAccess(EOS(STATIC_3689(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) → 3705_0_random_ConstantStackPush(EOS(STATIC_3705(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784)
3705_0_random_ConstantStackPush(EOS(STATIC_3705(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784) → 3728_0_random_IntArithmetic(EOS(STATIC_3728(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784, 1)
3728_0_random_IntArithmetic(EOS(STATIC_3728(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1784, matching1) → 3747_0_random_FieldAccess(EOS(STATIC_3747(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, +(i1784, 1)) | &&(>=(i1784, 0), =(matching1, 1))
3747_0_random_FieldAccess(EOS(STATIC_3747(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, i1907) → 3765_0_random_Load(EOS(STATIC_3765(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127)
3765_0_random_Load(EOS(STATIC_3765(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127) → 3794_0_random_NONNULL(EOS(STATIC_3794(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o3127, o3127)
3794_0_random_NONNULL(EOS(STATIC_3794(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub), java.lang.Object(o3282sub)) → 3832_0_random_NONNULL(EOS(STATIC_3832(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub), java.lang.Object(o3282sub))
3794_0_random_NONNULL(EOS(STATIC_3794(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3833_0_random_NONNULL(EOS(STATIC_3833(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL)
3832_0_random_NONNULL(EOS(STATIC_3832(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub), java.lang.Object(o3282sub)) → 3847_0_random_Load(EOS(STATIC_3847(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub))
3847_0_random_Load(EOS(STATIC_3847(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub)) → 3867_0_random_InvokeMethod(EOS(STATIC_3867(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub))
3867_0_random_InvokeMethod(EOS(STATIC_3867(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub)) → 3903_0_length_Load(EOS(STATIC_3903(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub), java.lang.Object(o3282sub))
3903_0_length_Load(EOS(STATIC_3903(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub), java.lang.Object(o3282sub)) → 3995_0_length_FieldAccess(EOS(STATIC_3995(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(o3282sub), java.lang.Object(o3282sub))
3995_0_length_FieldAccess(EOS(STATIC_3995(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), java.lang.Object(java.lang.String(o3578sub, i2130))) → 4028_0_length_FieldAccess(EOS(STATIC_4028(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), java.lang.Object(java.lang.String(o3578sub, i2130))) | &&(>=(i2130, 0), >=(i2131, 0))
4028_0_length_FieldAccess(EOS(STATIC_4028(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), java.lang.Object(java.lang.String(o3578sub, i2130))) → 4092_0_length_Return(EOS(STATIC_4092(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), i2130)
4092_0_length_Return(EOS(STATIC_4092(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(java.lang.String(o3578sub, i2130)), i2130) → 4223_0_random_Return(EOS(STATIC_4223(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4223_0_random_Return(EOS(STATIC_4223(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4251_0_createList_InvokeMethod(EOS(STATIC_4251(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4251_0_createList_InvokeMethod(EOS(STATIC_4251(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4279_0_<init>_Load(EOS(STATIC_4279(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4279_0_<init>_Load(EOS(STATIC_4279(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4438_0_<init>_InvokeMethod(EOS(STATIC_4438(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4438_0_<init>_InvokeMethod(EOS(STATIC_4438(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4471_0_<init>_Load(EOS(STATIC_4471(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4471_0_<init>_Load(EOS(STATIC_4471(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4529_0_<init>_Load(EOS(STATIC_4529(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4529_0_<init>_Load(EOS(STATIC_4529(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4574_0_<init>_FieldAccess(EOS(STATIC_4574(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4574_0_<init>_FieldAccess(EOS(STATIC_4574(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4589_0_<init>_Return(EOS(STATIC_4589(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130)
4589_0_<init>_Return(EOS(STATIC_4589(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2130) → 4600_0_createList_Store(EOS(STATIC_4600(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4600_0_createList_Store(EOS(STATIC_4600(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4612_0_createList_Load(EOS(STATIC_4612(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
4612_0_createList_Load(EOS(STATIC_4612(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 4622_0_createList_Load(EOS(STATIC_4622(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4622_0_createList_Load(EOS(STATIC_4622(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4631_0_createList_FieldAccess(EOS(STATIC_4631(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894)
4631_0_createList_FieldAccess(EOS(STATIC_4631(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894) → 4644_0_createList_Load(EOS(STATIC_4644(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
4644_0_createList_Load(EOS(STATIC_4644(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 4675_0_createList_NULL(EOS(STATIC_4675(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, o2894)
4675_0_createList_NULL(EOS(STATIC_4675(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(o5022sub)) → 4749_0_createList_NULL(EOS(STATIC_4749(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(o5022sub))
4675_0_createList_NULL(EOS(STATIC_4675(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4750_0_createList_NULL(EOS(STATIC_4750(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL)
4749_0_createList_NULL(EOS(STATIC_4749(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(o5022sub)) → 4782_0_createList_Load(EOS(STATIC_4782(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub))
4782_0_createList_Load(EOS(STATIC_4782(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub)) → 4795_0_createList_Load(EOS(STATIC_4795(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub))
4795_0_createList_Load(EOS(STATIC_4795(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub)) → 4804_0_createList_FieldAccess(EOS(STATIC_4804(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o5022sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4804_0_createList_FieldAccess(EOS(STATIC_4804(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4814_0_createList_FieldAccess(EOS(STATIC_4814(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4814_0_createList_FieldAccess(EOS(STATIC_4814(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4823_0_createList_Inc(EOS(STATIC_4823(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4823_0_createList_Inc(EOS(STATIC_4823(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4830_0_createList_JMP(EOS(STATIC_4830(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4830_0_createList_JMP(EOS(STATIC_4830(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930) → 4837_0_createList_Load(EOS(STATIC_4837(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930)
4837_0_createList_Load(EOS(STATIC_4837(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930) → 3390_0_createList_Load(EOS(STATIC_3390(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2930)
3390_0_createList_Load(EOS(STATIC_3390(i1784)), i193, o2894, i1785) → 3404_0_createList_Load(EOS(STATIC_3404(i1784)), i193, o2894, i1785, i1785)
4750_0_createList_NULL(EOS(STATIC_4750(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4783_0_createList_Inc(EOS(STATIC_4783(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4783_0_createList_Inc(EOS(STATIC_4783(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4796_0_createList_JMP(EOS(STATIC_4796(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4796_0_createList_JMP(EOS(STATIC_4796(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2911) → 4806_0_createList_Load(EOS(STATIC_4806(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2911)
4806_0_createList_Load(EOS(STATIC_4806(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2911) → 3390_0_createList_Load(EOS(STATIC_3390(i1907)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2911)
3833_0_random_NONNULL(EOS(STATIC_3833(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, NULL) → 3849_0_random_ConstantStackPush(EOS(STATIC_3849(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL)
3849_0_random_ConstantStackPush(EOS(STATIC_3849(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL) → 3869_0_random_Return(EOS(STATIC_3869(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, 0)
3869_0_random_Return(EOS(STATIC_3869(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), NULL, matching1) → 3904_0_createList_InvokeMethod(EOS(STATIC_3904(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3904_0_createList_InvokeMethod(EOS(STATIC_3904(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 4251_0_createList_InvokeMethod(EOS(STATIC_4251(i1907)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3605_0_random_GT(EOS(STATIC_3605(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i191, i1784) → 3613_0_random_ConstantStackPush(EOS(STATIC_3613(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | <=(i191, i1784)
3613_0_random_ConstantStackPush(EOS(STATIC_3613(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3626_0_random_Return(EOS(STATIC_3626(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0)
3626_0_random_Return(EOS(STATIC_3626(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3637_0_createList_InvokeMethod(EOS(STATIC_3637(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3637_0_createList_InvokeMethod(EOS(STATIC_3637(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3658_0_<init>_Load(EOS(STATIC_3658(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | =(matching1, 0)
3658_0_<init>_Load(EOS(STATIC_3658(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3690_0_<init>_InvokeMethod(EOS(STATIC_3690(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3690_0_<init>_InvokeMethod(EOS(STATIC_3690(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3708_0_<init>_Load(EOS(STATIC_3708(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3708_0_<init>_Load(EOS(STATIC_3708(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3730_0_<init>_Load(EOS(STATIC_3730(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | &&(=(matching1, 0), =(matching2, 0))
3730_0_<init>_Load(EOS(STATIC_3730(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, matching2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3749_0_<init>_FieldAccess(EOS(STATIC_3749(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3749_0_<init>_FieldAccess(EOS(STATIC_3749(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching2) → 3768_0_<init>_Return(EOS(STATIC_3768(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), 0) | &&(=(matching1, 0), =(matching2, 0))
3768_0_<init>_Return(EOS(STATIC_3768(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), matching1) → 3796_0_createList_Store(EOS(STATIC_3796(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) | =(matching1, 0)
3796_0_createList_Store(EOS(STATIC_3796(i1784)), i193, i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3835_0_createList_Load(EOS(STATIC_3835(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
3835_0_createList_Load(EOS(STATIC_3835(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 3851_0_createList_Load(EOS(STATIC_3851(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
3851_0_createList_Load(EOS(STATIC_3851(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3871_0_createList_FieldAccess(EOS(STATIC_3871(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894)
3871_0_createList_FieldAccess(EOS(STATIC_3871(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), o2894) → 3906_0_createList_Load(EOS(STATIC_3906(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894)
3906_0_createList_Load(EOS(STATIC_3906(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894) → 3963_0_createList_NULL(EOS(STATIC_3963(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, o2894, o2894)
3963_0_createList_NULL(EOS(STATIC_3963(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(o3506sub)) → 3998_0_createList_NULL(EOS(STATIC_3998(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(o3506sub))
3963_0_createList_NULL(EOS(STATIC_3963(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 3999_0_createList_NULL(EOS(STATIC_3999(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL)
3998_0_createList_NULL(EOS(STATIC_3998(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(o3506sub)) → 4030_0_createList_Load(EOS(STATIC_4030(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub))
4030_0_createList_Load(EOS(STATIC_4030(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub)) → 4096_0_createList_Load(EOS(STATIC_4096(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub))
4096_0_createList_Load(EOS(STATIC_4096(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub)) → 4227_0_createList_FieldAccess(EOS(STATIC_4227(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(o3506sub), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4227_0_createList_FieldAccess(EOS(STATIC_4227(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4254_0_createList_FieldAccess(EOS(STATIC_4254(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)))
4254_0_createList_FieldAccess(EOS(STATIC_4254(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 4285_0_createList_Inc(EOS(STATIC_4285(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4285_0_createList_Inc(EOS(STATIC_4285(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4373_0_createList_JMP(EOS(STATIC_4373(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4373_0_createList_JMP(EOS(STATIC_4373(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469) → 4443_0_createList_Load(EOS(STATIC_4443(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469)
4443_0_createList_Load(EOS(STATIC_4443(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469) → 3390_0_createList_Load(EOS(STATIC_3390(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2469)
3999_0_createList_NULL(EOS(STATIC_3999(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785, NULL, NULL) → 4032_0_createList_Inc(EOS(STATIC_4032(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785)
4032_0_createList_Inc(EOS(STATIC_4032(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i1785) → 4097_0_createList_JMP(EOS(STATIC_4097(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(i1785, 1))
4097_0_createList_JMP(EOS(STATIC_4097(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195) → 4229_0_createList_Load(EOS(STATIC_4229(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195)
4229_0_createList_Load(EOS(STATIC_4229(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195) → 3390_0_createList_Load(EOS(STATIC_3390(i1784)), i193, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), i2195)
R rules:

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


P rules:
3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, x2, x3, x3) → 4675_0_createList_NULL(EOS(STATIC_4675(+(x0, 1))), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x3, x2, x2) | &&(<(x3, x1), >(+(x0, 1), 0))
4675_0_createList_NULL(EOS(STATIC_4675(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC))) → 3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
4675_0_createList_NULL(EOS(STATIC_4675(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, NULL, NULL) → 3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1))
3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), x2, x2) → 3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, java.lang.Object(DoublyLinkedList.DoublyLinkedList(EOC)), +(x2, 1), +(x2, 1)) | <(x2, x1)
3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, NULL, x2, x2) → 3404_0_createList_Load(EOS(STATIC_3404(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_3404_0_createList_Load2(x1, x2, x3, x4, x5, x6) → Cond_3404_0_createList_Load2(x1, x2, x3, x5, x6)
Cond_3404_0_createList_Load1(x1, x2, x3, x4, x5, x6) → Cond_3404_0_createList_Load1(x1, x2, x3, x5, x6)
4675_0_createList_NULL(x1, x2, x3, x4, x5, x6) → 4675_0_createList_NULL(x1, x2, x4, x5, x6)

Filtered duplicate args:



3404_0_createList_Load(x1, x2, x3, x4, x5) → 3404_0_createList_Load(x1, x2, x3, x5)
Cond_3404_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_3404_0_createList_Load(x1, x2, x3, x4, x6)
4675_0_createList_NULL(x1, x2, x3, x4, x5) → 4675_0_createList_NULL(x1, x2, x3, x5)
Cond_3404_0_createList_Load1(x1, x2, x3, x4, x5) → Cond_3404_0_createList_Load1(x1, x2, x3, x5)
Cond_3404_0_createList_Load2(x1, x2, x3, x4, x5) → Cond_3404_0_createList_Load2(x1, x2, x3, x5)

Filtered all non-integer terms:



4675_0_createList_NULL(x1, x2, x3, x4) → 4675_0_createList_NULL(x1, x2, x3)
3404_0_createList_Load(x1, x2, x3, x4) → 3404_0_createList_Load(x1, x2, x4)

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


P rules:
3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, x2) → 3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, +(x2, 1)) | <(x2, x1)
3404_0_createList_Load(EOS(STATIC_3404(x0)), x1, x2) → 3404_0_createList_Load(EOS(STATIC_3404(+(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:
3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, x2) → COND_3404_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3404(x0)), x1, x2)
COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0)), x1, x2) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, +(x2, 1))
3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, x2) → COND_3404_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3404(x0)), x1, x2)
COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0)), x1, x2) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(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): 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0]) → COND_3404_0_CREATELIST_LOAD(x2[0] < x1[0], EOS(STATIC_3404(x0[0])), x1[0], x2[0])
(1): COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], x2[1] + 1)
(2): 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2]) → COND_3404_0_CREATELIST_LOAD1(x2[2] < x1[2] && x0[2] > -1, EOS(STATIC_3404(x0[2])), x1[2], x2[2])
(3): COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[3] + 1)), x1[3], x2[3] + 1)

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


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


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


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


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


(3) -> (2), if (EOS(STATIC_3404(x0[3] + 1)) →* EOS(STATIC_3404(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@53cf39d5 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 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, x2) → COND_3404_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3404(x0)), x1, x2) the following chains were created:
  • We consider the chain 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0]) → COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0]), COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:

    (1)    (<(x2[0], x1[0])=TRUEEOS(STATIC_3404(x0[0]))=EOS(STATIC_3404(x0[1]))∧x1[0]=x1[1]x2[0]=x2[1]3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0])≥NonInfC∧3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0])≥COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])∧(UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(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])=TRUE3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0])≥NonInfC∧3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0])≥COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])∧(UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧[1 + (-1)bso_13] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    (x1[0] + [-1] + [-1]x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (x1[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)



    We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (8)    (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)


    (9)    (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)







For Pair COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0)), x1, x2) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, +(x2, 1)) the following chains were created:
  • We consider the chain COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1)) which results in the following constraint:

    (10)    (COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1])≥NonInfC∧COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1])≥3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))∧(UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))), ≥))



    We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (11)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (12)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (13)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (13) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (14)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)







For Pair 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, x2) → COND_3404_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3404(x0)), x1, x2) the following chains were created:
  • We consider the chain 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2]) → COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(x0[2])), x1[2], x2[2]), COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:

    (15)    (&&(<(x2[2], x1[2]), >(x0[2], -1))=TRUEEOS(STATIC_3404(x0[2]))=EOS(STATIC_3404(x0[3]))∧x1[2]=x1[3]x2[2]=x2[3]3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2])≥NonInfC∧3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2])≥COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(x0[2])), x1[2], x2[2])∧(UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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)=TRUE3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2])≥NonInfC∧3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2])≥COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(x0[2])), x1[2], x2[2])∧(UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0)), x1, x2) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0, 1))), x1, +(x2, 1)) the following chains were created:
  • We consider the chain COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0[3], 1))), x1[3], +(x2[3], 1)) which results in the following constraint:

    (23)    (COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3])≥NonInfC∧COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3])≥3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0[3], 1))), x1[3], +(x2[3], 1))∧(UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥))



    We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (24)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(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)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(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)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(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)    ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(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.
  • 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, x2) → COND_3404_0_CREATELIST_LOAD(<(x2, x1), EOS(STATIC_3404(x0)), x1, x2)
    • (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
    • (x1[0] ≥ 0∧x2[0] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])), ≥)∧0 = 0∧[(-1)Bound*bni_12 + bni_12] + [bni_12]x1[0] ≥ 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

  • COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0)), x1, x2) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, +(x2, 1))
    • ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

  • 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0)), x1, x2) → COND_3404_0_CREATELIST_LOAD1(&&(<(x2, x1), >(x0, -1)), EOS(STATIC_3404(x0)), x1, x2)
    • (x1[2] ≥ 0∧x0[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(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 ⇒ (UIncreasing(COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(x0[2])), x1[2], x2[2])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x1[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)

  • COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0)), x1, x2) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0, 1))), x1, +(x2, 1))
    • ((UIncreasing(3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0[3], 1))), x1[3], +(x2[3], 1))), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_19] ≥ 0)




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(3404_0_CREATELIST_LOAD(x1, x2, x3)) = [-1]x3 + x2   
POL(EOS(x1)) = x1   
POL(STATIC_3404(x1)) = x1   
POL(COND_3404_0_CREATELIST_LOAD(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(COND_3404_0_CREATELIST_LOAD1(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(-1) = [-1]   

The following pairs are in P>:

3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0]) → COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])
3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2]) → COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(x0[2])), x1[2], x2[2])

The following pairs are in Pbound:

3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[0])), x1[0], x2[0]) → COND_3404_0_CREATELIST_LOAD(<(x2[0], x1[0]), EOS(STATIC_3404(x0[0])), x1[0], x2[0])
3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[2])), x1[2], x2[2]) → COND_3404_0_CREATELIST_LOAD1(&&(<(x2[2], x1[2]), >(x0[2], -1)), EOS(STATIC_3404(x0[2])), x1[2], x2[2])

The following pairs are in P:

COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], +(x2[1], 1))
COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(+(x0[3], 1))), x1[3], +(x2[3], 1))

There are no usable rules.

(27) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_3404_0_CREATELIST_LOAD(TRUE, EOS(STATIC_3404(x0[1])), x1[1], x2[1]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[1])), x1[1], x2[1] + 1)
(3): COND_3404_0_CREATELIST_LOAD1(TRUE, EOS(STATIC_3404(x0[3])), x1[3], x2[3]) → 3404_0_CREATELIST_LOAD(EOS(STATIC_3404(x0[3] + 1)), x1[3], x2[3] + 1)


The set Q is empty.

(28) IDependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE