For every DNF formula \(\psi \), the CNF obtained from \(\psi \) by flipping the polarity of every literal has the same variable bound as the term list of \(\psi \) viewed as a CNF, where the variable bound of a formula is one more than its largest variable index (and \(0\) if no literal occurs).

Let \(\psi \) be a DNF formula and let \(a, b : \mathbb {N} \to \{ 0,1\} \) be assignments with \(a(v) = b(v)\) for every \(v\) below the variable bound of \(\psi \) (one more than its largest variable index). Then \(\psi \) evaluates to the same truth value under \(a\) and under \(b\).

For every binary string \(x\), \(x\) lies outside \(\mathrm{TAUTOLOGY}\) if and only if there exists a binary word \(u\) of length exactly \(|x| + 1\) such that the DNF decoded from \(x\) evaluates to false under the assignment \(\alpha _u\) that reads variable \(v\) off the \(v\)-th bit of \(u\) (false for \(v \ge |u|\)).

Let \(N\) and \(i\) be natural numbers. If the bounded split search with parameters \((1,1)\) — which returns the least \(i \le N\) with \(i + (i+1) = N\), if any — returns \(i\) on \(N\), then \(i + (i + 1) = N\).

If natural numbers \(i\) and \(N\) satisfy \(i + (i + 1) = N\), then the bounded split search with parameters \((1,1)\), which looks for the least \(j \le N\) with \(j + (j+1) = N\), succeeds on \(N\) and returns exactly \(i\).

Let \(x\) and \(u\) be binary words with \(|u| = |x| + 1\), and let \(V\) be the set of binary strings \(z\) with \(|z| = i + (i+1)\) whose first \(i\) bits decode to a DNF that is false under the assignment read off the remaining bits. Then \(x \mathbin {+\! \! +} u \in V\) if and only if the DNF decoded from \(x\) evaluates to false under the assignment \(\alpha _u\) reading variable \(v\) off the \(v\)-th bit of \(u\) (false beyond \(|u|\)).

Let \(V\) be the set of binary strings \(z\) with \(|z| = i + (i + 1)\) for some \(i\) such that the DNF decoded from the first \(i\) bits of \(z\) is false under the assignment reading variable \(v\) off the \(v\)-th of the remaining bits (false beyond them). If \(V\) belongs to \(\mathrm{P}\), then \(\mathrm{TAUTOLOGY}\) belongs to coNP.

For every state \(q\) of the six-state formula syntax scanner with transition \(\delta \), every bit \(b\), and every binary string \(x\), the acceptance bit of the scan from \(q\) on \(b :: x\) equals the acceptance bit of the scan from \(\delta (q, b)\) on \(x\).

For every binary string \(x\), the acceptance bit of the six-state formula syntax scanner started in its error state and run over \(x\) is false.

For every binary string \(x\), the six-state formula syntax scanner started in its exact-end state accepts \(x\) if and only if \(x\) is empty.

For every binary string \(x\), if the leading-ones scanner returns the count \(k\) and the suffix \(s\) on \(x\), then \(x = 1^{k} \mathbin {+\! \! +} s\).

If the literal parser succeeds on a binary string \(x\), returning a literal \(\ell \) and a remainder \(r\), then \(x\) is exactly the serialization of \(\ell \) followed by \(r\).

For every fuel value, if the fuel-indexed clause parser succeeds on a binary string \(x\), returning a clause \(C\) and a remainder \(r\), then \(x\) is exactly the serialization of \(C\) (including its closing \(0\)) followed by \(r\).

For every fuel value, if the fuel-indexed formula parser succeeds on a binary string \(x\), returning a formula \(\varphi \) and a remainder \(r\), then \(x\) is exactly the serialization of \(\varphi \) followed by \(r\).

If the exact-consumption formula parser succeeds on a binary string \(x\), returning the formula \(\varphi \), then \(x\) equals the serialization of \(\varphi \).

For every binary string \(x\), write \(x = 1^k s\) where \(s\) is the suffix left by the leading-ones scanner. The six-state formula syntax scan from the unary-index state accepts \(x\) if and only if \(s = 0\, b\, r\) for some bit \(b\) and string \(r\) and the scan from the clause-level state accepts \(r\); if \(s\) has fewer than two bits or starts with \(1\), the scan rejects.

