| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 9 B |
|
Quellcode-Bibliothek big_ops_nat.pvs Sprache: PVS |
|||||||||
|
big_ops_nat[T:Type,o:(associative?[T]),id: {tid: T | FORALL (t:T): tid o t = t AND t o tid = t}]
BEGIN IMPORTING for_iterate[T] F,G : VAR [nat->T] i : VAR nat j : VAR int z : VAR nat p : VAR int rel : VAR (preorder?[T]) c : VAR T big_ops_nat(i,j,F): T = for(i,j,id,LAMBDA(k:subrange(i,j),t:T):t o F(k)) big_ops_nat_eq: LEMMA (FORALL (k:nat): i<=k AND k<=j IMPLIES F(k)=G(k)) IMPLIES big_ops_nat(i,j,F) = big_ops_nat(i,j,G) big_ops_nat_expand_right: LEMMA big_ops_nat(i,j,F) = (IF i <= j THEN big_ops_nat(i,j-1,F) o F(j) ELSE id ENDIF) big_ops_nat_expand_left: LEMMA big_ops_nat(i,j,F) = (IF i <= j THEN F(i) o big_ops_nat(i+1,j,F) ELSE id ENDIF) big_ops_nat_split: LEMMA i-1<=z AND z<=j IMPLIES big_ops_nat(i,j,F) = big_ops_nat(i,z,F) o big_ops_nat(z+1,j,F) big_ops_nat_shift: LEMMA i+p>=0 IMPLIES big_ops_nat(i+p,j+p,F) = big_ops_nat(i,j,LAMBDA (k:nat): IF k+p>=0 THEN F(k+p) ELSE id ENDI big_ops_nat_reverse: LEMMA commutative?[T](o) IMPLIES big_ops_nat(i,j,F) = big_ops_nat(i,j,LAMBDA (k:nat): IF i+j-k>=0 THEN F(i+j-k) ELSE id ENDI big_ops_nat_id : LEMMA (FORALL (k:nat): i<=k AND k<=j IMPLIES F(k) = id) IMPLIES big_ops_nat(i,j,F)=id big_ops_nat_comp: LEMMA commutative?[T](o) IMPLIES big_ops_nat(i,j,F) o big_ops_nat(i,j,G) = big_ops_nat(i,j,LAMBDA (k:nat): F(k) o G(k)) ; * : VAR [[T,T]->T] big_ops_nat_distrib: LEMMA i<=j AND (FORALL (t1,t2,t3:T): t1 * (t2 o t3) = (t1 * t2) o (t1 * t3)) IMPLIES c * big_ops_nat(i,j,F) = big_ops_nat(i,j,LAMBDA (k:nat): c * F(k)) END big_ops_nat ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
