Inductive counting

Umbrella file for the combinatorial core of Immerman–Szelepcsényi: a nondeterministic machine on a finite graph that accepts exactly when no target is reachable from a source, by counting the nodes of every layer (DescriptiveComplexity.InductiveCounting.Machine), and the two directions of its correctness (DescriptiveComplexity.InductiveCounting.Sound, DescriptiveComplexity.InductiveCounting.Complete). Nothing here is first-order; DescriptiveComplexity.TransitiveClosureCompl is what runs the machine inside a single TC.