GapCVP proof, part 12, continuation 02

def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingSuffixAt (index : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourcePreprocessingTM.paperSourcePreprocessingSuffixAt index = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix^[index]

noncomputable def GapCVP.SourcePreprocessingTM.paperPreprocessingSuffixAtComputable (index : ℕ) : BitTM (paperSourcePreprocessingSuffixAt index)

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingField (index : ℕ) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourcePreprocessingTM.paperSourcePreprocessingField index = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents ∘ GapCVP.SourcePreprocessingTM.paperSourcePreprocessingSuffixAt index

noncomputable def GapCVP.SourcePreprocessingTM.paperPreprocessingFieldComputable (index : ℕ) : BitTM (paperSourcePreprocessingField index)

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourceClauseLiteralWord (position : Fin 3) : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourceClauseVariableWord (position : Fin 3) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourcePreprocessingTM.paperSourceClauseVariableWordComputable (position : Fin 3) : BitTM (paperSourceClauseVariableWord position)

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourceClauseSignWord (position : Fin 3) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourcePreprocessingTM.paperSourceClauseSignWordComputable (position : Fin 3) : BitTM (paperSourceClauseSignWord position)

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourceClauseSecondKeepMarker : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourcePreprocessingTM.paperSourceClauseSecondKeepMarkerComputable : BitTM paperSourceClauseSecondKeepMarker

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourceClauseThirdKeepMarker : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperClauseSelectedSecondLiteral (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperClauseSelectedThirdLiteral (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourceClauseSecondKeepUnary (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourcePreprocessingTM.paperSourceClauseSecondKeepUnary input = if (GapCVP.SourcePreprocessingTM.paperSourceClauseSecondKeepMarker input).headD false = true then [true] else []

def GapCVP.SourcePreprocessingTM.paperSourceClauseThirdKeepUnary (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourcePreprocessingTM.paperSourceClauseThirdKeepUnary input = if (GapCVP.SourcePreprocessingTM.paperSourceClauseThirdKeepMarker input).headD false = true then [true] else []

def GapCVP.SourcePreprocessingTM.paperSourceClauseNormalizedRecord (input : 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.SourcePreprocessingTM.paperSourceClauseNormalizedRecordComputable : BitTM paperSourceClauseNormalizedRecord

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingValidState (formula : ThreeCNF) (originalBody normalizedBody : List Bool) (retainedCount : ℕ) (pending : ThreeCNF) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourcePreprocessingField_valid_two (formula : ThreeCNF) (originalBody normalizedBody : List Bool) (retainedCount : ℕ) (pending : ThreeCNF) : paperSourcePreprocessingField 2 (paperSourcePreprocessingValidState formula originalBody normalizedBody retainedCount pending) = List.replicate retainedCount true

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourcePreprocessingTM.paperSourceClauseNormalizedRecord_length_le (input : List Bool) : (paperSourceClauseNormalizedRecord input).length ≤ 3 * input.length + 10

Internal support shared across GapCVP continuation modules.

def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFinalState : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFinalField (index : ℕ) : 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.SourcePreprocessingTM.paperPreprocessingFinalFieldComputable (index : ℕ) : BitTM (paperSourcePreprocessingFinalField index)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourcePreprocessingTM.paperPreprocessingFilteredFormulaWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFilteredFormulaWordComputable : BitTM paperPreprocessingFilteredFormulaWord

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourcePreprocessingTM.paperSourcePreprocessingComputable : BitTM paperSourcePreprocessingOutput

GapCVP reduction support.

Equations

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

theorem GapCVP.SourcePreprocessingPairwiseIdentity.paperSourceEraseDupsThree_pairwise (first second third : Literal) : [first, second, third].eraseDups = first :: ((if first = second then [] else [second]) ++ if first = third ∨ second = third then [] else [third])

theorem GapCVP.SourcePreprocessingPairwiseIdentity.paperSourceNormalizedClause_pairwise (clause : ThreeClause) : SourcePreprocessingSemantics.paperSourceNormalizedClause clause = clause 0 :: ((if clause 0 = clause 1 then [] else [clause 1]) ++ if clause 0 = clause 2 ∨ clause 1 = clause 2 then [] else [clause 2])

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourceClauseVariableWord_valid (position : Fin 3) (clause : ThreeClause) (suffix : List Bool) : paperSourceClauseVariableWord position (BinaryEncoding.encodeThreeClause clause ++ suffix) = Computability.encodeNat (clause position).1

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourceClauseSignWord_valid (position : Fin 3) (clause : ThreeClause) (suffix : List Bool) : paperSourceClauseSignWord position (BinaryEncoding.encodeThreeClause clause ++ suffix) = [(clause position).2]

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourceClauseSecondKeepMarker_valid (clause : ThreeClause) (suffix : List Bool) : paperSourceClauseSecondKeepMarker (BinaryEncoding.encodeThreeClause clause ++ suffix) = [!decide (clause 0 = clause 1)]

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourceClauseNormalizedRecord_valid (clause : ThreeClause) (suffix : List Bool) : paperSourceClauseNormalizedRecord (BinaryEncoding.encodeThreeClause clause ++ suffix) = SourcePreprocessingSemantics.paperSourceNormalizedClauseRecord clause

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFinalState_valid (formula : ThreeCNF) : paperSourcePreprocessingFinalState (BinaryEncoding.encodeThreeCNF formula) = paperSourcePreprocessingValidState formula (List.flatMap BinaryEncoding.encodeThreeClause (BinarySourceTautologyNormalizationExact.noTautClauses formula)) (SourcePreprocessingSemantics.paperSourceNormalizedClauseStream formula) (List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) []

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFinalOriginalBody_valid (formula : ThreeCNF) : paperSourcePreprocessingFinalField 0 (BinaryEncoding.encodeThreeCNF formula) = List.flatMap BinaryEncoding.encodeThreeClause (BinarySourceTautologyNormalizationExact.noTautClauses formula)

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFilteredFormulaWord_valid (formula : ThreeCNF) : paperPreprocessingFilteredFormulaWord (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.encodeThreeCNF (BinarySourceTautologyNormalizationExact.noTautClauses formula)

theorem GapCVP.SourcePreprocessingTM.paperSourcePreprocessingOutput_valid (formula : ThreeCNF) : paperSourcePreprocessingOutput (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.lengthPrefixedWord (BinaryEncoding.encodeThreeCNF (BinarySourceTautologyNormalizationExact.noTautClauses formula)) ++ (BinaryEncoding.lengthPrefixedWord (SourcePreprocessingSemantics.paperSourceNormalizedClauseStream formula) ++ BinaryEncoding.encodeThreeCNF formula)

structure GapCVP.NormalizedRecordDecoder.PaperVariableArityNormalizedSourceDescriptor : Type

GapCVP reduction support.

• retainedFormula : ThreeCNF

  GapCVP reduction support.

• normalizedClauses : List (List Literal)

  GapCVP reduction support.

• originalFormula : ThreeCNF

  GapCVP reduction support.

• originalWord : List Bool

  GapCVP reduction support.

def GapCVP.NormalizedRecordDecoder.readPaperVariableArityNormalizedSourceDescriptor (bits : List Bool) : Option PaperVariableArityNormalizedSourceDescriptor

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.NormalizedRecordDecoder.readPaperVariableArityNormalizedSourceDescriptor_valid (formula : ThreeCNF) : readPaperVariableArityNormalizedSourceDescriptor (SourcePreprocessingTM.paperSourcePreprocessingOutput (BinaryEncoding.encodeThreeCNF formula)) = some { retainedFormula := BinarySourceTautologyNormalizationExact.noTautClauses formula, normalizedClauses := SourcePreprocessingSemantics.paperSourceNormalizedClauses formula, originalFormula := formula, originalWord := BinaryEncoding.encodeThreeCNF formula }

@[simp]

theorem GapCVP.NormalizedRecordDecoder.readPaperVariableArityNormalizedSourceDescriptor_retainedCount (formula : ThreeCNF) : (SourcePreprocessingSemantics.paperSourceNormalizedClauses formula).length = List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)

noncomputable def GapCVP.SourceOrder.paperVariableArityBooleanWordOrder (arity : ℕ) : Fin (2 ^ arity) ≃ (Fin arity → Bool)

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperVariableArityBooleanWordOrder arity = Equiv.ofBijective (GapCVP.BinaryFieldBasis.indexedWord arity) ⋯

theorem GapCVP.SourceOrder.paperVariableArityBooleanWordOrder_apply_testBit (arity : ℕ) (word : Fin (2 ^ arity)) (position : Fin arity) : (paperVariableArityBooleanWordOrder arity) word position = (↑word).testBit ↑position

The Boolean word order reads each coordinate as the corresponding rank bit.

noncomputable def GapCVP.SourceOrder.paperVariableArityRejectedWord (arity : ℕ) (sign : Fin arity → Bool) : Fin (2 ^ arity)

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperVariableArityRejectedWord arity sign = (GapCVP.SourceOrder.paperVariableArityBooleanWordOrder arity).symm fun (index : Fin arity) => !sign index

noncomputable def GapCVP.SourceOrder.paperSatisfyingWordOrder (arity : ℕ) (sign : Fin arity → Bool) : Fin (2 ^ arity - 1) ≃ { assignment : Fin arity → Bool // ∃ (index : Fin arity), assignment index = sign index }

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceOrder.paperSatisfyingWordOrder_apply_testBit (arity : ℕ) (sign : Fin arity → Bool) (tuple : Fin (2 ^ arity - 1)) (position : Fin arity) : ↑((paperSatisfyingWordOrder arity sign) tuple) position = (↑tuple + if ↑tuple < ↑(paperVariableArityRejectedWord arity sign) then 0 else 1).testBit ↑position

A satisfying word's bit is the rank bit after skipping the rejected assignment.

noncomputable def GapCVP.SourceOrder.paperLocalVariableWordOrder (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) : Fin clause.length ≃ (FormulaBridge.paperVariableAritySourceClause formula clause hclause).LocalVariable

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperLocalVariableWordOrder formula clause hclause = Equiv.ofBijective ⇑(GapCVP.SourceOrder.paperLocalVariableEmbedding✝ formula clause hclause) ⋯

theorem GapCVP.SourceOrder.paperLocalVariableWordOrder_apply_rank (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) (position : Fin clause.length) : ↑↑((paperLocalVariableWordOrder formula clause hclause) position) = FormulaBridge.paperVariableArityVariableRank formula (clause.get position).1

The local word order maps a clause position to its normalized variable rank.

noncomputable def GapCVP.SourceOrder.paperLocalAssignmentWordOrder (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) : (FormulaBridge.paperVariableAritySourceClause formula clause hclause).LocalAssignment ≃ (Fin clause.length → Bool)

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperLocalAssignmentWordOrder formula clause hclause = (GapCVP.SourceOrder.paperLocalVariableWordOrder formula clause hclause).symm.arrowCongr (Equiv.refl Bool)

theorem GapCVP.SourceOrder.paperVariableAritySourceClause_localSatisfied_iff (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) (assignment : (FormulaBridge.paperVariableAritySourceClause formula clause hclause).LocalAssignment) : (FormulaBridge.paperVariableAritySourceClause formula clause hclause).LocalSatisfied assignment = true ↔ ∃ (index : Fin clause.length), (paperLocalAssignmentWordOrder formula clause hclause) assignment index = (clause.get index).2

noncomputable def GapCVP.SourceOrder.paperVariableAritySatisfyingLocalTupleWordEquiv (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) : (FormulaBridge.paperVariableAritySourceClause formula clause hclause).SatisfyingLocalTuple ≃ { assignment : Fin clause.length → Bool // ∃ (index : Fin clause.length), assignment index = (clause.get index).2 }

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperVariableAritySatisfyingLocalTupleWordEquiv formula clause hclause = (GapCVP.SourceOrder.paperLocalAssignmentWordOrder formula clause hclause).subtypeEquiv ⋯

noncomputable def GapCVP.SourceOrder.sourceClauseTupleWordOrder (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) : Fin (2 ^ clause.length - 1) ≃ (FormulaBridge.paperVariableAritySourceClause formula clause hclause).SatisfyingLocalTuple

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceOrder.paperFormulaRetainedClause (formula : ThreeCNF) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : { clause : List Literal // clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula }

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperFormulaRetainedClause formula index = (GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClauses formula).attach.get (Fin.cast ⋯ index)

theorem GapCVP.SourceOrder.paperFormulaRetainedClause_sourceClause (formula : ThreeCNF) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : FormulaBridge.paperVariableAritySourceClause formula ↑(paperFormulaRetainedClause formula index) ⋯ = (FormulaBridge.srcFormula formula).clauses.get index

def GapCVP.SourceOrder.paperFormulaClauseWidth (formula : ThreeCNF) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperFormulaClauseWidth formula index = (↑(GapCVP.SourceOrder.paperFormulaRetainedClause formula index)).length

noncomputable def GapCVP.SourceOrder.paperFormulaClauseTupleWordOrder (formula : ThreeCNF) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : Fin (2 ^ paperFormulaClauseWidth formula index - 1) ≃ ((FormulaBridge.srcFormula formula).clauses.get index).SatisfyingLocalTuple

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperFormulaClauseVariableWordOrder (formula : ThreeCNF) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : Fin (paperFormulaClauseWidth formula index) ≃ ((FormulaBridge.srcFormula formula).clauses.get index).LocalVariable

GapCVP reduction support.

Equations

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

def GapCVP.SourceOrder.paperVariableArityLocalTagCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperVariableArityLocalTagWordOrder (formula : ThreeCNF) : Fin (paperVariableArityLocalTagCount formula) ≃ (index : Fin (FormulaBridge.srcFormula formula).clauses.length) × ((FormulaBridge.srcFormula formula).clauses.get index).SatisfyingLocalTuple

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.paperVariableArityLocalTagWordOrder formula = id (finSigmaFinEquiv.symm.trans (Equiv.sigmaCongrRight (GapCVP.SourceOrder.paperFormulaClauseTupleWordOrder formula)))

noncomputable def GapCVP.SourceOrder.sourceTypeWordOrder (formula : ThreeCNF) : Fin (1 + paperVariableArityLocalTagCount formula) ≃ Core.sourceSATTableType (FormulaBridge.srcFormula formula)

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.sourceTypeWordOrder formula = finSumFinEquiv.symm.trans (finOneEquiv.sumCongr (GapCVP.SourceOrder.paperVariableArityLocalTagWordOrder formula))

theorem GapCVP.SourceOrder.sourceTableType_card (formula : ThreeCNF) : Fintype.card (Core.sourceSATTableType (FormulaBridge.srcFormula formula)) = 1 + paperVariableArityLocalTagCount formula