GapCVP proof, part 05, continuation 06

noncomputable def GapCVP.CNFCappedUnaryMinimumTotalCert.actualCappedUnaryMinimumComputable : BitTM CNFCappedUnaryMinimumTM.cappedUnaryMinimumOutput

GapCVP reduction support.

Equations

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

def GapCVP.CNFCappedUnaryPairArithmeticTM.unaryPrefixSuffixOutput (input : List Bool) : List Bool

Discard the first unary field and return its remaining suffix.

Equations

• GapCVP.CNFCappedUnaryPairArithmeticTM.unaryPrefixSuffixOutput input = match GapCVP.BinaryEncoding.readUnaryPrefix input with | none => [] | some (fst, suffix) => suffix

@[simp]

theorem GapCVP.CNFCappedUnaryPairArithmeticTM.unaryPrefixSuffixOutput_valid (count : ℕ) (suffix : List Bool) : unaryPrefixSuffixOutput (List.replicate count true ++ false :: suffix) = suffix

noncomputable def GapCVP.CNFCappedUnaryPairArithmeticTM.actualUnaryPrefixSuffixComputable : BitTM unaryPrefixSuffixOutput

GapCVP reduction support.

Equations

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

def GapCVP.CNFCappedUnaryPairArithmeticTM.cappedUnarySourcePairRecurrenceWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFCappedUnaryPairArithmeticTM.cappedUnarySourcePairRecurrenceWord_valid (cap head tail : ℕ) (suffix : List Bool) : cappedUnarySourcePairRecurrenceWord (List.replicate cap true ++ false :: (CNFUnaryPairIndexTM.unarySourcePairWord head tail ++ suffix)) = List.replicate (min cap (Nat.pair head tail).succ) true

def GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFields (count : ℕ) (input : List Bool) : List Bool

Discard the specified number of leading unary fields.

Equations

• GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFields count input = GapCVP.CNFCappedUnaryPairArithmeticTM.unaryPrefixSuffixOutput^[count] input

noncomputable def GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFieldsComputable (count : ℕ) : BitTM (flatUnaryDropFields count)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFieldsComputable 0 = id (id (GapCVP.SourceMachineCert.prependWordComputable []))

def GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryValueWord (input : List Bool) : List Bool

Read the minimum of the first two unary values as a unary word.

Equations

• GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryValueWord input = GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimumOutput input

noncomputable def GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryValueComputable : BitTM flatDuplicatedUnaryValueWord

GapCVP reduction support.

Equations

• GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryValueComputable = GapCVP.CNFCappedUnaryMinimumTotalCert.actualCappedUnaryMinimumComputable

def GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryFieldWord (input : List Bool) : List Bool

Terminate the minimum-value unary word with a false bit.

Equations

• GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryFieldWord input = GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryValueWord input ++ [false]

def GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryFieldAt (offset : ℕ) (input : List Bool) : List Bool

Read a duplicated unary field after skipping the given number of fields.

Equations

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

def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListQuery (input : List Bool) : List Bool

Concatenate duplicated unary fields selected at offsets zero, two, and four.

Equations

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

def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListNextField (input : List Bool) : List Bool

Compute the next capped source-list field from its three-field query.

Equations

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

def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnaryPendingPair (input : List Bool) : List Bool

Read the pending source pair after the first six unary fields.

Equations

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

def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnaryPendingRemainder (input : List Bool) : List Bool

Return the suffix after the six header fields and pending pair.

Equations

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

def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListStep (input : List Bool) : List Bool

Advance the flat capped unary source-list encoding by one step.

Equations

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

noncomputable def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListStepComputable : BitTM flatCappedUnarySourceListStep

GapCVP reduction support.

Equations

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

def GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryField (value : ℕ) : List Bool

Encode a unary value twice as an adjacent pair.

Equations

• GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryField value = GapCVP.CNFUnaryPairIndexTM.unarySourcePairWord value value

def GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnarySourceStream (records : List ℕ) : List Bool

Concatenate duplicated unary encodings of the source records.

Equations

• GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnarySourceStream records = List.flatMap GapCVP.CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryField records

def GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListState (cap accumulator : ℕ) : List ℕ → List Bool

Encode the cap, current accumulator, and remaining source records.

Equations

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

@[simp]

theorem GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFields_two_unaryPair (first second : ℕ) (suffix : List Bool) : flatUnaryDropFields 2 (CNFUnaryPairIndexTM.unarySourcePairWord first second ++ suffix) = suffix

theorem GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFields_four_unaryPairs (first second third fourth : ℕ) (suffix : List Bool) : flatUnaryDropFields 4 (CNFUnaryPairIndexTM.unarySourcePairWord first second ++ CNFUnaryPairIndexTM.unarySourcePairWord third fourth ++ suffix) = suffix

theorem GapCVP.CNFCappedFlatSourceListFoldTM.flatUnaryDropFields_six_unaryPairs (first second third fourth fifth sixth : ℕ) (suffix : List Bool) : flatUnaryDropFields 6 (CNFUnaryPairIndexTM.unarySourcePairWord first second ++ CNFUnaryPairIndexTM.unarySourcePairWord third fourth ++ CNFUnaryPairIndexTM.unarySourcePairWord fifth sixth ++ suffix) = suffix

@[simp]

theorem GapCVP.CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListStep_state (cap head accumulator : ℕ) (remaining : List ℕ) : flatCappedUnarySourceListStep (flatCappedUnarySourceListState cap accumulator (head :: remaining)) = flatCappedUnarySourceListState cap (min cap (Nat.pair head accumulator).succ) remaining