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