Quelle  parallel_3D.pvs

parallel_3D: THEORY
BEGIN
  IMPORTING cross_3D, reals@abs_lems

  nzu,nzv     : VAR Nz_vector

  abs_cross_par : LEMMA
    abs(^(nzu)*^(nzv)) = 1 
    IFF
    cross(nzu,nzv) = zero

  parallel_dot_1: LEMMA 
    parallel?(nzu,nzv) IFF abs(^(nzu)*^(nzv)) = 1 

  parallel_cross_zero: LEMMA 
    parallel?(nzu,nzv) IFF cross(nzu,nzv) = zero

END parallel_3D