GapCVP proof, part 03, continuation 03

def GapCVP.SourceFormulaStructuralDecoder.suffixPrefixTrace (count : ℕ) (tail counter reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 0 (List.replicate count true ++ false :: tail) counter reversed output) (some (suffixConfiguration 1 tail (List.replicate count true ++ counter) reversed output)) (count + 1)

Consume a unary length prefix and its delimiter, recording the count.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixCopyTrace (payload suffix reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 1 (payload ++ suffix) (List.replicate payload.length true) reversed output) (some (suffixConfiguration 1 suffix [] (payload.reverse ++ reversed) output)) payload.length

Copy the counted payload into reversed scratch storage.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixDiscardTrace (input reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 2 input [] reversed output) (some (suffixConfiguration 3 input [] [] output)) (reversed.length + 1)

Discard the copied payload before collecting the remaining suffix.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixCollectTrace (input reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 3 input [] reversed output) (some (suffixConfiguration 4 [] [] (input.reverse ++ reversed) output)) (input.length + 1)

Collect the suffix in reversed scratch storage.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixRestoreTrace (reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 4 [] [] reversed output) (some (Turing.haltList suffixDecoderMachine (reversed.reverse ++ output))) (reversed.length + 1)

Restore the collected suffix to the output stack and halt.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixValidTrace (payload suffix : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 0 (BinaryEncoding.lengthPrefixedWord payload ++ suffix) [] [] []) (some (Turing.haltList suffixDecoderMachine suffix)) (3 * payload.length + 2 * suffix.length + 5)

Decode a valid length-prefixed payload and return its trailing suffix.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixFailureTrace (input counter reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 5 input counter reversed output) (some (Turing.haltList suffixDecoderMachine output)) (input.length + counter.length + reversed.length + 1)

Clear all work stacks after a malformed input and halt with the current output.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixMissingPrefixTrace (count : ℕ) (counter reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 0 (List.replicate count true) counter reversed output) (some (suffixConfiguration 5 [] (List.replicate count true ++ counter) reversed output)) (count + 1)

Enter the failure phase when a unary length prefix has no delimiter.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixMissingTrace (count : ℕ) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 0 (List.replicate count true) [] [] []) (some (Turing.haltList suffixDecoderMachine [])) (2 * count + 2)

Reject an input consisting only of a unary length prefix.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixPartialCopyTrace (payload remaining reversed output : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 1 payload (List.replicate payload.length true ++ remaining) reversed output) (some (suffixConfiguration 1 [] remaining (payload.reverse ++ reversed) output)) payload.length

Copy all available payload bits while leaving surplus count markers.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixTruncatedTrace (payload : List Bool) (extra : ℕ) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 0 (List.replicate (payload.length + extra + 1) true ++ false :: payload) [] [] []) (some (Turing.haltList suffixDecoderMachine [])) (3 * payload.length + 2 * extra + 6)

Reject a length prefix larger than the available payload.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix input = match GapCVP.BinaryEncoding.readLengthPrefixedWord input with | some (fst, suffix) => suffix | none => []

@[simp]

theorem GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix_valid (payload suffix : List Bool) : firstFieldSuffix (BinaryEncoding.lengthPrefixedWord payload ++ suffix) = suffix

def GapCVP.SourceFormulaStructuralDecoder.suffixTotalTrace (input : List Bool) : StateTransition.EvalsToInTime suffixDecoderMachine.step (suffixConfiguration 0 input [] [] []) (some (Turing.haltList suffixDecoderMachine (firstFieldSuffix input))) (3 * input.length + 6)

Decode the suffix for every input, including malformed prefixes.

Equations

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

noncomputable def GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffixComputable : BitTM firstFieldSuffix

GapCVP reduction support.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.literalSuffix : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFormulaStructuralDecoder.literalSuffix = List.tail ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.SourceFormulaStructuralDecoder.literalSuffixComputable : BitTM literalSuffix

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFormulaStructuralDecoder.literalSuffix_valid (literal : Literal) (suffix : List Bool) : literalSuffix (BinaryEncoding.encodeLiteral literal ++ suffix) = suffix

def GapCVP.SourceFormulaStructuralDecoder.clauseSuffix : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceFormulaStructuralDecoder.clauseSuffixComputable : BitTM clauseSuffix

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFormulaStructuralDecoder.clauseSuffix_valid (clause : ThreeClause) (suffix : List Bool) : clauseSuffix (BinaryEncoding.encodeThreeClause clause ++ suffix) = suffix

