Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: tarski_query_matrix.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.