For every binary string \(x\), the string \(1 :: x\) is accepted by the six-state formula syntax scan from the clause-level state if and only if the literal parser succeeds on \(1 :: x\) with some remainder \(r\) and \(r\) is accepted by the scan from the clause-level state; when the literal parser fails, the scan rejects.

Let \(f\) be a fuel value and \(x\) a binary string with \(|x| \le f\). The six-state formula syntax scan from the clause-level state accepts \(x\) if and only if the clause parser with fuel \(f\) succeeds on \(x\) with some remainder \(r\) and the scan from the formula-level state accepts \(r\); when the clause parser fails, the scan rejects.

Let \(f\) be a fuel value and \(x\) a binary string with \(|x| \le f\). The six-state formula syntax scan from the formula-level state accepts \(x\) if and only if the formula parser with fuel \(f\) succeeds on \(x\) with an empty remainder.

For every binary string \(x\), the string \(x\) is accepted by the six-state formula syntax scan from the formula-level state if and only if the exact-consumption formula parser succeeds on \(x\).

Let \(x\) be an input and \(i \le |x|\). In every configuration of the non-tautology verifier on \(x\) whose input head has consumed \(i\) bits, the symbol under the input head is the \(i\)-th bit of \(x\) when \(i \lt |x|\) and the blank when \(i = |x|\), regardless of state, work tape, and output.

Let \(x\) be an input with \(i + 1 \le |x|\). Applying the silent action that moves the input head right, moves the work head by \(e\), and enters state \(q'\) to a non-tautology verifier configuration on \(x\) in any state with \(i\) input bits consumed, work word \(u\), work head \(h\), and output \(o\) yields the configuration in state \(q'\) with \(i+1\) bits consumed, the same \(u\) and \(o\), and work head \(h + e\).

Let \(x\) be an input and \(i \le |x|\). Applying the silent action that keeps the input head fixed, moves the work head by \(e\), and enters state \(q'\) to a non-tautology verifier configuration on \(x\) in any state with \(i\) input bits consumed, work word \(u\), work head \(h\), and output \(o\) yields the configuration in state \(q'\) with the same index, \(u\), and \(o\), and work head \(h + e\).

Let \(x\) be an input with \(i + 2 \le |x|\) whose bits at positions \(i\) and \(i + 1\) both equal \(b\), and let \(s\) be a formula-scanner state with transition \(\delta \). Started in the syntax state carrying \(s\) with \(i\) input bits consumed, empty work tape, work head \(0\), and empty output, the non-tautology verifier reaches, after exactly two steps, the syntax state carrying \(\delta (s, b)\) with \(i + 2\) bits consumed and all else unchanged.

Let \(x\) be an input with \(i + 2 \le |x|\) whose bits at positions \(i\) and \(i+1\) are \(0\) and \(1\), and let \(s\) be a formula-scanner state. Started in the syntax state carrying \(s\) with \(i\) input bits consumed, empty work tape, head \(0\), and empty output, after exactly two steps the non-tautology verifier has consumed \(i+2\) bits and is in the certificate-copy state if \(s\) is the exact-end state, and in the verdict state with bit \(1\) otherwise.

Let \(a, u, p\) be binary words, \(x = p \mathbin {+\! \! +} \mathrm{pair}(a, u)\), and \(s\) a formula-scanner state. Started in the syntax state carrying \(s\) with \(|p|\) input bits consumed, empty work tape, head \(0\), and empty output, the non-tautology verifier after exactly \(2|a| + 2\) steps has consumed \(|p| + 2|a| + 2\) bits, with work tape and output still empty, and is in the certificate-copy state if folding the scanner transition over \(a\) from \(s\) ends in the exact-end state, and in the verdict state with bit \(1\) otherwise.

For every input \(x\), the initial configuration of the non-tautology verifier on \(x\) is the configuration in the syntax state carrying the formula-level scanner state, with no input bits consumed, an empty work tape, work head at cell \(0\), and empty output.

Let \(x\) be an input, \(i \le |x|\), \(u\) a word, \(h\) an integer, and \(b\) a bit. From the non-tautology verifier’s configuration in the verdict state with bit \(b\), \(i\) input bits consumed, work word \(u\), work head \(h\), and empty output, one step halts with output exactly the single bit \(b\), all other components unchanged.

Let \(x\) be a binary string on which the exact-consumption formula parser fails, and let \(u\) be any binary word. Then the non-tautology verifier, run on \(\mathrm{pair}(x, u)\), halts within \(2|x| + 3\) steps with output the single bit \(1\).

