/* * Existence of permutations. */ MACHINE PermEx INCLUDES ParFun, FunSeq ASSERTIONS !ss . (ss : FIN1(INTEGER) => %xx . (xx : ss | card({yy | yy:ss & yy<=xx})) : ss >->> 1..card(ss)) ; !ss . (ss : FIN1(INTEGER) => perm(ss) /= {}) END