GapCVP proof, part 03, continuation 04

def GapCVP.FormulaTotalCert.canonicalClearMissingTrace (position : Fin 3) (field binary : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalClearLabel position) [] [] field binary [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [false])) (field.length + binary.length + 2)

Reject a literal whose field has no following sign bit, clearing the remaining work stacks.

Equations

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

def GapCVP.FormulaTotalCert.canonicalDecrementNoneFailureTrace (bits : List Bool) (hdecrement : FormulaTuringTM.binaryStackDecrement bits = none) (input : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 13 input [] [] bits [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [false])) (input.length + 2 * bits.length + 2)

Reject a formula when decrementing its binary clause counter fails.

Equations

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

def GapCVP.FormulaTotalCert.canonicalBodyOutput : List Bool → Bool → Fin 3 → ℕ → List Bool → List Bool → Bool

Compute acceptance of a formula body from its parsing state and remaining clause count.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.FormulaTotalCert.canonicalBodyOutput [] true x✝³ x✝² x✝¹ x✝ = false
• GapCVP.FormulaTotalCert.canonicalBodyOutput [] false x✝¹ 0 [] x✝ = if x✝¹ = 0 then decide (GapCVP.FormulaTuringTM.binaryStackValue x✝ = 0) else false
• GapCVP.FormulaTotalCert.canonicalBodyOutput [] false x✝³ x✝² x✝¹ x✝ = false
• GapCVP.FormulaTotalCert.canonicalBodyOutput (bit :: rest) true x✝² count.succ x✝¹ x✝ = GapCVP.FormulaTotalCert.canonicalBodyOutput rest true x✝² count (bit :: x✝¹) x✝
• GapCVP.FormulaTotalCert.canonicalBodyOutput (head :: rest) true x✝¹ 0 (false :: tail) x✝ = false

def GapCVP.FormulaTotalCert.canonicalBodyPhase (payload : Bool) (position : Fin 3) : Fin 17

Select the prefix or payload machine phase for the current literal position.

Equations

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

def GapCVP.FormulaTotalCert.canonicalBodyBudget (binaryBound : ℕ) (input : List Bool) (counterLength : ℕ) (field : List Bool) : ℕ

Time bound for parsing a formula body with a bounded binary counter.

Equations

• GapCVP.FormulaTotalCert.canonicalBodyBudget binaryBound input counterLength field = (2 * binaryBound + 10) * (2 * input.length + counterLength + field.length + 1) + binaryBound + 4

def GapCVP.FormulaTotalCert.canonicalFailFromStep (source : FormulaTuringTM.canonicalFormulaMachine.Cfg) (input counter field binary borrow : List Bool) (hstep : FormulaTuringTM.canonicalFormulaMachine.step source = some (FormulaTuringTM.canonicalConfiguration 15 input counter field binary borrow [])) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step source (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [false])) (input.length + counter.length + field.length + binary.length + borrow.length + 2)

Extend a step into the failure phase to a complete rejecting execution.

Equations

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

def GapCVP.FormulaTotalCert.canonicalFinalCountTrace (binary : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPrefixLabel 0) [] [] [] binary [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [decide (FormulaTuringTM.binaryStackValue binary = 0)])) (2 * binary.length + 4)

Finish parsing by accepting exactly when the remaining clause count is zero.

Equations

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

def GapCVP.FormulaTotalCert.canonicalBodyTrace (binaryBound : ℕ) (input : List Bool) (payload : Bool) (position : Fin 3) (counterLength : ℕ) (field binary : List Bool) (hbinary : binary.length ≤ binaryBound) (hfield : payload = false → field = []) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (canonicalBodyPhase payload position) input (List.replicate counterLength true) field binary [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [canonicalBodyOutput input payload position counterLength field binary])) (canonicalBodyBudget binaryBound input counterLength field)

A bounded execution matching the recursive formula-body acceptance function.

Equations

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

def GapCVP.FormulaTotalCert.canonicalHeaderMissingPrefixTrace (count : ℕ) (counter field binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 (List.replicate count true) counter field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration 15 [] (List.replicate count true ++ counter) field binary borrow output)) (count + 1)

Detect a formula header whose length prefix has no delimiter.

Equations

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

def GapCVP.FormulaTotalCert.canonicalHeaderMissingTrace (count : ℕ) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 (List.replicate count true) [] [] [] [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [false])) (2 * count + 2)

A bounded rejecting execution for an undelimited formula header.

Equations

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

def GapCVP.FormulaTotalCert.canonicalHeaderPartialCopyTrace (payload remaining field binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 1 payload (List.replicate payload.length true ++ remaining) field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration 1 [] remaining (payload.reverse ++ field) binary borrow output)) payload.length

Copy the available header bits while retaining the unfinished length counter.

