Documentation

LeanPool.GapCVP.Part07C

GapCVP proof, part 07, continuation 03 #

def GapCVP.CNFAnnotatedSourceClausePairZipTM.flatAnnotatedSourceZipArchivedPair (pair : ℕ × ℕ) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

def GapCVP.CNFAnnotatedSourceClausePairZipTM.flatAnnotatedSourceZipHeadPair (offset : ℕ) (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceClausePairZipTM.annotatedSourceZipHeadPairComputable (offset : ℕ) :

BitTM (flatAnnotatedSourceZipHeadPair offset)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

def GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipState (first second : List ℕ) (archive suffix : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

def GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipStep (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipFoldComputable :

BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput flatAnnotatedCountedSourceZipStep)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

theorem GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.boundedRecordFoldOutput_flatAnnotatedCountedSourceZipPairs (pairs : List (ℕ × ℕ)) (firstRemaining secondRemaining : List ℕ) (archive suffix : List Bool) :

OutputBoundedDependentRecordFold.boundedRecordFoldOutput flatAnnotatedCountedSourceZipStep (OutputBoundedDependentRecordFold.unaryBoundedFoldWord pairs.length (flatAnnotatedCountedSourceZipState (List.map Prod.fst pairs ++ firstRemaining) (List.map Prod.snd pairs ++ secondRemaining) archive suffix)) = flatAnnotatedCountedSourceZipState firstRemaining secondRemaining (List.flatMap CNFAnnotatedSourceClausePairZipTM.flatAnnotatedSourceZipArchivedPair pairs.reverse ++ archive) suffix

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.countedPairZipPreparationWord (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourcePairZipPreparationComputable :

BitTM countedPairZipPreparationWord

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

@[simp]

theorem GapCVP.CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourcePairZipPreparationWord_valid (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) :

countedPairZipPreparationWord (CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix) = OutputBoundedDependentRecordFold.unaryBoundedFoldWord (min firstCount secondCount - 1) (BinaryEncoding.lengthPrefixedWord firstCodes ++ BinaryEncoding.lengthPrefixedWord secondCodes ++ BinaryEncoding.lengthPrefixedWord [] ++ BinaryEncoding.lengthPrefixedWord (List.replicate firstCount true) ++ BinaryEncoding.lengthPrefixedWord (List.replicate secondCount true) ++ CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix)

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFAnnotatedSourceCountedResidualTailTM.annotatedCountedResidualTailCount (offset : ℕ) (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

GapCVP.CNFAnnotatedSourceCountedResidualTailTM.annotatedCountedResidualTailCount offset input = (GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt (offset + 3) input).tail

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualTailCountComputable (offset : ℕ) :

BitTM (annotatedCountedResidualTailCount offset)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

def GapCVP.CNFAnnotatedSourceCountedResidualTailTM.annotatedCountedResidualHeadUnary (offset : ℕ) (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualHeadUnaryComputable (offset : ℕ) :

BitTM (annotatedCountedResidualHeadUnary offset)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

@[simp]

theorem GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualHeadUnary_first (head : ℕ) (remaining second : List ℕ) (archive suffix : List Bool) :

annotatedCountedResidualHeadUnary 0 (CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipState (head :: remaining) second archive suffix) = List.replicate head true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualHeadUnary_second (first : List ℕ) (head : ℕ) (remaining : List ℕ) (archive suffix : List Bool) :

annotatedCountedResidualHeadUnary 1 (CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipState first (head :: remaining) archive suffix) = List.replicate head true

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFAnnotatedSourceCountedResidualTailTM.annotatedCountedResidualCappedBinaryWord (offset capOffset : ℕ) :

List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualCappedBinaryComputable (offset capOffset : ℕ) :

BitTM (annotatedCountedResidualCappedBinaryWord offset capOffset)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

@[simp]

theorem GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualCappedBinaryWord_first (head : ℕ) (remaining : List ℕ) (opposite : ℕ) (secondRemaining : List ℕ) (archive suffix : List Bool) :

annotatedCountedResidualCappedBinaryWord 0 1 (CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipState (head :: remaining) (opposite :: secondRemaining) archive suffix) = Computability.encodeNat (CNFFlatSourceOrder.cappedFlatSourceListValue (opposite + 1) remaining)

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFAnnotatedSourceCountedResidualTailTM.flatAnnotatedCountedResidualCappedBinaryWord_second (opposite : ℕ) (firstRemaining : List ℕ) (head : ℕ) (remaining : List ℕ) (archive suffix : List Bool) :

annotatedCountedResidualCappedBinaryWord 1 0 (CNFAnnotatedSourceCountedClausePairZipTM.flatAnnotatedCountedSourceZipState (opposite :: firstRemaining) (head :: remaining) archive suffix) = Computability.encodeNat (CNFFlatSourceOrder.cappedFlatSourceListValue (opposite + 1) remaining)

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.fourFamilyTaggedGuardedWorkerWord (tag : List Bool) (worker : List Bool → List Bool) (input : List Bool) :

GapCVP reduction support.

Equations

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

Instances For

noncomputable def GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.fourFamilyTaggedGuardedWorkerComputable (tag : List Bool) {worker : List Bool → List Bool} (computer : BitTM worker) :

BitTM (fourFamilyTaggedGuardedWorkerWord tag worker)

GapCVP reduction support.

Equations

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

Instances For

@[simp]

theorem GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.sourceFourFamilyTaggedGuardedWorkerWord_valid (expected actual payload : List Bool) (worker : List Bool → List Bool) :

fourFamilyTaggedGuardedWorkerWord expected worker (BinaryEncoding.lengthPrefixedWord actual ++ payload) = if expected = actual then worker payload else []

def GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.fourFamilyTaggedPredicateMarker (interpolation normalization diagonal clause : List Bool → List Bool) (input : List Bool) :

GapCVP reduction support.

Equations

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

Instances For

noncomputable def GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.fourFamilyTaggedPredicateMarkerComputable {interpolation normalization diagonal clause : List Bool → List Bool} (hinterpolation : BitTM interpolation) (hnormalization : BitTM normalization) (hdiagonal : BitTM diagonal) (hclause : BitTM clause) :

BitTM (fourFamilyTaggedPredicateMarker interpolation normalization diagonal clause)

GapCVP reduction support.

Equations

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

Instances For

@[simp]

theorem GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.sourceFourFamilyTaggedPredicateMarker_interpolation (interpolation normalization diagonal clause : List Bool → List Bool) (payload : List Bool) :

fourFamilyTaggedPredicateMarker interpolation normalization diagonal clause (BinaryEncoding.lengthPrefixedWord [false , false ] ++ payload) = interpolation payload

@[simp]

theorem GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.sourceFourFamilyTaggedPredicateMarker_normalization (interpolation normalization diagonal clause : List Bool → List Bool) (payload : List Bool) :

fourFamilyTaggedPredicateMarker interpolation normalization diagonal clause (BinaryEncoding.lengthPrefixedWord [false , true ] ++ payload) = normalization payload

@[simp]

theorem GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.sourceFourFamilyTaggedPredicateMarker_diagonal (interpolation normalization diagonal clause : List Bool → List Bool) (payload : List Bool) :

fourFamilyTaggedPredicateMarker interpolation normalization diagonal clause (BinaryEncoding.lengthPrefixedWord [true , false ] ++ payload) = diagonal payload

@[simp]

theorem GapCVP.SourceFourFamilyTaggedPredicateDispatchTM.sourceFourFamilyTaggedPredicateMarker_clause (interpolation normalization diagonal clause : List Bool → List Bool) (payload : List Bool) :

fourFamilyTaggedPredicateMarker interpolation normalization diagonal clause (BinaryEncoding.lengthPrefixedWord [true , true ] ++ payload) = clause payload

def GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.annotatedSquareResolvedOrderingWord (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.flatAnnotatedSquareResolvedOrderingComputable :

BitTM annotatedSquareResolvedOrderingWord

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

theorem GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.flatAnnotatedSquareResolvedOrderingWord_valid (major : CNFEncodedClauseSort.EncodedWordOrdering) (first second : ℕ) (archive suffix : List Bool) :

annotatedSquareResolvedOrderingWord (BinaryEncoding.lengthPrefixedWord (CNFEncodedClauseSort.encodedWordOrderingWord major) ++ BinaryEncoding.lengthPrefixedWord (CNFAnnotatedSourceClausePairZipTM.flatAnnotatedSourceZipArchivedPair (first, second) ++ archive) ++ suffix) = CNFEncodedClauseSort.encodedWordOrderingWord (CNFFlatSourceOrder.resolveFlatSourceOrder major first second)

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.flatAnnotatedSquareResolutionState (major : CNFEncodedClauseSort.EncodedWordOrdering) (archive suffix : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

def GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.flatAnnotatedSquareResolutionStep (input : List Bool) :

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

noncomputable def GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.flatAnnotatedSquareResolutionFoldComputable :

BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput flatAnnotatedSquareResolutionStep)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

theorem GapCVP.CNFAnnotatedSourceSquareMajorResolutionTM.boundedRecordFoldOutput_flatAnnotatedSquareResolution (major : CNFEncodedClauseSort.EncodedWordOrdering) (pairs : List (ℕ × ℕ)) (archive suffix : List Bool) :

OutputBoundedDependentRecordFold.boundedRecordFoldOutput flatAnnotatedSquareResolutionStep (OutputBoundedDependentRecordFold.unaryBoundedFoldWord pairs.length (flatAnnotatedSquareResolutionState major (List.flatMap CNFAnnotatedSourceClausePairZipTM.flatAnnotatedSourceZipArchivedPair pairs ++ archive) suffix)) = flatAnnotatedSquareResolutionState (List.foldl (fun (current : CNFEncodedClauseSort.EncodedWordOrdering) (pair : ℕ × ℕ) => CNFFlatSourceOrder.resolveFlatSourceOrder current pair.1 pair.2) major pairs) archive suffix

Internal support shared across GapCVP continuation modules.