(0) Obligation:

JBC Problem based on JBC Program:
public class Hanoi {
private void solve(int h, int from, int to, int support) {
if (h < 1) return;
else if (h == 1) {
//System.out.println("from " + from + " to " + to + "\n");
}
else {
solve(h - 1, from, support, to);
//System.out.println("from " + from + " to " + to + "\n");
solve(h - 1, support, to, from);
}
}

public static void main(String[] args) {
new Hanoi().solve(5,1,2,3);
}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE