Cook-Levin: situation tables of a multi-stack machine and the correctness of the formula

Top of a stack as read from the windows to Next label/state code of a situation

• Top of a stack as read from the windows
• Symbolic effect of a statement tree
• Stack operations on a path of a statement tree
• Symbols a statement tree can push
• The symbolic effect grows by at most the number of stack operations
• Pushed symbols come from the start or from push nodes
• Encoding data for a finite TM2 machine
• Window depth of a machine
• The situation step
• Symbol-code bound
• Number of window combinations
• Number of situations
• Clause layout of a machine encoding
• Label/state code of a situation
• Window symbol code of a situation
• Position of a situation's variable
• Decoding a symbol code
• Decoded windows of a situation
• Effect of a situation
• Next label/state code of a situation

Push-count table of a situation to Top window of a stack

• Push-count table of a situation
• Consumption table of a situation
• Pushed-symbol table of a situation
• The symbol-code bound is positive
• Symbols left pushed by a situation are effective
• Pushed codes are valid symbol codes
• The transition tables of a machine are well formed
• The situation-definition tables of a machine are well formed
• The cell-shift tables of a machine are well formed
• Halted situations stay fixed
• Mixed-radix number
• Mixed-radix index of a situation
• Situation surjectivity
• Finite set of pushable symbols
• Pushable and input symbols of a stack
• The classical encoding record of a finite multi-stack machine
• Time bound of the transition-clause generator on the tables of a machine
• Time bound of the situation-definition generator on the tables of a machine
• Time bound of the shift generator on the tables of a machine
• Top window of a stack

Applying an effect to the original stacks to Reading back a list from its cells

• Applying an effect to the original stacks
• Reading the top through the windows
• The symbolic effect of a statement agrees with the real step
• Idle-extended step
• Idle-extended run
• Windows of a configuration
• The idle-extended step is the situation step applied to the stacks
• Label-and-state code of a configuration
• Cell code of a configuration
• Situation index of a configuration
• The table-driven row update
• Good configurations
• The situation index matches the code and windows
• Cells of a pushed prefix over a truncated stack
• The table-driven step
• Reads of the in-range shift stay in the row
• The idle-extended step preserves good configurations
• The table-driven step along a run
• Reading a list from a sequence of cells
• Reading back a list from its cells

Entries of a decoded stack on prefix-form input to Positive shift step on a real run (L3⁺)

• Entries of a decoded stack on prefix-form input
• Stack heights grow by at most the window depth per step
• C1 decoder (decoding a row)
• Well-formed rows of cells
• C1a (decoding recovers a good configuration)
• C1b (decoding a well-formed row loses nothing)
• C1c (cell arrays of good configurations are well-formed rows)
• C1d (decoded configurations are good)
• C1e (the row decoder reads only the window)
• Good configurations are determined by their row (C1f)
• C2' (decoding the table-driven row gives the next configuration)
• Truth of a variable under an assignment
• L0 (a satisfied dense clause has a satisfied listed literal)
• In-range shift forcing (L1)
• Cell block of a row equal to an array
• Cell literals of an array hold in a row
• Positive core of the shift step (L2⁺)
• Exact shift step (L2)
• Exact shift step on a real run (L3)
• Positive shift step on a real run (L3⁺)

Transition clauses force the next label to The three depth regions cover every depth exactly once

• Transition clauses force the next label
• Transition clauses force the next label, stack-and-depth form
• The code of a configuration holds in a row
• L2 (S-definition, positive)
• L3 (S-definition, real run)
• Composition with the shift family
• Update forcing (positive)
• Update forcing, real run
• Pushed-fill forcing
• Overflow forcing
• Pushed-fill forcing for a good configuration
• Overflow cells of the next row hold the table value
• Pushed-fill forcing on a real run
• Overflow cells of the next row on a real run
• Stack cap
• Stack heights along a run
• Stack heights are at most the cap minus the window depth
• Stack-cap constraint 1
• Stack-cap constraint 2
• The three depth regions cover every depth exactly once

Cell literals propagate one step along the real run to The init family discharges the init obligation

• Cell literals propagate one step along the real run
• One-step invariant
• One-step invariant at the stack cap
• Row-0 obligation
• Init obligation, input pinned
• Row-\(t\) induction
• Row induction at the stack cap
• Run tracking from the init obligation
• Satisfying a concatenation of CNF formulas
• Positive dense unit clauses force their variable
• Index of the empty-cell variable of the input stack
• Start-code clause of the init family
• Empty-stack clauses of the init family
• Input clauses of the init family
• Certificate clauses of the init family
• Prefix clauses of the init family
• Length-bound clauses of the init family
• The row-0 init family of an encoding
• Init semantics
• The init family discharges the init obligation

A satisfying assignment tracks a certified run to Unfolding the idle-extended run from the front

• A satisfying assignment tracks a certified run
• Faithful literal list
• Faithful dense clause family
• Faithful dense clause family with positive literals
• Exact clause semantics
• The all-true assignment satisfies a faithful clause with a positive literal
• Variables of rows up to the time bound
• The init family is faithful with positive literals
• Accepting code
• Accept-code clauses
• Accept-cell clauses
• The accept family
• Accept-code clauses pin the (label, state) code
• Accept-cell clauses pin the top output symbol
• Accepting configuration
• Satisfying assignments yield accepting runs
• No accepting certificate, no satisfying assignment
• The all-true assignment satisfies the transition, shift and init families
• The all-true assignment violates the accept family
• Unfolding the idle-extended run from the front

The idle-extended run follows the real run to Completeness of the five clause families

• The idle-extended run follows the real run
• A halted configuration is fixed by the idle-extended run
• The idle-extended run stays at the halting configuration
• Acceptance of a halting configuration
• Uniqueness of quotient and remainder
• Equal low-order digits give equal residues
• Situation injectivity
• The real run's literals
• The assignment of the real run's literals
• Faithful clauses with a literal agreeing with the real run are satisfied
• Situation variables lie in the label/state block
• Transition families with a run-literal head are satisfied by the run
• The run assignment satisfies the update family
• The run assignment satisfies the situation-definition family
• The run assignment satisfies the cell-shift family
• Unit clauses on run literals are satisfied
• Row-0 cells of the start configuration are run literals
• Completeness of the init family
• Completeness of the accept family
• Completeness of the five clause families

Part 9 of 9

• The five Cook–Levin clause families are satisfiable iff some certificate is accepted

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.