Documentation

MIPRE.TM.CookLevin.AnsEnd

The answer tapes end at T #

Two clauses beyond the tableau: the cell at position T + 3 of each of the two free tapes holds the blank. They are what makes the soundness direction of the describer give answers of length at most T: the free-tape clauses force the blanks of a free tape to be trailing (freeClauses), so a blank at T + 3 bounds the string read off the time-0 row by T (freeLen, Sound.lean). An accepting run on answers of length at most T satisfies them, so they cost the completeness direction nothing.

tableauPlus is the tableau together with them, tableauPlusF the formula, and eval_tableauPlusF its exactness (planning/succinct-cook-levin.md, S3).

source
def MIPRE.TM.CookLevin.Desc.ansEndClauses (e G T : ℕ) :
SAT.Cnf3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G)

The two clauses: the cell at position T + 3 of a free tape holds the blank.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def MIPRE.TM.CookLevin.Desc.AnsEnd (e T : ℕ) (c : Cand) :
    Prop

    The candidate is one of the two answer-end clauses.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.TM.CookLevin.Desc.ansEnd_iff (e G T : ℕ) (c : Cand) :
      AnsEnd e T c ↔ ∃ cl ∈ ansEndClauses e G T, Cand.Dec e G c cl
      source
      noncomputable def MIPRE.TM.CookLevin.Desc.tableauPlus (e T : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (chk : SAT.Circuit) :
      SAT.Cnf3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) chk.gates.length)

      The tableau together with the two answer-end clauses: the clause set the describer describes.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        As a formula #

        source
        def MIPRE.TM.CookLevin.Desc.ansEndF (e T : ℕ) (C : CandF) :
        SAT.Fml

        AnsEnd.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.TM.CookLevin.Desc.eval_ansEndF (e G T : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (hT : T + 3 < 2 ^ W e) :
          SAT.Fml.eval x (ansEndF e T C) = true ↔ AnsEnd e T (evalCand C x)
          source
          theorem MIPRE.TM.CookLevin.Desc.InputsLt.ansEndF (e T : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) :
          SAT.Fml.InputsLt n (Desc.ansEndF e T C)
          source
          noncomputable def MIPRE.TM.CookLevin.Desc.tableauPlusF (e G T : ℕ) (tabs : List (ℕ × SAT.Fml)) (frees : List ℕ) (tpls : List (List NTpl)) (C : CandF) :
          SAT.Fml

          The formula of the whole clause set.

          Equations
          Instances For
            source
            theorem MIPRE.TM.CookLevin.Desc.eval_tableauPlusF (e T : ℕ) {fixed : Fin 7 → Option (List Interp.Sym)} {tabs : List (ℕ × SAT.Fml)} {frees : List ℕ} {C : CandF} (hC : CandF.Lengths e chk.gates.length C) (x : ℕ → Bool) (ht : TapeSpec e C.A₁ fixed tabs) (hf : FreeSpec fixed frees) (hT : T + 3 < 2 ^ W e) :
            SAT.Fml.eval x (tableauPlusF e chk.gates.length T tabs frees (tplsOf chk.gates.length chk) C) = true ↔ ∃ cl ∈ tableauPlus e T fixed chk, Cand.Dec e chk.gates.length (evalCand C x) cl

            The describer's formula is exact: it accepts a candidate iff the candidate decodes to a clause of tableauPlus.

            source
            theorem MIPRE.TM.CookLevin.Desc.InputsLt.tableauPlusF (e G T : ℕ) {n : ℕ} (tabs : List (ℕ × SAT.Fml)) (htabs : ∀ jv ∈ tabs, SAT.Fml.InputsLt n jv.2) (frees : List ℕ) (tpls : List (List NTpl)) {C : CandF} (hC : CandF.InputsLt n C) :
            SAT.Fml.InputsLt n (Desc.tableauPlusF e G T tabs frees tpls C)