P versus NP: audited encodings and tableau frontier

PvsNP.DecisionProblem

A decision problem is a language over the Boolean alphabet, that is, an arbitrary set $L\subseteq B^*$ of finite Boolean lists, with no decidability, finiteness, or complexity requirement. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.inputLength

For every finite Boolean list $w$, its input length is defined to be $|w|$, the number of list entries; in particular the empty list has input length zero. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.PolynomialBound

For any function $t:\mathbb N\to\mathbb N$, having a polynomial bound means that there exists a polynomial $p$ with natural-number coefficients such that $\forall n\in\mathbb N,\ t(n)\le p(n)$. The inequality is non-strict, includes $n=0$, and is required for all inputs rather than only eventually; constant and zero polynomials are permitted.

PvsNP.coP

The set $coP$ consists of all languages $L\subseteq B^*$ whose complement $B^*\setminus L$ belongs to $P$; equivalently there exists $\chi:B^*\to B$ satisfying $D(\chi)$ and $\forall w,\ w\notin L\ \Longleftrightarrow\ \chi(w)=\mathrm{true}$. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. Write $D(\chi)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute the singleton output $[\chi(w)]$ from input $w$ in at most $p(|w|)$ steps. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.

PvsNP.coNP

The set $coNP$ consists of all languages $L\subseteq B^*$ for which there exist $R:B^*\times B^*\to B$ and $k\in\mathbb N$ satisfying $C(R)$ and $\forall w,\ w\notin L\ \Longleftrightarrow\ \exists y\in B^*,\ |y|\le |w|^k\land R(w,y)=\mathrm{true}$. Thus the complement is taken within all finite Boolean lists, including malformed encodings for any separate encoding scheme; $0^0=1$ and $0^k=0$ for $k>0$. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. Write $C(R)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for all $w,y\in B^*$, compute $[R(w,y)]$ in at most $p(|w|+|y|)$ steps from the list obtained by tagging every bit of $w$ with the left injection into $B\sqcup B$, tagging every bit of $y$ with the right injection, and concatenating those two lists. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.

PvsNP.NPHard

For every language $L\subseteq B^*$, being NP-hard is defined to mean $\forall A\subseteq B^*,\ A\in NP\ \Longrightarrow\ A\preceq L$; the definition does not additionally require $L\in NP$. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The set $NP$ consists exactly of languages $L\subseteq B^*$ for which there exist $R:B^*\times B^*\to B$ and $k\in\mathbb N$ satisfying $C(R)$ and $\forall w\in B^*,\ w\in L\ \Longleftrightarrow\ \exists y\in B^*,\ |y|\le |w|^k\ \land\ R(w,y)=\mathrm{true}$. This includes $k=0$ and empty input: $0^0=1$, whereas $0^k=0$ for $k>0$. Write $C(R)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for all $w,y\in B^*$, compute $[R(w,y)]$ in at most $p(|w|+|y|)$ steps from the list obtained by tagging every bit of $w$ with the left injection into $B\sqcup B$, tagging every bit of $y$ with the right injection, and concatenating those two lists. For languages $A,B_0\subseteq B^*$, write $A\preceq B_0$ to mean that there exists $f:B^*\to B^*$ satisfying $F(f)$ and $\forall w\in B^*,\ w\in A\ \Longleftrightarrow\ f(w)\in B_0$. Write $F(f)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute output list $f(w)$ from input list $w$ in at most $p(|w|)$ steps. Different existential computation witnesses may use different machines and polynomials. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.

PvsNP.FiniteWorkAlphabets

