The iff_gen() sets up the bidirectional if-and-only-if relationship. (Of course there is a unidirectional if_gen() as well.) In the above example, if the point xy is true then any of the ships connected to that point exist. And if none of those ships exist, then the point xy must be false. The iff_gen() function in general takes a pair of sets of terms, and each collection of terms has a "mode" of any or all to determine if just one term must be true or if all of the terms must be true. There was no need to set modeA here because there was only a single term so the any/all distinction is meaningless.