|
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.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
