ГОСТ Р ИСО/МЭК ТО 10023-93
k
eqns
forall
u, v : Tuplct
ofsor( Nat
h(TheOne) =0;
h (TheOther) —Succ (h (ThcOne));
ofsort B
c
>1
u eq u -h (u ) eq h’(v):
.*u ne v—not (u eq v);
cndtype (* TwoTuplet *)
type FourTuplet
is TwoTuplet
opns
TheThird. TheFourth:— > Tuplet
cqns
ofsort Nat
h(TheThird) - Succ (h (TheOther));
h(ThcFourth) ~ Succ (h (TheThird));
endtype {* FourTuplet •)
type OrdcredFourTuplet
is FourTuplet
tv*
opns
-It-. -Ie_, _ge_,
_gt_ :Tuplet, Tuplet—> Bool
eqns
forall
x, у : Tuplet
ofsort Bool
x It y=h(x) It h(y);
x le y= h(x) le h(y);
x ge y= h(x) ge h(y);
x gt y= h(x) gt h(y);
endtype (* OrderedFourTuplet *)
type POElement
is Element
formalopns
-le -, -It-, -ge .,
_gt_ : Element, Element—> FBool
endtype (• POElement ")
type POEIemenl2
is POElement rfenamedby
sortnames
Elernen<2 for Element
28