products/sources/formale sprachen/PVS/groups image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: repulsive_iterative.pvs   Sprache: PVS

Original von: PVS©


%%----------------------------------------------------------------
%%                                                                          
%% Author          : André Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%                    
%% Last Modified On: November 28, 2011
%%                                                                          
%%----------------------------------------------------------------


class_equation_scaf[D, T:TYPE]: THEORY

BEGIN


   IMPORTING algebra@lagrange_scaf[T], 
             sigma_set@sigma_set[finite_set[T]] 
 

      FP:  VAR finite_partition
       A: VAR finite_set[D]
       B: VAR finite_set[T]
m, n, x : VAR int



card_rest_aux: LEMMA nonempty?(FP) IMPLIES 
                       card(Union(FP)) = card(choose(FP)) + card(Union(rest(FP)))
 

card_partition: LEMMA (nonempty?(FP) AND FORALL (A: (FP)): card(A) /= 0) IMPLIES 
                             card(Union(FP)) = sigma_set.sigma(FP, card)


divide_sigma: LEMMA (nonempty?(FP) AND 
                          FORALL (A: (FP)): card(A) /= 0 AND divides(n, card(A))) IMPLIES 
                             divides(n,sigma_set.sigma(FP, card))

END class_equation_scaf

¤ Dauer der Verarbeitung: 0.9 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




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.


Bot Zugriff