@[simp]

theorem GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix_encodeThreeCNF (clauses : ThreeCNF) : firstFieldSuffix (BinaryEncoding.encodeThreeCNF clauses) = List.flatMap BinaryEncoding.encodeThreeClause clauses

def GapCVP.SourceVariableFormulaDecoder.variablePrefixLabel (position : Fin 3) : Fin 7

State label for reading the prefix of one of three clause literals.

Equations

• GapCVP.SourceVariableFormulaDecoder.variablePrefixLabel position = ⟨↑position, ⋯⟩

def GapCVP.SourceVariableFormulaDecoder.variablePayloadLabel (position : Fin 3) : Fin 7

State label for reading the payload of one of three clause literals.

Equations

• GapCVP.SourceVariableFormulaDecoder.variablePayloadLabel position = ⟨↑position + 3, ⋯⟩

def GapCVP.SourceVariableFormulaDecoder.nextLiteralPosition (position : Fin 3) : Fin 3

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceVariableFormulaDecoder.nextLiteralPosition position = if position = 0 then 1 else if position = 1 then 2 else 0

def GapCVP.SourceVariableFormulaDecoder.variablePrefixStatement (position : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 3) => Bool) (Fin 7) (Option Bool)

Parse a literal's unary prefix or enter its payload or failure phase.

Equations

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

def GapCVP.SourceVariableFormulaDecoder.variablePayloadStatement (position : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 3) => Bool) (Fin 7) (Option Bool)

Match a literal's payload against its prefix count and advance the clause.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceVariableFormulaDecoder.variableClauseMachine : Turing.FinTM2

Three-stack machine that checks the three encoded literals of a clause.

Equations

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

def GapCVP.SourceVariableFormulaDecoder.variableConfiguration (phase : Fin 7) (input counter : List Bool) (count : ℕ) : variableClauseMachine.Cfg

Decoder configuration with input, count markers, and accumulated output count.

Equations

• GapCVP.SourceVariableFormulaDecoder.variableConfiguration phase input counter count = { l := some phase, var := none, stk := ![input, counter, List.replicate count true] }

theorem GapCVP.SourceVariableFormulaDecoder.variablePrefixTrue (position : Fin 3) (input counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePrefixLabel position) (true :: input) counter count) = some (variableConfiguration (variablePrefixLabel position) input (true :: counter) count)

theorem GapCVP.SourceVariableFormulaDecoder.variablePrefixDelimiter (position : Fin 3) (input counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePrefixLabel position) (false :: input) counter count) = some (variableConfiguration (variablePayloadLabel position) input counter count)

theorem GapCVP.SourceVariableFormulaDecoder.variablePayloadStep (position : Fin 3) (bit counterBit : Bool) (input counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePayloadLabel position) (bit :: input) (counterBit :: counter) count) = some (variableConfiguration (variablePayloadLabel position) input counter count)

theorem GapCVP.SourceVariableFormulaDecoder.variableSignStep (position : Fin 3) (hposition : position ≠ 2) (sign : Bool) (input : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePayloadLabel position) (sign :: input) [] count) = some (variableConfiguration (variablePrefixLabel (nextLiteralPosition position)) input [] count)

theorem GapCVP.SourceVariableFormulaDecoder.variableCompleteClauseStep (sign : Bool) (input : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePayloadLabel 2) (sign :: input) [] count) = some (variableConfiguration (variablePrefixLabel 0) input [] (count + 1))

theorem GapCVP.SourceVariableFormulaDecoder.variableFinishValid (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePrefixLabel 0) [] [] count) = some (Turing.haltList variableClauseMachine (true :: List.replicate count true))

theorem GapCVP.SourceVariableFormulaDecoder.variablePrefixUnfinished (position : Fin 3) (bit : Bool) (counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePrefixLabel position) [] (bit :: counter) count) = some (variableConfiguration 6 [] (bit :: counter) count)

theorem GapCVP.SourceVariableFormulaDecoder.variablePrefixIncompleteClause (position : Fin 3) (hposition : position ≠ 0) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePrefixLabel position) [] [] count) = some (variableConfiguration 6 [] [] count)

theorem GapCVP.SourceVariableFormulaDecoder.variablePayloadMissing (position : Fin 3) (counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePayloadLabel position) [] counter count) = some (variableConfiguration 6 [] counter count)

