products/Sources/formale Sprachen/PVS/trig_fnd/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: constrintern.mli   Sprache: PVS

Original von: PVS©
parallel_2D: THEORY
BEGIN
  IMPORTING det_2D

  nzu,nzv     : VAR Nz_vector

  abs_det_par : LEMMA
    abs(^(nzu)*^(nzv)) = 1 
    IFF
    det(nzu,nzv) = 0

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

  parallel_det_0: LEMMA 
    parallel?(nzu,nzv) IFF det(nzu,nzv) = 0

  dot_perpL_parallel: LEMMA nzu*nzv = 0 IMPLIES
                           parallel?(perpL(nzu),nzv)


  dot_perpR_parallel: LEMMA nzu*nzv = 0 IMPLIES
                           parallel?(perpR(nzu),nzv)

END parallel_2D

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff