GapCVP proof, part 07, continuation 04

def GapCVP.CNFAnnotatedSourceCompleteFiniteSetComparatorSourceCert.annotatedCompleteTotalOrderingWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceCompleteFiniteSetComparatorSourceCert.annotatedCompleteTotalSourceComparison (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFAnnotatedSourceCompleteFiniteSetComparatorSourceCert.flatAnnotatedCompleteTotalSourceComparisonComputable : BitTM annotatedCompleteTotalSourceComparison

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFAnnotatedSourceCompleteFiniteSetComparatorSourceCert.flatAnnotatedCompleteTotalOrderingWord_valid (first second : List ℕ) (firstClause secondClause suffix : List Bool) : annotatedCompleteTotalOrderingWord (CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceAdjacentClauseWord firstClause (CNFCappedFlatSourceListFoldTM.flatDuplicatedUnarySourceStream first) first.length secondClause (CNFCappedFlatSourceListFoldTM.flatDuplicatedUnarySourceStream second) second.length suffix) = CNFEncodedClauseSort.encodedWordOrderingWord (CNFFlatSourceOrder.flatSortedSourceListOrdering first second)

@[simp]

theorem GapCVP.CNFAnnotatedSourceCompleteFiniteSetComparatorSourceCert.flatAnnotatedCompleteOriginalClausePair_records {T S : ℕ} (first second : CL.Clause T S) : CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord first ++ CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord second = CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceAdjacentClauseWord (CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseDescriptorPayload first) (CNFCappedFlatSourceListFoldTM.flatDuplicatedUnarySourceStream (CNFFlatSourceOrder.flatSourceFinsetCodes first)) (CNFFlatSourceOrder.flatSourceFinsetCodes first).length (CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseDescriptorPayload second) (CNFCappedFlatSourceListFoldTM.flatDuplicatedUnarySourceStream (CNFFlatSourceOrder.flatSourceFinsetCodes second)) (CNFFlatSourceOrder.flatSourceFinsetCodes second).length []

theorem GapCVP.CNFAnnotatedSourceCompleteFiniteSetComparatorSourceCert.flatAnnotatedCompleteTotalSourceComparison_correct : CNFAnnotatedSourceClauseBubblePassTM.CorrectFlatAnnotatedBundledSourceComparison annotatedCompleteTotalSourceComparison = true

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenOneBit_exists (marker : List Bool → List Bool) (hmarker : ∀ (input : List Bool), (marker input).length = 1) (input : List Bool) : ∃ (bit : Bool), marker input = [bit]

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveForbiddenOneBitGuardedWord (marker worker : List Bool → List Bool) (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveForbiddenOneBitGuardedWord marker worker input = if (marker input).headD false = true then worker input else []

noncomputable def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveForbiddenOneBitGuardedComputable {marker worker : List Bool → List Bool} (hmarker : BitTM marker) (hunique : ∀ (input : List Bool), (marker input).length = 1) (hworker : BitTM worker) : BitTM (fiveForbiddenOneBitGuardedWord marker worker)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedMinimum {α : Type} [Encodable α] (first second : α) : α

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedMinimum first second = if Encodable.encode first < Encodable.encode second then first else second

def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedMaximum {α : Type} [Encodable α] (first second : α) : α

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedMaximum first second = if Encodable.encode first < Encodable.encode second then second else first

def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveForbiddenEncodedSortedAtoms {α : Type} [Encodable α] (first second third fourth : α) : α × α × α × α

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveForbiddenEncodedSortedAtomList {α : Type} [Encodable α] (first second third fourth : α) : List α

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveFamilyForbiddenEncodedSortedAtomList_pairwise {α : Type} [Encodable α] (first second third fourth : α) : List.Pairwise (fun (left right : α) => Encodable.encode left ≤ Encodable.encode right) (fiveForbiddenEncodedSortedAtomList first second third fourth)

def GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.fiveForbiddenWindowSortedUniqueLiteralList {T S : ℕ} (window : CL.Window T) (symbols : CL.WindowSymbols S) : List (CL.SignedLiteral T S)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM.sortedElements_transitionClause_eq_sortedNetwork {T S : ℕ} (window : CL.Window T) (symbols : CL.WindowSymbols S) : ThreeCNFReduction.sortedElements (CL.transitionClause window symbols) = fiveForbiddenWindowSortedUniqueLiteralList window symbols

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceLessMarker (first second : List Bool → List Bool) : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceNotLessMarker (first second : List Bool → List Bool) : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveForbiddenRawSourceLessMarker_length (first second : List Bool → List Bool) (input : List Bool) : (fiveForbiddenRawSourceLessMarker first second input).length = 1

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert.fiveFamilyForbiddenRawSourceNotLessMarker_length (first second : List Bool → List Bool) (input : List Bool) : (fiveForbiddenRawSourceNotLessMarker first second input).length = 1

Internal support shared across GapCVP continuation modules.