theorem GapCVP.SourceVariableFormulaDecoder.variableFailureDropInput (bit : Bool) (input counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration 6 (bit :: input) counter count) = some (variableConfiguration 6 input counter count)

theorem GapCVP.SourceVariableFormulaDecoder.variableFailureDropCounter (bit : Bool) (counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration 6 [] (bit :: counter) count) = some (variableConfiguration 6 [] counter count)

theorem GapCVP.SourceVariableFormulaDecoder.variableFailureFinish (count : ℕ) : variableClauseMachine.step (variableConfiguration 6 [] [] count) = some (Turing.haltList variableClauseMachine (false :: List.replicate count true))

def GapCVP.SourceVariableFormulaDecoder.variableFailureTrace (input counter : List Bool) (count : ℕ) : StateTransition.EvalsToInTime variableClauseMachine.step (variableConfiguration 6 input counter count) (some (Turing.haltList variableClauseMachine (false :: List.replicate count true))) (input.length + counter.length + 1)

Clear the decoder work stacks and emit a failure marker.

Equations

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

def GapCVP.SourceVariableFormulaDecoder.variableScanPhase (payload : Bool) (position : Fin 3) : Fin 7

Select the prefix or payload state for the current literal.

Equations

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

def GapCVP.SourceVariableFormulaDecoder.variableScanOutput : List Bool → Bool → Fin 3 → List Bool → ℕ → List Bool

Output encoded by the remaining input and current clause parsing state.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.SourceVariableFormulaDecoder.variableScanOutput [] true x✝² x✝¹ x✝ = false :: List.replicate x✝ true
• GapCVP.SourceVariableFormulaDecoder.variableScanOutput [] false x✝¹ [] x✝ = if x✝¹ = 0 then true :: List.replicate x✝ true else false :: List.replicate x✝ true
• GapCVP.SourceVariableFormulaDecoder.variableScanOutput [] false x✝¹ (head :: tail) x✝ = false :: List.replicate x✝ true
• GapCVP.SourceVariableFormulaDecoder.variableScanOutput (head :: rest) true x✝¹ (head_1 :: counter) x✝ = GapCVP.SourceVariableFormulaDecoder.variableScanOutput rest true x✝¹ counter x✝

def GapCVP.SourceVariableFormulaDecoder.variableScanTrace (input : List Bool) (payload : Bool) (position : Fin 3) (counter : List Bool) (count : ℕ) : StateTransition.EvalsToInTime variableClauseMachine.step (variableConfiguration (variableScanPhase payload position) input counter count) (some (Turing.haltList variableClauseMachine (variableScanOutput input payload position counter count))) (2 * input.length + counter.length + 2)

Simulate the clause decoder through its remaining input to its final output.

Equations

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

def GapCVP.SourceVariableFormulaDecoder.variableClauseBodyOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceVariableFormulaDecoder.variableClauseBodyOutput input = GapCVP.SourceVariableFormulaDecoder.variableScanOutput input false 0 [] 0

noncomputable def GapCVP.SourceVariableFormulaDecoder.variableClauseBodyComputable : BitTM variableClauseBodyOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceVariableFormulaDecoder.variableClauseBodyOutput_valid (clauses : ThreeCNF) : variableClauseBodyOutput (List.flatMap BinaryEncoding.encodeThreeClause clauses) = true :: List.replicate (List.length clauses) true

noncomputable def GapCVP.SourceVariableFormulaDecoder.variableFormulaBodyComputable : BitTM (variableClauseBodyOutput ∘ SourceFormulaStructuralDecoder.firstFieldSuffix)

GapCVP reduction support.

Equations

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

def GapCVP.FormulaTuringTM.binaryStackValue : List Bool → ℕ

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.FormulaTuringTM.binaryStackValue [] = 0
• GapCVP.FormulaTuringTM.binaryStackValue (bit :: rest) = (if bit = true then 1 else 0) + 2 * GapCVP.FormulaTuringTM.binaryStackValue rest

theorem GapCVP.FormulaTuringTM.binaryStackValue_encodeNat (value : ℕ) : binaryStackValue (Computability.encodeNat value) = value

Internal support shared across GapCVP continuation modules.

def GapCVP.FormulaTuringTM.binaryStackDecrement : List Bool → Option (List Bool)

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.FormulaTuringTM.binaryStackDecrement [] = none
• GapCVP.FormulaTuringTM.binaryStackDecrement (true :: rest) = some (false :: rest)
• GapCVP.FormulaTuringTM.binaryStackDecrement (false :: rest) = match GapCVP.FormulaTuringTM.binaryStackDecrement rest with | none => none | some remaining => some (true :: remaining)

