%
% types for the computation of the next history vector
%
% $Id: types.pvs,v 1.5 2001/07/09 13:35:09 sbeyer Exp $
%
% $Log: types.pvs,v $
% Revision 1.5  2001/07/09 13:35:09  sbeyer
% * simplified import-chain
%
% Revision 1.4  2001/07/09 09:09:49  sbeyer
% * now using arrays for history_vector (since it is supported by pvs2hdl)
%
% Revision 1.3  2001/05/29 12:30:50  sbeyer
% * removed EXPORTING declaration
%
% Revision 1.2  2001/05/28 14:58:56  sbeyer
% * simplified importchain
%
% Revision 1.1  2001/03/09 13:31:35  sbeyer
% *** empty log message ***
%

history_types[K   :upfrom(2),
              logK:posnat]: THEORY
BEGIN
  ASSUMING
    logK_is_logK: ASSUMPTION 
      2^(logK-1) < K AND K <= 2^logK;
  ENDASSUMING

  basics : LIBRARY = "../basics";

  IMPORTING
    basics@basics;

  history_indext : TYPE+ = below(K);
  hit_vectort    : TYPE+ = bvec[K];
  history_datat  : TYPE+ = bvec[logK];
  history_vectort: TYPE+ = [below(K) -> bvec[logK]];

END history_types