For every machine $M$, having finite work alphabets is defined to mean $\forall k\in K,\ \Gamma_k$ is a finite type. This quantifies over every stack, including the designated input and output stacks, and asks for propositional finiteness rather than a supplied enumeration. Here $M$ is a TM2 machine with a finite type $K$ of stack indices and decidable equality on $K$, designated input and output indices $k_0,k_1$, stack-symbol types $\Gamma_k$, a finite type $\Lambda$ of program labels with a main label, a finite type $\sigma$ of control states with an initial state, a finite input alphabet $\Gamma_{k_0}$, and a statement $m(\ell)$ for each label $\ell\in\Lambda$. No finiteness of $\Gamma_k$ for other $k$ is assumed. A tagged symbol $(k,a)$ has $k\in K$ and $a\in\Gamma_k$; tags from different stacks remain distinct.

PvsNP.FinitePolyTime

For arbitrary types $\alpha,\beta,U,V$, arbitrary maps $e_i:\alpha\to U^*$ and $e_o:\beta\to V^*$, and arbitrary $f:\alpha\to\beta$, finite-alphabet polynomial-time computability is defined to mean that there exists a machine with input and output alphabet bijections to $U,V$ and a polynomial $p\in\mathbb N[X]$ such that, for every $a\in\alpha$, it computes the encoded output $e_o(f(a))$ from encoded input $e_i(a)$ in at most $p(|e_i(a)|)$ steps, and every stack alphabet of that machine is finite. The encodings are not assumed injective and the domain types are not assumed nonempty; the input/output alphabet bijections and the finiteness requirements still apply if no inputs exist. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.

PvsNP.parseData

For any fuel $f\in\mathbb N$ and Boolean word $w$, this partial parser returns either failure or a pair of Boolean words. At fuel zero it fails on every input. At positive fuel, an initial $[\mathrm{true},\mathrm{false}]$ is consumed and yields the empty decoded word paired with the suffix. Otherwise an initial $[\mathrm{false},b]$ is consumed, the suffix is parsed with fuel decreased by one, and on success $b$ is prepended to the returned decoded word while the returned suffix is kept. Every other input shape fails, as does any recursive failure. Thus a terminating delimiter must be reached while fuel is positive; an empty or one-bit input fails. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.bitsValue

The value of a finite Boolean digit list is defined recursively by $\operatorname{value}([])=0$ and $\operatorname{value}(b::u)=2\operatorname{value}(u)+\mathbf 1_{b=\mathrm{true}}$. Equivalently, for digits $b_0,\ldots,b_{m-1}$ it is $\sum_{j=0}^{m-1}\mathbf 1_{b_j=\mathrm{true}}2^j$, so the least significant digit comes first. This definition accepts noncanonical lists as well: appending false high digits does not change the value. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.parseLiteral

For any Boolean word $w$, literal parsing fails unless $w=[\mathrm{false},b]$ followed by a suffix $r$. It then parses a digit sequence from $r$ with fuel $|r|+1$: at zero fuel fail; with positive fuel consume $[\mathrm{true},\mathrm{false}]$ as the terminator, or consume $[\mathrm{false},d]$ as the next digit and continue with one less fuel; all other shapes and recursive failures fail. If the decoded digit list is $u$ and the remaining suffix is $z$, let $j=\sum_{h<|u|}\mathbf 1_{u_h=\mathrm{true}}2^h$. Parsing succeeds with $((b,j),z)$ exactly when $u$ is the canonical little-endian binary digit list of $j$; otherwise it fails. The canonical digit list for zero is empty, so extra false high digits are rejected. No condition is placed on the suffix $z$. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.parseClauseAux

