GapCVP proof, part 03

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.PaddedAcceptancePhaseAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

Decide whether a complete phase window satisfies stack, head, and acceptance coherence.

Equations

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

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptancePhaseAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

Compute the padded acceptance condition for a complete phase window.

Equations

• GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptancePhaseAllowed machine window = decide (GapCVP.CLPaddedAcceptanceCompiler.PaddedAcceptancePhaseAllowed machine window = true)

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSymbolAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSpecification (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : CL.Specification (Polynomial.eval x.length (CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine)) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)

GapCVP reduction support.

Equations

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

theorem GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptanceValidTraceFirstAcceptanceTrueHalt (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (trace : CLWholeTraceSoundness.AnchoredPhaseTrace bound machine x) (htrace : CL.ValidTrace (paddedAcceptancePhaseSpecification bound machine x) trace = true) : ∃ (time : Fin (CLCellRowBounds.rowWidth bound machine x)) (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)) (certificate : List Bool), have first := CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace time.castSucc); have next := CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace time.succ); CLPhaseTableauSimulation.AnchoredAcceptanceAllowed machine (CLPhaseGlobalSimulation.anchoredVerifierWindowAt machine.tm (CLCellRowBounds.rowWidth bound machine x) first next position) = true ∧ (∀ (other : CL.Position (CLCellRowBounds.rowWidth bound machine x)), (first other).mode = CLBoundedStates.PhaseTag.verifying) ∧ (∀ (other : CL.Position (CLCellRowBounds.rowWidth bound machine x)), CLWholeTraceSoundness.AnchoredPhaseMasks bound machine x other (first other) = true) ∧ (∀ (stack : machine.tm.K), CLCompactWindowSoundness.NoInteriorPaddingHoles machine.tm (CLBoundedRowInduction.fullPackedPhaseStackAtoms machine (CLCellRowBounds.rowWidth bound machine x) first stack) = true) ∧ certificate.length ≤ Polynomial.eval x.length bound ∧ CLAcceptanceAnchor.TrueOutputMachineHead machine (first 0) = true ∧ verifier (x, certificate) = true ∧ CLFullStackStepSoundness.decodedFullPackedPhaseConfiguration machine (CLCellRowBounds.rowWidth bound machine x) first = Turing.haltList machine.tm (CLVerifier.verifierOutput machine true) ∧ Nonempty (CLNondeterminism.FiniteRun (CLNondeterminism.GuessStep bound machine x) (CLNondeterminism.GuessState.guessing []) (CLNondeterminism.GuessState.verifying certificate (Turing.haltList machine.tm (CLVerifier.verifierOutput machine true))) ↑time) ∧ ↑time ≤ Polynomial.eval x.length (CLNondeterminism.guessTimePolynomial bound machine) ∧ ∀ (earlier : CL.Time (CLCellRowBounds.rowWidth bound machine x)), ↑earlier ≤ ↑time → ∀ (other : CL.Position (CLCellRowBounds.rowWidth bound machine x)), (CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace earlier) other).mode ≠ CLBoundedStates.PhaseTag.accepting

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptanceValidTraceGuessingExecution (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (trace : CLWholeTraceSoundness.AnchoredPhaseTrace bound machine x) (htrace : CL.ValidTrace (paddedAcceptancePhaseSpecification bound machine x) trace = true) : CLNondeterminism.GuessingExecution bound machine x

Extract an accepting guessing execution from a valid padded tableau trace.

Equations

• GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptanceValidTraceGuessingExecution bound machine x trace htrace = Classical.choice ⋯

noncomputable def GapCVP.CLPaddedAcceptanceCompiler.paddedAcceptanceLocalTableauCompiler (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : CLNondeterminism.LocalTableauCompiler bound machine

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CLStructuralCNFVariableBounds.tableauFiniteVariableCodeBound (T S : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CLStructuralCNFVariableBounds.tableauFiniteVariableCodeBound T S = ((T + S + 2) ^ 2 + 1) ^ 2

theorem GapCVP.CLStructuralCNFVariableBounds.tableauVariable_encode_lt {T S : ℕ} (v : CL.Variable T S) : Encodable.encode v < tableauFiniteVariableCodeBound T S

theorem GapCVP.CLStructuralCNFVariableBounds.sourceVariable_lt_tableauFiniteBound {T S : ℕ} (v : CL.Variable T S) : ThreeCNFReduction.sourceVariable v < 4 * tableauFiniteVariableCodeBound T S

def GapCVP.CLStructuralPrefixWriter.prefixWriterPeek (stack : Fin 4) (present absent : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Branch according to whether the selected stack has a top symbol.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterPop (stack : Fin 4) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Remove the top symbol of a stack, then continue.

Equations

• GapCVP.CLStructuralPrefixWriter.prefixWriterPop stack continuation = Turing.TM2.Stmt.pop stack (fun (symbol x : Option Bool) => symbol) continuation

def GapCVP.CLStructuralPrefixWriter.prefixWriterPushBit (stack : Fin 4) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Push the current bit onto a stack, defaulting to false when no bit is loaded.

Equations

• GapCVP.CLStructuralPrefixWriter.prefixWriterPushBit stack continuation = Turing.TM2.Stmt.push stack (fun (symbol : Option Bool) => symbol.getD false) continuation

def GapCVP.CLStructuralPrefixWriter.prefixWriterPushMarker (stack : Fin 4) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Push a true delimiter marker onto a stack.

Equations

• GapCVP.CLStructuralPrefixWriter.prefixWriterPushMarker stack continuation = Turing.TM2.Stmt.push stack (fun (x : Option Bool) => true) continuation

def GapCVP.CLStructuralPrefixWriter.prefixWriterGoto (phase : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Clear the current symbol and enter the specified phase.

Equations

• GapCVP.CLStructuralPrefixWriter.prefixWriterGoto phase = Turing.TM2.Stmt.load (fun (x : Option Bool) => none) (Turing.TM2.Stmt.goto fun (x : Option Bool) => phase)

def GapCVP.CLStructuralPrefixWriter.prefixWriterScanStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Move input bits to scratch while counting them with markers.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Restore the saved input bits to output and append a false separator.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterMarkerStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 3) (Option Bool)

Transfer one true marker per input bit to output, then halt.

Equations

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

@[reducible, inline]

abbrev GapCVP.CLStructuralPrefixWriter.structuralPrefixWriter : Turing.FinTM2

Four-stack machine that writes the length prefix before the input word.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterConfiguration (phase : Fin 3) (input scratch markers output : List Bool) : structuralPrefixWriter.Cfg

Configuration of the prefix writer in a chosen phase with four stack contents.

Equations

• GapCVP.CLStructuralPrefixWriter.prefixWriterConfiguration phase input scratch markers output = { l := some phase, var := none, stk := ![input, scratch, markers, output] }

def GapCVP.CLStructuralPrefixWriter.tacticPrefixWriterStepTac : Lean.ParserDescr

Executes the prefixWriterStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CLStructuralPrefixWriter.prefixWriterScanStep (bit : Bool) (input scratch markers output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 0 (bit :: input) scratch markers output) = some (prefixWriterConfiguration 0 input (bit :: scratch) (true :: markers) output)

theorem GapCVP.CLStructuralPrefixWriter.prefixWriterScanFinish (scratch markers output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 0 [] scratch markers output) = some (prefixWriterConfiguration 1 [] scratch markers output)

theorem GapCVP.CLStructuralPrefixWriter.prefixWriterRestoreStep (bit : Bool) (scratch markers output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 1 [] (bit :: scratch) markers output) = some (prefixWriterConfiguration 1 [] scratch markers (bit :: output))

theorem GapCVP.CLStructuralPrefixWriter.prefixWriterRestoreFinish (markers output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 1 [] [] markers output) = some (prefixWriterConfiguration 2 [] [] markers (false :: output))

theorem GapCVP.CLStructuralPrefixWriter.prefixWriterMarkerStep (bit : Bool) (markers output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 2 [] [] (bit :: markers) output) = some (prefixWriterConfiguration 2 [] [] markers (true :: output))

theorem GapCVP.CLStructuralPrefixWriter.prefixWriterFinish (output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 2 [] [] [] output) = some (Turing.haltList structuralPrefixWriter output)

def GapCVP.CLStructuralPrefixWriter.prefixWriterScanTrace (input scratch markers output : List Bool) : StateTransition.EvalsToInTime structuralPrefixWriter.step (prefixWriterConfiguration 0 input scratch markers output) (some (prefixWriterConfiguration 1 [] (input.reverse ++ scratch) (List.replicate input.length true ++ markers) output)) (input.length + 1)

The scan phase reverses the input onto scratch and records its length in markers.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterRestoreTrace (scratch markers output : List Bool) : StateTransition.EvalsToInTime structuralPrefixWriter.step (prefixWriterConfiguration 1 [] scratch markers output) (some (prefixWriterConfiguration 2 [] [] markers (false :: (scratch.reverse ++ output)))) (scratch.length + 1)

The restore phase copies scratch back to output after a false separator.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterMarkerTrace (markers output : List Bool) : StateTransition.EvalsToInTime structuralPrefixWriter.step (prefixWriterConfiguration 2 [] [] markers output) (some (Turing.haltList structuralPrefixWriter (List.replicate markers.length true ++ output))) (markers.length + 1)

The marker phase writes the unary length prefix and halts.

Equations

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

def GapCVP.CLStructuralPrefixWriter.prefixWriterTotalTrace (input : List Bool) : StateTransition.EvalsToInTime structuralPrefixWriter.step (prefixWriterConfiguration 0 input [] [] []) (some (Turing.haltList structuralPrefixWriter (BinaryEncoding.lengthPrefixedWord input))) (3 * input.length + 3)

The three phases write the complete length-prefixed word within linear time.

Equations

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

noncomputable def GapCVP.CLStructuralPrefixWriter.structuralPrefixWriterComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding fun (input : List Bool) => BinaryEncoding.lengthPrefixedWord input

GapCVP reduction support.

Equations

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

def GapCVP.SourceMachineCert.prependBitMachine (bit : Bool) : Turing.FinTM2

Single-step machine that prepends a fixed bit to its input.

Equations

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

noncomputable def GapCVP.SourceMachineCert.prependBitComputable (bit : Bool) : BitTM fun (input : List Bool) => bit :: input

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMachineCert.prependWordComputable (word : List Bool) : BitTM fun (input : List Bool) => word ++ input

GapCVP reduction support.

Equations

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

def GapCVP.SourceMachineCert.formulaVariables (formula : ThreeCNF) : List ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceMachineCert.formulaVariables formula = List.flatMap (fun (clause : GapCVP.ThreeClause) => [(clause 0).1, (clause 1).1, (clause 2).1]) formula

@[simp]

theorem GapCVP.SourceMachineCert.formulaVariables_length (formula : ThreeCNF) : (formulaVariables formula).length = 3 * List.length formula

theorem GapCVP.SourceMachineCert.mem_formulaVariables (formula : ThreeCNF) (clause : ThreeClause) (hclause : clause ∈ formula) (i : Fin 3) : (clause i).1 ∈ formulaVariables formula

def GapCVP.SourceMachineCert.variableRank (formula : ThreeCNF) (index : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceMachineCert.variableRank formula index = List.idxOf index (GapCVP.SourceMachineCert.formulaVariables formula)

def GapCVP.SourceMachineRouting.canonicalYesInstance : GapCVPInstance

GapCVP reduction support.

Equations

• GapCVP.SourceMachineRouting.canonicalYesInstance = { dimension := 1, basis := Matrix.of fun (x x_1 : Fin 1) => 1, target := fun (x : Fin 1) => 0, radius := 1 }

theorem GapCVP.SourceMachineRouting.canonicalYesInstance_wellFormed : gapCVPWellFormed canonicalYesInstance = true

theorem GapCVP.SourceMachineRouting.canonicalYesInstance_gapYES : gapYES canonicalYesInstance = true

def GapCVP.SourceMachineRouting.canonicalYesWord : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMachineRouting.canonicalYesWord = GapCVP.BinaryEncoding.encodeGapCVPInstance GapCVP.SourceMachineRouting.canonicalYesInstance

@[reducible, inline]

abbrev GapCVP.SourceUniformTuringTM.eraseMachine : Turing.FinTM2

Machine that pops every input bit and returns an empty word.

Equations

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

noncomputable def GapCVP.SourceUniformTuringTM.eraseComputable : BitTM fun (x : List Bool) => []

Polynomial-time realization of the constant empty-word function.

Equations

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

noncomputable def GapCVP.SourceUniformTuringTM.constantWordComputable (word : List Bool) : BitTM fun (x : List Bool) => word

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceStructuralTuringTM.unaryPrefixMachine : Turing.FinTM2

Two-stack machine that reads a unary prefix and writes its decoded payload.

Equations

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

def GapCVP.SourceStructuralTuringTM.unaryPrefixLength : List Bool → ℕ

GapCVP reduction support.

Equations

• GapCVP.SourceStructuralTuringTM.unaryPrefixLength [] = 0
• GapCVP.SourceStructuralTuringTM.unaryPrefixLength (false :: tail) = 0
• GapCVP.SourceStructuralTuringTM.unaryPrefixLength (true :: rest) = GapCVP.SourceStructuralTuringTM.unaryPrefixLength rest + 1

def GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter : List Bool → Bool

GapCVP reduction support.

Equations

• GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter [] = false
• GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter (false :: tail) = true
• GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter (true :: rest) = GapCVP.SourceStructuralTuringTM.unaryPrefixHasDelimiter rest

def GapCVP.SourceStructuralTuringTM.unaryPrefixOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceStructuralTuringTM.unaryPrefixComputable : BitTM unaryPrefixOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceStructuralTuringTM.unaryPrefixOutput_replicate_delimiter (count : ℕ) (suffix : List Bool) : unaryPrefixOutput (List.replicate count true ++ false :: suffix) = true :: List.replicate count true

@[reducible, inline]

abbrev GapCVP.SourceStructuralDecoder.payloadDecoderMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadConfiguration (phase : Fin 5) (input counter reversed output : List Bool) : payloadDecoderMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceStructuralDecoder.payloadConfiguration phase input counter reversed output = { l := some phase, var := none, stk := ![input, counter, reversed, output] }

theorem GapCVP.SourceStructuralDecoder.payload_prefix_true (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 0 (true :: input) counter reversed output) = some (payloadConfiguration 0 input (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payloadPrefixDelimiter (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 0 (false :: input) counter reversed output) = some (payloadConfiguration 1 input counter reversed output)

theorem GapCVP.SourceStructuralDecoder.payload_prefix_missing_delimiter (counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 0 [] counter reversed output) = some (payloadConfiguration 4 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_copy_step (bit : Bool) (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 1 (bit :: input) (true :: counter) reversed output) = some (payloadConfiguration 1 input counter (bit :: reversed) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_insufficient (counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 1 [] (true :: counter) reversed output) = some (payloadConfiguration 4 [] (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_counter_complete (input reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 1 input [] reversed output) = some (payloadConfiguration 2 input [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payloadReverseStep (bit : Bool) (input reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 2 input [] (bit :: reversed) output) = some (payloadConfiguration 2 input [] reversed (bit :: output))

theorem GapCVP.SourceStructuralDecoder.payload_reverse_complete (input output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 2 input [] [] output) = some (payloadConfiguration 3 input [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payloadDrainStep (bit : Bool) (input output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 3 (bit :: input) [] [] output) = some (payloadConfiguration 3 input [] [] output)

theorem GapCVP.SourceStructuralDecoder.payloadDrainFinish (output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 3 [] [] [] output) = some (Turing.haltList payloadDecoderMachine (true :: output))

theorem GapCVP.SourceStructuralDecoder.payload_failure_drop_input (bit : Bool) (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 (bit :: input) counter reversed output) = some (payloadConfiguration 4 input counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_drop_counter (bit : Bool) (counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 [] (bit :: counter) reversed output) = some (payloadConfiguration 4 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_drop_reversed (bit : Bool) (reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 [] [] (bit :: reversed) output) = some (payloadConfiguration 4 [] [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceStructuralDecoder.payload_failure_finish (output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 4 [] [] [] output) = some (Turing.haltList payloadDecoderMachine (false :: output))

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.SourceStructuralDecoder.replicate_true_append_cons (count : ℕ) (tail : List Bool) : List.replicate count true ++ true :: tail = true :: (List.replicate count true ++ tail)

def GapCVP.SourceStructuralDecoder.payloadPrefixTrace (count : ℕ) (tail counter reversed output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 0 (List.replicate count true ++ false :: tail) counter reversed output) (some (payloadConfiguration 1 tail (List.replicate count true ++ counter) reversed output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadCopyTrace (payload suffix reversed output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 1 (payload ++ suffix) (List.replicate payload.length true) reversed output) (some (payloadConfiguration 1 suffix [] (payload.reverse ++ reversed) output)) payload.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadReverseTrace (input reversed output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 2 input [] reversed output) (some (payloadConfiguration 2 input [] [] (reversed.reverse ++ output))) reversed.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceStructuralDecoder.payloadDrainTrace (suffix output : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 3 suffix [] [] output) (some (Turing.haltList payloadDecoderMachine (true :: output))) (suffix.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.SourceStructuralDecoder.payloadDecoderMachine_init (input : List Bool) : Turing.initList payloadDecoderMachine input = payloadConfiguration 0 input [] [] []

Internal support shared across GapCVP continuation modules.