Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class ListReverseCyclicList {
	public static void main(String... args) {
		List x = List.createCycle(args[0].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:
ListReverseCyclicList.main([Ljava/lang/String;)V: Graph of 216 nodes with 2 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: ListReverseCyclicList.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 49 IRules

P rules:
f1710_0_reverse_Store(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0)) → f1712_0_reverse_JMP(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0))
f1712_0_reverse_JMP(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0)) → f1714_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0))
f1714_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0)) → f1718_0_reverse_NULL(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0), o1647)
f1718_0_reverse_NULL(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub)) → f1720_0_reverse_NULL(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub))
f1720_0_reverse_NULL(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub)) → f1724_0_reverse_Load(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0))
f1724_0_reverse_Load(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0)) → f1733_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub))
f1733_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub)) → f1740_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub))
f1733_0_reverse_Store(EOS, java.lang.Object(o1707sub), java.lang.Object(o1707sub), java.lang.Object(o1648sub0), java.lang.Object(o1707sub)) → f1741_0_reverse_Store(EOS, java.lang.Object(o1707sub), java.lang.Object(o1707sub), java.lang.Object(o1648sub0), java.lang.Object(o1707sub))
f1740_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub)) → f1746_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1683sub), java.lang.Object(o1648sub0), java.lang.Object(o1683sub))
f1740_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1710sub), java.lang.Object(o1710sub), java.lang.Object(o1710sub)) → f1747_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1710sub), java.lang.Object(o1710sub), java.lang.Object(o1710sub))
f1746_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715))) → f1754_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)))
f1754_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715))) → f1762_0_reverse_Load(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)))
f1762_0_reverse_Load(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715))) → f1772_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(List(EOC, o1715)))
f1772_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(List(EOC, o1715))) → f1784_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)), o1715)
f1784_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)), o1715) → f1795_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)))
f1795_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715))) → f1806_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(List(EOC, o1715)))
f1806_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1715)), java.lang.Object(List(EOC, o1715))) → f1816_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(List(EOC, o1715)), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0))
f1816_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(List(EOC, o1715)), java.lang.Object(List(EOC, o1715)), java.lang.Object(o1648sub0)) → f1833_0_reverse_Load(EOS, java.lang.Object(o1649put0), o1715, java.lang.Object(List(EOC, java.lang.Object(o1648put-658075604))))
f1833_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(List(EOC, java.lang.Object(o1648sub-658075604)))) → f1709_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1715, java.lang.Object(List(EOC, java.lang.Object(o1648sub-658075604))))
f1709_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0)) → f1710_0_reverse_Store(EOS, java.lang.Object(o1649sub0), o1647, java.lang.Object(o1648sub0))
f1747_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1756_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)))
f1756_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1765_0_reverse_Load(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)))
f1765_0_reverse_Load(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1774_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)))
f1774_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1786_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), o1717)
f1786_0_reverse_Store(EOS, java.lang.Object(o1649sub0), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), o1717) → f1798_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)))
f1798_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1809_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)))
f1809_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1819_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)))
f1819_0_reverse_FieldAccess(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717)), java.lang.Object(List(EOC, o1717))) → f1839_0_reverse_Load(EOS, java.lang.Object(o1649put0), o1717, java.lang.Object(List(EOC, java.lang.Object(EOR))))
f1839_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, java.lang.Object(EOR)))) → f1709_0_reverse_Load(EOS, java.lang.Object(o1649sub0), o1717, java.lang.Object(List(EOC, java.lang.Object(EOR))))
f1741_0_reverse_Store(EOS, java.lang.Object(o1707sub), java.lang.Object(o1707sub), java.lang.Object(o1648sub0), java.lang.Object(o1707sub)) → f1752_0_reverse_Store(EOS, java.lang.Object(o1707sub), java.lang.Object(o1707sub), java.lang.Object(o1648sub0), java.lang.Object(o1707sub))
f1741_0_reverse_Store(EOS, java.lang.Object(o1713sub), java.lang.Object(o1713sub), java.lang.Object(o1713sub), java.lang.Object(o1713sub)) → f1753_0_reverse_Store(EOS, java.lang.Object(o1713sub), java.lang.Object(o1713sub), java.lang.Object(o1713sub), java.lang.Object(o1713sub))
f1752_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719))) → f1758_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)))
f1758_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719))) → f1767_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)))
f1767_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719))) → f1778_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)))
f1778_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719))) → f1790_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)), o1719)
f1790_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)), o1719) → f1801_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1719)), o1719, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)))
f1801_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1719)), o1719, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719))) → f1812_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1719)), o1719, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)))
f1812_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1719)), o1719, java.lang.Object(o1648sub0), java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719))) → f1824_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1719)), o1719, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0))
f1824_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1719)), o1719, java.lang.Object(List(EOC, o1719)), java.lang.Object(List(EOC, o1719)), java.lang.Object(o1648sub0)) → f1846_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o1648put-658075480))), o1719, java.lang.Object(List(EOC, java.lang.Object(o1648put-658075480))))
f1846_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o1648sub-658075480))), o1719, java.lang.Object(List(EOC, java.lang.Object(o1648sub-658075480)))) → f1709_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o1648sub-658075480))), o1719, java.lang.Object(List(EOC, java.lang.Object(o1648sub-658075480))))
f1753_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1760_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)))
f1760_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1771_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)))
f1771_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1781_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)))
f1781_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1793_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), o1721)
f1793_0_reverse_Store(EOS, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), o1721) → f1804_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1721)), o1721, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)))
f1804_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1721)), o1721, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1815_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1721)), o1721, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)))
f1815_0_reverse_Load(EOS, java.lang.Object(List(EOC, o1721)), o1721, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1826_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1721)), o1721, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)))
f1826_0_reverse_FieldAccess(EOS, java.lang.Object(List(EOC, o1721)), o1721, java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721)), java.lang.Object(List(EOC, o1721))) → f1851_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(EOR))), o1721, java.lang.Object(List(EOC, java.lang.Object(EOR))))
f1851_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(EOR))), o1721, java.lang.Object(List(EOC, java.lang.Object(EOR)))) → f1709_0_reverse_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(EOR))), o1721, java.lang.Object(List(EOC, java.lang.Object(EOR))))

