LeanPool.GapCVP.Part04B

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalLiftStep {first next : CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.Cfg} (hphase : first.l ≠ some 6) (hstep : CNFEncodedClauseSort.delimitedPairComparisonMachine.step first = some next) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step first (some next) 1

Transfer a pair-comparator step outside phase six to the natural-number comparator.

Equations

GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalLiftStep hphase hstep = GapCVP.TraceGolf.oneStep first next ⋯

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalFinishTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 7 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (Turing.haltList CNFNaturalOrderComparator.delimitedNaturalComparisonMachine (CNFEncodedClauseSort.delimitedCompareRestoredWord outcome input source sourcePrefix output))) (firstCounter.length + firstReversed.length + secondCounter.length + secondReversed.length + firstForward.length + secondForward.length + 3 * input.length + source.length + sourcePrefix.length + 5)

Restore the source and finish the natural comparison with the supplied ordering result.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalFirstPrefixTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (count : ℕ) (tail firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 0 outcome (List.replicate count true ++ false :: tail) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 1 outcome tail (List.replicate count true ++ firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (false :: (List.replicate count true ++ source)) (List.replicate (count + 1) true ++ sourcePrefix) output)) (count + 1)

Read the first unary length prefix into the counter and save the consumed source bits.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalFirstMissingPrefixTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (count : ℕ) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 0 outcome (List.replicate count true) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 7 CNFEncodedClauseSort.EncodedWordOrdering.invalid [] (List.replicate count true ++ firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (List.replicate count true ++ source) (List.replicate count true ++ sourcePrefix) output)) (count + 1)

Enter the invalid-result phase when the first length prefix lacks its delimiter.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalFirstPartialPayloadTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (payload remainingCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 1 outcome payload (List.replicate payload.length true ++ remainingCounter) firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 1 outcome [] remainingCounter (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) payload.length

Copy the available first payload while keeping its remaining length counter.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalSecondPrefixTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (count : ℕ) (tail firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 2 outcome (List.replicate count true ++ false :: tail) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 3 outcome tail firstCounter firstReversed (List.replicate count true ++ secondCounter) secondReversed firstForward secondForward (false :: (List.replicate count true ++ source)) (List.replicate (count + 1) true ++ sourcePrefix) output)) (count + 1)

Read the second unary length prefix into its counter and preserve the source.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalSecondMissingPrefixTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (count : ℕ) (firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 2 outcome (List.replicate count true) firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 7 CNFEncodedClauseSort.EncodedWordOrdering.invalid [] firstCounter firstReversed (List.replicate count true ++ secondCounter) secondReversed firstForward secondForward (List.replicate count true ++ source) (List.replicate count true ++ sourcePrefix) output)) (count + 1)

Enter the invalid-result phase when the second length prefix lacks its delimiter.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalSecondPartialPayloadTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (payload remainingCounter firstCounter firstReversed secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 3 outcome payload firstCounter firstReversed (List.replicate payload.length true ++ remainingCounter) secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 3 outcome [] firstCounter firstReversed remainingCounter (payload.reverse ++ secondReversed) firstForward secondForward (payload.reverse ++ source) (List.replicate payload.length true ++ sourcePrefix) output)) payload.length

Copy the available second payload while keeping its remaining length counter.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalFirstRecordTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (payload tail firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) :

