"Taking on a Challenge in SPARK Ada" - Sum ghost function in post-condition having unintended behavior

I am writing a piece of software in SPARK Ada which requires the post-condition to verify that the function return value is equal to the summed values of an array. Upon proving the file where the function resides, I keep getting an error which doesn't quite add up, no pun intended (I will post screenshots of the code so as to allow a better look). The only acceptable values allowed in the array of size 10 are 0s or 1s.

This is the fix:

 function CalcST(eegR: in eegReadings) return Natural is 
  
  supT: Integer := eegR(eegR'First);
  
 begin
  
  -- Sums the number of ones in the array
  
  for Index in eegR'First + 1 .. eegR'Last  loop
     
     pragma Loop_Invariant -- 
       (supT = sumEEGR (eegR) (Index - 1));

     pragma Loop_Invariant -- additional loop invariant
       (supT <= Index - 1);
     
     if eegR(Index) = 1
       
       then supT := supT + eegR(Index);
        
     end if;
     
  end loop;
  
  return supT;
  
 end CalcST;