Quellcode-Bibliothek remainder_sequence.pvs Sprache: PVS

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

quality97%

¤ 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.0.15Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.