// Generated by lsc from majority.ts

function occOf(arr: seq<int>, x: int, n: nat): int
  requires (0 <= n)
  requires (n <= |arr|)
  decreases n
{
  if (n == 0) then
    0
  else
    (occOf(arr, x, (n - 1)) + (if (arr[(n - 1)] == x) then 1 else 0))
}

method majority(arr: seq<int>) returns (res: int)
  requires forall k: nat :: ((k < |arr|) ==> (arr[k] >= 0))
  ensures ((res == -1) || ((res >= 0) && ((2 * occOf(arr, res, |arr|)) > |arr|)))
  ensures ((exists x: nat :: ((2 * occOf(arr, x, |arr|)) > |arr|)) ==> (res != -1))
{
  var cand := 0;
  var cnt := 0;
  var i := 0;
  while (i < |arr|)
    invariant (0 <= i)
    invariant (i <= |arr|)
    invariant (cnt >= 0)
    invariant (cand >= 0)
    invariant ((2 * occOf(arr, cand, i)) <= (i + cnt))
    invariant forall y: int :: ((y != cand) ==> ((2 * occOf(arr, y, i)) <= (i - cnt)))
    decreases (|arr| - i)
  {
    if (cnt == 0) {
      cand := arr[i];
      cnt := 1;
    } else if (arr[i] == cand) {
      cnt := (cnt + 1);
    } else {
      cnt := (cnt - 1);
    }
    i := (i + 1);
  }
  var occ := 0;
  var j := 0;
  while (j < |arr|)
    invariant (0 <= j)
    invariant (j <= |arr|)
    invariant (occ == occOf(arr, cand, j))
    decreases (|arr| - j)
  {
    if (arr[j] == cand) {
      occ := (occ + 1);
    }
    j := (j + 1);
  }
  if ((2 * occ) > |arr|) {
    return cand;
  } else {
    return -1;
  }
}