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]VAR [nat->T]VAR natVAR intVAR natVAR intVAR (preorder?[T])VAR TLAMBDA (k:subrange(i,j),t:T):t o F(k))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)LEMMA IF i <= j THEN big_ops_nat(i,j-1,F) o F(j) ELSE id ENDIF )LEMMA IF i <= j THEN F(i) o big_ops_nat(i+1,j,F) ELSE id ENDIF )LEMMA AND z<=j IMPLIES LEMMA IMPLIES LAMBDA (k:nat): IF k+p>=0 THEN F(k+p) ELSE id ENDIF )LEMMA IMPLIES LAMBDA (k:nat): IF i+j-k>=0 THEN F(i+j-k) ELSE id ENDIF )LEMMA FORALL (k:nat): i<=k AND k<=j IMPLIES F(k) = id) IMPLIES big_ops_nat(i,j,F)=idLEMMA IMPLIES LAMBDA (k:nat): F(k) o G(k))VAR [[T,T]->T]LEMMA AND FORALL (t1,t2,t3:T): t1 * (t2 o t3) = (t1 * t2) o (t1 * t3)) IMPLIES LAMBDA (k:nat): c * F(k))END big_ops_natquality 71%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
