1ОСТ Р ИСО/МЭК ТО 10023-М
endtype (■* POElement2 *)
type POEiement3
is POElement renamedby
sortnames
Element3 for Element
endtype (* POE!ement3 *)
type POEIement4
is POElement renaniedby
sortnames
E!ement4 for Element
endtype (* POEIement4
type BasicPOPair
is Pair actualizedby POElement, POEIement2 using
endtype (*. BasicPOPair “)
type POPair
is BasicPOPair
opns
-le.—, -It-, -ge-,
-g t-: Pair, Pair—> Bool
eqns
forall
x, у : Pair
ofsort Bool
First (x) le First (y). Second (x) le Second (y) = > x le y=
true;
not (First (x) le First (y)) » > x le у* false;
not (Second (x) le Second (y)) <*> x le у= false;
x ne у -«> x It
ym x
le y;
x eq у =•> x И у= false;
x ge y= y le x;
x ne у = > x gt y=x ge y;
x eq у = > x gt y= false;
endtype (* POPair *)
type BasicPOThreeTuple
is ThreeTuple actualizedby POElement. POEtement2, POElement3
using
endtype (* BasicPOThreeTuple *)
type POThreeTuple
is BasicPOThreeTuple
opns
_le_, -lt_, -gc_. -gt- : ThreeTuple, ThreeTuple — > Bool
feqns
forall
29