Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 4 kB

Quelle repulsive.pvs Sprache: PVS

%
% 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

quality86%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.