Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 726 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 512 ms)
        ↳7 intTRS
        ↳8 LinearRankingProcessor (⇔, 17 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 135 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇔, 1 ms)
        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:
package IntListSumRec;

public class IntListSumRec {
	public static void main(String[] args) {
		Random.args = args;
		List l = List.createList(Random.random());

		int sum = l.sumList();
	}
}

class List {
	int value;
	List next;

	public List(int v, List n) {
		this.value = v;
		this.next = n;
	}

	public int sumList() {
		if (this.next == null) {
			return this.value;
		} else {
			int firstTwo = this.value + this.next.value;
			List nextNext = this.next.next;
			List shorter = new List(firstTwo, nextNext);
			return shorter.sumList();
		}
	}

	public static List createList(int l) {
		if (l < 0) {
			return null;
		} else {
			return new List(Random.random(), createList(l - 1));
		}
	}
}

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

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


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

IntListSumRec.List.createList(I)LIntListSumRec/List;: Graph of 118 nodes with 0 SCCs.

IntListSumRec.List.sumList()I: Graph of 88 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: IntListSumRec.List.sumList()I
SCC calls the following helper methods: IntListSumRec.List.sumList()I
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • IntListSumRec.List: [next, value]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 70 IRules

P rules:
f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), java.lang.Object(IntListSumRec.List(EOC, o428, i478))) → f1643_0_sumList_NONNULL(EOS, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), o428)
f1643_0_sumList_NONNULL(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), java.lang.Object(o432sub)) → f1644_0_sumList_NONNULL(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), java.lang.Object(o432sub))
f1644_0_sumList_NONNULL(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), java.lang.Object(o432sub)) → f1647_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)))
f1647_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478))) → f1651_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)))
f1651_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478))) → f1654_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478)
f1654_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478) → f1657_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)))
f1657_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478))) → f1661_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478, java.lang.Object(o432sub))
f1661_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478, java.lang.Object(o432sub)) → f1679_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o432sub), i478)), i478, java.lang.Object(o432sub))
f1661_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o441sub), i478)), java.lang.Object(o441sub), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o441sub), i478)), i478, java.lang.Object(o441sub)) → f1681_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o441sub), i478)), java.lang.Object(o441sub), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(o441sub), i478)), i478, java.lang.Object(o441sub))
f1679_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, o445, i492))) → f1687_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, o445, i492)))
f1687_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, o445, i492))) → f1690_0_sumList_IntArithmetic(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i478, i492)
f1690_0_sumList_IntArithmetic(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i478, i492) → f1695_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), +(i478, i492))
f1695_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i495) → f1701_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i495)
f1701_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), i495) → f1706_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)))
f1706_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478))) → f1711_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, java.lang.Object(IntListSumRec.List(EOC, o445, i492)))
f1711_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, java.lang.Object(IntListSumRec.List(EOC, o445, i492))) → f1716_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445)
f1716_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445) → f1720_0_sumList_New(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445)
f1720_0_sumList_New(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445) → f1726_0_sumList_Duplicate(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)))
f1726_0_sumList_Duplicate(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1))) → f1729_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0))) | =(matching1, 0)
f1729_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2))) → f1732_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495) | &&(=(matching1, 0), =(matching2, 0))
f1732_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495) → f1738_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445) | &&(=(matching1, 0), =(matching2, 0))
f1738_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495, o445) → f1742_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445) | &&(=(matching1, 0), =(matching2, 0))
f1742_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i495, o445) → f1745_0__init__InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1745_0__init__InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching4))) → f1751_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1751_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i495, o445) → f1756_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1756_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching4))) → f1761_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), o445, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i495) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1761_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), o445, java.lang.Object(IntListSumRec.List(EOC, NULL, matching4)), i495) → f1767_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), o445) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1767_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), o445) → f1774_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), i495, o445, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)))
f1774_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), i495, o445, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, i495))) → f1779_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), o445)
f1779_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), i495, o445, java.lang.Object(IntListSumRec.List(EOC, NULL, i495)), o445) → f1787_0__init__Return(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), java.lang.Object(IntListSumRec.List(EOC, o445, i495)), i495, o445)
f1787_0__init__Return(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), java.lang.Object(IntListSumRec.List(EOC, o445, i495)), i495, o445) → f1793_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1793_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1797_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1797_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1801_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1801_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1806_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o445, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1801_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1806_1_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o445, i492)), i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1806_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o445, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1811_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o445, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1811_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o445, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1820_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o445, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1820_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o445, java.lang.Object(IntListSumRec.List(EOC, o445, i495))) → f1831_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o445, i495)), o429, java.lang.Object(IntListSumRec.List(EOC, o445, i495)))
f1831_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o429, i495)), o429, java.lang.Object(IntListSumRec.List(EOC, o429, i495))) → f1635_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o429, i495)), o429, java.lang.Object(IntListSumRec.List(EOC, o429, i495)))
f1635_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o428, i478))) → f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), o429, java.lang.Object(IntListSumRec.List(EOC, o428, i478)), java.lang.Object(IntListSumRec.List(EOC, o428, i478)))
f1681_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, o447, i493))) → f1688_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, o447, i493)))
f1688_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i478, java.lang.Object(IntListSumRec.List(EOC, o447, i493))) → f1693_0_sumList_IntArithmetic(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i478, i493)
f1693_0_sumList_IntArithmetic(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i478, i493) → f1699_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), +(i478, i493))
f1699_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i496) → f1703_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i496)
f1703_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), i496) → f1709_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)))
f1709_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478))) → f1714_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, java.lang.Object(IntListSumRec.List(EOC, o447, i493)))
f1714_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, java.lang.Object(IntListSumRec.List(EOC, o447, i493))) → f1718_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447)
f1718_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447) → f1724_0_sumList_New(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447)
f1724_0_sumList_New(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447) → f1728_0_sumList_Duplicate(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)))
f1728_0_sumList_Duplicate(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1))) → f1731_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0))) | =(matching1, 0)
f1731_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2))) → f1736_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496) | &&(=(matching1, 0), =(matching2, 0))
f1736_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496) → f1740_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447) | &&(=(matching1, 0), =(matching2, 0))
f1740_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496, o447) → f1744_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447) | &&(=(matching1, 0), =(matching2, 0))
f1744_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i496, o447) → f1749_0__init__InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1749_0__init__InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching4))) → f1755_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1755_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i496, o447) → f1759_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1759_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching4))) → f1765_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), o447, java.lang.Object(IntListSumRec.List(EOC, NULL, 0)), i496) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1765_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching1)), java.lang.Object(IntListSumRec.List(EOC, NULL, matching2)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching3)), o447, java.lang.Object(IntListSumRec.List(EOC, NULL, matching4)), i496) → f1772_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), o447) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1772_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), o447) → f1778_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), i496, o447, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, i496)))
f1778_0__init__Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), i496, o447, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, i496))) → f1782_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), o447)
f1782_0__init__FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), i496, o447, java.lang.Object(IntListSumRec.List(EOC, NULL, i496)), o447) → f1791_0__init__Return(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)), i496, o447)
f1791_0__init__Return(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)), i496, o447) → f1796_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1796_0_sumList_Store(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1800_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1800_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1804_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1804_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1809_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o447, java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1804_0_sumList_InvokeMethod(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1809_1_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, o447, i493)), i478)), java.lang.Object(IntListSumRec.List(EOC, o447, i493)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)), java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1809_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o447, java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1813_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o447, java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1813_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o447, java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1826_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o447, java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1826_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o447, java.lang.Object(IntListSumRec.List(EOC, o447, i496))) → f1837_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o447, i496)), o429, java.lang.Object(IntListSumRec.List(EOC, o447, i496)))
f1837_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o429, i496)), o429, java.lang.Object(IntListSumRec.List(EOC, o429, i496))) → f1635_0_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, o429, i496)), o429, java.lang.Object(IntListSumRec.List(EOC, o429, i496)))

