An S-flip of G is a flip for the partition into atomic types over S, $Flips.IsFlip G (Partitions.atomicTypes G S) H$.

The graph G ⊕ (p̄, R) is $flipOver G p R$. It is built with $SimpleGraph.fromRel$, which removes the diagonal and symmetrizes. For a symmetric relation R the relation that is symmetrized is already symmetric, so two distinct vertices are adjacent in $flipOver G p R$ exactly when their adjacency in G differs from membership of their atomic types in R. Every statement about $flipOver$ assumes R symmetric.

An s-definable flip, $IsDefinableFlip G s H$, is defined by the second, equivalent formulation: an S-flip for a finite set S of at most s vertices. The two formulations agree on every graph with at least one vertex, by listing S with repetitions as an s-tuple, or, if S is empty and s ≥ 1, by a constant tuple, since every ∅-flip is also a {v}-flip. On the empty graph there is no s-tuple for s ≥ 1, while the empty set still works. The formulation by sets makes "s-definable implies s'-definable for s' ≥ s" hold without exception.