|
%%----------------------------------------------------------------
%%
%% 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.1 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.
|
