Quelle definitions_3D.pvs Sprache: PVS

%------------------------------------------------------------------------------
% definitions_3D.pvs
% ACCoRD v1.0
%------------------------------------------------------------------------------

definitions_3D : THEORY
BEGIN

  IMPORTING definitions,
            vectors@vect_3D_2D

  s,v,
  vo1,vo2 : VAR Vect3
  nzs     : VAR Nz_vect3

  Zv2_vect3  : TYPE = {v | zero_vect2?(v)}
  Nzv2_vect3 : TYPE = {v | nz_vect2?(v)}

  nzv : VAR Nzv2_vect3

  nzv2 : JUDGEMENT
    vect2(nzv) HAS_TYPE Nz_vect2

%%
%% Symmetry breaking
%%

  break_symmetry(s) : Sign =
    IF s`z > 0 OR
       s`z = 0 AND s`x > 0 OR
       s`z = 0 AND s`x = 0 AND s`y > 0 THEN
       1
    ELSE
      -1
    ENDIF

  break_symmetry_neg : LEMMA
    break_symmetry(-nzs) = -break_symmetry(nzs)

%%
%% Kind of Resolutions
%%

  horizontal_only?(vo1)(vo2) : MACRO bool =
    vo1`z = vo2`z

  gs_only_3D?(vo1)(vo2) : MACRO bool =
    gs_only?(vo1)(vo2) AND
    vo1`z = vo2`z

  gsho : JUDGEMENT
    (gs_only_3D?(v)) SUBTYPE_OF (horizontal_only?(v))

  trk_only_3D?(vo1)(vo2) : MACRO bool =
    trk_only?(vo1)(vo2) AND
    vo1`z = vo2`z

  trkho : JUDGEMENT
    (trk_only_3D?(v)) SUBTYPE_OF (horizontal_only?(v))

  vs(v) : real = v`z

  vs_only?(vo1)(vo2) : bool =
    vect2(vo1) = vect2(vo2)

  vs_only_symm : LEMMA
    vs_only?(vo1)(vo2) IFF vs_only?(vo2)(vo1)

END definitions_3D

quality100%

¤ Dauer der Verarbeitung: 0.10 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.