  The ZX, ZW and ZH calculi are all graphical calculi for reasoning about pure
state qubit quantum mechanics. All of these languages use certain diagrammatic
decorations, called !-boxes and phase variables, to indicate not just one
diagram but an infinite family of diagrams. These decorations are powerful
enough to allow complete rulesets for these calculi to be expressed in around
fifteen rules. Historically rules involving !-boxes have not been verifiable by
computer. We present the first algorithm for reducing infinite families of
equations involving !-boxes into finite verifying subsets. The only requirement
for this method is a mild property on the connectivity of the !-boxes. Previous
results had focussed on finite case analysis of phase variables in ZX, a result
we also extend for ZW and ZH, as well as providing a general framework for
further languages. The results presented here allow proof assistants to reduce
infinite families of problems (involving combinations of phase variables and
!-boxes) down to undecorated, case-by-case verification, in a way not
previously possible. In particular we note the removal of the need to reason
directly with !-boxes in verification tasks as something entirely new. This
forms part of larger work in automated verification of quantum circuitry,
conjecture synthesis, and diagrammatic languages in general. The methods
described here extend to any diagrammatic languages that meet certain simple
conditions.