Combined rules. Obtained 4 IRules

P rules:
f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), x3, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2))) → f1806_1_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), x3, java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))), java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))))
f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), x3, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2))) → f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))), x0, java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))), java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))))
f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, x0, x1)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2))) → f1809_1_sumList_Load(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, x0, x1)), java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))), java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))))
f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, x0, x1)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListSumRec.List(EOC, java.lang.Object(IntListSumRec.List(EOC, x0, x1)), x2))) → f1637_0_sumList_FieldAccess(EOS, java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))), x0, java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))), java.lang.Object(IntListSumRec.List(EOC, x0, +(x2, x1))))

Filtered ground terms:


f1637_0_sumList_FieldAccess(x1, x2, x3, x4, x5) → f1637_0_sumList_FieldAccess(x2, x3, x4, x5)
f1806_1_sumList_Load(x1, x2, x3, x4, x5) → f1806_1_sumList_Load(x2, x3, x4, x5)
f1809_1_sumList_Load(x1, x2, x3, x4, x5) → f1809_1_sumList_Load(x2, x3, x4, x5)
IntListSumRec.List(x1, x2, x3) → IntListSumRec.List(x2, x3)

Filtered duplicate terms:


f1637_0_sumList_FieldAccess(x1, x2, x3, x4) → f1637_0_sumList_FieldAccess(x2, x4)
f1806_1_sumList_Load(x1, x2, x3, x4) → f1806_1_sumList_Load(x1, x2, x4)
f1809_1_sumList_Load(x1, x2, x3, x4) → f1809_1_sumList_Load(x1, x4)

