Quelle tarski_query_matrix.pvs Sprache: PVS

tarski_query_matrix: THEORY
BEGIN

IMPORTING tarski_query

  a,r,g : VAR [nat->int]
  n : VAR posnat
  d,i,j,k : VAR nat
  m: VAR posnat
  %m : VAR posnat
  x,y,c,b : VAR real
  rel: VAR [[real,real]->bool]
  babove,bbelow,bbelow2,babove2: VAR bool
  p : VAR nat

  GF: VAR [nat->[nat->int]]
  KF: VAR [nat->nat] % degrees
  GP: VAR [nat->subrange(0,2)]
  RelF,RelF1,RelF2: VAR [nat->subrange(-1,1)]
  ll: VAR list[int]

  TQ_vect3k(k,a,(n|a(n)/=0),GF,(KF|FORALL (i:upto(k)):GF(i)(KF(i))/=0)): {v: PosFullMatrix | rows(v)=3^(k+1) AND columns(v)=1} =
    LET GPFun = (LAMBDA (i,j): base_n(3,i)),
     eij = (LAMBDA (i,j): IF i>=3^(k+1) OR j>=1 THEN 0 ELSE TQ_fam(k,a,n,GF,KF,GPFun(i,j)) ENDIF)
    IN form_matrix(eij,3^(k+1),1)

  TQ_vect6k(k,a,(n|a(n)/=0),GF,(KF|FORALL (i:upto(k)):GF(i)(KF(i))/=0)): {v: PosFullMatrix | rows(v)=6^(k+1) AND columns(v)=1} =
    LET GPFun = (LAMBDA (i,j): base_n(6,i)),
     eij = (LAMBDA (i,j): IF i>=6^(k+1) OR j>=1 OR (EXISTS (p:upto(k)): GPFun(i,j)(p)>2) THEN 0 ELSE TQ_fam(k,a,n,GF,KF,GPFun(i,j)) ENDIF)
    IN form_matrix(eij,6^(k+1),1)

  NSol_vect3k(k,a,(n|a(n)/=0),GF,(KF|FORALL (i:upto(k)):GF(i)(KF(i))/=0)): {v: PosFullMatrix | rows(v)=3^(k+1) AND columns(v)=1} =
    LET eij = (LAMBDA (i,j): IF i>=3^(k+1) OR j>=1 THEN 0 ELSE NSol(k,a,n,GF,KF,sig_seq(base_n(3,i))) ENDIF)
    IN form_matrix(eij,3^(k+1),1)

  NSol_vect6k(k,a,(n|a(n)/=0),GF,(KF|FORALL (i:upto(k)):GF(i)(KF(i))/=0)): {v: PosFullMatrix | rows(v)=6^(k+1) AND columns(v)=1} =
    LET eij = (LAMBDA (i,j): IF i>=6^(k+1) OR j>=1 THEN 0 ELSE NSol_all(k,a,n,GF,KF,base_n(6,i)) ENDIF)
    IN form_matrix(eij,6^(k+1),1)

  A66_inv: {M: PosFullMatrix | rows(M)=6 AND columns(M)=6} =
    (: (: 1,   1,   1, 0, 0, 0 :),
                    (: 0,   1,  -1, 0, 0, 0 :),
       (: 0,   1,   1, 0, 0, 0 :),
       (: 0,  -1,  -1, 1, 0, 0 :),
       (:-1,  -1,   0, 0, 1, 0 :),
       (:-1,   0,  -1, 0, 0, 1 :) :)

  A66: {M: PosFullMatrix | rows(M)=6 AND columns(M)=6 AND M = inverse(A66_inv)} =
   (: (: 1, 0, -1, 0, 0, 0 :), (: 0, 1/2, 1/2, 0, 0, 0 :),
   (: 0, -1/2, 1/2, 0, 0, 0 :), (: 0, 0, 1, 1, 0, 0 :),
   (: 1, 1/2, -1/2, 0, 1, 0 :), (: 1, -1/2, -1/2, 0, 0, 1 :) :)

  multi_sturm_tarski_6by6: LEMMA a(n)/=0 AND
    (FORALL (i:upto(k)):GF(i)(KF(i))/=0)
    IMPLIES
    TQ_vect6k(k,a,n,GF, KF) = tensor_power_alt(A66_inv,k+1)*
    NSol_vect6k(k,a,n,GF,KF)

  multi_sturm_tarski_NSol: LEMMA a(n)/=0 AND
    (FORALL (i:upto(k)):GF(i)(KF(i))/=0)
    IMPLIES
    NSol_vect6k(k,a,n,GF,KF) = tensor_power_alt(A66,k+1)*
    TQ_vect6k(k,a,n,GF, KF)

  A63: {M: PosFullMatrix | rows(M)=6 AND columns(M)=3} =
   (: (: 1, 0, -1  :), (: 0, 1/2, 1/2  :),
   (: 0, -1/2, 1/2  :), (: 0, 0, 1 :),
   (: 1, 1/2, -1/2 :), (: 1, -1/2, -1/2 :) :)

  A63_def: LEMMA FORALL (i:upto(5),j:upto(2)):
    entry(A63)(i,j) = entry(A66)(i,j)

  multi_sturm_tarski_NSol63: LEMMA a(n)/=0 AND
    (FORALL (i:upto(k)):GF(i)(KF(i))/=0)
    IMPLIES
    NSol_vect6k(k,a,n,GF,KF) = tensor_power_alt(A63,k+1)*
    TQ_vect3k(k,a,n,GF, KF)

END tarski_query_matrix

quality80%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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.