theorem GapCVP.FormulaTuringTM.binaryStackDecrement_value (bits remaining : List Bool) (hdecrement : binaryStackDecrement bits = some remaining) : binaryStackValue remaining + 1 = binaryStackValue bits

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.binaryStackValue_eq_zero_iff (bits : List Bool) : binaryStackValue bits = 0 ↔ ∀ bit ∈ bits, bit = false

Internal support shared across GapCVP continuation modules.

def GapCVP.FormulaTuringTM.canonicalPrefixLabel (position : Fin 3) : Fin 17

GapCVP reduction support.

Equations

• GapCVP.FormulaTuringTM.canonicalPrefixLabel position = ⟨↑position + 4, ⋯⟩

def GapCVP.FormulaTuringTM.canonicalPayloadLabel (position : Fin 3) : Fin 17

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.FormulaTuringTM.canonicalPayloadLabel position = ⟨↑position + 7, ⋯⟩

def GapCVP.FormulaTuringTM.canonicalClearLabel (position : Fin 3) : Fin 17

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.FormulaTuringTM.canonicalClearLabel position = ⟨↑position + 10, ⋯⟩

def GapCVP.FormulaTuringTM.canonicalSignStatement (position : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 17) (Option Bool)

Consume a literal sign and advance to the next literal or final check.

Equations

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

def GapCVP.FormulaTuringTM.canonicalPrefixStatement (position : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 17) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.FormulaTuringTM.canonicalPayloadStatement (position : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 17) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.FormulaTuringTM.canonicalClearStatement (position : Fin 3) : Turing.TM2.Stmt (fun (x : Fin 6) => Bool) (Fin 17) (Option Bool)

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.FormulaTuringTM.canonicalFormulaMachine : Turing.FinTM2

GapCVP reduction support.

Equations

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

def GapCVP.FormulaTuringTM.canonicalConfiguration (phase : Fin 17) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.Cfg

GapCVP reduction support.

Equations

• GapCVP.FormulaTuringTM.canonicalConfiguration phase input counter field binary borrow output = { l := some phase, var := none, stk := ![input, counter, field, binary, borrow, output] }