Filtered unneeded terms:


IntListSumRec.List(x1, x2) → IntListSumRec.List(x1)

Prepared 4 rules for path length conversion:

P rules:
f1637_0_sumList_FieldAccess(x3, java.lang.Object(IntListSumRec.List(java.lang.Object(IntListSumRec.List(x0))))) → f1806_1_sumList_Load(java.lang.Object(IntListSumRec.List(java.lang.Object(IntListSumRec.List(x0)))), x3, java.lang.Object(IntListSumRec.List(x0)))
f1637_0_sumList_FieldAccess(x3, java.lang.Object(IntListSumRec.List(java.lang.Object(IntListSumRec.List(x0))))) → f1637_0_sumList_FieldAccess(x0, java.lang.Object(IntListSumRec.List(x0)))
f1637_0_sumList_FieldAccess(java.lang.Object(IntListSumRec.List(x0)), java.lang.Object(IntListSumRec.List(java.lang.Object(IntListSumRec.List(x0))))) → f1809_1_sumList_Load(java.lang.Object(IntListSumRec.List(java.lang.Object(IntListSumRec.List(x0)))), java.lang.Object(IntListSumRec.List(x0)))
f1637_0_sumList_FieldAccess(java.lang.Object(IntListSumRec.List(x0)), java.lang.Object(IntListSumRec.List(java.lang.Object(IntListSumRec.List(x0))))) → f1637_0_sumList_FieldAccess(x0, java.lang.Object(IntListSumRec.List(x0)))

Finished conversion. Obtained 2 rules.

P rules:
f1637_0_sumList_FieldAccess(v8, v9) → f1637_0_sumList_FieldAccess(v10, v11) | &&(&&(&&(&&(&&(>=(v9, +(v11, 2)), >=(v9, +(v10, 3))), >(+(v9, 1), 3)), >(+(v8, 1), 0)), >(+(v10, 1), 0)), >(+(v11, 1), 1))
f1637_0_sumList_FieldAccess(v12, v13) → f1637_0_sumList_FieldAccess(v14, v15) | &&(&&(&&(&&(&&(&&(&&(>(+(v15, 1), 1), <=(v15, v12)), <=(+(v15, 2), v13)), >(+(v14, 1), 0)), <=(+(v14, 3), v13)), <=(+(v14, 1), v12)), >(+(v13, 1), 3)), >(+(v12, 1), 1))

(7) Obligation:

