=====
>>> main.whiley
property max(int x, int y) -> (int r):
   if x >= y:
      return x
   else:
      return y

property max(int[] items, int i) -> (int r):
   if i < 0 || i >= |items|:
      return -1
   else if i+1 == |items|:
      return items[i]
   else:
      return max(items[i],max(items,i+1))

// Establish that an upper bound of the remaining items is an upper
// bound of max.
function lemma_1(int[] items, int i, int v)
requires i >= 0 && i < |items|
requires all { k in i..|items| | v >= items[k] }
ensures v >= max(items,i):
    //
    if i+1 == |items|:
       return
    else:
       lemma_1(items,i+1,v)

// Establish a correspondance between the quantified version of max,
// and the recursive property version.
function lemma_2(int[] items, int i, int v)
requires i >= 0 && i < |items|
requires all { k in i..|items| | v >= items[k] }
requires some { k in i..|items| | v == items[k] }
ensures v == max(items,i):
    //
    if i+1 == |items|:
       return
    else if items[i] != v:
       lemma_2(items,i+1,v)
    else:
       lemma_1(items,i+1,v)

// Run some tests
public export method test():
   assert max([1],0) == 1
   //
   assert max([1,2],0) == 2
   assert max([2,1],0) == 2
   //
   assert max([1,2,3],0) == 3
   assert max([1,3,2],0) == 3
   assert max([2,1,3],0) == 3
   assert max([3,2,1],0) == 3
---