The non-tautology verifier, run on the empty input, halts within \(2\) steps, and its output is the single bit \(0\).

Let the input be \(x = p \mathbin {+\! \! +} u\). Started in the certificate-copy state with \(|p|\) input bits consumed, empty work tape, work head \(0\), and empty output, for every \(j \le |u|\) the non-tautology verifier after exactly \(j\) steps is still in the copy state with \(|p| + j\) bits consumed, the first \(j\) bits of \(u\) on the work tape, the work head at cell \(j\), and empty output.

Let \(q\) and \(d\) be control states of the non-tautology verifier such that, in state \(q\), it silently moves the work head left with the input head fixed whenever the work cell is nonblank, and otherwise moves the work head right and enters \(d\). Then for every input \(x\), index \(i \le |x|\), work word \(u\), and \(n \le |u|\), starting in state \(q\) with work head at cell \(n - 1\), exactly \(n + 1\) steps reach state \(d\) with work head at cell \(0\), all other components unchanged.

Let \(x\) be a binary string on which the exact-consumption formula parser succeeds, and let \(u\) be any binary word. Then for some \(t \le 4(|\mathrm{pair}(x,u)| + 2)\), running the non-tautology verifier for \(t\) steps from its initial configuration on \(\mathrm{pair}(x,u)\) reaches the formula-level evaluation state with no input bits consumed, \(u\) on the work tape from cell \(0\), the work head at cell \(0\), and empty output.

Let \(x\) be an input with \(i + 2 \le |x|\) and \(i\)-th bit \(b\), let \(u\) be a word, \(h\) an integer, and \(q\) an evaluation state. Suppose the evaluation action for \(q\) on bit \(b\), with the work cell at \(h\) of the tape holding \(u\), is the silent move advancing the input head, moving the work head by \(e\), and entering \(q'\). Then from the non-tautology verifier’s evaluation configuration carrying \(q\) with \(i\) bits consumed, work word \(u\), and head \(h\), two steps reach state \(q'\) with \(i+2\) bits consumed and head \(h + e\).

For all binary words \(a\), \(b\), \(u\), the pair encoding satisfies \(\mathrm{pair}(a \mathbin {+\! \! +} b, u) = \overline{a} \mathbin {+\! \! +} \mathrm{pair}(b, u)\), where \(\overline{a}\) is the word obtained from \(a\) by doubling every bit.

For every binary word \(a\), the word obtained from \(a\) by replacing each bit \(v\) with \(v\, v\) has length exactly \(2|a|\).

Let \(k \in \mathbb {N}\), let \(r, u, p\) be binary words, and let the input be \(x = p \mathbin {+\! \! +} \mathrm{pair}(1^k \mathbin {+\! \! +} r, u)\). Started in the unary-index evaluation state with accumulator \(c\), \(|p|\) input bits consumed, work word \(u\), and work head \(h\), the non-tautology verifier after exactly \(2k\) steps is in the same state with \(|p| + 2k\) bits consumed and work head \(h + k\).

Let \(\ell = (v, b)\) be a literal and \(u\) a word with \(v \lt |u|\), and let the input be \(x = p \mathbin {+\! \! +} \mathrm{pair}(\sigma \mathbin {+\! \! +} r, u)\) where \(\sigma \) is the serialization of \(\ell \). Started in the clause-level evaluation state with accumulator \(c\), \(|p|\) bits consumed, work word \(u\), and head \(0\), the non-tautology verifier after exactly \(3v + 7\) steps is in the clause-level state with accumulator \(c \wedge (\alpha _u(v) = b)\), where \(\alpha _u\) reads \(v\) off the \(v\)-th bit of \(u\), with \(|p| + 2|\sigma |\) bits consumed and head \(0\).

Let \(C\) be a list of literals whose variable indices are all below \(|u|\) for a word \(u\), let \(\sigma \) be its serialization, and let the input be \(x = p \mathbin {+\! \! +} \mathrm{pair}(\sigma \mathbin {+\! \! +} r, u)\). Started in the clause-level evaluation state with accumulator \(c\), \(|p|\) bits consumed, work word \(u\), and head \(0\), the non-tautology verifier within some \(t \le 3|\sigma |\) steps has consumed \(|p| + 2|\sigma |\) bits, has head \(0\), and is in the verdict state with bit \(0\) if \(c\) holds and every literal of \(C\) is satisfied by the assignment read off \(u\), and in the formula-level evaluation state otherwise.

