|
permutations_seq[T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
% permutations_seq (basic definitions and properties)
% -------------------------------------------
%
% Author: Ricky W. Butler
%
%
% permutation?(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]):
% bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii))))
%
%
%------------------------------------------------------------------------
BEGIN
A,B,A1,A2,A3: VAR finite_sequence[T]
x, t: VAR T
i,j: VAR nat
in?(A)(x): bool = (EXISTS (ii: below(length(A))): seq(A)(ii) = x)
permutation?(A,B): bool = (EXISTS (f: [below(length(A)) -> below(length(B))]):
bijective?(f) AND
(FORALL (ii: below(length(A))): seq(A)(ii) = seq(B)(f(ii))))
IMPORTING finite_sets@finite_sets_card_eq, finite_sets@finite_sets_below
perm_length : LEMMA permutation?(A,B) IMPLIES length(A) = length(B)
perm_reflexive: LEMMA permutation?(A,A)
perm_symmetric: LEMMA permutation?(A,B) IMPLIES permutation?(B,A)
perm_tran : LEMMA permutation?(A1,A2) AND permutation?(A2,A3)
IMPLIES permutation?(A1,A3)
perm_in? : LEMMA permutation?(A1,A2) IMPLIES
(in?(A1)(x) = in?(A2)(x))
END permutations_seq
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
