|
remainder_sequence: THEORY
BEGIN
IMPORTING polynomial_pseudo_divide
a,r,g,h : VAR [nat->int]
p : VAR [nat->[nat->int]]
d,n,m,i,j,k : VAR nat
pn : VAR posnat
x,y,c,b : VAR real
curr: VAR list[list[int]]
is_neg_remainder_list?(g,(n|g(n)/=0),h,(m|h(m)/=0))(curr): bool =
(FORALL (icurr,jcurr:nat):icurr<jcurr AND jcurr<length(curr)-1
IMPLIES
length(nth(curr,icurr)) < length(nth(curr,jcurr))) AND
(FORALL (icurr:nat): icurr<length(curr) IMPLIES LET thiscurr = nth(curr,icurr) IN
length(thiscurr)>0 IMPLIES nth(thiscurr,length(thiscurr)-1)/=0) AND
(length(curr)>0 IMPLIES nth(curr,length(curr)-1) = array2list[int](n+1)(g)) AND
(length(curr)>1 IMPLIES nth(curr,length(curr)-2) = array2list[int](m+1)(h)) AND
(FORALL (j:nat): j<length(curr)-2 IMPLIES
LET pbig = list2array[int](0)(nth(curr,j+2)),
nbig = length(nth(curr,j+2))-1,
plittle = list2array[int](0)(nth(curr,j+1)),
nlittle:nat = length(nth(curr,j+1))-1
IN nth(curr,j) = adjusted_remainder(pbig,nbig)(plittle,nlittle))
compute_remainder_seq(g,(n|g(n)/=0),h,(m|h(m)/=0))
(curr:(is_neg_remainder_list?(g,n,h,m))):
RECURSIVE {crem:(is_neg_remainder_list?(g,n,h,m))|length(crem)>1 AND length(nth(crem,0))=0} =
LET currlength = length(curr) IN
IF currlength = 0 THEN
compute_remainder_seq(g,n,h,m)(cons[list[int]](array2list[int](m+1)(h),
cons[list[int]](array2list[int](n+1)(g),curr)))
ELSIF currlength = 1 THEN
compute_remainder_seq(g,n,h,m)(cons[list[int]](array2list[int](m+1)(h),
curr))
ELSIF length(nth(curr,0))=0 THEN curr
ELSE
LET csplittle = nth(curr,0),
cspbig = nth(curr,1),
newg = list2array[int](0)(cspbig),
newn = length(cspbig)-1,
newh = list2array[int](0)(csplittle),
newm = length(csplittle)-1,
newlist = adjusted_remainder(newg,newn)(newh,newm)
IN compute_remainder_seq(g,n,h,m)(cons(newlist,curr))
ENDIF MEASURE IF null?(curr) THEN m+n+4 ELSIF length(curr)=1 THEN m+n+3
ELSIF length(curr)=2 THEN m+n+2 ELSE length(nth(curr,0)) ENDIF
remainder_seq(g,(n|g(n)/=0),h,(m|h(m)/=0)):
{crem:(is_neg_remainder_list?(g,n,h,m))|length(crem)>1 AND length(nth(crem,0))=0} =
compute_remainder_seq(g,n,h,m)(null[list[int]])
sturm_chain(g,(pn|g(pn)/=0)) : MACRO list[list[int]] =
remainder_seq(g,pn,poly_deriv(g),pn-1)
remainder_seq_test: LEMMA
LET g=(LAMBDA (i:nat): IF i<=3 THEN 2 ELSIF i<=6
THEN -3 ELSE 0 ENDIF)
IN sturm_chain(g,6) =
(:(::),(:-1:),(:-579,-608:),(:2,4,55:),
(:126,140,105,120:),(:-70,-56,-42,-48,21:),
(:2,4,6,-12,-15,-18:),(:2,2,2,2,-3,-3,-3:):)
END remainder_sequence
¤ Dauer der Verarbeitung: 0.1 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.
|
