|
%
% Divergence
%
divergence[D:posreal] : THEORY
BEGIN
IMPORTING horizontal,
predicate_coordination_2D
s : VAR Vect2
v,vo,vi,
nv,nw : VAR Vect2
nvo,nvi : VAR Vect2
eps : VAR Sign
divergence_crit?: Criterion_2D = (LAMBDA (s,v,eps): (LAMBDA (nv): s*nv > 0))
divergence_pred?: Vector_Predicate_2D = (LAMBDA (s,v): (LAMBDA (nv): NOT divergent?(s,nv)))
divergence_crit_oriented: LEMMA symmetric_oriented_2D?(divergence_crit?)
divergence_crit_sum_indep: LEMMA sum_independent_2D?(divergence_crit?, divergence_pred?)
divergence_pred_sum_closed: LEMMA sum_closed_2D?(divergence_pred?)
divergence_crit_coordinated: LEMMA coordinated_oriented_2D?(divergence_crit?,divergence_pred?)
divergence_crit_coordinated2: LEMMA
NOT divergent?(s, zero, vo - vi, zero) AND
divergence_crit?(s, vo - vi, eps)(nvo - vi) AND
divergence_crit?(-s, vi - vo, eps)(nvi - vo)
IMPLIES
divergent?(s, zero, nvo - nvi, zero)
END divergence
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
