|
number_sign_changes: THEORY
BEGIN
IMPORTING reals@sign
a,b,r : VAR [nat->real]
i,j,k,d,n : VAR nat
sig: VAR real
NSC : TYPE = [# num: nat, lastnz: real #]
number_sign_changes(a,i): RECURSIVE NSC =
IF i = 0 THEN (# num:= 0, lastnz:= a(0) #)
ELSE LET prev = number_sign_changes(a,i-1)
IN IF a(i)/=0 AND prev`lastnz/=0 AND sign_ext(a(i))/=sign_ext(prev`lastnz)
THEN (# num:=prev`num+1,lastnz:=a(i) #)
ELSIF a(i)/=0
THEN prev WITH [lastnz:=a(i)]
ELSE prev
ENDIF
ENDIF MEASURE i
num : VAR nat
lastnz : VAR real
sign_changes(a,n,(i:subrange(1,n+1)),num,lastnz) : RECURSIVE
{m: nat | LET nsci = number_sign_changes(a,i-1),
nscn = number_sign_changes(a,n) IN
num = nsci`num AND lastnz = nsci`lastnz IMPLIES
m = nscn`num} =
IF i = n+1 THEN num
ELSIF a(i)/=0 AND lastnz/=0 AND sign_ext(a(i))/=sign_ext(lastnz) THEN
sign_changes(a,n,i+1,num+1,a(i))
ELSIF a(i)/=0 THEN
sign_changes(a,n,i+1,num,a(i))
ELSE
sign_changes(a,n,i+1,num,lastnz)
ENDIF
MEASURE n-i+1
num_sign_changes_def : LEMMA
number_sign_changes(a,i)`num = sign_changes(a,i,1,0,a(0))
number_sign_changes_lastnz_nonzero: LEMMA
number_sign_changes(a,i)`lastnz = 0 IFF
(FORALL (j:nat): j<=i IMPLIES a(j)=0)
number_sign_changes_lastnz: LEMMA
a(i)/=0 IMPLIES number_sign_changes(a,i)`lastnz=a(i)
number_sign_changes_eq: LEMMA
(FORALL (j:upto(i)): sign_ext(a(j))=sign_ext(b(j))) IMPLIES
LET nsca = number_sign_changes(a,i),
nscb = number_sign_changes(b,i)
IN (nsca`num = nscb`num AND sign_ext(nsca`lastnz)=sign_ext(nscb`lastnz))
testseqaa1(i):real = (-1)^i % (1,-1,1,-1,1,-1,1,-1,1,-1,...)
testseqaa2:sequence[real] = testseqaa1 WITH [6:=-1] % (1,-1,1,-1,1,-1,-1,-1,1,-1,1,...)
testseqaa3:sequence[real] = testseqaa2 WITH [7:=0] % (1,-1,1,-1,1,-1,-1,0,1,-1,1,...)
testseqaa4:sequence[real] = testseqaa1 WITH [4:=0] % (1,-1,1,-1,0,-1,1,-1,1,-1,...)
testseqaa5(i): real = IF i = 5 THEN 3 ELSIF i=6
THEN 4 ELSIF i=7 THEN 0 ELSIF i=8 THEN -4 ELSE (-1)^i ENDIF
% (1,-1,1,-1,1,3,4,0,-4,-1,1,-1,1,...)
testseqaa6(i):real = IF i = 0 OR i = 1 THEN 0 ELSE testseqaa1(i) ENDIF
number_sign_changes_easy: LEMMA number_sign_changes(testseqaa2,7 ) = (# num:=5,lastnz:=-1 #)
number_sign_changes_test1: LEMMA number_sign_changes(testseqaa1,i ) = (# num:=i,lastnz:=(-1)^i #)
number_sign_changes_test2: LEMMA number_sign_changes(testseqaa2,7 ) = (# num:=5,lastnz:=-1 #)
number_sign_changes_test3: LEMMA number_sign_changes(testseqaa2,8 ) = (# num:=6,lastnz:= 1 #)
number_sign_changes_test4: LEMMA number_sign_changes(testseqaa3,7 ) = (# num:=5,lastnz:=-1 #)
number_sign_changes_test5: LEMMA number_sign_changes(testseqaa3,9 ) = (# num:=7,lastnz:=-1 #)
number_sign_changes_test6: LEMMA number_sign_changes(testseqaa4,8 ) = (# num:=6,lastnz:= 1 #)
number_sign_changes_test7: LEMMA number_sign_changes(testseqaa5,10) = (# num:=6,lastnz:= 1 #)
nsc_regular_swap: LEMMA
k<=d AND
(FORALL (j): j<=k IMPLIES (sign_ext(a(j))=sign_ext(b(j)) OR
(sign_ext(a(j))/=sign_ext(b(j)) AND
a(j+1)/=0 AND
(j>0 IMPLIES sign_ext(a(j-1))=-sign_ext(a(j+1))) AND
(j>0 IMPLIES sign_ext(b(j-1))=-sign_ext(b(j+1))) AND
(j=0 IMPLIES sign_ext(a(0)) =-sign_ext(a(1))))))
AND sign_ext(a(k)) = sign_ext(b(k))
AND (FORALL (j:nat): j<k IMPLIES
a(j)/=0 AND b(j)/=0)
IMPLIES
LET nsca = number_sign_changes(a,k),
nscb = number_sign_changes(b,k)
IN ((k>=1 IMPLIES sign_ext(nsca`lastnz)=sign_ext(nscb`lastnz)) AND
nsca`num = nscb`num +
(IF k>=1 AND sign_ext(a(0))=-sign_ext(b(0)) THEN 1 ELSE 0 ENDIF))
nsc_edge_diff: LEMMA (sig=-1 OR sig=1) AND
k<=d AND
(FORALL (j): j<=k IMPLIES (sign_ext(a(j))=sign_ext(b(j)) OR b(j)=0))
AND (FORALL (j): 0<j AND j<=k AND b(j)=0 IMPLIES b(j-1)/=0)
AND sign_ext(a(k)) = sign_ext(b(k))
AND (FORALL (j:nat): j<k IMPLIES a(j)/=0)
AND (b(0)=0 IMPLIES sign_ext(a(0))=sig*sign_ext(a(1)))
AND (FORALL (j:nat): 0<j AND j<k AND b(j)=0 IMPLIES sign_ext(b(j-1))=-sign_ext(b(j+1)))
IMPLIES
LET nsca = number_sign_changes(a,k),
nscb = number_sign_changes(b,k)
IN ((k>=1 IMPLIES sign_ext(nsca`lastnz)=sign_ext(nscb`lastnz)) AND
nsca`num = nscb`num +
(IF k>=1 AND b(0)=0 AND sig=-1 THEN 1 ELSE 0 ENDIF))
nsc_multiroot: LEMMA (sig=-1 OR sig=1) AND
k<=d AND
(FORALL (j): 0<j AND j<=k IMPLIES sign_ext(a(j))=sig*sign_ext(b(j))) AND
sign_ext(a(0))=-sig*sign_ext(b(0)) AND
sign_ext(a(0))=-sign_ext(a(1)) AND
sign_ext(b(0))= sign_ext(b(1)) AND
(FORALL (j): j<k IMPLIES (a(j)/=0 AND b(j)/=0))
IMPLIES
LET nsca = number_sign_changes(a,k)`num,
nscb = number_sign_changes(b,k)`num
IN nsca = nscb + (IF k>=1 THEN 1 ELSE 0 ENDIF)
nsc_multiroot_full: LEMMA FORALL (sigfun:[nat->real]):
(sig=-1 OR sig=1) AND % The nominal sign
(FORALL (j): sigfun(j)=-1 OR sigfun(j)=1) AND
k<=d AND
(FORALL (j): 0<j AND j<=k IMPLIES sign_ext(a(j))=sigfun(j)*sign_ext(b(j))) AND
(FORALL (j): 0<j AND j<=k AND sigfun(j)/=sig
IMPLIES (1<j AND j<k AND sigfun(j-1)=sig AND sigfun(j+1)=sig
AND sign_ext(a(j-1))=-sign_ext(a(j+1)) AND sign_ext(b(j-1))=-sign_ext(b(j+1)))) AND
sign_ext(a(0))=-sig*sign_ext(b(0)) AND
sign_ext(a(0))=-sign_ext(a(1)) AND
sign_ext(b(0))= sign_ext(b(1)) AND
(FORALL (j): j<=k IMPLIES (a(j)/=0 AND b(j)/=0))
IMPLIES
LET nsca = number_sign_changes(a,k)`num,
nscb = number_sign_changes(b,k)`num
IN nsca = nscb + (IF k>=1 THEN 1 ELSE 0 ENDIF)
END number_sign_changes
¤ Dauer der Verarbeitung: 0.0 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.
|
