GapCVP proof, part 08, continuation 03

theorem GapCVP.CNFAnnotatedSourceCompleteSortedDedupTM.flatAnnotatedSortedDedupSourceClauseRecord_ne_nil {T S : ℕ} (clause : CL.Clause T S) : CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord clause ≠ []

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFAnnotatedSourceCompleteSortedDedupTM.flatAnnotatedSortedDedupHeadBit_nonemptyPrefix (record suffix : List Bool) (hrecord : record ≠ []) : CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalHeadBitWord (BinaryEncoding.lengthPrefixedWord record ++ suffix) = [true]

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyPhysicalBundledSourceCert.fiveIndependentActualSortedDistinctBundledSourceWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyIndependentFiveFamilyPhysicalBundledSourceCert.fiveFamilyIndependentActualSortedDistinctBundledSourceComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : BitTM (fiveIndependentActualSortedDistinctBundledSourceWord bound machine)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyIndependentFiveFamilyPhysicalBundledSourceCert.fiveFamilyIndependentActualSortedDistinctBundledSourceWord_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : fiveIndependentActualSortedDistinctBundledSourceWord bound machine original = CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseStream (CLStructuralWholeCNFOutputTM.structuralWholeSourceClauses bound machine original)

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatAnnotatedIndexedORGadgetState (clauseIndex prefixWord pending active emitted count : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatIndexedGadgetNegateLeadingBitWord : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatIndexedGadgetNegateLeadingBitWord [] = []
• GapCVP.CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatIndexedGadgetNegateLeadingBitWord (bit :: remaining) = (!bit) :: remaining

@[reducible, inline]

abbrev GapCVP.CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatIndexedGadgetNegateLeadingBitMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatIndexedGadgetNegateLeadingBitMachine_step (input : List Bool) : flatIndexedGadgetNegateLeadingBitMachine.step (Turing.initList flatIndexedGadgetNegateLeadingBitMachine input) = some (Turing.haltList flatIndexedGadgetNegateLeadingBitMachine (flatIndexedGadgetNegateLeadingBitWord input))

Internal support shared across GapCVP continuation modules.