%
%
% Purpose : a message with a linear order.
%
%
ordered_message[T: TYPE+, leq: (total_order?[T])]: THEORY
BEGIN
IMPORTING message[T]
d1, d2: VAR message
valid_iff_ord1: LEMMA (valid?(d1) IFF ord(d1) = 1)
d3: VAR message
<=(d1, d2): bool =
IF valid?(d1) & valid?(d2)
THEN leq(value(d1), value(d2))
ELSE ord(d1) <= ord(d2)
ENDIF
eq_iff: LEMMA d1 = d2 IFF
(valid?(d1) AND valid?(d2) AND value(d1) = value(d2)) OR
(ord(d1) = ord(d2) AND ord(d1) /= 1 )
message_total_order: JUDGEMENT <= HAS_TYPE (total_order?[message[T]])
END ordered_message
[ Verzeichnis aufwärts0.16unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|