/* * Basic properties on the domain and range of relations. */ MACHINE DomRan ASSERTIONS !(ss, tt, rr) . (ss : FIN(INTEGER) & tt : FIN(INTEGER) & rr : ss <-> tt => #ff . (ff : ss +-> tt & ff <: rr & dom(ff) = dom(rr))) ; !(ss, tt, rr) . (ss : FIN(INTEGER) & tt : FIN(INTEGER) & rr : ss <-> tt => card(dom(rr)) <= card(rr)) ; !(ss, tt, rr) . (ss : FIN(INTEGER) & tt : FIN(INTEGER) & rr : ss <-> tt => card(ran(rr)) <= card(rr)) END