|
product_seq_scaf: THEORY
BEGIN
IMPORTING finite_sequences[posnat]
fs: VAR finite_sequence
product_rec(fs: finite_sequence, i: below(length(fs)) ): RECURSIVE posnat =
IF i = 0 THEN seq(fs)(0)
ELSE seq(fs)(i) * product_rec(fs,i-1)
ENDIF MEASURE i
fs1,fs2: VAR finite_sequence
n,m: VAR nat
product_rec_mult: LEMMA n < length(fs1 o fs2) IMPLIES
product_rec(fs1 o fs2,n) =
IF n < length(fs1) THEN
product_rec(fs1,n)
ELSIF length(fs1) = 0 THEN
product_rec(fs2,n)
ELSE
product_rec(fs1,length(fs1)-1)
* product_rec(fs2,n-length(fs1))
ENDIF
product_rec_caret: LEMMA n < length(fs) AND m < length(fs)
AND n <= m IMPLIES product_rec(fs, n) =
product_rec(fs ^ (0, m), n)
END product_seq_scaf
[ zur Elbe Produktseite wechseln0.3Quellennavigators
Analyse erneut starten
]
|
