### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: TestJulia5
`public class Node1 implements Node {    private Node next;    private int value;    public Node1(int value, Node next) {	this.value = value;	this.next = next;    }    public Node getNext() {	return next;    }    public void setNext(Node next) {	this.next = next;    }    public int getValue() {	return value;    }    public void setValue(int value) {	this.value = value;    }}public class Node2 implements Node {    private Node next;    private int value;    public Node2(int value, Node next) {	this.value = value;	this.next = next;    }    public Node getNext() {	return next;    }    public void setNext(Node next) {	this.next = next;    }    public int getValue() {	return value;    }    public void setValue(int value) {	this.value = value;    }}public class Node3 implements Node {    private Node next;    private int value;    public Node3(int value, Node next) {	this.value = value;	this.next = next;    }    public Node getNext() {	return next;    }    public void setNext(Node next) {	this.next = next;    }    public int getValue() {	return value;    }    public void setValue(int value) {	this.value = value;    }}public interface Node {    public Node getNext();    public void setNext(Node next);    public int getValue();    public void setValue(int value);}/** * Method main() terminates. */public class TestJulia5 {    public static void main(String[] args) {	Node last = new Node1(1,null);	Node n = new Node2(2,last);	int counter = 0;	n = new Node1(3,n);	n = new Node3(4,n);	n = new Node1(5,n);	n = new Node2(6,n);	n = new Node3(7,n);	last.setNext(n);	while (n != null && counter++ < last.getValue()) {	    if (n instanceof Node2)		n.setValue(n.getValue() + 1);	    n = n.getNext();	}    }}`

### (1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

### (2) Obligation:

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

### (3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs