Termination proof of /tmp/tmpGtQmDl/List2.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 458 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 303 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 20 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 80 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class List2 {
	private List2 next;
	private int mark;

	static void visit(List2 c) {
		int expectedMark = c.mark;
		while (c != null && c.mark == expectedMark) {
			c.mark = expectedMark + 1;
			c = c.next;
		}
	}

	public static void main(String[] args) {
		//Create cyclic list:
		int length = args.length;
		List2 cur = new List2();
		List2 last = cur;
		while (length-- > 0) {
			List2 n = new List2();
			n.next = cur;
			cur = n;
		}
		last.next = cur;

		visit(cur);		
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
List2.main([Ljava/lang/String;)V: Graph of 80 nodes with 1 SCC.

List2.visit(LList2;)V: Graph of 60 nodes with 1 SCC.

(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: List2.visit(LList2;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List2: [mark, next]
Marker field analysis yielded the following relations that could be markers:
- List2.mark = i29 (Introduced counter i150)

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 49 IRules

P rules:
f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) → f482_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58)
f482_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) → f486_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58)
f486_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) → f504_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) | &&(>(o58[List2.next]o56, 0), >(o58[List2.next]o58, 0))
f486_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o68, o68[List2.next]o57, o68[List2.next]o68) → f505_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) | =(o57[List2.next]o56, +(o68[List2.next]o68, -1))
f504_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) → f521_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) | &&(&&(&&(>(o57[List2.next]o57, 0), >(o57[List2.next]o58, 0)), >(o58[List2.next]o57, 0)), >(o58[List2.next]o58, 0))
f504_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o74sub1136605123))), java.lang.Object(o74sub0), i29, java.lang.Object(o74sub0), i150, o74[List2.next]o56, o74[List2.next]o56, o74[List2.next]o74, o57[List2.next]o58, o58[List2.next]o57, o74[List2.next]o74) → f522_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o74sub1136605123))), java.lang.Object(o74sub0), i29, java.lang.Object(o74sub0), i150, o74[List2.next]o56, o74[List2.next]o74)
f521_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o75[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o75[List2.next]o57, o75[List2.next]o75) → f531_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) | &&(&&(=(o76[List2.next]o56, +(o75[List2.next]o56, -1)), =(o76[List2.next]o57, +(o75[List2.next]o57, -1))), =(o76[List2.next]o75, +(o75[List2.next]o75, -1)))
f531_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f550_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f550_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f563_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i46, java.lang.Object(o76sub1136607014))), i29, i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f563_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f590_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i29, i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f590_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i29, i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f632_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f632_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f662_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f662_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f684_0_visit_ConstantStackPush(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f684_0_visit_ConstantStackPush(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f700_0_visit_IntArithmetic(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, 1, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f700_0_visit_IntArithmetic(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, matching1, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f719_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), +(i29, 1), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) | =(matching1, 1)
f719_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o76sub1136607014))), i67, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f734_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i67, java.lang.Object(o76sub1136607014))), i29, +(i150, -1), o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) | >=(i150, 0)
f734_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(List2(EOC, i67, java.lang.Object(o76sub1136607014))), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f752_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), i29, java.lang.Object(List2(EOC, i67, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75)
f752_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), i29, java.lang.Object(List2(EOC, i67, java.lang.Object(o76sub1136607014))), i150, o57[List2.next]o56, o57[List2.next]o57, o57[List2.next]o75, o76[List2.next]o56, o76[List2.next]o57, o76[List2.next]o75) → f769_0_visit_Store(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), i29, java.lang.Object(o76sub0), i150, o57[List2.next]o56, o57[List2.next]o57, o76[List2.next]o56, o76[List2.next]o57, o57[List2.next]o76, o76[List2.next]o76)
f769_0_visit_Store(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), i29, java.lang.Object(o76sub0), i150, o57[List2.next]o56, o57[List2.next]o57, o76[List2.next]o56, o76[List2.next]o57, o57[List2.next]o76, o76[List2.next]o76) → f881_0_visit_JMP(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o76sub0), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o76[List2.next]o56, o76[List2.next]o57, o57[List2.next]o76, o76[List2.next]o76)
f881_0_visit_JMP(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o76sub0), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o76[List2.next]o56, o76[List2.next]o57, o57[List2.next]o76, o76[List2.next]o76) → f894_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o76sub0), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o76[List2.next]o56, o76[List2.next]o57, o57[List2.next]o76, o76[List2.next]o76)
f894_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o76sub0), i29, i150, o57[List2.next]o56, o57[List2.next]o57, o76[List2.next]o56, o76[List2.next]o57, o57[List2.next]o76, o76[List2.next]o76) → f473_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o76sub0), i29, i150, o57[List2.next]o56, o76[List2.next]o56, o57[List2.next]o57, o57[List2.next]o76, o76[List2.next]o57, o76[List2.next]o76)
f473_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58) → f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136605123))), java.lang.Object(o58sub0), i29, java.lang.Object(o58sub0), i150, o57[List2.next]o56, o58[List2.next]o56, o57[List2.next]o57, o57[List2.next]o58, o58[List2.next]o57, o58[List2.next]o58)
f522_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i150, o78[List2.next]o56, o78[List2.next]o78) → f537_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i150, o79[List2.next]o56, o79[List2.next]o78) | &&(=(o79[List2.next]o56, +(o78[List2.next]o56, -1)), =(o79[List2.next]o78, +(o78[List2.next]o78, -1)))
f537_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i150, o79[List2.next]o56, o79[List2.next]o78) → f556_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f556_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f571_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i47, java.lang.Object(o79sub1136607107))), i29, i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f571_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f597_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i29, i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f597_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i29, i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f643_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f643_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f672_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i150, o79[List2.next]o56, o79[List2.next]o78)
f672_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i150, o79[List2.next]o56, o79[List2.next]o78) → f692_0_visit_ConstantStackPush(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f692_0_visit_ConstantStackPush(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f706_0_visit_IntArithmetic(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, 1, i150, o79[List2.next]o56, o79[List2.next]o78)
f706_0_visit_IntArithmetic(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, matching1, i150, o79[List2.next]o56, o79[List2.next]o78) → f724_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), +(i29, 1), i150, o79[List2.next]o56, o79[List2.next]o78) | =(matching1, 1)
f724_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o79sub1136607107))), i70, i150, o79[List2.next]o56, o79[List2.next]o78) → f742_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79put-2021755066))))), java.lang.Object(List2(EOC, i70, java.lang.Object(o79put1136607107))), i29, +(i150, -1), o79[List2.next]o56, o79[List2.next]o78) | >=(i150, 0)
f742_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub1136607107))), i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f755_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), i29, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub1136607107))), i150, o79[List2.next]o56, o79[List2.next]o78)
f755_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), i29, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub1136607107))), i150, o79[List2.next]o56, o79[List2.next]o78) → f843_0_visit_Store(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), i29, java.lang.Object(o79sub0), i150, o79[List2.next]o56, o79[List2.next]o78)
f843_0_visit_Store(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), i29, java.lang.Object(o79sub0), i150, o79[List2.next]o56, o79[List2.next]o78) → f884_0_visit_JMP(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), java.lang.Object(o79sub0), i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f884_0_visit_JMP(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), java.lang.Object(o79sub0), i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f904_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), java.lang.Object(o79sub0), i29, i150, o79[List2.next]o56, o79[List2.next]o78)
f904_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), java.lang.Object(o79sub0), i29, i150, o79[List2.next]o56, o79[List2.next]o78) → f473_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(List2(EOC, i70, java.lang.Object(o79sub-2021755066))))), java.lang.Object(o79sub0), i29, i150, o78[List2.next]o56, o79[List2.next]o56, o78[List2.next]o78, o78[List2.next]o79, o79[List2.next]o78, o79[List2.next]o79) | &&(&&(=(o78[List2.next]o78, 0), =(o78[List2.next]o79, 1)), =(o79[List2.next]o79, 0))
f505_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f526_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i29, i41, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f526_0_visit_Load(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i29, i41, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f544_0_visit_NE(EOS, java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i41, java.lang.Object(o57sub1136606146))), i29, i41, i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f544_0_visit_NE(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i29, i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f558_0_visit_NE(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i29, i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f558_0_visit_NE(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i29, i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f585_0_visit_Load(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f585_0_visit_Load(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f608_0_visit_Load(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f608_0_visit_Load(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f653_0_visit_ConstantStackPush(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f653_0_visit_ConstantStackPush(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f681_0_visit_IntArithmetic(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, 1, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f681_0_visit_IntArithmetic(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, matching1, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f698_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), +(i29, 1), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) | =(matching1, 1)
f698_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i29, java.lang.Object(o57sub1136606146))), i64, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f712_0_visit_Load(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57put1136606146))), java.lang.Object(List2(EOC, i64, java.lang.Object(o57put1136606146))), i29, +(i150, -1), o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) | >=(i150, 0)
f712_0_visit_Load(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i29, i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f727_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f727_0_visit_FieldAccess(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f746_0_visit_Store(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(o57sub0), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68)
f746_0_visit_Store(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(o57sub0), i150, o57[List2.next]o68, o57[List2.next]o57, o68[List2.next]o68) → f769_0_visit_Store(EOS, java.lang.Object(List2(EOC, i64, java.lang.Object(o57sub1136606146))), i29, java.lang.Object(o57sub0), i150, o57[List2.next]o68, o57[List2.next]o57, o57[List2.next]o68, o57[List2.next]o57, o57[List2.next]o57, o57[List2.next]o57)

Combined rules. Obtained 3 IRules

P rules:
f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, x0, java.lang.Object(x1))), java.lang.Object(List2(EOC, x2, java.lang.Object(x3))), x2, java.lang.Object(List2(EOC, x2, java.lang.Object(x3))), x4, x5, x6, x7, x8, x9, x10) → f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, x0, java.lang.Object(x1))), java.lang.Object(x11), x2, java.lang.Object(x11), -(x4, 1), x5, -(x6, 1), x7, x13, -(x9, 1), x15) | &&(&&(&&(&&(&&(>(x9, 0), >(x8, 0)), >(x7, 0)), >(x6, 0)), >(+(x4, 1), 0)), >(x10, 0))
f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, x0, java.lang.Object(List2(EOC, x1, java.lang.Object(x2))))), java.lang.Object(List2(EOC, x1, java.lang.Object(x3))), x1, java.lang.Object(List2(EOC, x1, java.lang.Object(x3))), x4, x5, x5, x6, x7, x8, x6) → f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, x0, java.lang.Object(List2(EOC, +(x1, 1), java.lang.Object(x9))))), java.lang.Object(x10), x1, java.lang.Object(x10), -(x4, 1), x11, -(x5, 1), 0, 1, -(x6, 1), 0) | &&(&&(>(x6, 0), >(+(x4, 1), 0)), >(x5, 0))
f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, x0, java.lang.Object(x1))), java.lang.Object(List2(EOC, x0, java.lang.Object(x1))), x0, java.lang.Object(List2(EOC, x0, java.lang.Object(x1))), x2, x3, x4, x5, x3, x6, x7) → f479_0_visit_NULL(EOS, java.lang.Object(List2(EOC, +(x0, 1), java.lang.Object(x8))), java.lang.Object(x9), x0, java.lang.Object(x9), -(x2, 1), x3, x3, x5, x5, x5, x5) | >(+(x2, 1), 0)

