%------------------------------------------------------------------------- % % The relationship between the cardinality comparison functions when % applied to finite sets, and the finite_sets card(S) function. % % For PVS version 3.2. November 4, 2004 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: finite_sets[T1], finite_sets[T2] % sets_aux: card_comp_set[T1,T2], card_comp_set[T2,T1], % card_comp_set_props[T1,T2], card_finite[T1,T2] % %-------------------------------------------------------------------------
card_finite[T1: TYPE, T2: TYPE]: THEORY BEGIN
