| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 31 kB |
|
Quelle finite_seqs.pvs Sprache: PVS |
|||||||||
|
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, 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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28