StateTransition.EvalsToInTime CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step (CNFNaturalOrderComparator.naturalCompareConfiguration 0 outcome (BinaryEncoding.lengthPrefixedWord payload ++ tail) [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) (some (CNFNaturalOrderComparator.naturalCompareConfiguration 2 outcome tail [] (payload.reverse ++ firstReversed) secondCounter secondReversed firstForward secondForward ((BinaryEncoding.lengthPrefixedWord payload).reverse ++ source) (List.replicate (BinaryEncoding.lengthPrefixedWord payload).length true ++ sourcePrefix) output)) (2 * payload.length + 2)

Read a complete first length-prefixed record and advance to the second record.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalValidTrace (first second suffix : List Bool) :

Compare two valid encoded natural numbers within a linear time bound, preserving the source.

Equations

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

Instances For

source

Finish with an invalid result when the first record has an undelimited length prefix.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalTruncatedFirstTrace (count : ℕ) (payload : List Bool) (hshort : payload.length < count) :

Finish with an invalid result when the first payload is shorter than declared.

Equations

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

Instances For

source

Finish with an invalid result when the second record has an undelimited length prefix.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNaturalTruncatedSecondTrace (first : List Bool) (count : ℕ) (payload : List Bool) (hshort : payload.length < count) :

Finish with an invalid result when the second payload is shorter than declared.

Equations

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

Instances For

source

A linear-time natural-comparison execution for every input, including malformed records.

Equations

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

Instances For

source

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.sourcePreservingDelimitedNaturalComparisonComputable :

BitTM CNFNaturalOrderComparator.sourcePreservingDelimitedNaturalComparisonWord

GapCVP reduction support.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.sourcePreservingPolynomialMarkerWord (polynomial : Polynomial ℕ) (input : List Bool) :

List Bool

GapCVP reduction support.

Equations

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

Instances For

source

theorem GapCVP.CNFPolynomialRowMarkerTM.firstFieldSuffix_sourcePreservingPolynomialMarkerWord (polynomial : Polynomial ℕ) (input : List Bool) :

SourceFormulaStructuralDecoder.firstFieldSuffix (sourcePreservingPolynomialMarkerWord polynomial input) = BinaryEncoding.lengthPrefixedWord (List.replicate (Polynomial.eval input.length polynomial) true)

Internal support shared across GapCVP continuation modules.

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerHorner (polynomial : Polynomial ℕ) (value : ℕ) :

ℕ → ℕ → ℕ

Internal support shared across GapCVP continuation modules.

Equations

One or more equations did not get rendered due to their size.
GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerHorner polynomial value 0 x✝ = x✝

Instances For

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerHorner_eval (polynomial : Polynomial ℕ) (value : ℕ) :

polynomialRowMarkerHorner polynomial value (polynomial.natDegree + 1) 0 = Polynomial.eval value polynomial

Internal support shared across GapCVP continuation modules.

source

@[reducible, inline]

abbrev GapCVP.CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage (polynomial : Polynomial ℕ) :

Type

Internal support shared across GapCVP continuation modules.

Equations

GapCVP.CNFPolynomialRowMarkerTM.PolynomialRowMarkerStage polynomial = Fin (polynomial.natDegree + 1)

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerTopStage (polynomial : Polynomial ℕ) :

PolynomialRowMarkerStage polynomial

Internal support shared across GapCVP continuation modules.

Equations

GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerTopStage polynomial = ⟨polynomial.natDegree, ⋯⟩

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPeek (polynomial : Polynomial ℕ) (stack : Fin 7) (present absent : Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Read a row-marker stack head into the state and branch on whether it is present.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPop (polynomial : Polynomial ℕ) (stack : Fin 7) (continuation : Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Pop a row-marker stack while preserving the bit stored in the machine state.

Equations

GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPop polynomial stack continuation = Turing.TM2.Stmt.pop stack (fun (bit x : Option Bool) => bit) continuation

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPushBit (polynomial : Polynomial ℕ) (stack : Fin 7) (continuation : Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Push the stored row-marker bit, defaulting to false when the state is empty.

Equations

GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPushBit polynomial stack continuation = Turing.TM2.Stmt.push stack (fun (bit : Option Bool) => bit.getD false) continuation

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPushConstant (polynomial : Polynomial ℕ) (stack : Fin 7) (bit : Bool) (continuation : Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Push a fixed bit on a row-marker stack before the continuation.

Equations

GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPushConstant polynomial stack bit continuation = Turing.TM2.Stmt.push stack (fun (x : Option Bool) => bit) continuation

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerGoto (polynomial : Polynomial ℕ) (phase : Fin 9) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Clear the stored bit and enter the selected polynomial stage and machine phase.

Equations

GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerGoto polynomial phase stage = Turing.TM2.Stmt.load (fun (x : Option Bool) => none) (Turing.TM2.Stmt.goto fun (x : Option Bool) => (phase, stage))

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPushBits (polynomial : Polynomial ℕ) (stack : Fin 7) :

List Bool → Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool) → Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Push a sequence of constant bits, in list order, before executing the continuation.

Equations

One or more equations did not get rendered due to their size.
GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPushBits polynomial stack [] x✝ = x✝

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerScanStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerMultiplyStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerBaseStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerRestoreBaseStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPredStage (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (_hstage : ↑stage ≠ 0) :

PolynomialRowMarkerStage polynomial

Internal support shared across GapCVP continuation modules.

Equations

GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPredStage polynomial stage _hstage = ⟨↑stage - 1, ⋯⟩

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerCoefficientStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPayloadStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerHeaderStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerSourceStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerPrefixStatement (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) :

Turing.TM2.Stmt (fun (x : Fin 7) => Bool) (Fin 9 × PolynomialRowMarkerStage polynomial) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

@[reducible, inline]

abbrev GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine (polynomial : Polynomial ℕ) :

Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

def GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerConfiguration (polynomial : Polynomial ℕ) (phase : Fin 9) (stage : PolynomialRowMarkerStage polynomial) (input source base baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

Instances For

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarkerMachine_init (polynomial : Polynomial ℕ) (input : List Bool) :

Turing.initList (polynomialRowMarkerMachine polynomial) input = polynomialRowMarkerConfiguration polynomial 0 (polynomialRowMarkerTopStage polynomial) input [] [] [] [] [] []

Internal support shared across GapCVP continuation modules.

source

def GapCVP.CNFPolynomialRowMarkerTM.tacticPolynomialRowMarkerStepTac :

Lean.ParserDescr

Executes the polynomialRowMarkerStepTac machine-step simplifier.

Equations

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

Instances For

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_scan_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (bit : Bool) (input source base baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 0 stage (bit :: input) source base baseScratch accumulator product output) = some (polynomialRowMarkerConfiguration polynomial 0 stage input (bit :: source) (true :: base) baseScratch accumulator product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_scan_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 0 stage [] source base baseScratch accumulator product output) = some (polynomialRowMarkerConfiguration polynomial 1 stage [] source base baseScratch accumulator product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_multiply_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 1 stage [] source base baseScratch (true :: accumulator) product output) = some (polynomialRowMarkerConfiguration polynomial 2 stage [] source base baseScratch accumulator product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_multiply_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base baseScratch product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 1 stage [] source base baseScratch [] product output) = some (polynomialRowMarkerConfiguration polynomial 4 stage [] source base baseScratch [] product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_base_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 2 stage [] source (true :: base) baseScratch accumulator product output) = some (polynomialRowMarkerConfiguration polynomial 2 stage [] source base (true :: baseScratch) accumulator (true :: product) output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_base_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 2 stage [] source [] baseScratch accumulator product output) = some (polynomialRowMarkerConfiguration polynomial 3 stage [] source [] baseScratch accumulator product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_restoreBase_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base baseScratch accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 3 stage [] source base (true :: baseScratch) accumulator product output) = some (polynomialRowMarkerConfiguration polynomial 3 stage [] source (true :: base) baseScratch accumulator product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_restoreBase_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 3 stage [] source base [] accumulator product output) = some (polynomialRowMarkerConfiguration polynomial 1 stage [] source base [] accumulator product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_product_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] accumulator (true :: product) output) = some (polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] (true :: accumulator) product output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_coefficient_zero_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (hstage : ↑stage = 0) (source base accumulator output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] accumulator [] output) = some (polynomialRowMarkerConfiguration polynomial 5 stage [] source base [] (List.replicate (polynomial.coeff ↑stage) true ++ accumulator) [] output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_coefficient_succ_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (hstage : ↑stage ≠ 0) (source base accumulator output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] accumulator [] output) = some (polynomialRowMarkerConfiguration polynomial 1 (polynomialRowMarkerPredStage polynomial stage hstage) [] source base [] (List.replicate (polynomial.coeff ↑stage) true ++ accumulator) [] output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_payload_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base accumulator product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 5 stage [] source base [] (true :: accumulator) product output) = some (polynomialRowMarkerConfiguration polynomial 5 stage [] source base [] accumulator (true :: product) (true :: output))

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_payload_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 5 stage [] source base [] [] product output) = some (polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] product (false :: output))

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_header_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base product output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] (true :: product) output) = some (polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] product (true :: output))

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_header_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (source base output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] [] output) = some (polynomialRowMarkerConfiguration polynomial 7 stage [] source base [] [] [] output)

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_source_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (bit : Bool) (source base output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 7 stage [] (bit :: source) base [] [] [] output) = some (polynomialRowMarkerConfiguration polynomial 7 stage [] source base [] [] [] (bit :: output))

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_source_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (base output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 7 stage [] [] base [] [] [] output) = some (polynomialRowMarkerConfiguration polynomial 8 stage [] [] base [] [] [] (false :: output))

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_prefix_step (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (base output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 8 stage [] [] (true :: base) [] [] [] output) = some (polynomialRowMarkerConfiguration polynomial 8 stage [] [] base [] [] [] (true :: output))

Internal support shared across GapCVP continuation modules.

source

theorem GapCVP.CNFPolynomialRowMarkerTM.polynomialRowMarker_finish (polynomial : Polynomial ℕ) (stage : PolynomialRowMarkerStage polynomial) (output : List Bool) :

(polynomialRowMarkerMachine polynomial).step (polynomialRowMarkerConfiguration polynomial 8 stage [] [] [] [] [] [] output) = some (Turing.haltList (polynomialRowMarkerMachine polynomial) output)

Internal support shared across GapCVP continuation modules.

Documentation

LeanPool.GapCVP.Part04B

GapCVP proof, part 04, continuation 02 #