GapCVP proof, part 04, continuation 05

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldValidScanTrace {worker : List Bool → List Bool} (computer : BitTM worker) (count : ℕ) (seed counter : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer (List.map computer.inputAlphabet.invFun (unaryBoundedFoldWord count seed)) counter) (some (boundedFoldDispatchConfiguration computer (List.map computer.inputAlphabet.invFun seed) (List.replicate count true ++ counter))) (count + 1)

Scans a valid unary fold prefix and reaches dispatch within count + 1 steps.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldDrainTrace {worker : List Bool → List Bool} (computer : BitTM worker) (output : List (computer.tm.Γ computer.tm.k₁)) (counter scratch : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldDrainConfiguration computer output counter scratch) (some (boundedFoldRestoreConfiguration computer [] counter (List.map (⇑computer.outputAlphabet) output.reverse ++ scratch))) (output.length + 1)

Drains the worker output into scratch before restoring it as the next input.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldRestoreTrace {worker : List Bool → List Bool} (computer : BitTM worker) (scratch : List Bool) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldRestoreConfiguration computer input counter scratch) (some (boundedFoldDispatchConfiguration computer (List.map computer.inputAlphabet.invFun scratch.reverse ++ input) counter)) (scratch.length + 1)

Restores saved bits to the input stack and resumes fold dispatch.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldOutputTransportTrace {worker : List Bool → List Bool} (computer : BitTM worker) (output counter : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldDrainConfiguration computer (List.map computer.outputAlphabet.invFun output) counter []) (some (boundedFoldDispatchConfiguration computer (List.map computer.inputAlphabet.invFun output) counter)) (2 * output.length + 2)

Transfers one worker output to the next iteration's input within a linear step bound.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerExecutionTrace {worker : List Bool → List Bool} (computer : BitTM worker) (input counter : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldWorkerConfiguration computer counter (Turing.initList computer.tm (List.map computer.inputAlphabet.invFun input))) (some (boundedFoldDrainConfiguration computer (List.map computer.outputAlphabet.invFun (worker input)) counter [])) (Polynomial.eval input.length computer.time)

Runs the worker machine from its fold configuration within its time bound.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldRunBudget {worker : List Bool → List Bool} (computer : BitTM worker) : ℕ → List Bool → ℕ

Recursive step budget for the remaining fold iterations.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.OutputBoundedDependentRecordFold.boundedFoldRunBudget computer 0 x✝ = 1

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldIterationTrace {worker : List Bool → List Bool} (computer : BitTM worker) (count : ℕ) (seed : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldDispatchConfiguration computer (List.map computer.inputAlphabet.invFun seed) (List.replicate count true)) (some (Turing.haltList (boundedDependentRecordFoldMachine computer) (List.map computer.inputAlphabet.invFun (worker^[count] seed)))) (boundedFoldRunBudget computer count seed)

