| products/sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: mf8llt Sprache: PVSOriginal von: PVS© |
|
||||||
|
mixed_products[T, H: TYPE FROM int]: THEORY
BEGIN ASSUMING connected_domain1: ASSUMPTION (FORALL (x, y: T), (z: integer): x <= z AND z <= y IMPLIES T_pred(z)) connected_domain2: ASSUMPTION (FORALL (x, y: H), (z: integer): x <= z AND z <= y IMPLIES H_pred(z)) ENDASSUMING IMPORTING product[T],product[H] tlow : VAR T_low[T] thigh : VAR T_high[T] hlow : VAR T_low[H] hhigh : VAR T_high[H] i,j : VAR T k,l : VAR H rng, nn : VAR nat pn : VAR posnat z : VAR int a,x,B : VAR real F : VAR [T -> real] G : VAR [H -> real] mixed_products_const_eq: LEMMA thigh-tlow = hhigh-hlow AND (FORALL (i:nat): i<=thigh-tlow IMPLIES F(tlow + i) = G(hlow + i)) IMPLIES x*product[T](tlow,thigh,F) = x*product[H](hlow,hhigh,G) mixed_products_eq: LEMMA thigh-tlow = hhigh-hlow AND (FORALL (i:nat): i<=thigh-tlow IMPLIES F(tlow + i) = G(hlow + i)) IMPLIES product[T](tlow,thigh,F) = product[H](hlow,hhigh,G) END mixed_products ¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
