// Add explicit 'decreases' clauses so that the Dafny termination checker accepts these definitions.

function SumRange(s: seq<int>, lo: int, hi: int): int
  requires 0 <= lo <= hi <= |s|
{
  if hi == lo then 0 else SumRange(s, lo, hi - 1) + s[hi - 1]
}

function SumRange'(s: seq<int>, lo: int, hi: int): int
  requires 0 <= lo <= hi <= |s|
{
  if hi == lo then 0 else s[lo] + SumRange'(s, lo + 1, hi)
}