| products/sources/formale sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sqrt_rew.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% Monoids % % 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 %------------------------------------------------------------------------------ monoid[T:Type+,*:[T,T->T],one:T]: THEORY BEGIN ASSUMING IMPORTING monoid_def[T,*,one], semigroup_def fullset_is_monoid: ASSUMPTION monoid?(fullset[T]) ENDASSUMING IMPORTING monoid_def[T,*,one], monad[T,*,one], semigroup[T,*] monoid: TYPE+ = (monoid?) CONTAINING fullset[T] S: VAR set[T] M: VAR monoid a: VAR T n,m: VAR nat monoid_is_monad: JUDGEMENT monoid SUBTYPE_OF monad monoid_is_semigroup: JUDGEMENT monoid SUBTYPE_OF semigroup submonoid?(S,M): bool = subset?(S,M) AND monoid?(S) power_0: LEMMA power(a,0) = one power_1: LEMMA power(a,1) = a one_power: LEMMA power(one,n) = one power_def: LEMMA power(a,n+1) = power(a,n)*a power_mult: LEMMA power(a,n)*power(a,m) = power(a,n+m) power_power: LEMMA power(power(a,n),m) = power(a,n*m) power_commutes: LEMMA power(a,n)*power(a,m) = power(a,m)*power(a,n) power_member: LEMMA member(a,M) IMPLIES member(power(a,n),M) one_is_monoid: LEMMA monoid?(singleton[T](one)) AUTO_REWRITE+ power_0 AUTO_REWRITE+ power_1 AUTO_REWRITE+ one_power AUTO_REWRITE+ one_is_monoid generated_is_submonoid: LEMMA member(a,M) IMPLIES submonoid?(generated_set(a),M) generated_set_card_1: LEMMA member(a,M) AND is_finite(generated_set(a)) AND card(generated_set(a)) = 1 IMPLIES a = one AND generated_set(a) = singleton[T](one) finite_monoid: TYPE+ = (finite_monoid?) F: VAR finite_monoid finite_monoid_is_monoid: JUDGEMENT finite_monoid SUBTYPE_OF monoid finite_monoid_is_finite_monad: JUDGEMENT finite_monoid SUBTYPE_OF finite_monad finite_submonoids: LEMMA submonoid?(S,M) IMPLIES finite_monoid?(F) commutative_monoid: TYPE+ = (commutative_monoid?) commutative_monoid_is_monoid: JUDGEMENT commutative_monoid SUBTYPE_OF monoid commutative_monoid_is_commutative_monad: JUDGEMENT commutative_monoid SUBTYPE_OF commutative_monad H: VAR commutative_monoid commutative_submonoids: LEMMA submonoid?(S,H) IMPLIES commutative_monoid?(S) END monoid ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
