Examples
~~~~~~~~

predicate smallestIndex( int index, int cur, int[] a ) {
    // true if a[index] is not greater than any element in
    // a[cur]..a[a.length-1]
    cur >= a.length() ||
	( a[index] <= a[cur] &&
	  smallestIndex( index, cur+1, a ) );
}

predicate smallestIndex( int index, int[] a ) {
    foreach ( int v = a[int cur] ) {
	v >= a[index]
    }
}

TODO:  translation for some subset of language
    - handle functions but not objects
    - formalize translation
    - if it helps, put objects into target language