Termination proof of /tmp/tmpN2Ip3J/ListReversePanhandleList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 842 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 94 ms)

        ↳7 intTRS

        ↳8 LinearRankingProcessor (⇔, 6 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 17 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 1 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 3 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇔, 2 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIntTRSProof (⇒, 2 ms)

        ↳22 intTRS

        ↳23 PolynomialOrderProcessor (⇔, 0 ms)

        ↳24 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class ListReversePanhandleList {
	public static void main(String... args) {
		List x = List.createPanhandleList(args[0].length(), args[1].length());
		List.reverse(x);
	}
}

class List {
	List n;

	public List(List next) {
		this.n = next;
	}

	public static void reverse(List x) {		
		List y = null;
		while (x != null) {
			List z = x;
			x = x.n;
			z.n = y;
			y = z;
		}
	}

	public static List createList(int l, List end) {
		while (--l > 0) {
			end = new List(end);
		}
		return end;
	}

	public static List createCycle(int l) {
		List last = new List(null);
		List first = createList(l - 1, last);
		last.n = first;
		return first;
	}

	public static List createPanhandleList(int pl, int cl) {
		return createList(pl, createCycle(cl));
	}

}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ListReversePanhandleList.main([Ljava/lang/String;)V: Graph of 294 nodes with 4 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 4 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

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

Used field analysis yielded the following read fields:
- List: [n]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 28 IRules

P rules:
f2280_0_reverse_JMP(EOS, java.lang.Object(o1550sub0), o1548, java.lang.Object(o1549sub0)) → f2282_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1548, java.lang.Object(o1549sub0))
f2282_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1548, java.lang.Object(o1549sub0)) → f2285_0_reverse_NULL(EOS, java.lang.Object(o1550sub0), o1548, java.lang.Object(o1549sub0), o1548)
f2285_0_reverse_NULL(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0), java.lang.Object(o1577sub)) → f2287_0_reverse_NULL(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0), java.lang.Object(o1577sub))
f2287_0_reverse_NULL(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0), java.lang.Object(o1577sub)) → f2289_0_reverse_Load(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0))
f2289_0_reverse_Load(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0)) → f2296_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0), java.lang.Object(o1577sub))
f2296_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0), java.lang.Object(o1577sub)) → f2301_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1577sub), java.lang.Object(o1549sub0), java.lang.Object(o1577sub))
f2296_0_reverse_Store(EOS, java.lang.Object(o1598sub), java.lang.Object(o1598sub), java.lang.Object(o1549sub0), java.lang.Object(o1598sub)) → f2302_0_reverse_Store(EOS, java.lang.Object(o1598sub), java.lang.Object(o1598sub), java.lang.Object(o1549sub0), java.lang.Object(o1598sub))
f2301_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600))) → f2305_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)))
f2305_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600))) → f2308_0_reverse_Load(EOS, java.lang.Object(o1550sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)))
f2308_0_reverse_Load(EOS, java.lang.Object(o1550sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600))) → f2312_0_reverse_FieldAccess(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(List(EOC, o1600)))
f2312_0_reverse_FieldAccess(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(List(EOC, o1600))) → f2317_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)), o1600)
f2317_0_reverse_Store(EOS, java.lang.Object(o1550sub0), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)), o1600) → f2323_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)))
f2323_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600))) → f2328_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(List(EOC, o1600)))
f2328_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1600)), java.lang.Object(List(EOC, o1600))) → f2333_0_reverse_FieldAccess(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(List(EOC, o1600)), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0))
f2333_0_reverse_FieldAccess(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(List(EOC, o1600)), java.lang.Object(List(EOC, o1600)), java.lang.Object(o1549sub0)) → f2344_0_reverse_Load(EOS, java.lang.Object(o1550put0), o1600, java.lang.Object(List(EOC, java.lang.Object(o1549put407282514))))
f2344_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(List(EOC, java.lang.Object(o1549sub407282514)))) → f2345_0_reverse_Load(EOS, java.lang.Object(o1550sub0), o1600, java.lang.Object(List(EOC, java.lang.Object(o1549sub407282514))))
f2345_0_reverse_Load(EOS, java.lang.Object(o1737sub0), o1734, java.lang.Object(List(EOC, o1736407336206))) → f2355_0_reverse_Store(EOS, java.lang.Object(o1737sub0), o1734, java.lang.Object(List(EOC, o1736407336206)))
f2355_0_reverse_Store(EOS, java.lang.Object(o1737sub0), o1734, java.lang.Object(List(EOC, o1736407336206))) → f2277_0_reverse_Store(EOS, java.lang.Object(o1737sub0), o1734, java.lang.Object(List(EOC, o1736407336206)))
f2277_0_reverse_Store(EOS, java.lang.Object(o1550sub0), o1548, java.lang.Object(o1549sub0)) → f2280_0_reverse_JMP(EOS, java.lang.Object(o1550sub0), o1548, java.lang.Object(o1549sub0))
f2302_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602))) → f2306_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)))
f2306_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602))) → f2310_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)))
f2310_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602))) → f2314_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)))
f2314_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602))) → f2320_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)), o1602)
f2320_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)), o1602) → f2325_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1602)), o1602, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)))
f2325_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1602)), o1602, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602))) → f2331_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1602)), o1602, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)))
f2331_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1602)), o1602, java.lang.Object(o1549sub0), java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602))) → f2336_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1602)), o1602, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0))
f2336_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1602)), o1602, java.lang.Object(List(EOC, o1602)), java.lang.Object(List(EOC, o1602)), java.lang.Object(o1549sub0)) → f2350_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o1549put407303408))), o1602, java.lang.Object(List(EOC, java.lang.Object(o1549put407303408))))
f2350_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o1549sub407303408))), o1602, java.lang.Object(List(EOC, java.lang.Object(o1549sub407303408)))) → f2345_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o1549sub407303408))), o1602, java.lang.Object(List(EOC, java.lang.Object(o1549sub407303408))))

