|
%%-------------------** Fundamental Counting Principle and Permutations with Repetition **-------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%------------------------------------------------------------------------------------------------------
cauchy_scaf[T:TYPE]: THEORY
BEGIN
IMPORTING structures@seq_extras[T],
finite_sets@finite_sets_eq,
finite_sets@finite_sets_card_eq
S: VAR finite_set[finseq]
M: VAR finite_set[T]
a: VAR T
n: VAR nat
p: VAR posnat
add_element(S)(a): set[finseq] = {seq: finseq | EXISTS (s: (S)): seq = add_first(a, s)}
add_set(S)(M): setofsets[finseq] = {C: set[finseq] | EXISTS (a: (M)): C = add_element(S)(a)}
set_seq(M)(n): set[finseq] = {seq: finseq | length(seq) = n AND
FORALL (i: below[n]): member(seq(i), M)}
emptyset_gives_emptyset: LEMMA empty?(S) IMPLIES empty?(add_element(S)(a))
emptyset_gives_emptyset1: LEMMA empty?(M) IMPLIES empty?(add_set(S)(M))
set_seq_singleton: LEMMA set_seq(M)(0) = singleton(empty_seq)
set_seq_empty: LEMMA empty?(M) IMPLIES empty?(set_seq(M)(p))
add_element_add_set: LEMMA NOT member(a, M) IMPLIES
LET B = add_set(S)(M),
A = add_element(S)(a) IN
Union(add_set(S)(add(a, M)))= union(Union(B), A)
card_add_element_aux: LEMMA
LET A = add_element(S)(a) IN
EXISTS (g:[(A)->(S)]): bijective?(g)
card_add_element: LEMMA
LET A = add_element(S)(a) IN
card(A) = card(S)
disjoint_add_set: LEMMA
LET B = add_set(S)(M),
A = add_element(S)(a) IN
NOT member(a, M) IMPLIES disjoint?(Union(B),A)
add_set_is_add_ele: LEMMA
LET B = add_set(S)(M),
A = add_element(S)(a) IN
M = singleton(a) IMPLIES Union(B) = A
add_set_is_finite_aux: LEMMA
nonempty?(S) IMPLIES
LET B = add_set(S)(M) IN
EXISTS (g:[(M)->(B)]): bijective?(g)
add_set_is_finite: LEMMA
LET B = add_set(S)(M) IN
is_finite(B)
%%%%% Fundamental Counting Principle %%%%%
card_add_set: LEMMA
LET B = add_set(S)(M) IN
card(Union(B)) = card(S)*card(M)
set_seq_is_finite: LEMMA
LET C = set_seq(M)(n) IN
is_finite(C)
set_seq_is_add_set: LEMMA
LET C = set_seq(M)(p),
D = set_seq(M)(p-1) IN
C = Union(add_set(D)(M))
%%%%% Permutations with Repetition %%%%%
card_set_seq: LEMMA
LET C = set_seq(M)(n) IN
card(C) = card(M)^n
END cauchy_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.
|