Rules:
f1637_0_sumList_FieldAccess(v8, v9) → f1637_0_sumList_FieldAccess(v10, v11) | &&(&&(&&(&&(&&(>=(v9, +(v11, 2)), >=(v9, +(v10, 3))), >(+(v9, 1), 3)), >(+(v8, 1), 0)), >(+(v10, 1), 0)), >(+(v11, 1), 1))
f1637_0_sumList_FieldAccess(v12, v13) → f1637_0_sumList_FieldAccess(v14, v15) | &&(&&(&&(&&(&&(&&(&&(>(+(v15, 1), 1), <=(v15, v12)), <=(+(v15, 2), v13)), >(+(v14, 1), 0)), <=(+(v14, 3), v13)), <=(+(v14, 1), v12)), >(+(v13, 1), 3)), >(+(v12, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f1637_0_sumList_FieldAccess(x)] = 1/2·x2

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


f1637_0_sumList_FieldAccess(x0, x1) → f1637_0_sumList_FieldAccess(x2, x3) | &&(&&(&&(&&(&&(>=(x1, +(x3, 2)), >=(x1, +(x2, 3))), >(+(x1, 1), 3)), >(+(x0, 1), 0)), >(+(x2, 1), 0)), >(+(x3, 1), 1))
f1637_0_sumList_FieldAccess(x4, x5) → f1637_0_sumList_FieldAccess(x6, x7) | &&(&&(&&(&&(&&(&&(&&(>(+(x7, 1), 1), <=(x7, x4)), <=(+(x7, 2), x5)), >(+(x6, 1), 0)), <=(+(x6, 3), x5)), <=(+(x6, 1), x4)), >(+(x5, 1), 3)), >(+(x4, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: IntListSumRec.List.createList(I)LIntListSumRec/List;
SCC calls the following helper methods: IntListSumRec.List.createList(I)LIntListSumRec/List;
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • java.lang.String: [count]
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 30 IRules

P rules:
f746_0_createList_GE(EOS, i122, i122, i122) → f749_0_createList_GE(EOS, i122, i122, i122)
f749_0_createList_GE(EOS, i122, i122, i122) → f753_0_createList_New(EOS, i122, i122) | >=(i122, 0)
f753_0_createList_New(EOS, i122, i122) → f756_0_createList_Duplicate(EOS, i122, i122)
f756_0_createList_Duplicate(EOS, i122, i122) → f759_0_createList_InvokeMethod(EOS, i122, i122)
f759_0_createList_InvokeMethod(EOS, i122, i122) → f766_0_random_FieldAccess(EOS, i122, i122)
f766_0_random_FieldAccess(EOS, i122, i122) → f770_0_random_FieldAccess(EOS, i122, i122, java.lang.Object(ARRAY(i41)))
f770_0_random_FieldAccess(EOS, i122, i122, java.lang.Object(ARRAY(i41))) → f772_0_random_ArrayAccess(EOS, i122, i122, java.lang.Object(ARRAY(i41)), i118)
f772_0_random_ArrayAccess(EOS, i122, i122, java.lang.Object(ARRAY(i41)), i118) → f774_0_random_ArrayAccess(EOS, i122, i122, java.lang.Object(ARRAY(i41)), i118)
f774_0_random_ArrayAccess(EOS, i122, i122, java.lang.Object(ARRAY(i41)), i118) → f777_0_random_Store(EOS, i122, i122, o119) | <(i118, i41)
f777_0_random_Store(EOS, i122, i122, o119) → f781_0_random_FieldAccess(EOS, i122, i122, o119)
f781_0_random_FieldAccess(EOS, i122, i122, o119) → f783_0_random_ConstantStackPush(EOS, i122, i122, o119, i118)
f783_0_random_ConstantStackPush(EOS, i122, i122, o119, i118) → f787_0_random_IntArithmetic(EOS, i122, i122, o119, i118, 1)
f787_0_random_IntArithmetic(EOS, i122, i122, o119, i118, matching1) → f791_0_random_FieldAccess(EOS, i122, i122, o119, +(i118, 1)) | &&(>(i118, 0), =(matching1, 1))
f791_0_random_FieldAccess(EOS, i122, i122, o119, i128) → f793_0_random_Load(EOS, i122, i122, o119)
f793_0_random_Load(EOS, i122, i122, o119) → f797_0_random_InvokeMethod(EOS, i122, i122, o119)
f797_0_random_InvokeMethod(EOS, i122, i122, java.lang.Object(o122sub)) → f801_0_random_InvokeMethod(EOS, i122, i122, java.lang.Object(o122sub))
f801_0_random_InvokeMethod(EOS, i122, i122, java.lang.Object(o122sub)) → f805_0_length_Load(EOS, i122, i122, java.lang.Object(o122sub), java.lang.Object(o122sub))
f805_0_length_Load(EOS, i122, i122, java.lang.Object(o122sub), java.lang.Object(o122sub)) → f816_0_length_FieldAccess(EOS, i122, i122, java.lang.Object(o122sub), java.lang.Object(o122sub))
f816_0_length_FieldAccess(EOS, i122, i122, java.lang.Object(java.lang.String(o127sub, i137)), java.lang.Object(java.lang.String(o127sub, i137))) → f819_0_length_FieldAccess(EOS, i122, i122, java.lang.Object(java.lang.String(o127sub, i137)), java.lang.Object(java.lang.String(o127sub, i137)))
f819_0_length_FieldAccess(EOS, i122, i122, java.lang.Object(java.lang.String(o127sub, i137)), java.lang.Object(java.lang.String(o127sub, i137))) → f825_0_length_Return(EOS, i122, i122, java.lang.Object(java.lang.String(o127sub, i137)))
f825_0_length_Return(EOS, i122, i122, java.lang.Object(java.lang.String(o127sub, i137))) → f830_0_random_Return(EOS, i122, i122)
f830_0_random_Return(EOS, i122, i122) → f832_0_createList_Load(EOS, i122, i122)
f832_0_createList_Load(EOS, i122, i122) → f838_0_createList_ConstantStackPush(EOS, i122, i122)
f838_0_createList_ConstantStackPush(EOS, i122, i122) → f844_0_createList_IntArithmetic(EOS, i122, i122, 1)
f844_0_createList_IntArithmetic(EOS, i122, i122, matching1) → f849_0_createList_InvokeMethod(EOS, i122, -(i122, 1)) | &&(>=(i122, 0), =(matching1, 1))
f849_0_createList_InvokeMethod(EOS, i122, i139) → f855_0_createList_Load(EOS, i139, i139)
f849_0_createList_InvokeMethod(EOS, i122, i139) → f855_1_createList_Load(EOS, i122, i139, i139)
f855_0_createList_Load(EOS, i139, i139) → f863_0_createList_Load(EOS, i139, i139)
f863_0_createList_Load(EOS, i139, i139) → f743_0_createList_Load(EOS, i139, i139)
f743_0_createList_Load(EOS, i119, i119) → f746_0_createList_GE(EOS, i119, i119, i119)

Combined rules. Obtained 2 IRules

P rules:
f746_0_createList_GE(EOS, x0, x0, x0) → f855_1_createList_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(+(x0, 1), 0)
f746_0_createList_GE(EOS, x0, x0, x0) → f746_0_createList_GE(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(+(x0, 1), 0)

Filtered ground terms:


f746_0_createList_GE(x1, x2, x3, x4) → f746_0_createList_GE(x2, x3, x4)
Cond_f746_0_createList_GE(x1, x2, x3, x4, x5) → Cond_f746_0_createList_GE(x1, x3, x4, x5)
f855_1_createList_Load(x1, x2, x3, x4) → f855_1_createList_Load(x2, x3, x4)
Cond_f746_0_createList_GE1(x1, x2, x3, x4, x5) → Cond_f746_0_createList_GE1(x1, x3, x4, x5)

Filtered duplicate terms:


f746_0_createList_GE(x1, x2, x3) → f746_0_createList_GE(x3)
Cond_f746_0_createList_GE(x1, x2, x3, x4) → Cond_f746_0_createList_GE(x1, x4)
f855_1_createList_Load(x1, x2, x3) → f855_1_createList_Load(x3)
Cond_f746_0_createList_GE1(x1, x2, x3, x4) → Cond_f746_0_createList_GE1(x1, x4)

Filtered unneeded terms:


Cond_f746_0_createList_GE(x1, x2) → Cond_f746_0_createList_GE(x1)

Prepared 2 rules for path length conversion:

P rules:
f746_0_createList_GE(x0) → f855_1_createList_Load(-(x0, 1)) | >(+(x0, 1), 0)
f746_0_createList_GE(x0) → f746_0_createList_GE(-(x0, 1)) | >(+(x0, 1), 0)

Finished conversion. Obtained 1 rules.

P rules:
f746_0_createList_GE(x1) → f746_0_createList_GE(-(x1, 1)) | >(x1, -1)

(12) Obligation:

Rules:
f746_0_createList_GE(x1) → f746_0_createList_GE(-(x1, 1)) | >(x1, -1)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f746_0_createList_GE(x2)] = x2

Therefore the following rule(s) have been dropped:


f746_0_createList_GE(x0) → f746_0_createList_GE(-(x0, 1)) | >(x0, -1)

(14) YES