Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Delphi/Bille 0.71/ (Columbo Version 0.7^©) Datei vom 17.0.2013 mit Größe 36 kB

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

quality94%