END relation_props
relation_props
[T1:TYPE,
T2:TYPE,
T3:TYPE]
:
THEORY
BEGIN
x:
VAR
T1
y:
VAR
T2
z:
VAR
T3
O(R1,
R2)(x,
z):
bool
=
EXISTS
y
:
R1(x,
y)
AND
R2(y,
z);
total
composition:
LEMMA
(total?(R1)
&
total?(R2))
=
>
total?(R1
o
R2)
onto
composition:
LEMMA
(onto?(R1)
&
onto?(R2))
=
>
onto?(R1
o
R2)
%%(TCC)
composition_total:
OBLIGATION
composition
total:
JUDGEMENT
O((R1:(total?[T1,
T2])
),
(R2:(total?[T2,
T3])
))
HAS_TYPE
(total?[T1,
T3])
%%(TCC)
composition_onto:
OBLIGATION
composition
onto:
JUDGEMENT
O((R1:(onto?[T1,
T2])
),
(R2:(onto?[T2,
T3])
))
HAS_TYPE
(onto?[T1,
T3])
END
relation_props