| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle omega_2D.pvs Sprache: PVS |
|||||||||
|
omega_2D[D:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN IMPORTING cd2d[D,B,T], horizontal_criteria[D], vect_analysis@vect2_Heine, analysis@metric_space_real_fun[[real,Vect2],d], analysis@ms_composition_cont[[real,Vect2],d,Vect2,dist,real,real_dist], analysis@continuity_of_max_min[[real,Vect2],d], analysis@convex_function_props s,v,w : VAR Vect2 t,tlh,t1,t2 : VAR Lookahead ttt,tw,tx,ty : VAR real dir,eps : VAR Sign M : VAR real sz,vz : VAR real % 1 Distance Functions % 1.B Horizontal Distance % 1.B.2 Continuity horiz_dist_cont_scaf: LEMMA continuous?(horiz_dist_scaf(s),fullset[[Lookahead,Vect conflict_2D_on_open_interval: LEMMA conflict_2D?(s,v) IFF EXISTS (topen: Lookahead): B<topen AND topen <T AND sqv(s+topen*v)<sq(D) % 1.B.4 Trajectory Information circle_hit: LEMMA horiz_dist_scaf(s)(t,v) < M IMPLIES EXISTS (epsilon: posreal): FORALL (t1: Lookahead): abs(t1 - t) < epsilon IMPLIES horiz_dist_scaf(s)(t1,v) < M % 1.C Cylindrical Distance % 1.C.1 Definitions % 1.C.2 Continuity/Boundedness of omega/omega_2D horiz_dist_scaf_bounded_below : LEMMA bounded_below?(LAMBDA(t: Lookahead):horiz_dist_scaf(s)(t,v)) omega_2D(s)(v) : real = inf(LAMBDA(t: Lookahead):horiz_dist_scaf(s)(t,v)) tau_2D_nonempty : LEMMA nonempty?({t: Lookahead | horiz_dist_scaf(s)(t,v) = omega_2D(s)(v)}) % 1.C.4 tau_2D Definitions and Basic Properties tau_2D(s,v) : Lookahead = choose({t: Lookahead | horiz_dist_scaf(s)(t,v) = omega_2D(s)(v)}) tau_2D_def: LEMMA horiz_dist_scaf(s)(tau_2D(s,v),v) = omega_2D(s)(v) omega_2D_min_rew: LEMMA omega_2D(s)(v) = min({r: real | EXISTS (t: Lookahead):horiz_dist_ tau_2D_min : LEMMA horiz_dist_scaf(s)(tau_2D(s,v),v) <= horiz_dist_scaf(s)(t,v) omega_2D_continuous: LEMMA continuous?(omega_2D(s)) tau_2D_unique: LEMMA v /= zero AND horiz_dist_scaf(s)(tau_2D(s,v),v) = horiz_dist_scaf(s)(t,v) IMPLIES tau_2D(s,v) = t tau_2D_connected: LEMMA horiz_dist_scaf(s)(tau_2D(s,v),v) = 0 AND horiz_dist_scaf(s)(t,v) = 0 IMPLIES (FORALL (ttt: real): 0<=ttt AND ttt<= 1 IMPLIES horiz_dist_scaf(s)(ttt*tau_2D(s,v) + (1-ttt)*t,v)=0) tau_2D_v2: LEMMA v/= zero IMPLIES tau_2D(s,v) = tau_v2(s,v) omega_2D_horizontal_omega: LEMMA v/= zero IMPLIES omega_2D(s)(v) = horizontal_omega(s,v % 1.C.5 Conflicts omega_2D_conflict : LEMMA omega_2D(s)(v) < 0 IFF conflict_2D?(s,v) % 2 Critical Points % 2.A Case Subdivision omega_2D_eq_0 : LEMMA omega_2D(s)(v) = 0 IFF on_D?(s+tau_2D(s,v)*v) parts_of_v_nonzero_2D: LEMMA omega_2D(s)(v) = 0 AND NOT horiz_dist_scaf(s)(0,v)=0 IMPLIES v /= zero % 2.C Open Tape Solutions % 2.C.2 Line Solutions or 2-D Circle Solutions % tape hit solution lower_circle_hit_solution: LEMMA omega_2D(s)(v) = 0 AND on_D?(s+B*v) IMPLIES circle_solution_2D?(s,v,B,Exit) circle_hit_solution: LEMMA NOT v = zero AND omega_2D(s)(v) = 0 AND sqv(s+B*v) /= sq(D) IMPLIES horizontal_sep?(s) AND line_solution?(s,v) OR circle_solution_2D?(s,v,T,Entry) % 2.C.4 |s`z|<H and v`z = 0: 2-D circle solutions % 2.D Open Disc Solutions % 2.D.4 omega_2D(s)(v) = 0 and v = 0 implies s is inside circle % no_horiz_speed_closed_circle no_horiz_speed_on_D: LEMMA omega_2D(s)(v) = 0 AND v = zero IMPLIES sqv(s) = sq(D) % 2.E Corner Solutions % 2.E.1 Delta >= 0 omega_2D_Delta: LEMMA omega_2D(s)(v) <= 0 IMPLIES Delta(s,v) >= 0 % 2.E.2 Relationship Between Theta_D(Entry) and Theta_D(Exit) Theta_Ds_equal_line_sol_2D: LEMMA omega_2D(s)(v) = 0 AND strict_horizontal_sep?(s) AND Theta_D(s,v,Entry) = Theta_D(s,v,Exit) IMPLIES line_solution?(s,v) % 2 The Final Theorem For omega_2D % 2.B The Critical Points of omega_2D critical_points_2D : THEOREM omega_2D(s)(v) = 0 IMPLIES horizontal_sep?(s) AND line_solution?(s,v) OR circle_solution_2D?(s,v,T,Entry) OR circle_solution_2D?(s,v,B,Exit) END omega_2D ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28