For any natural fuel and Boolean input word, this partial clause parser fails at zero fuel, including on an empty input or a clause delimiter. With positive fuel, a leading $[\mathrm{true},\mathrm{true}]$ returns the empty clause and the suffix after that pair. In every other case it parses a literal by the procedure described here; after success with literal $l$ and suffix $z$, it parses the remainder of the clause from $z$ with fuel decreased by one and, on success, prepends $l$ to the resulting clause and retains the resulting suffix. Any failure propagates. The returned clause is a list of sign/index pairs and the suffix is unconstrained. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The parser $\operatorname{parse}(w)$ works as follows. Its outer recursion starts with fuel $|w|+1$, returns the empty formula on an empty remainder even at fuel zero, and otherwise fails at fuel zero; with positive fuel it parses one clause from the current nonempty remainder using clause fuel equal to that remainder’s length plus one, then recurses on the returned suffix with outer fuel reduced by one. Clause parsing fails at fuel zero; with positive fuel it consumes $[\mathrm{true},\mathrm{true}]$ as the end of an empty remaining clause, or parses one literal and recurses on its suffix with clause fuel reduced by one. Literal parsing requires an initial pair $[\mathrm{false},b]$ for the sign. On the remainder $r$ it starts data fuel $|r|+1$: zero data fuel fails; with positive data fuel $[\mathrm{true},\mathrm{false}]$ ends the digit sequence, while $[\mathrm{false},d]$ contributes digit $d$ and decreases fuel by one; all other cases fail. The collected digits are interpreted little-endian and accepted only if they equal the canonical binary digits of the resulting natural number. A parsed literal is that sign/index pair together with the suffix after its delimiter; any failed subparse makes the containing parse fail. Success of the outer parse requires consuming the complete input.

PvsNP.parseCNFAux

For every natural fuel and Boolean input word, this partial formula parser returns the empty formula on the empty input regardless of fuel, fails on nonempty input at zero fuel, and at positive fuel on a nonempty word $w$ parses a clause with fuel $|w|+1$, then parses the returned suffix with outer fuel decreased by one. If both succeed, it prepends the parsed clause to the returned formula; otherwise it fails. Consequently there is no unconsumed suffix in a successful result, and at most the supplied number of clauses can be parsed from a nonempty input. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The parser $\operatorname{parse}(w)$ works as follows. Its outer recursion starts with fuel $|w|+1$, returns the empty formula on an empty remainder even at fuel zero, and otherwise fails at fuel zero; with positive fuel it parses one clause from the current nonempty remainder using clause fuel equal to that remainder’s length plus one, then recurses on the returned suffix with outer fuel reduced by one. Clause parsing fails at fuel zero; with positive fuel it consumes $[\mathrm{true},\mathrm{true}]$ as the end of an empty remaining clause, or parses one literal and recurses on its suffix with clause fuel reduced by one. Literal parsing requires an initial pair $[\mathrm{false},b]$ for the sign. On the remainder $r$ it starts data fuel $|r|+1$: zero data fuel fails; with positive data fuel $[\mathrm{true},\mathrm{false}]$ ends the digit sequence, while $[\mathrm{false},d]$ contributes digit $d$ and decreases fuel by one; all other cases fail. The collected digits are interpreted little-endian and accepted only if they equal the canonical binary digits of the resulting natural number. A parsed literal is that sign/index pair together with the suffix after its delimiter; any failed subparse makes the containing parse fail. Success of the outer parse requires consuming the complete input.

PvsNP.parseCNF

For every Boolean word $w$, this formula parser is the outer parsing procedure described here, initialized with fuel $|w|+1$; it returns either a list of clauses of sign/index literals or failure. In particular it returns the empty formula on the empty word. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The parser $\operatorname{parse}(w)$ works as follows. Its outer recursion starts with fuel $|w|+1$, returns the empty formula on an empty remainder even at fuel zero, and otherwise fails at fuel zero; with positive fuel it parses one clause from the current nonempty remainder using clause fuel equal to that remainder’s length plus one, then recurses on the returned suffix with outer fuel reduced by one. Clause parsing fails at fuel zero; with positive fuel it consumes $[\mathrm{true},\mathrm{true}]$ as the end of an empty remaining clause, or parses one literal and recurses on its suffix with clause fuel reduced by one. Literal parsing requires an initial pair $[\mathrm{false},b]$ for the sign. On the remainder $r$ it starts data fuel $|r|+1$: zero data fuel fails; with positive data fuel $[\mathrm{true},\mathrm{false}]$ ends the digit sequence, while $[\mathrm{false},d]$ contributes digit $d$ and decreases fuel by one; all other cases fail. The collected digits are interpreted little-endian and accepted only if they equal the canonical binary digits of the resulting natural number. A parsed literal is that sign/index pair together with the suffix after its delimiter; any failed subparse makes the containing parse fail. Success of the outer parse requires consuming the complete input.

