exists(F_1)F_2

The semantics of exists are as follows:

F[[exists(F_1)F_2]] = F[[cut(forall(F_1)f_2)]]

forall(F_1)boolExpr

The semantics of forall is the following:
* in the forward direction:
  forall(F_1)boolExpr evaluates to a boolean value
  F_1 must be of the following form: T x = p
  boolExpr must be a boolean expression
  evaluate to true if, for each iteration of F_1, F_2 is true
  
  F[[forall(F_1)boolExpr]] = 

public boolean forall$$n$$forwards() {
  boolean flag = true;
  Enumeration e = F[[F_1]]m \Gamma C
  while(flag && e.hasNext() && T x = e.Next()) {
     Assignments F_1 with e
     flag = F[[boolExpr]]m \Gamma C;
  }
  return flag;
}


* in the backward direction:

Consider the variable we are solving for.  We want to return
an enumeration containing those variables for which the forall,
in the forwards direction, is true:

Intuitively, we do the following: we create an enumeration for
the domain of the variable we are solving for.  Then, we run the
forward direction of the forall for each value of the enumeration,
filtering out those for which it is true, and returning the enumeration.

F[[forall(F)e]] = 

class Enum implements Enumeration {
   Enumeration e;
   State s;
   boolean morevalues = false;
   Enum() { e = F[[F]]; hasMore(); }

   boolean hasMore() {
      if(!e.hasMore()) {
          return false;
      } else if (!morevalues) {
          s = e.getNext();
          Assignments of F with s
          if (e) { morevalues = true; return true; }
          else {
             return hasMore();
          }
      } else {
          return true;
      }
   }

   state getNext() {
      if (moreValues) {
          morevalues = false;
          return s;
      } else {
          if (hasNext()) {
             return s;
          } else {
             throw Exception
          }

      }
   }
}

new Enum()

Note that translation of "exists" is very similar.
    
Translation for cut F

   F[[cut F]] = Enumeration e = F[[F]]; State s = e.nextValue();


Translation for exists:

For the forward direction, it is the same exact thing

For the backward direction, it is:

F[[exists(F_1)F_2]] = F[[cut(forall(F_1)F_2)]]

Translation:

Examples:
[a,i->; a->i]
predicate si(int[] a, int i) {
   forall(int v = a[int j]) {
      a[i] <= v;
   }
}

[a,v->; a->v]
predicate contains(int[] a, int v) {
   exists(int v1 = a[int i]) {
       v == v1;
   }
}

It seems that the crux of translating things backwards is the
following: consider the varaible we are translating for.  We need to
determine how to iterate over all possible values of the variable -
perhaps inferring an iterator during typechecking is the way to go.