|
finite_seqs[T: TYPE+]: THEORY
BEGIN
IMPORTING structures@seqs[T], structures@majority_seq[T]
s, s1, s2: VAR ne_seqs
fs: VAR finite_sequence[T]
in_consensus_function: TYPE = [s: ne_seqs -> {t: T | in?(t, s)}]
i: VAR nat
choose(i)(s): T =
IF i < s`length THEN s`seq(i)
ELSE s`seq(0)
ENDIF
choose_in?: LEMMA in?(choose(i)(s), s)
choose_consensus: JUDGEMENT choose(i) HAS_TYPE in_consensus_function
choose_extend(s): sequence[T] = LAMBDA i: choose(i)(s)
t, d: VAR T
majority_function: TYPE = [fs: finite_sequence[T] -> {t: T | maj_exists(fs) => is_majority(t, fs)}]
mf: VAR majority_function
maj_exists_same: LEMMA
maj_exists(fs)
IMPLIES
mf(fs) = maj(fs)
mf_lem: LEMMA
is_majority(t, fs)
IMPLIES
mf(fs) = t
majority_choose(s): T =
IF maj_exists(s) THEN maj(s) ELSE choose(0)(s) ENDIF
majority_choose_consensus: JUDGEMENT majority_choose HAS_TYPE in_consensus_function
majority_choose2(fs): T =
IF fs`length = 0 THEN choose({t:T | TRUE})
ELSE majority_choose(fs)
ENDIF
majority2_choose_majority: JUDGEMENT majority_choose2 HAS_TYPE majority_function
k: VAR nat
uniform(fs, t, k): finite_set[below(k)] = { i : below(k) | fs`length = k & fs`seq(i) = t }
is_majority?(fs, t, k): bool = 2 * card(uniform(fs, t, k)) > k
majority_same: LEMMA is_majority(t, fs) IFF is_majority?(fs, t, fs`length)
END finite_seqs
¤ 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.
|