Filtered ground terms:

f479_0_visit_NULL(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → f479_0_visit_NULL(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
Cond_f479_0_visit_NULL(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) → Cond_f479_0_visit_NULL(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)
Cond_f479_0_visit_NULL1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) → Cond_f479_0_visit_NULL1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)
Cond_f479_0_visit_NULL2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → Cond_f479_0_visit_NULL2(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)
List2(x1, x2, x3) → List2(x2, x3)

Filtered duplicate terms:

f479_0_visit_NULL(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f479_0_visit_NULL(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)
Cond_f479_0_visit_NULL(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → Cond_f479_0_visit_NULL(x1, x2, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)
Cond_f479_0_visit_NULL1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → Cond_f479_0_visit_NULL1(x1, x2, x5, x6, x8, x10, x11, x12, x13, x14, x15)
Cond_f479_0_visit_NULL2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → Cond_f479_0_visit_NULL2(x1, x5, x6, x8, x9, x10, x11, x12, x13, x14)

Filtered unneeded terms:

f479_0_visit_NULL(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f479_0_visit_NULL(x1, x3, x4, x5, x6, x7, x8, x9, x10)
List2(x1, x2) → List2(x2)
Cond_f479_0_visit_NULL(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → Cond_f479_0_visit_NULL(x1, x2, x4, x5, x6, x7, x9, x11, x12, x13)
Cond_f479_0_visit_NULL1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f479_0_visit_NULL1(x1, x4, x5, x8, x9, x10, x11)
Cond_f479_0_visit_NULL2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f479_0_visit_NULL2(x1, x3, x5, x6, x9, x10)

Prepared 3 rules for path length conversion:

P rules:
f479_0_visit_NULL(java.lang.Object(List2(java.lang.Object(x1))), java.lang.Object(List2(java.lang.Object(x3))), x4, x5, x6, x7, x8, x9, x10) → f479_0_visit_NULL(java.lang.Object(List2(java.lang.Object(x1))), java.lang.Object(x11), -(x4, 1), x5, -(x6, 1), x7, x13, -(x9, 1), x15) | &&(&&(&&(&&(&&(>(x9, 0), >(x8, 0)), >(x7, 0)), >(x6, 0)), >(+(x4, 1), 0)), >(x10, 0))
f479_0_visit_NULL(java.lang.Object(List2(java.lang.Object(List2(java.lang.Object(x2))))), java.lang.Object(List2(java.lang.Object(x3))), x4, x5, x5, x6, x7, x8, x6) → f479_0_visit_NULL(java.lang.Object(List2(java.lang.Object(List2(java.lang.Object(x9))))), java.lang.Object(x10), -(x4, 1), x11, -(x5, 1), 0, 1, -(x6, 1), 0) | &&(&&(>(x6, 0), >(+(x4, 1), 0)), >(x5, 0))
f479_0_visit_NULL(java.lang.Object(List2(java.lang.Object(x1))), java.lang.Object(List2(java.lang.Object(x1))), x2, x3, x4, x5, x3, x6, x7) → f479_0_visit_NULL(java.lang.Object(List2(java.lang.Object(x8))), java.lang.Object(x9), -(x2, 1), x3, x3, x5, x5, x5, x5) | >(+(x2, 1), 0)

Finished conversion. Obtained 3 rules.

P rules:
f479_0_visit_NULL(v40, v41, x2, x3, x4, x5, x6, x7, x8) → f479_0_visit_NULL(v42, v43, -(x2, 1), x3, -(x4, 1), x5, x10, -(x7, 1), x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x8, 0), >(x7, 0)), >(x6, 0)), >(x5, 0)), >(x4, 0)), >(x2, -1)), >(+(v43, 1), 1)), >(+(v42, 1), 3)), <=(v42, v40)), >(+(v41, 1), 3)), >(+(v40, 1), 3))
f479_0_visit_NULL(v44, v45, x14, x15, x151, x16, x17, x18, x161) → f479_0_visit_NULL(v46, v47, -(x14, 1), x21, -(x15, 1), 0, 1, -(x16, 1), 0) | &&(&&(&&(&&(&&(&&(&&(&&(>(x16, 0), >(x15, 0)), >(x14, -1)), >(+(v47, 1), 1)), >(+(v46, 1), 5)), >(+(v45, 1), 3)), >(+(v44, 1), 5)), =(x15, x151)), =(x16, x161))
f479_0_visit_NULL(v48, v49, x23, x24, x25, x26, x241, x27, x28) → f479_0_visit_NULL(v50, v51, -(x23, 1), x24, x24, x26, x26, x26, x26) | &&(&&(&&(&&(&&(>(x23, -1), >(+(v51, 1), 1)), >(+(v50, 1), 3)), >(+(v49, 1), 3)), >(+(v48, 1), 3)), =(x24, x241))

