OAI.TwoWayComplementation.explicit_family_main

The theorem states that for every natural number n ≥ 4, writing H = Fin(n−2) (natural-number subtraction), there is a read-only two-way nondeterministic finite automaton A with exactly n states (state type Fin n) whose input alphabet is the set of binary relations on H, such that three things hold. First, the language accepted by A equals the source language: the set of finite words of relations on H whose relational composition (the empty word giving the identity relation) is nonempty. Acceptance for these machines means some finite run, possibly of length zero, from the initial state on the left endmarker reaches an accepting state, with the head confined to the input between two distinct endmarkers and each transition choosing a next state and a move left, stay, or right. Second, for every finite-state-type Q and every such two-way automaton B over the same alphabet with state type Q whose language is exactly the complement of A's language, the cardinality of Q is at least (1/2)·2^⌊(n−4)/127⌋ − 1, where the exponent uses natural-number floor division. Third, if additionally n ≥ 131, then every deterministic such automaton D (at most one next-state and move pair for each state and scanned symbol) over any finite state type Q that accepts exactly A's language has at least (1/2)·2^⌊(n−4)/127⌋ states. Both lower bounds thus hold for the same n-state witness A. The statement is admitted in the source without a proof.