Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Diff

public class Diff {

    // We assume that A and B have no repetitions.

 static void dif(int[] A, int[] B, int[] D){

    int k=0;

    int i=0;

    int l1=A.length;

    int l2=B.length;

    boolean found;

    while(i<l1){

        int j=0;

        found=false;

	while((j<l2)&&(!found)){

	  if(A[i]==B[j]) found=true;

	  else j++;

         }



	if (!found) {

            D[k]=A[i];

	    k++;

	}

      i++;

    }

 }



    public static void main(String[] args) {

	dif(new int[20],new int[20],new int[20]);

    }

}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 664 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) TRUE