PUBS: A Practical Upper Bounds Solver
```
class Delete{
static void del(ListReverse l, int p, int a[], int la, int b[], int lb){
while (l!=null){
if (l.data < p)
la=rm_vec(l.data,a,la);  //la=la-1;
else
lb=rm_vec(l.data,b,lb);  //lb=lb-1;
l=l.next;
}
}

static int rm_vec(int e, int a[], int la){
int i=0;
while (i < la && a[i]=0,la>=0,lb>=0

loop1[l,la,lb] ==   2,

size: l=0

loop1[l,la,lb] ==   23 +  loop2[lb,0] + loop1[l',la,lb'],

size: lb>= -1 , lb-1 <= lb' <= lb , l-l'>=1 , l'>=0

loop1[l,la,lb] ==   27 +  loop3[lb,j] + loop2[lb,0] + loop1[l',la,lb'],

size: lb >= j ,  j>=0   , lb-1 <= lb' <= lb , l-l'>=1 , l'>=0

loop1[l,la,lb] ==   24 +  loop2[la,0] + loop1[l',la',lb],

size: la>= -1 , la-1 <= la' <= la  , l-l'>=1 , l'>=0

loop1[l,la,lb] ==   28 +  loop3[la,j] + loop2[la,0] + loop1[l',la',lb],

size: la-1 <= la' <= la , la >=j , j>=0  , l-l'>=1 , l'>=0

-------------------------------------------------
loop2[la,i] ==   3,
size: i>=la , i>=0 ,

loop2[la,i] ==   8,
size: i=0 ,

loop2[la,i] ==   10 + loop2[la,i'],

size: i < la , i>=0 , i'= i+1

--------------------------------------------------
loop3[la,j] ==   5,

size: j>= la-1 , j>=0

loop3[la,j] ==   15 + m2[la,j'],

size: j < la-1, j>=0 , j'=j+1

*/

```