ГОСТ Р ИСО’МЭК ТО 10023-93
Tuple :
First
Third
— > Element3
—> Bool
endtype <* ThreeTuple *)
type FourTuple
is Element, Elemen’2, Flement3, Elements Boolean
sorts
FourTuple
opns
Flement. EIement2, Elemcnt3, Elementl
—■> FourTuple
: FourTuple
— > Element
Second: FourTuple
— > Element2
: FoureTupIe
Fourth: FoureTupIe
—> Elemenl4
_cq_, _nc_: FourTuple, FourTuple
eqns
torall
x !. уI: Element, x2, y2 : Element2, x3, y3 : Element3,
x4. y4 : Element4
ofsort Element
First (Tupie(xl. x2. x3, x 4 ) ) - x l ;
ofsort Element2
Second (Tuple (xl. x2, x3. x 4))—x2;
ofsort Elornfcnt3
Third(Tuple(xl, x2, x3. x4))=x3;
ofsort Element3
Fourth(Tuple(xl, x2, x3. x4))=x4;
ofsort Bool
Tuplefxl, x2, x3. x4) eq Tuple (xl, x2, x3. x4)-Truo;
xl ne yl —> Tuple(xl. x2. x3. x4) cq Tuplefyl, y2, y3. y4)
-False;
x2 ne y2 = > Tuple(xl. x2. x3, x4) eq Tuplfefyl, y2. y3, y4)
= False;
x3 ne y3 = > Tuplefxl, x2. x3, x4) eq Tuple(y1, y2, y3, y4)
. “ False;
x4 ne y4 = > Tuple(xI, x2, x3, x4) eq Tuple(yl, y2. y3, y4)
-False;
endtype (* FourTuple *)
type TwoTupIet
is Boolean, NaluralNumber
sorts
Tuple!
opns
TheOnc. TheOther
—> Tuplet
-eq_, _ne-
Tuplet, Tuplet—> Bool