|
tarski_query: THEORY
BEGIN
IMPORTING poly_families, reals@product_nat,
matrices@tensor_product, matrices@matrices,
matrices@query_coeff
a,r,g : VAR [nat->int]
n : VAR posnat
d,i,j,k : VAR nat
m: VAR posnat
x,y,c,b : VAR real
rel: VAR [[real,real]->bool]
babove,bbelow,bbelow2,babove2: VAR bool
% k is the degree of g
NSol_squared_gt: LEMMA a(n)/=0 IMPLIES
NSol(a,n,polynomial_prod(g,k,g,k),2*k,>) =
NSol(a,n,g,k,/=)
NSol_squared_lt: LEMMA a(n)/=0 IMPLIES
NSol(a,n,polynomial_prod(g,k,g,k),2*k,<) = 0
NSol_poly1_lt: LEMMA a(n)/=0 IMPLIES
NSol(a,n,poly1,0,<)=0
A3: {M: PosFullMatrix | rows(M)=3 AND columns(M)=3} =
(: (: 1, 0, -1 :), (: 0, 1/2, 1/2 :), (: 0, -1/2, 1/2 :) :)
A3_inv: {M: PosFullMatrix | rows(M)=3 AND columns(M)=3 AND det(M)/=0 AND inverse(M)=A3} =
(: (: 1,1,1 :), (: 0,1,-1 :), (: 0,1,1 :) :)
TQ_vect3(a,(n|a(n)/=0),g,(k|g(k)/=0)): {v: PosFullMatrix | rows(v)=3 AND columns(v)=1} =
(: (: TQ(a,n,poly1,0) :),(: TQ(a,n,g,k) :), (: TQ(a,n,polynomial_prod(g,k,g,k),2*k) :) :)
NSol_vect3(a,(n|a(n)/=0),g,(k|g(k)/=0)): {v: PosFullMatrix | rows(v)=3 AND columns(v)=1} =
(: (: NSol(a,n,g,k,=) :),(: NSol(a,n,g,k,>) :), (: NSol(a,n,g,k,<) :) :)
tarski_query_system_basic_3: LEMMA a(n)/=0 AND g(k)/=0 IMPLIES
A3*TQ_vect3(a,n,g,k) = NSol_vect3(a,n,g,k)
A6: {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 :) :)
NSol_vect6(a,(n|a(n)/=0),g,(k|g(k)/=0)): {v: PosFullMatrix | rows(v)=6 AND columns(v)=1} =
(: (: NSol(a,n,g,k,=) :),(: NSol(a,n,g,k,>) :), (: NSol(a,n,g,k,<) :),
(: NSol(a,n,g,k,/=) :),(: NSol(a,n,g,k,>=) :), (: NSol(a,n,g,k,<=) :) :)
tarski_query_system_basic_6: LEMMA a(n)/=0 AND g(k)/=0 IMPLIES
A6*TQ_vect3(a,n,g,k) = NSol_vect6(a,n,g,k)
END tarski_query
¤ Dauer der Verarbeitung: 0.16 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.
|