Let \(\varphi \) be a formula whose variable indices are all below \(|u|\) for a word \(u\), let \(\sigma \) be its serialization, and let the input be \(x = p \mathbin {+\! \! +} \mathrm{pair}(\sigma , u)\). Started in the formula-level evaluation state with \(|p|\) bits consumed, work word \(u\), and head \(0\), the non-tautology verifier halts within some \(t \le 3|\sigma | + 1\) steps, with work head \(0\) and output the single bit that negates the truth value of \(\varphi \) read as a DNF under the assignment \(\alpha _u\) reading variable \(v\) off the \(v\)-th bit of \(u\) (false beyond \(|u|\)).

For every list \(s\) of natural numbers and every member \(n\) of \(s\), \(n\) is at most the maximum of \(s\), computed as the right fold of \(\max \) with initial value \(0\).

Let \(\varphi \) be a CNF formula, \(C\) a clause of \(\varphi \), and \(\ell = (v, b)\) a literal of \(C\). Then \(v\) is strictly less than the variable bound of \(\varphi \), i.e. one more than the largest variable index occurring in \(\varphi \).

Let \(x\) and \(u\) be binary words with \(|u| = |x| + 1\). The non-tautology verifier, run on \(\mathrm{pair}(x, u)\), halts within \(10(|\mathrm{pair}(x,u)| + 1)\) steps with output the single bit that negates the truth value of the DNF decoded from \(x\) under the assignment \(\alpha _u\) reading variable \(v\) off the \(v\)-th bit of \(u\) (false beyond \(|u|\)).

For every binary string \(z\), let \(z'\) be the pair encoding of the first \(i\) bits of \(z\) with the rest if \(|z| = 2i + 1\), and the empty word if \(|z|\) is even. The non-tautology verifier, run on \(z'\), halts within \(40(|z| + 1)\) steps with output the single bit that is \(0\) if \(|z|\) is even and otherwise negates the truth value of the DNF decoded from the first \(i\) bits of \(z\) under the assignment read off the remaining bits.

Let \(M\) and \(U\) be finite multi-tape Turing machines over the binary alphabet, let \(f, g\) be functions on binary strings, and let \(T_1, T_2 : \mathbb {N} \to \mathbb {N}\). If \(M\) computes \(f\) within \(T_1\), and for every input \(x\) the machine \(U\) run on \(f(x)\) halts within \(T_2(|x|)\) steps with output \(g(x)\), then some finite machine computes \(g\) within time \(n \mapsto 2\, T_1(n) + T_2(n) + 2\).

The set of binary strings \(z\) such that \(|z| = i + (i + 1)\) for some \(i\) and the DNF decoded from the first \(i\) bits of \(z\) evaluates to false under the assignment reading variable \(v\) off the \(v\)-th of the remaining \(i + 1\) bits (false beyond them) belongs to \(\mathrm{P}\).

For every \(n \in \mathbb {N}\) and binary string \(r\), the polarity-flipping scan from the unary-index state of the formula syntax scanner maps \(1^n \mathbin {+\! \! +} r\) to \(1^n\) followed by the polarity-flipping scan of \(r\) from the unary-index state.

For every literal \((v, b)\) and binary string \(r\), the polarity-flipping scan from the clause-level state of the formula syntax scanner maps the serialization of \((v, b)\) followed by \(r\) to the serialization of \((v, \neg b)\) followed by the polarity-flipping scan of \(r\) from the clause-level state.

For every clause \(C\) and binary string \(r\), the polarity-flipping scan from the clause-level state of the formula syntax scanner maps the serialization of \(C\) followed by \(r\) to the serialization of the clause obtained from \(C\) by negating every literal’s polarity, followed by the polarity-flipping scan of \(r\) from the formula-level state.

For every CNF formula \(\varphi \), the polarity-flipping scan from the formula-level state of the formula syntax scanner maps the serialization of \(\varphi \) to the serialization of its De Morgan dual, the DNF obtained from \(\varphi \) by negating every literal in place.

For every binary string \(x\), the guarded dual output of \(x\) — the polarity-flipping scan of \(x\) if \(x\) passes the formula syntax scan, and the word \(0\) otherwise — equals the serialization of the De Morgan dual (every literal negated, read as a DNF) of the CNF formula decoded from \(x\).