Combined rules. Obtained 2 IRules

P rules:
f2280_0_reverse_JMP(EOS, java.lang.Object(x0), java.lang.Object(List(EOC, x1)), java.lang.Object(x2)) → f2280_0_reverse_JMP(EOS, java.lang.Object(x3), x1, java.lang.Object(List(EOC, java.lang.Object(x4))))
f2280_0_reverse_JMP(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), java.lang.Object(x1)) → f2280_0_reverse_JMP(EOS, java.lang.Object(List(EOC, java.lang.Object(x2))), x0, java.lang.Object(List(EOC, java.lang.Object(x2))))

Filtered ground terms:

f2280_0_reverse_JMP(x1, x2, x3, x4) → f2280_0_reverse_JMP(x2, x3, x4)
List(x1, x2) → List(x2)

Prepared 2 rules for path length conversion:

P rules:
f2280_0_reverse_JMP(java.lang.Object(x0), java.lang.Object(List(x1)), java.lang.Object(x2)) → f2280_0_reverse_JMP(java.lang.Object(x3), x1, java.lang.Object(List(java.lang.Object(x4))))
f2280_0_reverse_JMP(java.lang.Object(List(x0)), java.lang.Object(List(x0)), java.lang.Object(x1)) → f2280_0_reverse_JMP(java.lang.Object(List(java.lang.Object(x2))), x0, java.lang.Object(List(java.lang.Object(x2))))

Finished conversion. Obtained 2 rules.

