```// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// Find the first element of an array that has a certain property. In the case//
// below, the property has already been applied to form a boolean array, and  //
// thus, we seek the index of the first "true" in the array.                  //
// The algorithm requires time O(1) using O(N^2) processors.                  //
// ************************************************************************** //

macro N = 16;

module FirstOne([N]bool ?a,nat{N} index, event !rdy) {
[N]bool x;

// use O(N) processors to copy a to x; one might apply a desired property
// to a[i] before copying, so that arbitrary properties can be checked
for(i=0..N-1)
x[i] = a[i];

// use O(N^2) processors to erase all x[i] that do not have the least index
for(i=0..N-2)
for(j=i+1..N-1)
if(x[i] & x[j])
next(x[j]) = false;
pause;

// here, at most one x[i] is true; if so, i is the desired index
for(i=0..N-1)
if(x[i])
index = i;
emit(rdy);
}
drivenby {
for(i=0..N-1)
a[i] = i==3 | i==5 | i==7;
await(rdy);
assert(a[index] -> forall(i=0..N-1) (i<index -> !a[i]));
}
```