poly_divide(g,n)(h,(m|h(m)/=0))(i): RECURSIVE DivType = IF m>n OR i>n-m THEN make_divtype(LAMBDA (j:nat): 0,0,g,n) ELSIF m = 0 THEN make_divtype((1/h(m))*g,n-m,LAMBDA (j:nat): 0,0) ELSE LET ldt = IF i=n-m THEN make_divtype(LAMBDA (j:nat): 0,n-m,g,n) ELSE poly_divide(g,n)(h,m)(i+1) ENDIF,
thisterm = ldt`rem(ldt`rdeg)/h(m) IN make_divtype(ldt`quot WITH [(i):=thisterm],
n-m,LAMBDA (j:nat): IF j>m+i THEN 0 ELSIF j<i THEN ldt`rem(j) ELSE ldt`rem(j)-thisterm*h(j-i) ENDIF,m+i-1) ENDIF MEASURE max(n-m-i+1,0)
poly_divide_def: LEMMA
h(m)/=0 IMPLIES LET pd = poly_divide(g,n)(h,m)(i) IN FORALL (x:real):
polynomial(g,n)(x) =
polynomial(pd`quot,pd`qdeg)(x)*polynomial(h,m)(x)
+ polynomial(pd`rem,pd`rdeg)(x)
poly_divide_struct: LEMMA h(m)/=0 IMPLIES LET pd = poly_divide(g,n)(h,m)(0) IN
(m=0 AND pd`rdeg = 0 AND pd`rem = (LAMBDA (i:nat): 0)) OR
(m>0 AND pd`rdeg < m)
poly_divide_lengths: LEMMA h(m)/=0 IMPLIES LET pd = poly_divide(g,n)(h,m)(i) IN
pd`qdeg = (IF i<=n-m THEN n-m ELSE 0 ENDIF) AND
pd`rdeg = (IF i>n-m THEN n ELSIF m=0 THEN 0 ELSE m+i-1 ENDIF)
END polynomial_division
¤ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet)
¤
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.