Executes all remaining fold iterations from the dispatch configuration.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldValidTotalTrace {worker : List Bool → List Bool} (computer : BitTM worker) (count : ℕ) (seed : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (Turing.initList (boundedDependentRecordFoldMachine computer) (List.map computer.inputAlphabet.invFun (unaryBoundedFoldWord count seed))) (some (Turing.haltList (boundedDependentRecordFoldMachine computer) (List.map computer.inputAlphabet.invFun (worker^[count] seed)))) (count + 1 + boundedFoldRunBudget computer count seed)

Runs a valid unary encoded fold input from initialization to its result.

Equations

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

theorem GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold_eq_word (input : List Bool) (count : ℕ) (seed : List Bool) (hparse : parseUnaryBoundedFold input = some (count, seed)) : input = unaryBoundedFoldWord count seed

theorem GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFoldNoneEqReplicate (input : List Bool) (hparse : parseUnaryBoundedFold input = none) : input = List.replicate input.length true

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldMissingScanTrace {worker : List Bool → List Bool} (computer : BitTM worker) (count : ℕ) (counter : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer (List.map computer.inputAlphabet.invFun (List.replicate count true)) counter) (some (boundedFoldMalformedConfiguration computer (List.replicate count true ++ counter))) (count + 1)

Scans a prefix with no delimiter and enters malformed-input handling.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldMalformedTrace {worker : List Bool → List Bool} (computer : BitTM worker) (count : ℕ) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (boundedFoldMalformedConfiguration computer (List.replicate count true)) (some (Turing.haltList (boundedDependentRecordFoldMachine computer) [])) (count + 1)

Clears a malformed unary prefix and halts with empty output.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldMalformedTotalTrace {worker : List Bool → List Bool} (computer : BitTM worker) (count : ℕ) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (Turing.initList (boundedDependentRecordFoldMachine computer) (List.map computer.inputAlphabet.invFun (List.replicate count true))) (some (Turing.haltList (boundedDependentRecordFoldMachine computer) [])) (2 * count + 2)

Runs an input lacking a fold delimiter to empty output from initialization.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldTimePolynomial {worker : List Bool → List Bool} (computer : BitTM worker) (bound : Polynomial ℕ) : Polynomial ℕ

Polynomial time bound for a fold with polynomially bounded intermediate states.

Equations

• GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldTimePolynomial computer bound = Polynomial.X * (computer.time.comp bound + 2 * bound + 3) + 2 * Polynomial.X + 5

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFoldValidTotalBudgetLe {worker : List Bool → List Bool} (computer : BitTM worker) (bound : Polynomial ℕ) (hbounded : PolynomiallyBoundedFoldStates worker bound = true) (input : List Bool) (count : ℕ) (seed : List Bool) (hparse : parseUnaryBoundedFold input = some (count, seed)) : count + 1 + boundedFoldRunBudget computer count seed ≤ Polynomial.eval input.length (boundedDependentRecordFoldTimePolynomial computer bound)

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFoldMalformedTotalBudgetLe {worker : List Bool → List Bool} (computer : BitTM worker) (bound : Polynomial ℕ) (inputLength : ℕ) : 2 * inputLength + 2 ≤ Polynomial.eval inputLength (boundedDependentRecordFoldTimePolynomial computer bound)

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldTotalTrace {worker : List Bool → List Bool} (computer : BitTM worker) (bound : Polynomial ℕ) (hbounded : PolynomiallyBoundedFoldStates worker bound = true) (input : List Bool) : StateTransition.EvalsToInTime (boundedDependentRecordFoldMachine computer).step (Turing.initList (boundedDependentRecordFoldMachine computer) (List.map computer.inputAlphabet.invFun input)) (some (Turing.haltList (boundedDependentRecordFoldMachine computer) (List.map computer.inputAlphabet.invFun (boundedRecordFoldOutput worker input)))) (Polynomial.eval input.length (boundedDependentRecordFoldTimePolynomial computer bound))

Total execution trace of the bounded fold, including malformed inputs.

Equations

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

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldComputable {worker : List Bool → List Bool} (computer : BitTM worker) (bound : Polynomial ℕ) (hbounded : PolynomiallyBoundedFoldStates worker bound = true) : BitTM (boundedRecordFoldOutput worker)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (literal : Literal) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor literal = GapCVP.BinaryEncoding.lengthPrefixedWord (literal.2 :: Computability.encodeNat literal.1)

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep_descriptor (literal : Literal) (suffix : List Bool) : flatLiteralRecordStep (flatSignedLiteralDescriptor literal ++ suffix) = suffix ++ BinaryEncoding.encodeLiteral literal

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptorStream (literals : List Literal) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptorStream literals = List.flatMap GapCVP.CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor literals

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep_polynomiallyBoundedFoldStates : OutputBoundedDependentRecordFold.PolynomiallyBoundedFoldStates flatLiteralRecordStep Polynomial.X = true

Internal support shared across GapCVP continuation modules.

structure GapCVP.CNFFlatStructuralRecordWorkerTM.FlatLiteralRecordState : Type

Internal support shared across GapCVP continuation modules.

• inspected : Option Bool

  The inspected literal bit, when present.

• sign : Option Bool

  The literal sign bit, when present.

@[instance_reducible]

instance GapCVP.CNFFlatStructuralRecordWorkerTM.instFintypeFlatLiteralRecordState : Fintype FlatLiteralRecordState

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPeek (stack : Fin 6) (present absent : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Inspects the top bit of a stack and branches on whether it is present.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPop (stack : Fin 6) (continuation : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Removes the top bit of a stack and continues without changing the state.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPushBit (stack : Fin 6) (continuation : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Pushes the inspected bit, using false when no bit was inspected.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPushConstant (stack : Fin 6) (bit : Bool) (continuation : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Pushes a fixed bit onto a stack before continuing.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordGoto (phase : Fin 8) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Clears the inspected bit and enters the given control phase.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPrefixStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSignStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPayloadStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordMarkerStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSuffixScanStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSuffixRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordInvalidStatement : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 8) FlatLiteralRecordState

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

abbrev GapCVP.CNFFlatStructuralRecordWorkerTM.actualFlatLiteralRecordWorker : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordConfiguration (phase : Fin 8) (sign : Option Bool) (input count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.actualFlatLiteralRecordWorker_init (input : List Bool) : Turing.initList actualFlatLiteralRecordWorker input = flatLiteralRecordConfiguration 0 none input [] [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFFlatStructuralRecordWorkerTM.tacticFlatLiteralRecordStepTac : Lean.ParserDescr

Executes the flatLiteralRecordStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_prefix_true (sign : Option Bool) (input count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign (true :: input) count reversed markers suffix output) = some (flatLiteralRecordConfiguration 0 sign input (true :: count) reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_prefix_false (sign : Option Bool) (input count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign (false :: input) count reversed markers suffix output) = some (flatLiteralRecordConfiguration 1 sign input count reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_prefix_missing (sign : Option Bool) (count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign [] count reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] count reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_sign_step (oldSign : Option Bool) (sign marker : Bool) (input count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 1 oldSign (sign :: input) (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 2 (some sign) input count reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_sign_empty (sign : Option Bool) (input reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 1 sign input [] reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign input [] reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_sign_missing (sign : Option Bool) (marker : Bool) (count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 1 sign [] (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] (marker :: count) reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_payload_step (sign : Option Bool) (bit marker : Bool) (input count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 sign (bit :: input) (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 2 sign input count (bit :: reversed) (true :: markers) suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_payload_finish (sign : Bool) (input reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 (some sign) input [] reversed markers suffix output) = some (flatLiteralRecordConfiguration 3 (some sign) input [] reversed markers suffix (sign :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_payload_missing (sign : Option Bool) (marker : Bool) (count reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 sign [] (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] (marker :: count) reversed markers suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_restore_step (sign : Option Bool) (bit : Bool) (input reversed markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 3 sign input [] (bit :: reversed) markers suffix output) = some (flatLiteralRecordConfiguration 3 sign input [] reversed markers suffix (bit :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_restore_finish (sign : Option Bool) (input markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 3 sign input [] [] markers suffix output) = some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_marker_step (sign : Option Bool) (marker : Bool) (input markers suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 4 sign input [] [] (marker :: markers) suffix output) = some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_marker_finish (sign : Option Bool) (input suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 4 sign input [] [] [] suffix output) = some (flatLiteralRecordConfiguration 5 sign input [] [] [] suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_scan_step (sign : Option Bool) (bit : Bool) (input suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 5 sign (bit :: input) [] [] [] suffix output) = some (flatLiteralRecordConfiguration 5 sign input [] [] [] (bit :: suffix) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_scan_finish (sign : Option Bool) (suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 5 sign [] [] [] [] suffix output) = some (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_restore_step (sign : Option Bool) (bit : Bool) (suffix output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 6 sign [] [] [] [] (bit :: suffix) output) = some (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix (bit :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_suffix_restore_finish (sign : Option Bool) (output : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 6 sign [] [] [] [] [] output) = some (Turing.haltList actualFlatLiteralRecordWorker output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_count (sign : Option Bool) (bit : Bool) (input count reversed markers : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input (bit :: count) reversed markers [] []) = some (flatLiteralRecordConfiguration 7 sign input count reversed markers [] [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_reversed (sign : Option Bool) (bit : Bool) (input reversed markers : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input [] (bit :: reversed) markers [] []) = some (flatLiteralRecordConfiguration 7 sign input [] reversed markers [] [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_markers (sign : Option Bool) (bit : Bool) (input markers : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input [] [] (bit :: markers) [] []) = some (flatLiteralRecordConfiguration 7 sign input [] [] markers [] [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_input (sign : Option Bool) (bit : Bool) (input : List Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign (bit :: input) [] [] [] [] []) = some (flatLiteralRecordConfiguration 7 sign input [] [] [] [] [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecord_invalid_finish (sign : Option Bool) : actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign [] [] [] [] [] []) = some (Turing.haltList actualFlatLiteralRecordWorker [])

Internal support shared across GapCVP continuation modules.