|
product_perm_lems: THEORY
%------------------------------------------------------------------------------
%
% NOTE: At some point this theory should be integrated with
% structures@permutation
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING reals@product_fseq_posnat
IMPORTING structures@permutations_fseq[posnat,<=]
IMPORTING structures@sort_fseq[posnat,<=]
fs,fs1,fs2: VAR fseq[posnat]
swap(fs)(i,j: nat): fseq[posnat] =
(# length := length(fs),
seq := (LAMBDA (ii: nat):
IF ii >= length(fs) THEN default
ELSIF ii = i THEN fs(j)
ELSIF ii = j THEN fs(i)
ELSE fs(ii)
ENDIF)
#)
i,j,k,l: VAR nat
swap_len: LEMMA length(swap(fs)(i,j)) = length(fs)
swap_eq_arg: LEMMA swap(fs)(i,i) = fs
swap_symm: LEMMA swap(fs)(i,j) = swap(fs)(j,i)
prod_swap_prep: LEMMA i <= j AND (j < k OR i > l) IMPLIES
product(k, l, swap(fs)(i, j)`seq)
= product(k,l, fs`seq)
prod_swap_prep2: LEMMA i <= j AND (i < k AND j > l) IMPLIES
product(k, l, swap(fs)(i, j)`seq) = product(k,l, fs`seq)
product_swap: LEMMA FORALL (i,j: below(length(fs))):
product(swap(fs)(i,j)) = product(fs)
swap_is_permutation: LEMMA FORALL (i,j: below(length(fs))):
permutation?(swap(fs)(i,j),fs)
product_permutation: LEMMA permutation?(fs1,fs2) IMPLIES
product(fs1) = product(fs2)
non_decreasing?(fs): bool =
(FORALL (i,j: below(length(fs))): i < j IMPLIES seq(fs)(i) <= seq(fs)(j))
length_sort: LEMMA (sort(fs))`length = fs`length
product_sort: LEMMA product(sort(fs)) = product(fs)
END product_perm_lems
¤ Dauer der Verarbeitung: 0.18 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.
|
