|
box : THEORY
BEGIN
IMPORTING interval, structures@listn
Box : TYPE = list[Interval]
Env : TYPE = ARRAY[nat->real]
box : VAR Box
vs : VAR Env
ProperBox?(box:Box) : bool =
every(Proper?)(box)
ProperBox : TYPE = (ProperBox?)
pox : VAR ProperBox
proper_box : LEMMA
FORALL (pox:ProperBox,i:below(length(pox))) : Proper?(nth(pox,i))
proper_append : LEMMA
FORALL (pox1,pox2: ProperBox):
ProperBox?(append(pox1,pox2))
vars_in_box?(box)(vs) : bool =
FORALL(i:below(length(box))):vs(i) ## nth(box,i)
vars_in_box_rec(box:Box,n:nat,(i:nat | i+length(box) = n))(vs) : RECURSIVE
{ b : bool | b = (FORALL (k:subrange(i,n-1)): vs(k) ## nth(box,k-i)) } =
null?(box) OR (vs(i) ## car(box) AND vars_in_box_rec(cdr(box),n,i+1)(vs))
MEASURE box BY <<
vars_in_box : LEMMA
FORALL (box:Box):
vars_in_box?(box) = vars_in_box_rec(box,length(box),0)
midvars(pox) : (vars_in_box?(pox)) =
LAMBDA(v:nat) : IF v < length(pox) THEN midpoint(nth(pox,v)) ELSE 0 ENDIF
Lbbox(box:Box): listn[Interval](length(box)) =
map(LAMBDA (X:Interval): [|lb(X)|])(box)
length_Lbbox : LEMMA
length(Lbbox(pox))=length(pox)
Ubbox(box:Box): listn[Interval](length(box)) =
map(LAMBDA (X:Interval): [|ub(X)|])(box)
length_Ubbox : LEMMA
length(Ubbox(pox))=length(pox)
Midbox(box:Box): listn[Interval](length(box)) =
map(LAMBDA (X:Interval): [|midpoint(X)|])(box)
length_Midbox : LEMMA
length(Midbox(pox))=length(pox)
box1,box2 : VAR Box
Inclusion?(box1,box2) : bool =
length(box1) = length(box2) AND
FORALL(i:below(length(box1))) : nth(box1,i) << nth(box2,i)
Inclusion_reflx : LEMMA
FORALL(box:Box): Inclusion?(box,box)
Inclusion_trans : LEMMA
FORALL(box1,box2,box:Box):
Inclusion?(box1,box2) AND Inclusion?(box2,box) IMPLIES
Inclusion?(box1,box)
Inclusion_Proper : LEMMA
Inclusion?(pox,box) IMPLIES
ProperBox?(box)
Lbbox_Proper : JUDGEMENT Lbbox(pox) HAS_TYPE ProperBox
Ubbox_Proper : JUDGEMENT Ubbox(pox) HAS_TYPE ProperBox
Midbox_Proper : JUDGEMENT Midbox(pox) HAS_TYPE ProperBox
Lbbox_Inclusion : LEMMA
Inclusion?(Lbbox(pox),pox)
Ubbox_Inclusion : LEMMA
Inclusion?(Ubbox(pox),pox)
Midbox_Inclusion : LEMMA
Inclusion?(Midbox(pox),pox)
vars_in_box_Inclusion : LEMMA
Inclusion?(box1,box2) AND
vars_in_box?(box1)(vs) IMPLIES
vars_in_box?(box2)(vs)
END box
¤ Dauer der Verarbeitung: 0.18 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.
|
