|
%------------------------------------------------------------------------------
% horizontal_los_criterion.pvs
%
%------------------------------------------------------------------------------
horizontal_los_criterion : THEORY
BEGIN
IMPORTING repulsive
s,
vo,vi,
nvo,nvi : VAR Nz_vect2
eps : VAR Sign
horizontal_los_criterion(s, vo, vi, nvo, eps): MACRO bool = repulsive_criteria(s,vo-vi,eps)(nvo-vi)
horizontal_los_criterion_repulsive: LEMMA
horizontal_los_criterion(s,vo,vi,nvo,eps)
IMPLIES
repulsive?(s,vo-vi)(nvo-vi)
horizontal_los_criterion_coordinately_repulsive: LEMMA
horizontal_los_criterion(s,vo,vi,nvo,eps) AND
horizontal_los_criterion(-s,vi,vo,nvi,eps)
IMPLIES
repulsive?(s,vo-vi)(nvo-nvi)
END horizontal_los_criterion
¤ 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.
|