(7) Obligation:

Rules:
f479_0_visit_NULL(v40, v41, x2, x3, x4, x5, x6, x7, x8) → f479_0_visit_NULL(v42, v43, -(x2, 1), x3, -(x4, 1), x5, x10, -(x7, 1), x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x8, 0), >(x7, 0)), >(x6, 0)), >(x5, 0)), >(x4, 0)), >(x2, -1)), >(+(v43, 1), 1)), >(+(v42, 1), 3)), <=(v42, v40)), >(+(v41, 1), 3)), >(+(v40, 1), 3))
f479_0_visit_NULL(v44, v45, x14, x15, x151, x16, x17, x18, x161) → f479_0_visit_NULL(v46, v47, -(x14, 1), x21, -(x15, 1), 0, 1, -(x16, 1), 0) | &&(&&(&&(&&(&&(&&(&&(&&(>(x16, 0), >(x15, 0)), >(x14, -1)), >(+(v47, 1), 1)), >(+(v46, 1), 5)), >(+(v45, 1), 3)), >(+(v44, 1), 5)), =(x15, x151)), =(x16, x161))
f479_0_visit_NULL(v48, v49, x23, x24, x25, x26, x241, x27, x28) → f479_0_visit_NULL(v50, v51, -(x23, 1), x24, x24, x26, x26, x26, x26) | &&(&&(&&(&&(&&(>(x23, -1), >(+(v51, 1), 1)), >(+(v50, 1), 3)), >(+(v49, 1), 3)), >(+(v48, 1), 3)), =(x24, x241))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f479_0_visit_NULL(x37, x39, x41, x43, x45, x47, x49, x51, x53)] = x41