Equations

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

def GapCVP.FormulaTotalCert.canonicalHeaderTruncatedTrace (payload : List Bool) (extra : ℕ) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 (List.replicate (payload.length + extra + 1) true ++ false :: payload) [] [] [] [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [false])) (3 * payload.length + 2 * extra + 6)

Reject a formula header shorter than its declared length.

Equations

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

def GapCVP.FormulaTotalCert.canonicalMachineOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.FormulaTotalCert.canonicalMachineOutputLengthPrefixed (header body : List Bool) : canonicalMachineOutput (BinaryEncoding.lengthPrefixedWord header ++ body) = if FormulaCert.isCanonicalBinaryWord header = true then [canonicalBodyOutput body false 0 0 [] header] else [false]

def GapCVP.FormulaTotalCert.canonicalInputBudget (input : List Bool) : ℕ

GapCVP reduction support.

Equations

• GapCVP.FormulaTotalCert.canonicalInputBudget input = 64 * (input.length + 1) * (input.length + 1) + 64

def GapCVP.FormulaTotalCert.canonicalHeaderValidTrace (header body : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 (BinaryEncoding.lengthPrefixedWord header ++ body) [] [] [] [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine (canonicalMachineOutput (BinaryEncoding.lengthPrefixedWord header ++ body)))) (canonicalInputBudget (BinaryEncoding.lengthPrefixedWord header ++ body))

A bounded execution parsing a length-prefixed header and its following formula body.

Equations

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

@[simp]

theorem GapCVP.FormulaTotalCert.canonicalMachineOutputMissing (count : ℕ) : canonicalMachineOutput (List.replicate count true) = [false]

@[simp]

theorem GapCVP.FormulaTotalCert.canonicalMachineOutputTruncated (payload : List Bool) (extra : ℕ) : canonicalMachineOutput (List.replicate (payload.length + extra + 1) true ++ false :: payload) = [false]

def GapCVP.FormulaTotalCert.canonicalTotalTrace (input : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 input [] [] [] [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine (canonicalMachineOutput input))) (canonicalInputBudget input)

GapCVP reduction support.

Equations

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

theorem GapCVP.FormulaSemanticCert.readLengthPrefixedWord_some_reconstruct (input word suffix : List Bool) (hread : BinaryEncoding.readLengthPrefixedWord input = some (word, suffix)) : input = BinaryEncoding.lengthPrefixedWord word ++ suffix

theorem GapCVP.FormulaSemanticCert.canonicalMachineOutput_eq_expected (input : List Bool) : FormulaTotalCert.canonicalMachineOutput input = FormulaTotalCert.canonicalFormulaExpected input

def GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrement : List Bool → List Bool

Increment a binary word whose least significant digit comes first.

Equations

• GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrement [] = [true]
• GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrement (false :: digits) = true :: digits
• GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrement (true :: digits) = false :: GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrement digits

def GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryCarrySplit : List Bool → ℕ × List Bool

Split an increment into the number of cleared low digits and the remaining high digits.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryCarrySplit [] = (0, [true])
• GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryCarrySplit (false :: digits) = (0, true :: digits)

theorem GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrementEqCarrySplit (digits : List Bool) : structuralBinaryIncrement digits = List.replicate (structuralBinaryCarrySplit digits).1 false ++ (structuralBinaryCarrySplit digits).2

theorem GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryCarrySplitCountLe (digits : List Bool) : (structuralBinaryCarrySplit digits).1 ≤ digits.length

def GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrementN : ℕ → List Bool → List Bool

Apply binary increment the specified number of times.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrementN 0 x✝ = x✝

theorem GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrementNEncodeNat (count number : ℕ) : structuralBinaryIncrementN count (Computability.encodeNat number) = Computability.encodeNat (number + count)

theorem GapCVP.CLStructuralNaturalBinaryWriter.structuralBinaryIncrementNLengthLe (count : ℕ) (digits : List Bool) : (structuralBinaryIncrementN count digits).length ≤ digits.length + count

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPeek (stack : Fin 4) (present absent : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Read a stack head into the state and branch on whether the stack is empty.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPop (stack : Fin 4) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Remove a stack head while preserving the bit stored in the machine state.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPushBit (stack : Fin 4) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Push the bit held in the state, defaulting to false when the state is empty.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPushConstant (stack : Fin 4) (bit : Bool) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Push a fixed bit before executing the continuation.

Equations

• GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPushConstant stack bit continuation = Turing.TM2.Stmt.push stack (fun (x : Option Bool) => bit) continuation

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterGoto (phase : Fin 5) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Clear the stored bit and transfer control to the requested phase.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterInputStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Consume one input bit and increment the counter, or begin output preparation.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarryStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Propagate a binary carry, saving cleared digits on the carry stack.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Restore saved carry digits to the binary counter before reading more input.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPrepareStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Reverse the counter onto the carry stack in preparation for output.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterOutputStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 5) (Option Bool)

