| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle opt_vertical.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% opt_vertical.pvs % ACCoRD v.1.0 %------------------------------------------------------------------------------ opt_vertical[D,H:posreal] : THEORY BEGIN IMPORTING opt_trk_gs[D], vertical_criterion[D,H] s,nvo : VAR Vect3 sp : VAR Sp2_vect3 vo,vi : VAR Nzv2_vect3 epsh,epsv : VAR Sign opt_vertical(s,vo,vi,epsh,epsv): {nvo | nz_vect2?(nvo) => horizontal_only?(vo)(nvo)} = IF vo`z = vi`z THEN zero ELSE LET v = vo-vi, dir:Sign = IF abs(s`z) >= H THEN epsv*sign(s`z) ELSE Entry ENDIF, t = Theta_H(s`z,v`z,-dir) IN IF t > 0 AND epsv = sign(s`z + t*v`z) THEN LET nvo2 = opt_trk_gs_vertical(s,vo,vi,t,dir) IN IF horizontal_los?(s) OR horizontal_criterion?(s,epsh)(nvo2-vo) THEN nvo2 WITH [z |-> vo`z] ELSE zero ENDIF ELSE zero ENDIF ENDIF opt_vertical?(s,vo,vi,epsh,epsv)(nvo) : bool = nz_vect2?(nvo) AND nvo = opt_vertical(s,vo,vi,epsh,epsv) %------------% % LEMMAS % %------------% opt_vertical_meets_horizontal_criterion : THEOREM opt_vertical?(sp,vo,vi,epsh,epsv)(nvo) IMPLIES horizontal_criterion?(sp,epsh)(nvo-vo) opt_vertical_meets_vertical_criterion : THEOREM opt_vertical?(s,vo,vi,epsh,epsv)(nvo) IMPLIES vertical_criterion?(epsv)(s,vo-vi)(nvo-vi) END opt_vertical ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28