% Shows that if the max delay will result in a conflict free maneuver % with a given new velocity, then any turn off to that velocity before % then will also be conflict free.
BEGIN
IMPORTING cd3d
nnt: VAR posreal % conflict time
rt : VAR posreal % future resolution time
s,v,nv,so,si,vo,vi,nvo,nvi: VAR Vect3
delay_conflict_free_rel: LEMMA
nnt <= rt AND
conflict?[D,H](s,v) AND
(NOT conflict_3D?[D,H,0,rt](s,v)) AND
(NOT conflict?[D,H](s + rt*v,nv)) IMPLIES
(NOT conflict_3D?[D,H,0,nnt](s,v)) AND
(NOT conflict?[D,H](s+nnt*v,nv))
delay_conflict_free: LEMMA
nnt <= rt AND
conflict?[D,H](so-si,vo-vi) AND
(NOT conflict_3D?[D,H,0,rt](so-si,vo-vi)) AND
(NOT conflict?[D,H]((so+rt*vo)-(si+rt*vi),nvo-vi)) IMPLIES
(NOT conflict_3D?[D,H,0,nnt](so-si,vo-vi)) AND
(NOT conflict?[D,H]((so+nnt*vo)-(si+nnt*vi),nvo-vi))
END delay_3D
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
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.