theorem GapCVP.FormulaTuringTM.canonical_header_prefix_true (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 0 (true :: input) counter field binary borrow output) = some (canonicalConfiguration 0 input (true :: counter) field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonicalHeaderPrefixDelimiter (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 0 (false :: input) counter field binary borrow output) = some (canonicalConfiguration 1 input counter field binary borrow output)

theorem GapCVP.FormulaTuringTM.canonical_header_prefix_missing (counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 0 [] counter field binary borrow output) = some (canonicalConfiguration 15 [] counter field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_header_payload_step (bit : Bool) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 1 (bit :: input) (true :: counter) field binary borrow output) = some (canonicalConfiguration 1 input counter (bit :: field) binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_header_payload_missing (counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 1 [] (true :: counter) field binary borrow output) = some (canonicalConfiguration 15 [] (true :: counter) field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_header_payload_complete (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 1 input [] field binary borrow output) = some (canonicalConfiguration 2 input [] field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_header_check_true (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 2 input [] (true :: field) binary borrow output) = some (canonicalConfiguration 3 input [] (true :: field) binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_header_check_false (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 2 input [] (false :: field) binary borrow output) = some (canonicalConfiguration 15 input [] (false :: field) binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_header_check_zero (input binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 2 input [] [] binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel 0) input [] [] binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonicalHeaderReverseStep (bit : Bool) (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 3 input [] (bit :: field) binary borrow output) = some (canonicalConfiguration 3 input [] field (bit :: binary) borrow output)

theorem GapCVP.FormulaTuringTM.canonicalHeaderReverseComplete (input binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 3 input [] [] binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel 0) input [] [] binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalBorrowZero (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 13 input counter field (false :: binary) borrow output) = some (canonicalConfiguration 13 input counter field binary (true :: borrow) output)

theorem GapCVP.FormulaTuringTM.canonicalBorrowOne (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 13 input counter field (true :: binary) borrow output) = some (canonicalConfiguration 14 input counter field (false :: binary) borrow output)

theorem GapCVP.FormulaTuringTM.canonicalBorrowExhausted (input counter field borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 13 input counter field [] borrow output) = some (canonicalConfiguration 15 input counter field [] borrow output)

theorem GapCVP.FormulaTuringTM.canonicalBorrowRestoreStep (bit : Bool) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 14 input counter field binary (bit :: borrow) output) = some (canonicalConfiguration 14 input counter field (true :: binary) borrow output)

theorem GapCVP.FormulaTuringTM.canonicalBorrowRestoreComplete (input counter field binary output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 14 input counter field binary [] output) = some (canonicalConfiguration (canonicalPrefixLabel 0) input counter field binary [] output)

theorem GapCVP.FormulaTuringTM.canonicalZeroCheckFalse (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 16 input counter field (false :: binary) borrow output) = some (canonicalConfiguration 16 input counter field binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalZeroCheckTrue (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 16 input counter field (true :: binary) borrow output) = some (canonicalConfiguration 15 input counter field (true :: binary) borrow output)

theorem GapCVP.FormulaTuringTM.canonicalZeroCheckFinish : canonicalFormulaMachine.step (canonicalConfiguration 16 [] [] [] [] [] []) = some (Turing.haltList canonicalFormulaMachine [true])

theorem GapCVP.FormulaTuringTM.canonical_literal_prefix_true (position : Fin 3) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPrefixLabel position) (true :: input) counter field binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel position) input (true :: counter) field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_literal_prefix_delimiter (position : Fin 3) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPrefixLabel position) (false :: input) counter field binary borrow output) = some (canonicalConfiguration (canonicalPayloadLabel position) input counter field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_literal_payload_step (position : Fin 3) (bit : Bool) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPayloadLabel position) (bit :: input) (true :: counter) field binary borrow output) = some (canonicalConfiguration (canonicalPayloadLabel position) input counter (bit :: field) binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_literal_payload_missing (position : Fin 3) (counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPayloadLabel position) [] (true :: counter) field binary borrow output) = some (canonicalConfiguration 15 [] (true :: counter) field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_literal_field_true (position : Fin 3) (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPayloadLabel position) input [] (true :: field) binary borrow output) = some (canonicalConfiguration (canonicalClearLabel position) input [] (true :: field) binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_literal_field_false (position : Fin 3) (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPayloadLabel position) input [] (false :: field) binary borrow output) = some (canonicalConfiguration 15 input [] (false :: field) binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_literal_clear_step (position : Fin 3) (bit : Bool) (input field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalClearLabel position) input [] (bit :: field) binary borrow output) = some (canonicalConfiguration (canonicalClearLabel position) input [] field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonicalClearSignStep (position : Fin 3) (hposition : position ≠ 2) (sign : Bool) (input binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalClearLabel position) (sign :: input) [] [] binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel (SourceVariableFormulaDecoder.nextLiteralPosition position)) input [] [] binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalClearCompleteClause (sign : Bool) (input binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalClearLabel 2) (sign :: input) [] [] binary borrow output) = some (canonicalConfiguration 13 input [] [] binary borrow output)

