END equality_props
equality_props provides some properties of IF and =.
equality_props
[T:TYPE]
:
THEORY
BEGIN
x:
VAR
T
y:
VAR
T
z:
VAR
T
IF
true:
POSTULATE
IF
TRUE
THEN
x
ELSE
y
ENDIF
=
x
IF
false:
POSTULATE
IF
FALSE
THEN
x
ELSE
y
ENDIF
=
y
IF
same:
LEMMA
IF
b
THEN
x
ELSE
x
ENDIF
=
x
reflexivity
of
equals:
POSTULATE
x
=
x
transitivity
of
equals:
POSTULATE
((x
=
y)
AND
(y
=
z))
IMPLIES
(x
=
z)
symmetry
of
equals:
POSTULATE
(x
=
y)
IMPLIES
(y
=
x)
END
equality_props