| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle ring_nz_closed.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Rings in which the nonzero elements are closed under * % % This is defined so that inheriting properties of nz_T work % correctly in field, where we rejoin properties from divison rings % and intgral domains. % % % Author: Rick Butler % David Lester, Manchester University & NIA % % 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[T:Type+,+,*:[T,T->T],zero:T]: THEORY BEGIN ASSUMING IMPORTING ring_def[T,+,*,zero], ring_nz_closed_def[T,+,*,zero] fullset_is_ring_nz_closed: ASSUMPTION ring_nz_closed?(fullset[T]) ENDASSUMING IMPORTING ring_nz_closed_def[T,+,*,zero], ring[T,+,*,zero], monoid, operator_defs_more[T] ring_nz_closed: TYPE+ = (ring_nz_closed?) CONTAINING fullset[T] R: VAR ring_nz_closed x,y: VAR T nzx,nzy: VAR nz_T ring_nz_closed_is : LEMMA ring_nz_closed?(R) ring_nz_closed_is_ring : JUDGEMENT ring_nz_closed SUBTYPE_OF ring nz_T_times_nz_T_is_nz_T : JUDGEMENT *(nzx, nzy) HAS_TYPE nz_T negate_nz_T_is_nz_T : JUDGEMENT inv(nzx) HAS_TYPE nz_T times_is_zero : LEMMA x * y = zero IFF x = zero OR y = zero nz_T_times : LEMMA nzx * y = zero IFF y = zero times_nz_T : LEMMA x * nzy = zero IFF x = zero nz_T_times_nz_T_is_not_zero: LEMMA nzx * nzy /= zero sq_nz_is_nz : JUDGEMENT sq(nzx) HAS_TYPE nz_T sq_eq_zero : LEMMA sq(x) = zero IFF x = zero END ring_nz_closed ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28