|
%------------------------------------------------------------------------------
% tangent_line.pvs
% ACCoRD v1.0
%
% This file provides a simple framework to compute line solutions.
% By definition all line solutions lay on the tangent lines to the
% protected zone. We consider two cases, if sq(s) = sq(D), tangent
% solutions lay on a vector perpendicular to s. Otherwise, tangent solutions
% lay on the line defined by the two points s and Q(s,eps), where
% eps = +-1.
%------------------------------------------------------------------------------
tangent_line[D: posreal] : THEORY
BEGIN
IMPORTING line_solutions[D],
vectors@parallel_2D
sp : VAR Sp_vect2
ss : VAR Ss_vect2
eps : VAR Sign
vo,vi,v,
nvo,nvi : VAR Vect2
nzv : VAR Nz_vect2
alpha(ss) : {x:posreal | x < 1} = sq(D)/sqv(ss)
beta(ss) : nnreal = D*sqrt(sqv(ss)-sq(D))/sqv(ss)
alpha_neg : LEMMA
alpha(-ss) = alpha(ss)
beta_neg : LEMMA
beta(-ss) = beta(ss)
sq_alpha_beta : LEMMA
sq(alpha(ss)) + sq(beta(ss)) = alpha(ss)
Q(ss,eps) : Vect2 = alpha(ss)*ss+eps*beta(ss)*perpR(ss)
Q_on_D : LEMMA
sqv(Q(ss,eps)) = sq(D)
Q_asymm : LEMMA
Q(-ss,eps) = -Q(ss,eps)
Qs(ss,eps) : Vect2 =
Q(ss,eps)-ss
Qs_asymm : LEMMA
Qs(-ss,eps) = -Qs(ss,eps)
sqv_Qs : LEMMA
sqv(Qs(ss,eps)) = sqv(ss) - sq(D)
Qs_nzv : JUDGEMENT
Qs(ss,eps) HAS_TYPE Nz_vect2
s_dot_Qs_lt_0 : LEMMA
ss*Qs(ss,eps) < 0
det_s_Qs_lt_0 : LEMMA
eps*det(ss,Qs(ss,eps)) < 0
alpha_D : LEMMA
alpha(ss)*sqv(ss) = sq(D)
beta_R : LEMMA
beta(ss)*sqv(ss)*R(ss) = sqv(ss)-sq(D)
alpha_beta: LEMMA
alpha(ss)*R(ss) = beta(ss)
beta_alpha : LEMMA
-beta(ss)*R(ss) = alpha(ss)-1
det_v_Q : LEMMA
det(v,Q(ss,eps)) = alpha(ss)*(det(v,ss)) - eps*beta(ss)*(ss*v)
s_dot_Q : LEMMA
ss*Q(ss,eps) = alpha(ss)*sqv(ss)
det_s_Qs : LEMMA
det(ss,Qs(ss,eps)) = -eps*(beta(ss)*sqv(ss))
det_Q_s : LEMMA
det(Q(ss,eps),ss) = eps*D*sqrt(sqv(ss)-sq(D))
Q_eq_Qs_perp : LEMMA
Q(ss,eps) = -eps*(D/sqrt(sqv(ss)-sq(D)))*perpR(Qs(ss,eps))
line_solution_Qs: LEMMA
line_solution?(ss,Qs(ss,eps),eps)
parallel_nzv_Qs : LEMMA
line_solution?(ss,nzv,eps) IMPLIES
dir_parallel?(nzv,Qs(ss,eps))
parallel_nzv_perp : LEMMA
on_D?(sp) AND
line_solution?(sp,nzv,eps) IMPLIES
dir_parallel?(nzv,eps*perpR(sp))
tangent_line(sp,eps) : Nz_vect2 =
IF on_D?(sp) THEN
eps*perpR(sp)
ELSE
Qs(sp,eps)
ENDIF
tangent_line_asymm : LEMMA
tangent_line(-sp,eps) = -tangent_line(sp,eps)
line_solution_tangent_line: LEMMA
line_solution?(sp,tangent_line(sp,eps),eps)
parallel_nzv_tangent_line: LEMMA
line_solution?(sp,nzv,eps) IMPLIES
dir_parallel?(nzv,tangent_line(sp,eps))
tangent_line?(sp,v,eps) : bool =
EXISTS (nnk:nnreal): v = nnk*tangent_line(sp,eps)
tangent_line_solution : LEMMA
tangent_line?(sp,v,eps) IFF
line_solution?(sp,v,eps)
tangent_line_independence : LEMMA
tangent_line?(sp,v,eps) IMPLIES
NOT horizontal_conflict_ever?(sp,v)
tangent_line_coordination: LEMMA
horizontal_conflict?(sp,vo-vi) AND
tangent_line?(sp,nvo-vi,eps) AND
tangent_line?(-sp,nvi-vo,eps)
IMPLIES
NOT horizontal_conflict?(sp,nvo-nvi)
END tangent_line
¤ Dauer der Verarbeitung: 0.14 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.
|
