/* * There exists an injection from S to T iff S has less elements than T. */ MACHINE InjEx INCLUDES DomRan, PermEx ASSERTIONS !(ss, tt) . (ss : FIN1(INTEGER) & tt : FIN1(INTEGER) => ((card(ss) <= card(tt)) <=> ((ss >-> tt) /= {}))) END