|
%
% Repulsivity for horizontal vectors
% This is a 2D theory.
%
repulsive : THEORY
BEGIN
IMPORTING horizontal,
predicate_coordination_2D,
vectors@basis_2D
s,v,vo,vi,
nv,nw,nh : VAR Vect2
nvo,nvi : VAR Vect2
eps : VAR Sign
cc : VAR posreal
pt,px : VAR posreal
% Time of closest approach
tca(s,v) : real =
IF zero_vect2?(v) THEN 0
ELSE horizontal_tca(s,v)
ENDIF
repulsive?(s,v)(nv) : bool =
LET tau1 = tca(s,v),
tau2 = tca(s,nv) IN
(s*v < 0 AND
(tau2 <= 0 OR
norm(s+tau1*v) < norm(s+tau2*nv)))
OR
(s*v>=0 AND (v = zero IMPLIES s*nv>=0) AND (v/=zero IMPLIES s*nv>s*v))
repulsive_simple: LEMMA
repulsive?(s,v)(nv) IMPLIES
(s*v<0 AND tca(s,v)>0 AND
(FORALL (t:nnreal): norm(s+t*nv)>=norm(s+tca(s,v)*v)))
OR
(s*v>=0 AND
(FORALL (t:nnreal): norm(s+t*nv)>=norm(s)))
repulsive_transitive: LEMMA
repulsive?(s,v)(nv) AND
repulsive?(s,nv)(nw) IMPLIES
repulsive?(s,v)(nw)
not_repulsive_sum_closed: LEMMA
sum_closed_2D?(LAMBDA (s,v): LAMBDA (nv): s*v<0 AND NOT repulsive?(s,v)(nv))
repulsive_criteria(s,v,eps)(nv): bool =
s /= zero AND
nv /= zero AND
eps*det(s,v) <= 0 AND
eps*det(s,nv) < 0 AND
((s*v < 0 AND
eps*det(nv,v) < 0)
OR
(s*v>=0 AND (v = zero IMPLIES s*nv>=0)
AND (v/= zero IMPLIES s*nv> s*v)
AND eps*det(nv,v) <= 0))
repulsive_criteria_scal_s: LEMMA
repulsive_criteria(s,v,eps)(nv) IFF
repulsive_criteria(cc*s,v,eps)(nv)
repulsive_criteria_scal_nv: LEMMA
(s*v<0 AND (repulsive_criteria(s,v,eps)(cc*nv) IFF
repulsive_criteria(s,v,eps)(nv)))
OR
(s*v>=0 AND (repulsive_criteria(s,v,eps)(cc*nv) IFF
repulsive_criteria(s,(1/cc)*v,eps)(nv)))
wedge_containment: LEMMA
FORALL (e,f,g,h:Nz_vect2):
(e*h>=0 AND f*h>0 AND g*h>0) AND
(NOT (det(e,g)>=0 AND det(f,g)>0)) AND
(NOT (det(e,g)<=0 AND det(f,g)<0)) AND
e*v>=0 AND f*v>0 IMPLIES g*v>0
repulsive_criteria_transitive: LEMMA
repulsive_criteria(s,v,eps)(nv) AND
repulsive_criteria(s,nv,eps)(nw) IMPLIES
repulsive_criteria(s,v,eps)(nw)
repulsive_criteria_transitive_odd1: LEMMA
s*v<0 AND (s+pt*nv)*nv<0 AND
repulsive_criteria(s,v,eps)(nv) AND
repulsive_criteria(s+pt*nv,nv,eps)(nw) IMPLIES
repulsive_criteria(s,v,eps)((s+pt*nv+px*nw)-s)
rep_crit_odd2_ax: LEMMA
FORALL(sx,sy,vx,vy,nvx,nvy,nwx,nwy:real,pt,px:posreal,eps:Sign) :
px>0 AND pt>0
AND nvx*sx+nvy*sy+nvx*nvx*pt+nvy*nvy*pt>=0
AND sx*vx+sy*vy<0 AND sx*vy*eps-sy*vx*eps<=0
AND nvy*sx*eps-nvx*sy*eps<0
AND nvx*vy*eps-nvy*vx*eps<0
AND nvy*sx*eps-nvx*sy*eps<=0
AND -1*(nwx*sy*eps)-nvy*nwx*eps*pt+nwy*sx*eps+nvx*nwy*eps*pt<0
AND nwx*sx+nwy*sy+nvx*nwx*pt+nvy*nwy*pt>nvx*sx+nvy*sy+nvx*nvx*pt+nvy*nvy*pt
AND nwx*vy*eps-nwy*vx*eps<0
IMPLIES
-1*(nvx*sy*eps*pt)-nwx*sy*eps*px+nvy*sx*eps*pt+nwy*sx*eps*px<0
repulsive_criteria_transitive_odd2: LEMMA
s*v<0 AND (s+pt*nv)*nv>=0 AND
repulsive_criteria(s,v,eps)(nv) AND
repulsive_criteria(s+pt*nv,nv,eps)(nw) AND eps*det(nw,v) < 0
IMPLIES
repulsive_criteria(s,v,eps)((s+pt*nv+px*nw)-s)
repulsive_criteria_transitive_odd3: LEMMA
s*v>=0 AND pt>=1 AND
repulsive_criteria(s,v,eps)(nv) AND
repulsive_criteria(s+pt*nv,nv,eps)(nw) IMPLIES
repulsive_criteria(s,v,eps)((s+pt*nv+px*nw)-s)
repulsive_criteria_sum_closed: LEMMA
repulsive_criteria(s,v,eps)(nv) AND
repulsive_criteria(s,v,eps)(nw) IMPLIES
repulsive_criteria(s,v,eps)(nv+nw)
repulsive_criteria_indep_of_length: LEMMA
s*v < 0 IMPLIES
FORALL (c:posreal):
repulsive_criteria(s,v,eps)(nv) IFF
repulsive_criteria(s,v,eps)(c*nv)
repulsive_criteria_repulsive: LEMMA
repulsive_criteria(s,v,eps)(nv)
IMPLIES
repulsive?(s,v)(nv)
repulsive_criteria_repulsive2: LEMMA
repulsive?(s,v)(nv)
AND eps * det(s, v) <= 0 AND eps * det(s, nv) < 0 AND nv /= zero
AND (s*v>=0 IMPLIES eps*det(nv,v)<=0)
IMPLIES
repulsive_criteria(s,v,eps)(nv)
repulsive_criteria_symmetric: LEMMA
repulsive_criteria(s,v,eps)(nv) IFF
repulsive_criteria(-s,-v,eps)(-nv)
repulsive_criteria_coordinately_repulsive: LEMMA
repulsive_criteria(s,vo-vi,eps)(nvo-vi) AND
repulsive_criteria(-s,vi-vo,eps)(nvi-vo)
IMPLIES
repulsive?(s,vo-vi)(nvo-nvi)
foo: LEMMA
repulsive_criteria(s,vo-vi,eps)(nvo-vi) AND
repulsive_criteria(-s,vi-vo,eps)(nvi-vo)
IMPLIES
repulsive?(s,vo-vi)(nvo-nvi)
repulsive_increases_dist: LEMMA
repulsive?(s,v)(nv) IMPLIES
(s*v<0 AND horizontal_tca(s,v)>0 AND v/=zero AND
FORALL (nnt:nnreal): norm(s+nnt*nv)>norm(s+horizontal_tca(s,v)*v))
OR
(s*v>=0 AND v/=zero AND horizontal_tca(s,v)<=0 AND
FORALL (pt:posreal): norm(s+pt*nv)>norm(s))
OR
(v=zero AND FORALL (nnt:nnreal): norm(s+nnt*nv)>=norm(s))
END repulsive
¤ Dauer der Verarbeitung: 0.19 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.
|
