```// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Given an array a[0..N-1], the algorithm below determines its maximum using //
// O(N^1.5) processors in constant time. Thus, it improves Maximum_O1 in that //
// less processors are required while still requiring only O(1) time.         //
// It is possible to generate another algorithm that applies the algorithm    //
// below analogously to the use of Maximum_O1 here which then yields another  //
// algorithm to compute the maximum in time O(1) using only O(N^1.25) proc.   //
// This can be repeated as often as desired to generate algorithms that run   //
// in time O(1) requiring only O(N^1.5), O(N^1.25), O(N^1.125), ... processors//
// so that we can speak of an algorithm that requires only O(N^{1+eps}) many  //
// processors to compute the maximum in time O(1).                            //
// ************************************************************************** //

macro M = 8;
macro N = M*M;
macro R = 32;

macro isArrayMax(a,x)   = forall(i=0..N-1) (a[i] <= x);
macro isArrayMin(a,x)   = forall(i=0..N-1) (a[i] >= x);
macro contains(a,x)     = exists(i=0..N-1) (a[i] == x);

module Maximum_O1Opt([N]int{R} ?a, int{R} max) {
event [N]bool m0;
event [M]bool m1;
event [M]int{R} a1;

// apply algorithm Maximum_O1 to each subsequence of size M in parallel;
// this requires time O(1) using M^3 processors
for(k=0..M-1) {
// compute maximum of block a[k*M..(k+1)*M-1]
// set m0[i] iff some a[j] is greater than a[i]
for(i=0..M-1)
for(j=0..M-1)
if(a[k*M+i] < a[k*M+j])
m0[k*M+i] = true;
// thus, those i where m[i] is false are the indices of the maximum a[i]
// note: there might be several such indices (containing the same value)
for(i=0..M-1)
if(!m0[k*M+i])
a1[k] = a[k*M+i];
}
// at this stage, we determined the maxima m1[0..M-1] of all subsequences of
// size M; thus, we finally apply algorithm Maximum_O1 once more to compute
// the maximum of this array which is also the maximum of array a
// set m1[i] iff some m0[j] is greater than m0[i]
for(i=0..M-1)
for(j=0..M-1)
if(a1[i] < a1[j])
m1[i] = true;
// thus, those i where m1[i] is false are the indices of the maximum a[i]
// again, there might be several such indices (containing the same value)
for(i=0..M-1)
if(!m1[i])
max = a1[i];
}
satisfies {
correct : assert(contains(a,max) & isArrayMax(a,max));
}
drivenby {
for(i=0..N/2-1)
a[i] = i;
for(i=N/2..N-1)
a[i] = N-1-i;
assert(contains(a,max) & isArrayMax(a,max));
}
```