| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle mixed_sigmas.pvs Sprache: PVS |
|||||||||
|
mixed_sigmas[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 sigma[T],sigma[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_sigmas_const_eq: LEMMA thigh-tlow = hhigh-hlow AND (FORALL (i:nat): i<=thigh-tlow IMPLIES F(tlow + i) = G(hlow + i)) IMPLIES x*sigma[T](tlow,thigh,F) = x*sigma[H](hlow,hhigh,G) mixed_sigmas_eq: LEMMA thigh-tlow = hhigh-hlow AND (FORALL (i:nat): i<=thigh-tlow IMPLIES F(tlow + i) = G(hlow + i)) IMPLIES sigma[T](tlow,thigh,F) = sigma[H](hlow,hhigh,G) END mixed_sigmas ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28