PvsNP.variableNames

For every finite formula $F$, the variable-name list is obtained by concatenating its clause lists, extracting the natural-number index from each sign/index literal in that order, and deleting duplicate occurrences while retaining the first occurrence of each index. It has one entry for each index appearing anywhere in $F$, regardless of sign, and is empty when no literals occur; no numerical sorting is performed. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.certificateAssignment

For every formula $F$, Boolean word $y$, and natural index $j$, the assigned Boolean value is obtained by zipping the list $V(F)$ with $y$, looking up key $j$ in that list of pairs, and defaulting to false if no pair has that key. Zipping stops when either list ends, so extra bits of $y$ are ignored, and variables whose position exceeds a short $y$ are assigned false. The index $j$ may be any natural number, including one absent from $F$; no length equality is required by this definition. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. The variable list $V(F)$ is obtained by reading the indices of all literals in the flattened clause list in order and deleting duplicate occurrences while retaining the first occurrence of each index.

PvsNP.satVerifier

For every ordered pair $(w,y)$ of finite Boolean words, the verifier is the Boolean function defined by the parsing, length check, and formula evaluation described here. It accepts the pair of empty words because the empty word parses as the empty formula, whose variable list is empty and whose evaluation is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The parser $\operatorname{parse}(w)$ works as follows. Its outer recursion starts with fuel $|w|+1$, returns the empty formula on an empty remainder even at fuel zero, and otherwise fails at fuel zero; with positive fuel it parses one clause from the current nonempty remainder using clause fuel equal to that remainder’s length plus one, then recurses on the returned suffix with outer fuel reduced by one. Clause parsing fails at fuel zero; with positive fuel it consumes $[\mathrm{true},\mathrm{true}]$ as the end of an empty remaining clause, or parses one literal and recurses on its suffix with clause fuel reduced by one. Literal parsing requires an initial pair $[\mathrm{false},b]$ for the sign. On the remainder $r$ it starts data fuel $|r|+1$: zero data fuel fails; with positive data fuel $[\mathrm{true},\mathrm{false}]$ ends the digit sequence, while $[\mathrm{false},d]$ contributes digit $d$ and decreases fuel by one; all other cases fail. The collected digits are interpreted little-endian and accepted only if they equal the canonical binary digits of the resulting natural number. A parsed literal is that sign/index pair together with the suffix after its delimiter; any failed subparse makes the containing parse fail. Success of the outer parse requires consuming the complete input. The variable list $V(F)$ is obtained by reading the indices of all literals in the flattened clause list in order and deleting duplicate occurrences while retaining the first occurrence of each index. The Boolean verifier on $(w,y)$ first applies this parser to $w$, returning false on failure. For a parsed formula $F$, it returns false unless $|y|=|V(F)|$; if the lengths agree, it evaluates $F$ under the assignment that gives the $j$th variable in $V(F)$ the $j$th bit of $y$, and gives every unlisted index false. More generally this assignment is formed by zipping $V(F)$ with $y$, looking up an index in that truncated list of pairs, and using false when it is absent. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true.

PvsNP.TableauSpec

The structure consists of exactly six fields: a natural number $s$ named steps, a natural number $i$ named interior, a natural number $r$ named symbols, a list $I$ of lists of natural numbers named initialAllowed, a list $A$ of natural numbers named acceptingSymbols, and a list $H$ of lists of natural numbers named allowedWindows. It contains no equations, inequalities, length requirements, distinctness conditions, alphabet-membership requirements, or other proof fields; in particular all three natural numbers may be zero, all lists may be empty, and entries may be arbitrary natural numbers.