theorem GapCVP.FormulaTuringTM.canonical_zero_field_sign_step (position : Fin 3) (hposition : position ≠ 2) (sign : Bool) (input binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPayloadLabel position) (sign :: input) [] [] binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel (SourceVariableFormulaDecoder.nextLiteralPosition position)) input [] [] binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_zero_field_completeClause (sign : Bool) (input binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPayloadLabel 2) (sign :: input) [] [] binary borrow output) = some (canonicalConfiguration 13 input [] [] binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonical_body_finish (binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration (canonicalPrefixLabel 0) [] [] [] binary borrow output) = some (canonicalConfiguration 16 [] [] [] binary borrow output)

Internal support shared across GapCVP continuation modules.

def GapCVP.FormulaTuringTM.canonicalBorrowZerosTrace (zeros : ℕ) (tail input counter field borrow output : List Bool) : StateTransition.EvalsToInTime canonicalFormulaMachine.step (canonicalConfiguration 13 input counter field (List.replicate zeros false ++ true :: tail) borrow output) (some (canonicalConfiguration 14 input counter field (false :: tail) (List.replicate zeros true ++ borrow) output)) (zeros + 1)

Borrow across zero bits until a one bit is reached.

Equations

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

def GapCVP.FormulaTuringTM.canonicalRestoreTrace (zeros : ℕ) (input counter field binary output : List Bool) : StateTransition.EvalsToInTime canonicalFormulaMachine.step (canonicalConfiguration 14 input counter field binary (List.replicate zeros true) output) (some (canonicalConfiguration (canonicalPrefixLabel 0) input counter field (List.replicate zeros true ++ binary) [] output)) (zeros + 1)

Restore borrowed markers as one bits and return to prefix parsing.

Equations

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

def GapCVP.FormulaTuringTM.canonicalDecrementTrace (zeros : ℕ) (tail input counter field output : List Bool) : StateTransition.EvalsToInTime canonicalFormulaMachine.step (canonicalConfiguration 13 input counter field (List.replicate zeros false ++ true :: tail) [] output) (some (canonicalConfiguration (canonicalPrefixLabel 0) input counter field (List.replicate zeros true ++ false :: tail) [] output)) (2 * zeros + 2)

Decrement a positive binary stack by borrowing and restoring markers.

Equations

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

theorem GapCVP.FormulaTuringTM.binaryStackDecrement_replicate (zeros : ℕ) (tail : List Bool) : binaryStackDecrement (List.replicate zeros false ++ true :: tail) = some (List.replicate zeros true ++ false :: tail)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTuringTM.canonicalFailureDropInput (bit : Bool) (input counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 (bit :: input) counter field binary borrow output) = some (canonicalConfiguration 15 input counter field binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalFailureDropCounter (bit : Bool) (counter field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 [] (bit :: counter) field binary borrow output) = some (canonicalConfiguration 15 [] counter field binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalFailureDropField (bit : Bool) (field binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 [] [] (bit :: field) binary borrow output) = some (canonicalConfiguration 15 [] [] field binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalFailureDropBinary (bit : Bool) (binary borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 [] [] [] (bit :: binary) borrow output) = some (canonicalConfiguration 15 [] [] [] binary borrow output)

theorem GapCVP.FormulaTuringTM.canonicalFailureDropBorrow (bit : Bool) (borrow output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 [] [] [] [] (bit :: borrow) output) = some (canonicalConfiguration 15 [] [] [] [] borrow output)

theorem GapCVP.FormulaTuringTM.canonicalFailureFinish (output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 [] [] [] [] [] output) = some (Turing.haltList canonicalFormulaMachine (false :: output))

def GapCVP.FormulaTuringTM.canonicalFailureTrace (input counter field binary borrow output : List Bool) : StateTransition.EvalsToInTime canonicalFormulaMachine.step (canonicalConfiguration 15 input counter field binary borrow output) (some (Turing.haltList canonicalFormulaMachine (false :: output))) (input.length + counter.length + field.length + binary.length + borrow.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaTuringTM.canonicalZeroTrace (zeros : ℕ) : StateTransition.EvalsToInTime canonicalFormulaMachine.step (canonicalConfiguration 16 [] [] [] (List.replicate zeros false) [] []) (some (Turing.haltList canonicalFormulaMachine [true])) (zeros + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaCert.isCanonicalBinaryWord (word : List Bool) : Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.FormulaCert.isCanonicalBinaryWord word = match word.reverse with | [] => true | true :: tail => true | false :: tail => false

theorem GapCVP.FormulaCert.encodeNat_canonical (number : ℕ) : isCanonicalBinaryWord (Computability.encodeNat number) = true

Internal support shared across GapCVP continuation modules.

def GapCVP.FormulaCert.canonicalHeaderPrefixTrace (length : ℕ) (tail counter field binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 0 (List.replicate length true ++ false :: tail) counter field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration 1 tail (List.replicate length true ++ counter) field binary borrow output)) (length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaCert.canonicalHeaderCopyTrace (header suffix field binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 1 (header ++ suffix) (List.replicate header.length true) field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration 1 suffix [] (header.reverse ++ field) binary borrow output)) header.length

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaCert.canonicalHeaderReverseTrace (field input binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 3 input [] field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPrefixLabel 0) input [] [] (field.reverse ++ binary) borrow output)) (field.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

structure GapCVP.FormulaCert.PositiveBinarySplit (bits : List Bool) : Type

Internal support shared across GapCVP continuation modules.

• zeros : ℕ

  Number of leading zero bits.

• tail : List Bool

  Bits following the first positive bit.

• shape : bits = List.replicate self.zeros false ++ true :: self.tail

  Decomposition of the positive binary word.

def GapCVP.FormulaCert.positiveBinarySplit (bits : List Bool) (hpositive : 0 < FormulaTuringTM.binaryStackValue bits) : PositiveBinarySplit bits

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.FormulaCert.binaryStackDecrement_none_shape (bits : List Bool) (hdecrement : FormulaTuringTM.binaryStackDecrement bits = none) : bits = List.replicate bits.length false

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaCert.binaryStackValue_zero_shape (bits : List Bool) (hzero : FormulaTuringTM.binaryStackValue bits = 0) : bits = List.replicate bits.length false

Internal support shared across GapCVP continuation modules.

def GapCVP.FormulaCert.canonicalBorrowFailureTrace (zeros : ℕ) (input counter field borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 13 input counter field (List.replicate zeros false) borrow output) (some (FormulaTuringTM.canonicalConfiguration 15 input counter field [] (List.replicate zeros true ++ borrow) output)) (zeros + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaCert.canonicalClearFieldTrace (position : Fin 3) (hposition : position ≠ 2) (field : List Bool) (sign : Bool) (input binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalClearLabel position) (sign :: input) [] field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPrefixLabel (SourceVariableFormulaDecoder.nextLiteralPosition position)) input [] [] binary borrow output)) (field.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaCert.canonicalClearThirdFieldTrace (field : List Bool) (sign : Bool) (input binary borrow output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalClearLabel 2) (sign :: input) [] field binary borrow output) (some (FormulaTuringTM.canonicalConfiguration 13 input [] [] binary borrow output)) (field.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

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

GapCVP reduction support.

Equations

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

theorem GapCVP.FormulaTotalCert.canonicalFormulaExpected_eq_true_iff (input : List Bool) : canonicalFormulaExpected input = [true] ↔ ∃ (formula : ThreeCNF), BinaryEncoding.encodeThreeCNF formula = input

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTotalCert.binaryStackDecrement_length (bits remaining : List Bool) (hdecrement : FormulaTuringTM.binaryStackDecrement bits = some remaining) : remaining.length = bits.length

Internal support shared across GapCVP continuation modules.

def GapCVP.FormulaTotalCert.canonicalDecrementSomeTrace (bits remaining : List Bool) (hdecrement : FormulaTuringTM.binaryStackDecrement bits = some remaining) (input counter field output : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 13 input counter field bits [] output) (some (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPrefixLabel 0) input counter field remaining [] output)) (2 * bits.length + 2)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.FormulaTotalCert.canonicalZeroPrefixTrace (zeros : ℕ) (tail : List Bool) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 16 [] [] [] (List.replicate zeros false ++ tail) [] []) (some (FormulaTuringTM.canonicalConfiguration 16 [] [] [] tail [] [])) zeros

Skip leading zero bits during the final zero check.

Equations

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

def GapCVP.FormulaTotalCert.canonicalZeroFailureTrace (bits : List Bool) (hpositive : 0 < FormulaTuringTM.binaryStackValue bits) : StateTransition.EvalsToInTime FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration 16 [] [] [] bits [] []) (some (Turing.haltList FormulaTuringTM.canonicalFormulaMachine [false])) (2 * bits.length + 3)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.FormulaTotalCert.canonical_literal_prefix_missing_counter (position : Fin 3) (counterBit : Bool) (counter field binary borrow output : List Bool) : FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPrefixLabel position) [] (counterBit :: counter) field binary borrow output) = some (FormulaTuringTM.canonicalConfiguration 15 [] (counterBit :: counter) field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTotalCert.canonical_literal_prefix_incomplete (position : Fin 3) (hposition : position ≠ 0) (field binary borrow output : List Bool) : FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPrefixLabel position) [] [] field binary borrow output) = some (FormulaTuringTM.canonicalConfiguration 15 [] [] field binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTotalCert.canonical_zero_field_missing_sign (position : Fin 3) (binary borrow output : List Bool) : FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalPayloadLabel position) [] [] [] binary borrow output) = some (FormulaTuringTM.canonicalConfiguration 15 [] [] [] binary borrow output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.FormulaTotalCert.canonical_clear_missing_sign (position : Fin 3) (binary borrow output : List Bool) : FormulaTuringTM.canonicalFormulaMachine.step (FormulaTuringTM.canonicalConfiguration (FormulaTuringTM.canonicalClearLabel position) [] [] [] binary borrow output) = some (FormulaTuringTM.canonicalConfiguration 15 [] [] [] binary borrow output)

Internal support shared across GapCVP continuation modules.