prog_ver_ex                : THEORY

  BEGIN

  n:int
  i:VAR posnat
  AType: TYPE+
  key: VAR AType


  A(i:{k:nat|1<=k&k<=n}):AType

  V(i,key):bool = (0<= n)
  B(i,key):bool = (i<=n & A(i)/=key)
  I(i,key):bool = (1<=i)&(i<=n+1)& (forall (j:{k:posnat|k<=i-1}): A(j)/=key)
  P(i,key):bool = 1<=i & i<=n+1 &  (forall (j:{k:posnat|k<=i-1}): A(j)/=key)
                   & (i=n+1 OR A(i)=key)

  Condition1: PROPOSITION V(i,key) => I(1,key)
  Condition2: PROPOSITION I(i,key)& B(i,key) => I(i+1,key)
  Condition3: PROPOSITION I(i,key)& NOT B(i,key) => P(i,key)


  END prog_ver_ex