SSL ring_nz_closed_def.pvs   Interaktion und
PortierbarkeitPVS

%------------------------------------------------------------------------------
% Rings in which the nonzero elements are closed under *, definition file
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

ring_nz_closed_def[T:Type+,+,*:[T,T->T],zero:T]: THEORY

BEGIN

   IMPORTING ring_def[T,+,*,zero], groupoid_def

   S: VAR set[T]

   nz_T: Type = {x:T | x /= zero}

   nz_closed?(S): bool = star_closed?[T,*](remove(zero,S))

   ring_nz_closed?(S):bool = ring?(S) AND nz_closed?(S)

END ring_nz_closed_def