For every input \(x\), applying the zero-work-tape action that moves the input head by \(d\), enters \(q'\), and optionally emits \(o\) to the configuration with state \(q\), head position \(p\), and output \(w\) yields the configuration with state \(q'\), head position \(p\) moved by \(d\) (clamped at the boundary blanks), and output \(w\) followed by \(o\).

Let \(x\) be an input and \(i \le |x|\). In every configuration of the dual transducer on \(x\) with input head at position \(i + 1\), the symbol read is the \(i\)-th bit of \(x\) when \(i \lt |x|\) and the right boundary blank when \(i = |x|\).

For every configuration \(c\) of the dual transducer, running it for \(0\) steps from \(c\) reaches \(c\) without visiting the anchor state strictly before, so \(c\) to \(c\) is a segment of length \(0\).

Let \(c\) and \(d\) be configurations of the dual transducer such that one step takes \(c\) to \(d\) and \(c\) is not in the anchor state. Then one step from \(c\) reaches \(d\) with no anchor visit before it, i.e. \(c\) to \(d\) is an anchor-free segment of length \(1\).

Let \(c, d, e\) be configurations of the dual transducer. If running \(a\) steps from \(c\) reaches \(d\) without visiting the anchor state before time \(a\), and running \(b\) steps from \(d\) reaches \(e\) without visiting the anchor before time \(b\), then running \(a + b\) steps from \(c\) reaches \(e\) without visiting the anchor before time \(a + b\).

Let the input be \(x = p \mathbin {+\! \! +} r\), let \(q\) be a formula-scanner state, and let \(o\) be an output word. Started in the scanning state carrying \(q\) at head position \(|p| + 1\) with output \(o\), the dual transducer reaches the scanning state carrying the fold of the scanner transition over \(r\) from \(q\), at position \(|x| + 1\) with output still \(o\), in exactly \(|r|\) steps and without visiting the anchor state before then.

Let the input be \(x = p \mathbin {+\! \! +} r\), let \(q\) be a formula-scanner state, and let \(o\) be an output word. Started in the copying state carrying \(q\) at head position \(|p| + 1\) with output \(o\), the dual transducer reaches, in exactly \(|r|\) steps and without visiting the anchor state before then, the copying state carrying the fold of the scanner transition over \(r\) from \(q\), at position \(|x| + 1\), with output \(o\) followed by the polarity-flipping scan of \(r\) from \(q\).

Let \(x\) be an input, \(o\) an output word, \(f\) a flag, and \(p \le |x|\). Started in the rewind state with flag \(f\) at head position \(p\) and output \(o\), the dual transducer reaches head position \(1\) with output \(o\), in the anchor state if \(f\) is true and in the formula-level copying state otherwise, in exactly \(p + 1\) steps and without visiting the anchor before then.

For every input \(x\), output word \(o\), and formula-scanner state \(q\), the configuration reached by one step of the dual transducer from the copying state carrying \(q\) at the right boundary position \(|x| + 1\) with output \(o\) is the rewind state with flag true at position \(|x|\) with output still \(o\), and the anchor state is not visited.

Let \(x\) be a binary string on which the six-state formula syntax scan from formula level ends in the exact-end state. Started in the formula-level scanning state at head position \(1\) with empty output, the dual transducer reaches the anchor state at position \(1\) with output the polarity-flipping scan of \(x\), in exactly \(4|x| + 4\) steps and without visiting the anchor before then.

Let \(x\) be a binary string on which the six-state formula syntax scan from formula level does not end in the exact-end state. Started in the formula-level scanning state at head position \(1\) with empty output, the dual transducer reaches the anchor state at position \(1\) with output the single bit \(0\), in exactly \(2|x| + 2\) steps and without visiting the anchor before then.

For every binary string \(x\), let \(c\) be the dual transducer’s configuration on \(x\) in the anchor state with input head at position \(1\) and empty output. There is a time \(t\) with \(0 \lt t \le 4|x| + 5\) such that the configurations at all times \(j\) with \(0 \lt j \lt t\) are not in the anchor state, and the configuration at time \(t\) equals \(c\) except that its output is the guarded dual output of \(x\): the polarity-flipping scan of \(x\) if \(x\) passes the formula syntax scan, and the single bit \(0\) otherwise.

The function that maps a binary string \(x\) to the serialization of the De Morgan dual of the CNF formula decoded from \(x\) — the DNF obtained by negating every literal in place — is polynomial-time computable.