Transfer prepared digits to the output stack and halt when none remain.

Equations

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

@[reducible, inline]

abbrev GapCVP.CLStructuralNaturalBinaryWriter.structuralNaturalBinaryWriter : Turing.FinTM2

The four-stack machine that writes the binary encoding of its input length.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterConfiguration (phase : Fin 5) (input digits carry output : List Bool) : structuralNaturalBinaryWriter.Cfg

A writer configuration with explicit input, counter, carry, and output stacks.

Equations

• GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterConfiguration phase input digits carry output = { l := some phase, var := none, stk := ![input, digits, carry, output] }

def GapCVP.CLStructuralNaturalBinaryWriter.tacticNaturalBinaryWriterStepTac : Lean.ParserDescr

Executes the naturalBinaryWriterStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterInputStep (bit : Bool) (input digits carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 0 (bit :: input) digits carry output) = some (naturalBinaryWriterConfiguration 1 input digits carry output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterInputFinish (digits carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 0 [] digits carry output) = some (naturalBinaryWriterConfiguration 3 [] digits carry output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarryTrueStep (input digits carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 1 input (true :: digits) carry output) = some (naturalBinaryWriterConfiguration 1 input digits (false :: carry) output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarryFalseStep (input digits carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 1 input (false :: digits) carry output) = some (naturalBinaryWriterConfiguration 2 input (true :: digits) carry output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarryEmptyStep (input carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 1 input [] carry output) = some (naturalBinaryWriterConfiguration 2 input [true] carry output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterRestoreStep (bit : Bool) (input digits carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 2 input digits (bit :: carry) output) = some (naturalBinaryWriterConfiguration 2 input (bit :: digits) carry output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterRestoreFinish (input digits output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 2 input digits [] output) = some (naturalBinaryWriterConfiguration 0 input digits [] output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPrepareStep (bit : Bool) (digits carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 3 [] (bit :: digits) carry output) = some (naturalBinaryWriterConfiguration 3 [] digits (bit :: carry) output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPrepareFinish (carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 3 [] [] carry output) = some (naturalBinaryWriterConfiguration 4 [] [] carry output)

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterOutputStep (bit : Bool) (carry output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 4 [] [] (bit :: carry) output) = some (naturalBinaryWriterConfiguration 4 [] [] carry (bit :: output))

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterOutputFinish (output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 4 [] [] [] output) = some (Turing.haltList structuralNaturalBinaryWriter output)

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarrySearchTrace (input digits carry output : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 1 input digits carry output) (some (naturalBinaryWriterConfiguration 2 input (structuralBinaryCarrySplit digits).2 (List.replicate (structuralBinaryCarrySplit digits).1 false ++ carry) output)) (digits.length + 1)

Propagate a carry to the first zero bit or the end of the binary counter.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarryRestoreTrace (input digits carry output : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 2 input digits carry output) (some (naturalBinaryWriterConfiguration 0 input (carry.reverse ++ digits) [] output)) (carry.length + 1)

Restore the saved carry bits and return to the input phase.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterCarryTrace (input digits output : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 1 input digits [] output) (some (naturalBinaryWriterConfiguration 0 input (structuralBinaryIncrement digits) [] output)) (2 * digits.length + 2)

Complete one binary increment within a linear bound in the counter length.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterScanBudget : List Bool → List Bool → ℕ

Recursive time bound for consuming input and incrementing the binary counter.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterScanBudget [] x✝ = 1

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterScanTrace (input digits output : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 0 input digits [] output) (some (naturalBinaryWriterConfiguration 3 [] (structuralBinaryIncrementN input.length digits) [] output)) (naturalBinaryWriterScanBudget input digits)

Consume every input bit, incrementing the binary counter once per bit.

Equations

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

theorem GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterScanBudgetLe (input digits : List Bool) : naturalBinaryWriterScanBudget input digits ≤ 2 * input.length * (digits.length + input.length + 1) + 1

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterPrepareTrace (digits carry output : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 3 [] digits carry output) (some (naturalBinaryWriterConfiguration 4 [] [] (digits.reverse ++ carry) output)) (digits.length + 1)

Reverse the binary counter onto the carry stack within a linear time bound.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterOutputTrace (carry output : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 4 [] [] carry output) (some (Turing.haltList structuralNaturalBinaryWriter (carry.reverse ++ output))) (carry.length + 1)

Write the prepared carry stack to output and halt within a linear time bound.

Equations

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

def GapCVP.CLStructuralNaturalBinaryWriter.naturalBinaryWriterTotalTrace (input : List Bool) : StateTransition.EvalsToInTime structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 0 input [] [] []) (some (Turing.haltList structuralNaturalBinaryWriter (Computability.encodeNat input.length))) (8 * (input.length + 1) ^ 2 + 8)

A quadratic-time execution writing the binary encoding of the input length.

Equations

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

noncomputable def GapCVP.CLStructuralNaturalBinaryWriter.structuralNaturalBinaryWriterComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding fun (input : List Bool) => Computability.encodeNat input.length

GapCVP reduction support.

Equations

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

def GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWord input = GapCVP.BinaryEncoding.encodeAtomic input.length

theorem GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWord_eq_prefix (input : List Bool) : structuralAtomicNaturalWord input = BinaryEncoding.lengthPrefixedWord (Computability.encodeNat input.length)

noncomputable def GapCVP.CLStructuralAtomicNaturalWriter.structuralAtomicNaturalWriterComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding structuralAtomicNaturalWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.paddedStructuralTableauSimulation (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : CLVerifier.TableauSimulation bound machine

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeSourceClauses (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : List (CL.Clause (CLCellRowBounds.rowWidth bound machine x) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeThreeCNF (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : ThreeCNF

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeCNFWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine x = GapCVP.BinaryEncoding.encodeThreeCNF (GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeThreeCNF bound machine x)

theorem GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeCNFWord_mem_threeSAT_iff (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : threeSATLanguage (structuralWholeCNFWord bound machine x) = true ↔ ∃ (certificate : List Bool), certificate.length ≤ Polynomial.eval x.length bound ∧ verifier (x, certificate) = true

theorem GapCVP.CLStructuralWholeCNFOutputTM.structuralWholeThreeCNF_allDistinct (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : ThreeCNFReduction.allDistinct (structuralWholeThreeCNF bound machine x) = true

theorem GapCVP.CLStructuralWholeCNFOutputTM.structuralNatSize_le_self (value : ℕ) : value.size ≤ value

noncomputable def GapCVP.CNFClauseLoop.clauseLoopFiniteElements (α : Type) [Fintype α] : List α

GapCVP reduction support.

Equations

• GapCVP.CNFClauseLoop.clauseLoopFiniteElements α = List.ofFn ⇑(Fintype.equivFin α).symm

theorem GapCVP.CNFClauseLoop.mem_clauseLoopFiniteElements (α : Type) [Fintype α] (value : α) : value ∈ clauseLoopFiniteElements α

theorem GapCVP.CNFSortingDedup.replicate_append_bit_cons (bit : Bool) (count : ℕ) (tail : List Bool) : List.replicate count bit ++ bit :: tail = bit :: (List.replicate count bit ++ tail)

inductive GapCVP.CNFEncodedClauseSort.EncodedWordOrdering : Type

GapCVP reduction support.

• invalid : EncodedWordOrdering
• less : EncodedWordOrdering
• equal : EncodedWordOrdering
• greater : EncodedWordOrdering

@[instance_reducible]

instance GapCVP.CNFEncodedClauseSort.instDecidableEqEncodedWordOrdering : DecidableEq EncodedWordOrdering

Equations

• GapCVP.CNFEncodedClauseSort.instDecidableEqEncodedWordOrdering x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

noncomputable instance GapCVP.CNFEncodedClauseSort.instFintypeEncodedWordOrdering : Fintype EncodedWordOrdering

Equations

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

def GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst : EncodedWordOrdering → Bool

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.invalid = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal = true
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater = true

def GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond : EncodedWordOrdering → Bool

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.invalid = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less = true
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal = false
• GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater = true

def GapCVP.CNFEncodedClauseSort.encodedWordOrderingWord (outcome : EncodedWordOrdering) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.encodedWordOrderingWord outcome = [GapCVP.CNFEncodedClauseSort.encodedWordOrderingFirst outcome, GapCVP.CNFEncodedClauseSort.encodedWordOrderingSecond outcome]

def GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering : List Bool → List Bool → EncodedWordOrdering

GapCVP reduction support.

Equations

• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering [] [] = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering [] (head :: tail) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (head :: tail) [] = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (false :: tail) (true :: tail_1) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (true :: tail) (false :: tail_1) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (false :: left) (false :: right) = GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering left right
• GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering (true :: left) (true :: right) = GapCVP.CNFEncodedClauseSort.lexicographicEncodedWordOrdering left right

def GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering (input : List Bool) : EncodedWordOrdering

GapCVP reduction support.

Equations

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

def GapCVP.CNFEncodedClauseSort.sourcePreservingDelimitedPairComparisonWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFEncodedClauseSort.delimitedPairWordOrdering_valid (first second suffix : List Bool) : delimitedPairWordOrdering (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = lexicographicEncodedWordOrdering first second