|
big_ops_nat[T:Type,o:(associative?[T]),id: {tid: T | FORALL (t:T): tid o t = t AND t o tid = t}]: THEORY
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 ENDIF)
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 ENDIF)
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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
