products/sources/formale Sprachen/Delphi/Bille 0.71/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 17.0.2013 mit Größe 36 kB image not shown  

Quelle  ring_nz_closed_def.pvs   Sprache: unbekannt

 
%------------------------------------------------------------------------------
% 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

94%


[ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ]