Quelle  indexed_sets_extra.pvs

% supplement to indexed_sets: monotony properties
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Dec 2004

indexed_sets_extra[index, T: TYPE]: THEORY

BEGIN

  IMPORTING indexed_sets[index, T]

  i: VAR index
  A, B: VAR [index -> set[T]]

  IUnion_is_monotone: LEMMA
    (FORALL i: subset?(A(i), B(i))) =>
      subset?(IUnion(A), IUnion(B))

  IIntersection_is_monotone: LEMMA
    (FORALL i: subset?(A(i), B(i))) =>
      subset?(IIntersection(A), IIntersection(B))

END indexed_sets_extra