GapCVP proof, part 04, continuation 02

noncomputable def GapCVP.CNFNaturalOrderCertifiedComparator.sourcePreservingDelimitedNaturalComparisonComputable : BitTM CNFNaturalOrderComparator.sourcePreservingDelimitedNaturalComparisonWord

GapCVP reduction support.

Equations

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

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.

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.

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✝

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.

@[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)

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

Internal support shared across GapCVP continuation modules.

Equations

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

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.

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.

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.

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.

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, ⋯⟩

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.

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.

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.

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.

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.

@[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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.