GapCVP proof, part 03, continuation 04

def GapCVP.FormulaTotalCert.canonicalMachineOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.FormulaTotalCert.canonicalInputBudget (input : List Bool) : ℕ

GapCVP reduction support.

Equations

• GapCVP.FormulaTotalCert.canonicalInputBudget input = 64 * (input.length + 1) * (input.length + 1) + 64

def GapCVP.FormulaTotalCert.canonicalTotalTrace (input : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 input [] [] [] [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine (canonicalMachineOutput input))) (canonicalInputBudget input)

GapCVP reduction support.

Equations

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

theorem GapCVP.FormulaSemanticCert.readLengthPrefixedWord_some_reconstruct (input word suffix : List Bool) (hread : BinaryEncoding.readLengthPrefixedWord input = some (word, suffix)) : input = BinaryEncoding.lengthPrefixedWord word ++ suffix

theorem GapCVP.FormulaSemanticCert.canonicalMachineOutput_eq_expected (input : List Bool) : FormulaTotalCert.canonicalMachineOutput input = FormulaTotalCert.canonicalFormulaExpected input

def GapCVP.CLStructuralNaturalBinaryWriter.tacticNaturalBinaryWriterStepTac : Lean.ParserDescr

Executes the naturalBinaryWriterStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.CLStructuralNaturalBinaryWriter.structuralNaturalBinaryWriterComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding fun (input : List Bool) => Computability.encodeNat input.length

GapCVP reduction support.

Equations

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

def GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWord input = GapCVP.BinaryEncoding.encodeAtomic input.length

theorem GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWord_eq_prefix (input : List Bool) : structuralAtomicNaturalWord input = BinaryEncoding.lengthPrefixedWord (Computability.encodeNat input.length)

noncomputable def GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWriterComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding structuralAtomicNaturalWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.paddedStructuralTableauSimulation (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : CLVerifier.TableauSimulation bound machine

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine x) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeThreeCNF (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : ThreeCNF

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeCNFWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine x = GapCVP.BinaryEncoding.encodeThreeCNF (GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeThreeCNF bound machine x)

theorem GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeCNFWord_mem_threeSAT_iff (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : threeSATLanguage (structuralWholeCNFWord bound machine x) = true ↔ ∃ (certificate : List Bool), certificate.length ≤ Polynomial.eval x.length bound ∧ verifier (x, certificate) = true

theorem GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeThreeCNF_allDistinct (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : ThreeCNFReduction.allDistinct (structuralWholeThreeCNF bound machine x) = true

theorem GapCVP.CLStructuralWholeCNFOutputTM.structuralNatSize_le_self (value : ℕ) : value.size ≤ value

noncomputable def GapCVP.CNFClauseLoop.clauseLoopFiniteElements (α : Type) [Fintype α] : List α

GapCVP reduction support.

Equations

• GapCVP.CNFClauseLoop.clauseLoopFiniteElements α = List.ofFn ⇑(Fintype.equivFin α).symm

theorem GapCVP.CNFClauseLoop.mem_clauseLoopFiniteElements (α : Type) [Fintype α] (value : α) : value ∈ clauseLoopFiniteElements α

theorem GapCVP.CNFSortingDedup.replicate_append_bit_cons (bit : Bool) (count : ℕ) (tail : List Bool) : List.replicate count bit ++ bit :: tail = bit :: (List.replicate count bit ++ tail)

inductive GapCVP.CNFEncodedClauseSort.EncodedWordOrdering : Type

GapCVP reduction support.

• invalid : EncodedWordOrdering
• less : EncodedWordOrdering
• equal : EncodedWordOrdering
• greater : EncodedWordOrdering

@[instance_reducible]

instance GapCVP.CNFEncodedClauseSort.instDecidableEqEncodedWordOrdering : DecidableEq EncodedWordOrdering

Equations

• GapCVP.CNFEncodedClauseSort.instDecidableEqEncodedWordOrdering x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

noncomputable instance GapCVP.CNFEncodedClauseSort.instFintypeEncodedWordOrdering : Fintype EncodedWordOrdering

Equations

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

def GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst : EncodedWordOrdering → Bool

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.invalid = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal = true
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater = true

def GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond : EncodedWordOrdering → Bool

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.invalid = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less = true
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater = true

def GapCVP.CNFEncodedClauseSort.encodedWordOrderingWord (outcome : EncodedWordOrdering) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.encodedWordOrderingWord outcome = [GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst outcome, GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond outcome]

def GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering : List Bool → List Bool → EncodedWordOrdering

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering [] [] = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering [] (head :: tail) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (head :: tail) [] = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (false :: tail) (true :: tail_1) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (true :: tail) (false :: tail_1) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (false :: left) (false :: right) = GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering left right
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (true :: left) (true :: right) = GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering left right

def GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering (input : List Bool) : EncodedWordOrdering

GapCVP reduction support.

Equations

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

def GapCVP.CNFEncodedClauseSort.sourcePreservingDelimitedPairComparisonWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering_valid (first second suffix : List Bool) : delimitedPairWordOrdering (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = lexicographicEncodedWordOrdering first second