PvsNP.tableauWidth

For every six-field specification $S$, its width is defined to be $W=i+2$, so there are always at least two columns, even when the interior field is zero. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing.

PvsNP.tableauAlphabet

For every six-field specification $S$, its alphabet bound is defined to be $Q=r+1$, so it is always positive, including when the symbols field is zero. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing.

PvsNP.tableauVar

For every six-field specification $S$ and every $t,c,a\in\mathbb N$, the variable index is defined to be $(t(i+2)+c)(r+1)+a$. The arguments are unrestricted: the definition does not require $t\le s$, $c<i+2$, or $a<r+1$, and does not assert injectivity on all triples. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing.

PvsNP.cellClauses

For every specification $S$ and all $t,c\in\mathbb N$, the returned formula starts with the single clause of positive literals $(\mathrm{true},v(t,c,a))$ for $a=0,\ldots,Q-1$ in increasing order, then contains the two-negative-literal clause $[(\mathrm{false},v(t,c,a)),(\mathrm{false},v(t,c,b))]$ for each $0\le a<b<Q$, ordered first by $a$ and then by $b$. No bounds on $t,c$ are required. Since $Q\ge1$, the first clause is never empty; when $Q=1$, there are no two-literal clauses. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.cellsCNF

For every specification $S$, this definition returns the cell formula described here, concatenating the clause lists for all of the indicated cells. It covers one row when $s=0$ and still covers two columns when $i=0$. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The cell formula consists, in increasing $t=0,\ldots,s$ and then increasing $c=0,\ldots,W-1$, of the clause of all positive literals $(\mathrm{true},v(t,c,a))$ for $a=0,\ldots,Q-1$, followed by every two-literal clause $[(\mathrm{false},v(t,c,a)),(\mathrm{false},v(t,c,b))]$ with $0\le a<b<Q$, ordered first by $a$ and then by $b$. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.initialCNF

For every specification $S$, this definition returns the initial formula described here. A missing list $I_c$ is treated as empty and therefore generates a negative unit clause for every $a<Q$ at that column; duplicate allowed entries have no extra effect, entries outside $0,\ldots,Q-1$ generate no positive permission in this construction, and lists beyond the first $W$ columns are ignored. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The initial formula has, in increasing $c<W$ and then increasing $a<Q$, the negative unit clause $[(\mathrm{false},v(0,c,a))]$ exactly when $a\notin I_c$. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.boundaryCNF

For every specification $S$, this definition returns the boundary formula described here: the list of two unit clauses per row asserting symbol zero at the first and last columns. It includes row zero even when $s=0$; since $W=i+2$, the two designated boundary columns are distinct even when $i=0$. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The boundary formula has, for each $t=0,\ldots,s$ in order, the two positive unit clauses at $v(t,0,0)$ and $v(t,i+1,0)$, in that order. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.acceptingCNF

For every specification $S$, this definition returns the accepting formula described here. Membership in $A$ is tested as list membership, so duplicate entries do not duplicate literals for a fixed cell/symbol pair, and entries at least $Q$ are ignored. Boundary columns are included among the eligible columns, and acceptance is tested at row $s$, including row zero when $s=0$. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The accepting formula is a list containing one clause; its literals are $(\mathrm{true},v(s,c,a))$ for every $0\le c<W$ and $0\le a<Q$ with $a\in A$, ordered first by $c$ and then by $a$. If no such $a$ exists, this is an empty clause rather than an empty formula. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.wordsOfLength

For every natural alphabet bound $a$ and natural length $n$, this definition returns a list of lists: at $n=0$ it is the singleton list containing the empty word; at $n+1$ it concatenates, for $d=0,\ldots,a-1$ in order, the lists formed by prepending $d$ to every previously constructed length-$n$ word. Thus it enumerates, in increasing lexicographic order, exactly the words of length $n$ with entries below $a$. For $a=0$ it still returns the singleton empty word at length zero and returns the empty list at every positive length.

