|
clock_minmax[rho : nonneg_real]: THEORY
BEGIN
IMPORTING
physical_clocks[rho],
finite_sets@finite_sets_minmax_props[real, <=],
function_image_nonempty[good_clock, real]
c: VAR good_clock
T: VAR int
participant: VAR non_empty_finite_set[good_clock]
t_at(T)(c): real = c(T)
clock_min(participant)(T): real = min(image(t_at(T), participant))
clock_max(participant)(T): real = max(image(t_at(T), participant))
clock_min_witness: LEMMA
EXISTS c: participant(c) AND clock_min(participant)(T) = c(T)
clock_max_witness: LEMMA
EXISTS c: participant(c) AND clock_max(participant)(T) = c(T)
clock_min_is_min: LEMMA
participant(c) IMPLIES clock_min(participant)(T) <= c(T)
clock_max_is_max: LEMMA
participant(c) IMPLIES c(T) <= clock_max(participant)(T)
clock_min_clock: JUDGEMENT clock_min(participant) HAS_TYPE good_clock
clock_max_clock: JUDGEMENT clock_max(participant) HAS_TYPE good_clock
hst: VAR [nat -> non_empty_finite_set[good_clock]]
j: VAR nat
ic_min(hst)(j): good_clock = clock_min(hst(j))
ic_max(hst)(j): good_clock = clock_max(hst(j))
END clock_minmax
¤ Dauer der Verarbeitung: 0.19 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.
|
