| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 821 B |
|
SSL group_rew.pvs Sprache: PVS |
|||||||||
|
group_rew[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN ASSUMING IMPORTING group_def[T,*,one] fullset_is_group: ASSUMPTION group?(fullset[T]) ENDASSUMING IMPORTING group[T,*,one] S,R: VAR set[T] H,G: VAR group a,b,x,y,z: VAR T m: VAR nat i,j: VAR int inv_left : LEMMA inv(x) * x = one inv_right : LEMMA x * inv(x) = one inv_inv : LEMMA inv(inv(x)) = x inv_one : LEMMA inv(one) = one inv_in : LEMMA FORALL (a:(G)): G(inv(a)) expt_0 : LEMMA a^0 = one expt_1 : LEMMA a^1 = a expt_m1 : LEMMA a^(-1) = inv(a) one_expt : LEMMA one^i = one one_left : LEMMA one * x = x one_right : LEMMA x * one = x END group_rew ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28