Therefore the following rule(s) have been dropped:

f479_0_visit_NULL(x0, x1, x2, x3, x4, x5, x6, x7, x8) → f479_0_visit_NULL(x9, x10, -(x2, 1), x3, -(x4, 1), x5, x11, -(x7, 1), x12) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x8, 0), >(x7, 0)), >(x6, 0)), >(x5, 0)), >(x4, 0)), >(x2, -1)), >(+(x10, 1), 1)), >(+(x9, 1), 3)), <=(x9, x0)), >(+(x1, 1), 3)), >(+(x0, 1), 3))
f479_0_visit_NULL(x13, x14, x15, x16, x17, x18, x19, x20, x21) → f479_0_visit_NULL(x22, x23, -(x15, 1), x24, -(x16, 1), 0, 1, -(x18, 1), 0) | &&(&&(&&(&&(&&(&&(&&(&&(>(x18, 0), >(x16, 0)), >(x15, -1)), >(+(x23, 1), 1)), >(+(x22, 1), 5)), >(+(x14, 1), 3)), >(+(x13, 1), 5)), =(x16, x17)), =(x18, x21))
f479_0_visit_NULL(x25, x26, x27, x28, x29, x30, x31, x32, x33) → f479_0_visit_NULL(x34, x35, -(x27, 1), x28, x28, x30, x30, x30, x30) | &&(&&(&&(&&(&&(>(x27, -1), >(+(x35, 1), 1)), >(+(x34, 1), 3)), >(+(x26, 1), 3)), >(+(x25, 1), 3)), =(x28, x31))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: List2.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 18 IRules

