(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: ListInt
`/** * A set of functions over lists of integers. * * All calls terminate. * * Julia + BinTerm prove that all calls terminate * * Note that cyclicity is introduced by the statement * <tt>l1.tail.tail = l1</tt>. However, this is not enough to induce * non-termination in the program. If you instead uncomment the line * <tt>l0.tail.tail = l0</tt>, most of the calls cannot be proved to terminate * anymore. * * @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A> */public class ListInt {    private int head;    private ListInt tail;    public static void main(String[] args) {	ListInt l0 = new ListInt(5,new ListInt(6,null));	ListInt l1 = new ListInt(1,new ListInt(3,null));	l0.merge(l1);	l1.tail.tail = l1;	//l0.tail.tail = l0;	l0.append(l1);	l0.iter();	l0.reverseAcc(null);	l0.reverse();    }    public ListInt(int head, ListInt tail) {	this.head = head;	this.tail = tail;    }    private void iter() {	if (tail != null) tail.iter();    }    private ListInt append(ListInt other) {	if (tail == null) return new ListInt(head,other);	else return new ListInt(head,tail.append(other));    }    private ListInt reverseAcc(ListInt acc) {	if (tail == null) return new ListInt(head,acc);	else return tail.reverseAcc(new ListInt(head,acc));    }    private ListInt reverse() {	if (tail == null) return this;	else return tail.reverse().append(new ListInt(head,null));    }    private ListInt merge(ListInt other) {	if (other == null) return this;	else if (head <= other.head)	    if (tail != null) return new ListInt(head,tail.merge(other));	    else return new ListInt(head,other);	else return new ListInt(other.head,merge(other.tail));    }}`

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
ListInt.main([Ljava/lang/String;)V: Graph of 277 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs: