%% Examples of strategies in Field 6.0
%% Cesar Munoz
%% http://shemesh.larc.nasa.gov/people/cam/Field
%% NASA LaRC
field_examples : THEORY
BEGIN
a,b,c : VAR real
pa,pb,pc : VAR posreal
nza,nzb : VAR nzreal
f1 : LEMMA
a > 1 AND b > 1 =>
(a+1)/((a+1)/(b+1)) - b = 1
%|- f1 : PROOF (then (skeep) (field)) QED
f2 : LEMMA
b >1 AND a > 1 =>
(b-1)/((b-1)/(a-1)) - a = -1
%|- f2 : PROOF (then (skeep) (field)) QED
f3 : LEMMA
b >1 AND a > 1 =>
(b-1)/((b-1)/(a-1)) - a < 0
%|- f3 : PROOF (then (skeep) (field)) QED
f4 : LEMMA
(pa+1)/((pa+1)/(pb+1)) - pb >= 1
%|- f4 : PROOF (then (skeep) (field)) QED
f5 : LEMMA
(1+pb+(pa*pb+pa))/(1+pa) - pb = 1
%|- f5 : PROOF (then (skeep) (field)) QED
f6 : LEMMA
a > 1 IMPLIES
a/((a-1) * (a+1)) - 1 /((a-1)*(a+1)) >= 1 /(a+1) - 1
%|- f6 : PROOF (then (skeep) (field)) QED
f7: LEMMA
1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
1/(1+ pb/(1+ 1/(1+pb))) = pa
%|- f7 : PROOF (then (skeep) (field)) QED
f8: LEMMA
1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
1/(1+ pb/(1+ 1/(1+pb))) >= pa
%|- f8 : PROOF (then (skeep) (field)) QED
f9: LEMMA
1 - pa*(pb+1) = (pa-1)/(pb+1) IMPLIES
1/(1+ pb/(1+ 1/(1+pb))) <= pa
%|- f9 : PROOF (then (skeep) (field)) QED
f10 : LEMMA
a*(pa+b)/(pa+1) - b*(pa+a)/(pa+1) = 0 IMPLIES a = b
%|- f10 : PROOF (then (skeep) (field - :cancel? t)) QED
f11 : LEMMA
a /= 1 IMPLIES
1 / (1-a) = 1 + a + a * a + (a*a*a)/(1-a)
%|- f11 : PROOF (then (skeep) (field 2)) QED
cf1 : LEMMA
4*(pa*pb) + (pa*6)*pa = pa*((c+1)*2) =>
2*pb + 3*pa - 1 = c
%|- cf1 : PROOF (then (skeep) (cancel-formula -)) QED
cf2 : LEMMA
4*(pa*pb) + (pa*6)*pa <= pa*((c+1)*2) =>
2*pb + 3*pa - c <= 1
%|- cf2 : PROOF (then (skeep) (cancel-formula -)) QED
cf3 : LEMMA
4*((pa+1)*pb) + ((pa+1)*6)*(pa+1) = -(pa+1)*((c+1)*2) IMPLIES
2*pb + 3*(pa+1) + c + 1 = 0
%|- cf3 : PROOF (then (skeep) (cancel-formula -)) QED
cf4 : LEMMA
c+2 < 0 IMPLIES
c*(c+2)*pa + pa*2*(c+2) > pb*pa*(c+2)
%|- cf4 : PROOF (then (skeep) (cancel-formula)) QED
cf5 : LEMMA
c+2 < 0 AND
c*(c+2)*pa + pa*2*(c+2) < b*pa*(c+2) IMPLIES
b < 0
%|- cf5 : PROOF (then (skeep) (cancel-formula -2)) QED
gr1 : LEMMA
a /= -4 IMPLIES
(a+3)*(a*a+9*a+20)/(a+4) = (a+3)*(a+5)
%|- gr1 : PROOF (grind-reals) QED
gr2 : LEMMA
a /= 6 AND a /= 0 AND b = 3/(a*a-6*a) IMPLIES
(a+3)/(a*(a-6)) = 1/(a-6)+b
%|- gr2 : PROOF (grind-reals) QED
gr3 : LEMMA
a /= 6 AND a /=0 IMPLIES
(a+3)/(a*(a-6)) = 1/(a-6)+3/(a*(a-6))
%|- gr3 : PROOF (grind-reals) QED
%%% The following examples are taken from developments at NASA LaRC
IMPORTING reals@sqrt
A : VAR nzreal
B,C,Delta,x : VAR real
eps : VAR {x:real|x=1 OR x=-1}
quadratic : LEMMA
Delta = (B * B) - (4 * (A * C)) AND
Delta >= 0 AND
x = (eps * sqrt(Delta) - B) / (2 * A)
IMPLIES A * x * x + B * x + C = 0
%|- quadratic : PROOF
%|- (then (skeep :preds? t) (replaces (-6 -8)) (field 2))
%|- QED
t,vix,viy,vox,voy,s : VAR real
D : VAR posreal
kb3d : LEMMA
vox > 0 AND
s*s - D*D > D AND
s * vix * voy - s * viy * vox /= 0 AND
((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) /
(s * (vix * voy - vox * viy)) * s * vox /= 0 AND
voy * sqrt(s * s - D * D) - D * vox /= 0
IMPLIES
(viy * sqrt(s * s - D * D) - vix * D) /
(voy * sqrt(s * s - D * D) - vox * D)
=
(D * D - s * s) /
(((s * s - D * D) * voy - D * vox * sqrt(s * s - D * D)) /
(s * (vix * voy - vox * viy)) * s * vox) +
vix / vox
%|- kb3d : PROOF (grind-reals) QED
END field_examples
¤ 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.
|
