GapCVP proof, part 03, continuation 03

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

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

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.

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