PvsNP.windowValues

For every function $T:\mathbb N\times\mathbb N\to\mathbb N$ and all $t,c\in\mathbb N$, this definition returns the six-entry list $[T(t,c),T(t,c+1),T(t,c+2),T(t+1,c),T(t+1,c+1),T(t+1,c+2)]$, in the displayed order. There are no bounds on the arguments or values and no reference to a tableau specification.

PvsNP.forbiddenWindowClause

For every specification $S$, all $t,c\in\mathbb N$, and every natural-number list $u$, the clause is obtained by pairing the ordered position list $[(t,c),(t,c+1),(t,c+2),(t+1,c),(t+1,c+1),(t+1,c+2)]$ with $u$, truncating to the shorter list, and replacing each pair $((t_0,c_0),a)$ by the negative literal $(\mathrm{false},v(t_0,c_0,a))$. Hence the clause has $\min(6,|u|)$ literals, is empty for $u=[]$, and ignores entries of $u$ after the sixth. Neither $|u|=6$ nor any bounds on $t,c,a$ are assumed. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.transitionCNF

For every specification $S$, this definition returns the transition formula described here. Every generated clause has exactly six literals, since only six-entry words are enumerated; allowed-window lists of other lengths or containing entries at least $Q$ cannot match an enumerated word, and repetitions in $H$ have no additional effect. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The transition formula ranges in increasing order over $0\le t<s$, $0\le c<i$, and lexicographically over all six-tuples $u\in\{0,\ldots,Q-1\}^6$ absent from the list $H$. For each such tuple it has the clause of the six negative literals at positions $(t,c),(t,c+1),(t,c+2),(t+1,c),(t+1,c+1),(t+1,c+2)$ with symbol indices given by the corresponding entries of $u$, in that order. If $s=0$ or $i=0$, the transition formula is empty. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.tableauCNF

For every specification $S$, the returned formula is the five-part concatenation described here, with no extra clauses, tests, or hypotheses on $S$. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The full tableau formula is the concatenation, in order, of the cell, initial, boundary, accepting, and transition formulas described here. The cell formula consists, in increasing $t=0,\ldots,s$ and then increasing $c=0,\ldots,W-1$, of the clause of all positive literals $(\mathrm{true},v(t,c,a))$ for $a=0,\ldots,Q-1$, followed by every two-literal clause $[(\mathrm{false},v(t,c,a)),(\mathrm{false},v(t,c,b))]$ with $0\le a<b<Q$, ordered first by $a$ and then by $b$. The initial formula has, in increasing $c<W$ and then increasing $a<Q$, the negative unit clause $[(\mathrm{false},v(0,c,a))]$ exactly when $a\notin I_c$. The boundary formula has, for each $t=0,\ldots,s$ in order, the two positive unit clauses at $v(t,0,0)$ and $v(t,i+1,0)$, in that order. The accepting formula is a list containing one clause; its literals are $(\mathrm{true},v(s,c,a))$ for every $0\le c<W$ and $0\le a<Q$ with $a\in A$, ordered first by $c$ and then by $a$. If no such $a$ exists, this is an empty clause rather than an empty formula. The transition formula ranges in increasing order over $0\le t<s$, $0\le c<i$, and lexicographically over all six-tuples $u\in\{0,\ldots,Q-1\}^6$ absent from the list $H$. For each such tuple it has the clause of the six negative literals at positions $(t,c),(t,c+1),(t,c+2),(t+1,c),(t+1,c+1),(t+1,c+2)$ with symbol indices given by the corresponding entries of $u$, in that order. If $s=0$ or $i=0$, the transition formula is empty. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.TableauEncoding

