SSL product_perm_lems.pvs Interaktion und
PortierbarkeitPVS

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

quality93%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.11Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.

SSL product_perm_lems.pvs Interaktion und PortierbarkeitPVS

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.11Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

Haftungshinweis

Bemerkung:

SSL product_perm_lems.pvs Interaktion und
PortierbarkeitPVS