Combined rules. Obtained 4 IRules

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

Filtered ground terms:


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

Prepared 4 rules for path length conversion:

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

Finished conversion. Obtained 4 rules.

P rules:
f1710_0_reverse_Store(v15, v16, v17) → f1710_0_reverse_Store(v18, v19, v20) | &&(&&(&&(&&(&&(&&(>(+(v20, 1), 3), >(+(v19, 1), 0)), <=(+(v19, 1), v16)), >(+(v18, 1), 1)), >(+(v17, 1), 1)), >(+(v16, 1), 1)), >(+(v15, 1), 1))
f1710_0_reverse_Store(v21, v22, v23) → f1710_0_reverse_Store(v24, v25, v26) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v26, 1), 3), <=(-(v26, 2), v23)), <=(-(v26, 2), v22)), <=(-(v26, 2), v21)), >(+(v25, 1), 0)), <=(+(v25, 1), v23)), <=(+(v25, 1), v22)), >(+(v24, 1), 1)), >(+(v23, 1), 1)), >(+(v22, 1), 1)), >(+(v21, 1), 1))
f1710_0_reverse_Store(v27, v28, v29) → f1710_0_reverse_Store(v30, v31, v32) | &&(&&(&&(&&(&&(&&(&&(>(+(v32, 1), 3), >(+(v31, 1), 0)), <=(+(v31, 1), v28)), <=(+(v31, 1), v27)), >(+(v30, 1), 3)), >(+(v29, 1), 1)), >(+(v28, 1), 1)), >(+(v27, 1), 1))
f1710_0_reverse_Store(v33, v34, v35) → f1710_0_reverse_Store(v36, v37, v38) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v38, 1), 3), <=(-(v38, 2), v35)), <=(-(v38, 2), v34)), <=(-(v38, 2), v33)), >(+(v37, 1), 0)), <=(+(v37, 1), v35)), <=(+(v37, 1), v34)), <=(+(v37, 1), v33)), >(+(v36, 1), 3)), <=(-(v36, 2), v35)), <=(-(v36, 2), v34)), <=(-(v36, 2), v33)), >(+(v35, 1), 1)), >(+(v34, 1), 1)), >(+(v33, 1), 1))

