% Arrays: function version
arrays[elem: TYPE+]: THEORY
  BEGIN

    arr: TYPE = [ nat, [nat -> elem] ]

    a,b: VAR arr
    n, i, j: VAR nat
    e: VAR elem

    anyelem: elem
    anyarray: arr

    new (n): arr = (n, (lambda n: anyelem))
    length(a): nat = a`1 
    put(a, i, e): arr = 
      IF i < a`1 THEN (a`1, a`2 WITH [(i) := e]) ELSE anyarray ENDIF
    get(a, i): elem = 
      IF i < a`1 THEN a`2(i) ELSE anyelem ENDIF

    length1: THEOREM
      FORALL(n):
        length(new(n)) = n

    length2: THEOREM
      FORALL(a, i, e):
        0 <= i AND i < length(a) IMPLIES 
          length(put(a, i, e)) = length(a)

    get1: THEOREM
      FORALL(a, i, e):
        0 <= i AND i < length(a) IMPLIES 
          get(put(a, i, e), i) = e

    get2: THEOREM
      FORALL(a, i, j, e):
        0 <= i AND i < length(a) AND 
        0 <= j AND j < length(a) AND i /= j IMPLIES 
          get(put(a, i, e), j) = get(a, j)

    unassigned: AXIOM
      FORALL(a, i): i >= a`1 IMPLIES a`2(i) = anyelem

    equality: THEOREM
      FORALL(a, b):
        a = b IFF
          length(a) = length(b) AND
          FORALL(i): 0 <= i AND i < length(a) IMPLIES get(a,i) = get(b,i)

  END arrays