P rules:
f931_0_main_Inc(EOS, i94, i94, o258[List2.next]o259) → f933_0_main_LE(EOS, +(i94, -1), i94, o258[List2.next]o259)
f933_0_main_LE(EOS, i96, i100, o258[List2.next]o259) → f936_0_main_LE(EOS, i96, i100, o258[List2.next]o259)
f936_0_main_LE(EOS, i96, i100, o258[List2.next]o259) → f939_0_main_New(EOS, i96, o258[List2.next]o259) | >(i100, 0)
f939_0_main_New(EOS, i96, o258[List2.next]o259) → f942_0_main_Duplicate(EOS, i96, o258[List2.next]o259)
f942_0_main_Duplicate(EOS, i96, o258[List2.next]o259) → f945_0_main_InvokeMethod(EOS, i96, o258[List2.next]o259)
f945_0_main_InvokeMethod(EOS, i96, o258[List2.next]o259) → f954_0__init__Load(EOS, i96, o258[List2.next]o259)
f954_0__init__Load(EOS, i96, o258[List2.next]o259) → f965_0__init__InvokeMethod(EOS, i96, o258[List2.next]o259)
f965_0__init__InvokeMethod(EOS, i96, o258[List2.next]o259) → f970_0__init__Return(EOS, i96, o258[List2.next]o259)
f970_0__init__Return(EOS, i96, o258[List2.next]o259) → f976_0_main_Store(EOS, i96, o258[List2.next]o259)
f976_0_main_Store(EOS, i96, o258[List2.next]o259) → f978_0_main_Load(EOS, i96, o258[List2.next]o259)
f978_0_main_Load(EOS, i96, o258[List2.next]o259) → f1037_0_main_Load(EOS, i96, o258[List2.next]o259)
f1037_0_main_Load(EOS, i96, o258[List2.next]o259) → f1061_0_main_FieldAccess(EOS, i96, o258[List2.next]o259)
f1061_0_main_FieldAccess(EOS, i96, o258[List2.next]o259) → f1069_0_main_Load(EOS, i96, o258[List2.next]o259)
f1069_0_main_Load(EOS, i96, o258[List2.next]o259) → f1071_0_main_Store(EOS, i96, o258[List2.next]o259)
f1071_0_main_Store(EOS, i96, o258[List2.next]o259) → f1072_0_main_JMP(EOS, i96, o258[List2.next]o259)
f1072_0_main_JMP(EOS, i96, o258[List2.next]o259) → f1084_0_main_Load(EOS, i96, o258[List2.next]o259)
f1084_0_main_Load(EOS, i96, o258[List2.next]o259) → f929_0_main_Load(EOS, i96, o264[List2.next]o259)
f929_0_main_Load(EOS, i94, o258[List2.next]o259) → f931_0_main_Inc(EOS, i94, i94, o258[List2.next]o259)

Combined rules. Obtained 1 IRules

P rules:
f931_0_main_Inc(EOS, x0, x0, x1) → f931_0_main_Inc(EOS, -(x0, 1), -(x0, 1), x2) | >(x0, 0)

Filtered ground terms:

f931_0_main_Inc(x1, x2, x3, x4) → f931_0_main_Inc(x2, x3, x4)
Cond_f931_0_main_Inc(x1, x2, x3, x4, x5, x6) → Cond_f931_0_main_Inc(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f931_0_main_Inc(x1, x2, x3) → f931_0_main_Inc(x2, x3)
Cond_f931_0_main_Inc(x1, x2, x3, x4, x5) → Cond_f931_0_main_Inc(x1, x3, x4, x5)

Filtered unneeded terms:

Cond_f931_0_main_Inc(x1, x2, x3, x4) → Cond_f931_0_main_Inc(x1, x2)
f931_0_main_Inc(x1, x2) → f931_0_main_Inc(x1)

Prepared 1 rules for path length conversion:

P rules:
f931_0_main_Inc(x0) → f931_0_main_Inc(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.