(7) Obligation:

Rules:
f1710_0_reverse_Store(v15, v16, v17) → f1710_0_reverse_Store(v18, v19, v20) | &&(&&(&&(&&(&&(&&(>(+(v20, 1), 3), >(+(v19, 1), 0)), <=(+(v19, 1), v16)), >(+(v18, 1), 1)), >(+(v17, 1), 1)), >(+(v16, 1), 1)), >(+(v15, 1), 1))
f1710_0_reverse_Store(v21, v22, v23) → f1710_0_reverse_Store(v24, v25, v26) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v26, 1), 3), <=(-(v26, 2), v23)), <=(-(v26, 2), v22)), <=(-(v26, 2), v21)), >(+(v25, 1), 0)), <=(+(v25, 1), v23)), <=(+(v25, 1), v22)), >(+(v24, 1), 1)), >(+(v23, 1), 1)), >(+(v22, 1), 1)), >(+(v21, 1), 1))
f1710_0_reverse_Store(v27, v28, v29) → f1710_0_reverse_Store(v30, v31, v32) | &&(&&(&&(&&(&&(&&(&&(>(+(v32, 1), 3), >(+(v31, 1), 0)), <=(+(v31, 1), v28)), <=(+(v31, 1), v27)), >(+(v30, 1), 3)), >(+(v29, 1), 1)), >(+(v28, 1), 1)), >(+(v27, 1), 1))
f1710_0_reverse_Store(v33, v34, v35) → f1710_0_reverse_Store(v36, v37, v38) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v38, 1), 3), <=(-(v38, 2), v35)), <=(-(v38, 2), v34)), <=(-(v38, 2), v33)), >(+(v37, 1), 0)), <=(+(v37, 1), v35)), <=(+(v37, 1), v34)), <=(+(v37, 1), v33)), >(+(v36, 1), 3)), <=(-(v36, 2), v35)), <=(-(v36, 2), v34)), <=(-(v36, 2), v33)), >(+(v35, 1), 1)), >(+(v34, 1), 1)), >(+(v33, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f1710_0_reverse_Store(x)] = 1·x2

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



Therefore the following rule(s) have been dropped:


f1710_0_reverse_Store(x0, x1, x2) → f1710_0_reverse_Store(x3, x4, x5) | &&(&&(&&(&&(&&(&&(>(+(x5, 1), 3), >(+(x4, 1), 0)), <=(+(x4, 1), x1)), >(+(x3, 1), 1)), >(+(x2, 1), 1)), >(+(x1, 1), 1)), >(+(x0, 1), 1))
f1710_0_reverse_Store(x6, x7, x8) → f1710_0_reverse_Store(x9, x10, x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x11, 1), 3), <=(-(x11, 2), x8)), <=(-(x11, 2), x7)), <=(-(x11, 2), x6)), >(+(x10, 1), 0)), <=(+(x10, 1), x8)), <=(+(x10, 1), x7)), >(+(x9, 1), 1)), >(+(x8, 1), 1)), >(+(x7, 1), 1)), >(+(x6, 1), 1))
f1710_0_reverse_Store(x12, x13, x14) → f1710_0_reverse_Store(x15, x16, x17) | &&(&&(&&(&&(&&(&&(&&(>(+(x17, 1), 3), >(+(x16, 1), 0)), <=(+(x16, 1), x13)), <=(+(x16, 1), x12)), >(+(x15, 1), 3)), >(+(x14, 1), 1)), >(+(x13, 1), 1)), >(+(x12, 1), 1))
f1710_0_reverse_Store(x18, x19, x20) → f1710_0_reverse_Store(x21, x22, x23) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x23, 1), 3), <=(-(x23, 2), x20)), <=(-(x23, 2), x19)), <=(-(x23, 2), x18)), >(+(x22, 1), 0)), <=(+(x22, 1), x20)), <=(+(x22, 1), x19)), <=(+(x22, 1), x18)), >(+(x21, 1), 3)), <=(-(x21, 2), x20)), <=(-(x21, 2), x19)), <=(-(x21, 2), x18)), >(+(x20, 1), 1)), >(+(x19, 1), 1)), >(+(x18, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: ListReverseCyclicList.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 17 IRules

P rules:
f301_0_createList_Load(EOS, i35, o40[List.n]o42) → f304_0_createList_LE(EOS, i35, i35, o40[List.n]o42)
f304_0_createList_LE(EOS, i39, i39, o40[List.n]o42) → f309_0_createList_LE(EOS, i39, i39, o40[List.n]o42)
f309_0_createList_LE(EOS, i39, i39, o40[List.n]o42) → f314_0_createList_New(EOS, i39, o40[List.n]o42) | >(i39, 0)
f314_0_createList_New(EOS, i39, o40[List.n]o42) → f319_0_createList_Duplicate(EOS, i39, o40[List.n]o42)
f319_0_createList_Duplicate(EOS, i39, o40[List.n]o42) → f324_0_createList_Load(EOS, i39, o40[List.n]o42)
f324_0_createList_Load(EOS, i39, o40[List.n]o42) → f329_0_createList_InvokeMethod(EOS, i39, o40[List.n]o42)
f329_0_createList_InvokeMethod(EOS, i39, o40[List.n]o42) → f334_0__init__Load(EOS, i39, o40[List.n]o42)
f334_0__init__Load(EOS, i39, o40[List.n]o42) → f362_0__init__InvokeMethod(EOS, i39, o40[List.n]o42)
f362_0__init__InvokeMethod(EOS, i39, o40[List.n]o42) → f377_0__init__Load(EOS, i39, o40[List.n]o42)
f377_0__init__Load(EOS, i39, o40[List.n]o42) → f385_0__init__Load(EOS, i39, o40[List.n]o42)
f385_0__init__Load(EOS, i39, o40[List.n]o42) → f393_0__init__FieldAccess(EOS, i39, o40[List.n]o42)
f393_0__init__FieldAccess(EOS, i39, o40[List.n]o42) → f403_0__init__Return(EOS, i39, o40[List.n]o42)
f403_0__init__Return(EOS, i39, o40[List.n]o42) → f411_0_createList_Store(EOS, i39, o40[List.n]o42)
f411_0_createList_Store(EOS, i39, o40[List.n]o42) → f417_0_createList_JMP(EOS, i39, o40[List.n]o42)
f417_0_createList_JMP(EOS, i39, o40[List.n]o42) → f440_0_createList_Inc(EOS, i39, o40[List.n]o42)
f440_0_createList_Inc(EOS, i39, o40[List.n]o42) → f295_0_createList_Inc(EOS, i39, o47[List.n]o42)
f295_0_createList_Inc(EOS, i32, o40[List.n]o42) → f301_0_createList_Load(EOS, +(i32, -1), o40[List.n]o42)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f301_0_createList_Load(x1, x2, x3) → f301_0_createList_Load(x2, x3)
Cond_f301_0_createList_Load(x1, x2, x3, x4, x5) → Cond_f301_0_createList_Load(x1, x3, x4, x5)

Filtered unneeded terms:


Cond_f301_0_createList_Load(x1, x2, x3, x4) → Cond_f301_0_createList_Load(x1, x2)
f301_0_createList_Load(x1, x2) → f301_0_createList_Load(x1)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

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

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f301_0_createList_Load(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(14) YES