P rules:
f2280_0_reverse_JMP(v11, v12, v13) → f2280_0_reverse_JMP(v14, v15, v16) | &&(&&(&&(&&(&&(&&(>(+(v16, 1), 3), >(+(v15, 1), 0)), <=(+(v15, 1), v12)), >(+(v14, 1), 1)), >(+(v13, 1), 1)), >(+(v12, 1), 1)), >(+(v11, 1), 1))
f2280_0_reverse_JMP(v17, v18, v19) → f2280_0_reverse_JMP(v20, v21, v22) | &&(&&(&&(&&(&&(&&(&&(>(+(v22, 1), 3), >(+(v21, 1), 0)), <=(+(v21, 1), v18)), <=(+(v21, 1), v17)), >(+(v20, 1), 3)), >(+(v19, 1), 1)), >(+(v18, 1), 1)), >(+(v17, 1), 1))

(7) Obligation:

Rules:
f2280_0_reverse_JMP(v11, v12, v13) → f2280_0_reverse_JMP(v14, v15, v16) | &&(&&(&&(&&(&&(&&(>(+(v16, 1), 3), >(+(v15, 1), 0)), <=(+(v15, 1), v12)), >(+(v14, 1), 1)), >(+(v13, 1), 1)), >(+(v12, 1), 1)), >(+(v11, 1), 1))
f2280_0_reverse_JMP(v17, v18, v19) → f2280_0_reverse_JMP(v20, v21, v22) | &&(&&(&&(&&(&&(&&(&&(>(+(v22, 1), 3), >(+(v21, 1), 0)), <=(+(v21, 1), v18)), <=(+(v21, 1), v17)), >(+(v20, 1), 3)), >(+(v19, 1), 1)), >(+(v18, 1), 1)), >(+(v17, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f2280_0_reverse_JMP(x)] = 1·x₂

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f2280_0_reverse_JMP(x0, x1, x2) → f2280_0_reverse_JMP(x3, x4, x5) | &&(&&(&&(&&(&&(&&(>(+(x5, 1), 3), >(+(x4, 1), 0)), <=(+(x4, 1), x1)), >(+(x3, 1), 1)), >(+(x2, 1), 1)), >(+(x1, 1), 1)), >(+(x0, 1), 1))
f2280_0_reverse_JMP(x6, x7, x8) → f2280_0_reverse_JMP(x9, x10, x11) | &&(&&(&&(&&(&&(&&(&&(>(+(x11, 1), 3), >(+(x10, 1), 0)), <=(+(x10, 1), x7)), <=(+(x10, 1), x6)), >(+(x9, 1), 3)), >(+(x8, 1), 1)), >(+(x7, 1), 1)), >(+(x6, 1), 1))

(9) YES

(10) Obligation:

Used field analysis yielded the following read fields:
- List: [n]
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 16 IRules

P rules:
f1657_0_reverse_Store(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1662_0_reverse_JMP(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1662_0_reverse_JMP(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1667_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1667_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1679_0_reverse_NULL(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1679_0_reverse_NULL(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1685_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1685_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1696_0_reverse_Store(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1696_0_reverse_Store(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1712_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1712_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1726_0_reverse_FieldAccess(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)
f1726_0_reverse_FieldAccess(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1737_0_reverse_FieldAccess(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) | &&(>(o686[List.n]o687, 0), >(o687[List.n]o687, 0))
f1737_0_reverse_FieldAccess(EOS, o838[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1745_0_reverse_FieldAccess(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) | =(o839[List.n]o687, +(o838[List.n]o687, -1))
f1745_0_reverse_FieldAccess(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) → f1755_0_reverse_Store(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687)
f1755_0_reverse_Store(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) → f1765_0_reverse_Load(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687)
f1765_0_reverse_Load(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) → f1776_0_reverse_Load(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687)
f1776_0_reverse_Load(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) → f1784_0_reverse_FieldAccess(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687)
f1784_0_reverse_FieldAccess(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) → f1815_0_reverse_Load(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687)
f1815_0_reverse_Load(EOS, o687[List.n]o687, o688[List.n]o690, o839[List.n]o687) → f1652_0_reverse_Load(EOS, o839[List.n]o687, o687[List.n]o687, o838[List.n]o690)
f1652_0_reverse_Load(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690) → f1657_0_reverse_Store(EOS, o686[List.n]o687, o687[List.n]o687, o688[List.n]o690)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f1657_0_reverse_Store(x1, x2, x3, x4) → f1657_0_reverse_Store(x2, x3, x4)
Cond_f1657_0_reverse_Store(x1, x2, x3, x4, x5, x6) → Cond_f1657_0_reverse_Store(x1, x3, x4, x5, x6)

Filtered unneeded terms:

Cond_f1657_0_reverse_Store(x1, x2, x3, x4, x5) → Cond_f1657_0_reverse_Store(x1, x2, x3)
f1657_0_reverse_Store(x1, x2, x3) → f1657_0_reverse_Store(x1, x2)

Prepared 1 rules for path length conversion:

P rules:
f1657_0_reverse_Store(x0, x1) → f1657_0_reverse_Store(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

Finished conversion. Obtained 1 rules.

P rules:
f1657_0_reverse_Store(x0, x1) → f1657_0_reverse_Store(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(12) Obligation:

Rules:
f1657_0_reverse_Store(x0, x1) → f1657_0_reverse_Store(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1657_0_reverse_Store(x3, x5)] = x3

Therefore the following rule(s) have been dropped:

f1657_0_reverse_Store(x0, x1) → f1657_0_reverse_Store(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(14) YES

(15) Obligation:

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

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f1244_0_createList_Load(EOS, i154, o319[List.n]o320, o320[List.n]o320) → f1245_0_createList_LE(EOS, i154, i154, o319[List.n]o320, o320[List.n]o320)
f1245_0_createList_LE(EOS, i158, i158, o319[List.n]o320, o320[List.n]o320) → f1249_0_createList_LE(EOS, i158, i158, o319[List.n]o320, o320[List.n]o320)
f1249_0_createList_LE(EOS, i158, i158, o319[List.n]o320, o320[List.n]o320) → f1251_0_createList_New(EOS, i158, o319[List.n]o320, o320[List.n]o320) | >(i158, 0)
f1251_0_createList_New(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1254_0_createList_Duplicate(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1254_0_createList_Duplicate(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1258_0_createList_Load(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1258_0_createList_Load(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1261_0_createList_InvokeMethod(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1261_0_createList_InvokeMethod(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1264_0__init__Load(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1264_0__init__Load(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1271_0__init__InvokeMethod(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1271_0__init__InvokeMethod(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1274_0__init__Load(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1274_0__init__Load(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1277_0__init__Load(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1277_0__init__Load(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1282_0__init__FieldAccess(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1282_0__init__FieldAccess(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1291_0__init__Return(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1291_0__init__Return(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1296_0_createList_Store(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1296_0_createList_Store(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1301_0_createList_JMP(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1301_0_createList_JMP(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1316_0_createList_Inc(EOS, i158, o319[List.n]o320, o320[List.n]o320)
f1316_0_createList_Inc(EOS, i158, o319[List.n]o320, o320[List.n]o320) → f1241_0_createList_Inc(EOS, i158, o341[List.n]o320, o320[List.n]o320)
f1241_0_createList_Inc(EOS, i149, o319[List.n]o320, o320[List.n]o320) → f1244_0_createList_Load(EOS, +(i149, -1), o319[List.n]o320, o320[List.n]o320) | >=(i149, 0)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f1244_0_createList_Load(x1, x2, x3, x4) → f1244_0_createList_Load(x2, x3, x4)
Cond_f1244_0_createList_Load(x1, x2, x3, x4, x5, x6) → Cond_f1244_0_createList_Load(x1, x3, x4, x5, x6)

Filtered unneeded terms:

Cond_f1244_0_createList_Load(x1, x2, x3, x4, x5) → Cond_f1244_0_createList_Load(x1, x2)
f1244_0_createList_Load(x1, x2, x3) → f1244_0_createList_Load(x1)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(17) Obligation:

Rules:
f1244_0_createList_Load(x0) → f1244_0_createList_Load(-(x0, 1)) | >(x0, 0)

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1244_0_createList_Load(x2)] = x2

Therefore the following rule(s) have been dropped:

f1244_0_createList_Load(x0) → f1244_0_createList_Load(-(x0, 1)) | >(x0, 0)

(19) YES

(20) Obligation:

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

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f503_0_createList_Load(EOS, i69, o159[List.n]o161) → f504_0_createList_LE(EOS, i69, i69, o159[List.n]o161)
f504_0_createList_LE(EOS, i73, i73, o159[List.n]o161) → f508_0_createList_LE(EOS, i73, i73, o159[List.n]o161)
f508_0_createList_LE(EOS, i73, i73, o159[List.n]o161) → f512_0_createList_New(EOS, i73, o159[List.n]o161) | >(i73, 0)
f512_0_createList_New(EOS, i73, o159[List.n]o161) → f515_0_createList_Duplicate(EOS, i73, o159[List.n]o161)
f515_0_createList_Duplicate(EOS, i73, o159[List.n]o161) → f518_0_createList_Load(EOS, i73, o159[List.n]o161)
f518_0_createList_Load(EOS, i73, o159[List.n]o161) → f522_0_createList_InvokeMethod(EOS, i73, o159[List.n]o161)
f522_0_createList_InvokeMethod(EOS, i73, o159[List.n]o161) → f526_0__init__Load(EOS, i73, o159[List.n]o161)
f526_0__init__Load(EOS, i73, o159[List.n]o161) → f560_0__init__InvokeMethod(EOS, i73, o159[List.n]o161)
f560_0__init__InvokeMethod(EOS, i73, o159[List.n]o161) → f579_0__init__Load(EOS, i73, o159[List.n]o161)
f579_0__init__Load(EOS, i73, o159[List.n]o161) → f587_0__init__Load(EOS, i73, o159[List.n]o161)
f587_0__init__Load(EOS, i73, o159[List.n]o161) → f595_0__init__FieldAccess(EOS, i73, o159[List.n]o161)
f595_0__init__FieldAccess(EOS, i73, o159[List.n]o161) → f604_0__init__Return(EOS, i73, o159[List.n]o161)
f604_0__init__Return(EOS, i73, o159[List.n]o161) → f607_0_createList_Store(EOS, i73, o159[List.n]o161)
f607_0_createList_Store(EOS, i73, o159[List.n]o161) → f613_0_createList_JMP(EOS, i73, o159[List.n]o161)
f613_0_createList_JMP(EOS, i73, o159[List.n]o161) → f667_0_createList_Inc(EOS, i73, o159[List.n]o161)
f667_0_createList_Inc(EOS, i73, o159[List.n]o161) → f496_0_createList_Inc(EOS, i73, o169[List.n]o161)
f496_0_createList_Inc(EOS, i66, o159[List.n]o161) → f503_0_createList_Load(EOS, +(i66, -1), o159[List.n]o161)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f503_0_createList_Load(x1, x2, x3) → f503_0_createList_Load(x2, x3)
Cond_f503_0_createList_Load(x1, x2, x3, x4, x5) → Cond_f503_0_createList_Load(x1, x3, x4, x5)

Filtered unneeded terms:

Cond_f503_0_createList_Load(x1, x2, x3, x4) → Cond_f503_0_createList_Load(x1, x2)
f503_0_createList_Load(x1, x2) → f503_0_createList_Load(x1)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(22) Obligation:

Rules:
f503_0_createList_Load(x0) → f503_0_createList_Load(-(x0, 1)) | >(x0, 0)

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f503_0_createList_Load(x2)] = x2

Therefore the following rule(s) have been dropped:

f503_0_createList_Load(x0) → f503_0_createList_Load(-(x0, 1)) | >(x0, 0)

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) LinearRankingProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIntTRSProof (SOUND transformation)

(22) Obligation:

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

(24) YES