Nach dem Mausklick ist die Projektion eines vierdimensionalen Würfels zu sehen vect_trig_2D.pvs   Interaktion und
PortierbarkeitPVS

vect_trig_2D: THEORY
BEGIN

  IMPORTING det_2D

  u,v : VAR Nz_vector

  % sin(u,v) provides the sin of the angle from u to v (counter-clockwise)
  % cos(u,v) provides the cos of the angle from u to v (any direction) 

  sin(u,v): real = det(u,v)/(norm(u)*norm(v))

  cos(u,v): real = u*v/(norm(u)*norm(v))

  trig_range  : TYPE = {x:real | -1 <= x AND x <= 1}

  sin_range   : JUDGEMENT sin(u,v) HAS_TYPE trig_range

  cos_range   : JUDGEMENT cos(u,v) HAS_TYPE trig_range

  sin2_cos2: THEOREM sq(sin(u,v)) + sq(cos(u,v)) = 1

  sin_asym: LEMMA sin(u,v) = -sin(v,u)
 
  cos_symm: LEMMA cos(u,v) = cos(v,u)

END vect_trig_2D