For every specification $S$, Boolean assignment $\tau:\mathbb N\to B$, and natural-valued two-argument function $T$, this predicate is exactly the encoding condition described here. The row bound is non-strict and the column and symbol bounds are strict, so row zero is always included and $Q\ge1$ even when the symbols field is zero. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The encoding condition for $\tau:\mathbb N\to B$ and $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$ and $\forall t\le s,\ \forall c<W,\ \forall a<Q,\ \tau(v(t,c,a))=\mathrm{true}\ \Longleftrightarrow\ T(t,c)=a$. Values of $T$ outside this rectangle and Boolean values not constrained by these displayed indices are unrestricted. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.ValidTableau

For every specification $S$ and function $T:\mathbb N\times\mathbb N\to\mathbb N$, this predicate is exactly the five conjuncts of the validity condition described here. It makes no additional connection between the allowed-window lists and any machine program, includes boundary cells as possible accepting cells, and imposes no requirement that acceptance first occur at the final row. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The validity condition for $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of: $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$; $\forall c<W,\ T(0,c)\in I_c$; $\forall t\le s,\ T(t,0)=0\land T(t,i+1)=0$; $\exists c<W,\ T(s,c)\in A$; and $\forall t<s,\ \forall c<i,\ [T(t,c),T(t,c+1),T(t,c+2),T(t+1,c),T(t+1,c+1),T(t+1,c+2)]\in H$. Values outside the rectangle are unrestricted; the last condition is vacuous for $s=0$ or $i=0$, and a missing required $I_c$ or an empty $A$ makes the condition unsatisfiable.

PvsNP.encodeTableauSpec

For every specification $S$, this definition returns the Boolean word $J(S)$ described here. The first four counts are represented by lengths of clauses of repeated positive variable-zero literals, rather than by binary numeral fields. No restriction on the six specification fields is assumed. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The specification encoding $J(S)$ is $E(G_S)$, where $G_S$ is the following clause list: first a clause of $s$ copies of $(\mathrm{true},0)$, then a clause of $i$ copies, then a clause of $r$ copies, then a clause of $|I|$ copies; next, for each list $x$ in $I$ in order, the clause $[(\mathrm{true},a):a\text{ runs through }x]$; next one clause formed in the same way from $A$; finally one such clause for each list in $H$ in order. These are raw formula encodings: no satisfiability condition is part of $J$. Empty lists and zero replication counts give empty clauses, which still have their clause delimiters. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

PvsNP.MachineTableauSpec

For every specification $S$, this predicate is the conjunction of the additional specification conditions described here. In particular it requires positive steps and interior, exactly $i+2$ initial lists, nonzero accepting symbols, and length-six allowed windows with in-range entries; it does not impose transition consistency with a separately given machine, require satisfiability, or require the listed choices to be nonempty. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The additional specification condition is exactly $s>0$, $i>0$, $0\notin A$, $|I|=W$, every entry of every list in $I$ is below $Q$, every entry of $A$ is below $Q$, and every list in $H$ has length exactly six and every one of its entries is below $Q$. It imposes no nonemptiness condition on an individual list in $I$, on $A$, or on $H$, and allows $r=0$; in that case $Q=1$ and the accepting list must be empty.

PvsNP.EXPTIME

This definition gives the class of languages described here, using an everywhere-valid upper bound of the form $2^{p(n)}$ on a chosen time-bound function. A witness consists of the Boolean decider, the time-bounded machine, and the natural-coefficient polynomial; it need not specify finite alphabets for all non-input stacks. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The set $EXPTIME$ consists exactly of languages $L\subseteq B^*$ for which there are a Boolean function $\chi:B^*\to B$, a machine with a natural-valued time bound $t:\mathbb N\to\mathbb N$ computing $[\chi(w)]$ from $w$ within $t(|w|)$ steps for every $w$, and $p\in\mathbb N[X]$ with $\forall n\in\mathbb N,\ t(n)\le 2^{p(n)}$, such that $\forall w,\ w\in L\ \Longleftrightarrow\ \chi(w)=\mathrm{true}$. The bound includes $n=0$. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations.