GapCVP proof, part 05

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairValidBudget (first second : ℕ) : ℕ

Step budget for indexing a well-formed unary pair.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairValidTrace (first second : ℕ) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 0 (CNFUnaryPairIndexTM.unarySourcePairWord first second) [] [] [] [] [] [] [] []) (some (Turing.haltList CNFUnaryPairIndexTM.actualUnaryPairIndexMachine (List.replicate (Nat.pair first second) true))) (unaryPairValidBudget first second)

Runs the unary-pair index machine on a well-formed pair.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairFailureTrace (input first second matchedFirst matchedSecond base outer scratch : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 11 input first second matchedFirst matchedSecond base outer [] scratch) (some (Turing.haltList CNFUnaryPairIndexTM.actualUnaryPairIndexMachine [])) (input.length + first.length + second.length + matchedFirst.length + matchedSecond.length + base.length + outer.length + scratch.length + 1)

Clears the stacks after invalid unary-pair input and halts empty.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairFirstMissingTrace (count : ℕ) (first second matchedFirst matchedSecond base outer output scratch : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 0 (List.replicate count true) first second matchedFirst matchedSecond base outer output scratch) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 11 [] (List.replicate count true ++ first) second matchedFirst matchedSecond base outer output scratch)) (count + 1)

Detects a first unary component with no delimiter.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairSecondMissingTrace (count : ℕ) (first second matchedFirst matchedSecond base outer output scratch : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 1 (List.replicate count true) first second matchedFirst matchedSecond base outer output scratch) (some (CNFUnaryPairIndexTM.unaryPairConfiguration 11 [] first (List.replicate count true ++ second) matchedFirst matchedSecond base outer output scratch)) (count + 1)

Detects a second unary component with no delimiter.

Equations

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

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairInputBudget (input : List Bool) : ℕ

Quadratic step budget for the unary-pair index machine on arbitrary input.

Equations

• GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairInputBudget input = 64 * input.length ^ 2 + 128 * input.length + 128

def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.unaryPairTotalTrace (input : List Bool) : StateTransition.EvalsToInTime CNFUnaryPairIndexTM.actualUnaryPairIndexMachine.step (CNFUnaryPairIndexTM.unaryPairConfiguration 0 input [] [] [] [] [] [] [] []) (some (Turing.haltList CNFUnaryPairIndexTM.actualUnaryPairIndexMachine (CNFUnaryPairIndexTM.unarySourcePairOutput input))) (unaryPairInputBudget input)

Runs the unary-pair index machine within its quadratic budget for every input.

Equations

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

noncomputable def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.actualUnaryPairIndexComputable : BitTM CNFUnaryPairIndexTM.unarySourcePairOutput

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFPairedSourceGridDescriptorTM.pairedAccumulatorSignedLiteralDescriptorWord (sign : Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFPairedSourceGridDescriptorTM.pairedAccumulatorSignedLiteralDescriptorComputable (sign : Bool) : BitTM (pairedAccumulatorSignedLiteralDescriptorWord sign)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFPairedSourceGridDescriptorTM.pairedAccumulatorSignedLiteralDescriptorWord_pair (clauseIndex prefixIndex : ℕ) (sign : Bool) : pairedAccumulatorSignedLiteralDescriptorWord sign (CNFUnaryPairIndexTM.unarySourcePairWord clauseIndex prefixIndex) = CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (ThreeCNFReduction.accumulatorVariable clauseIndex prefixIndex, sign)

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixOutput_pair (first second : ℕ) (suffix : List Bool) : sourcePairPrefixOutput (CNFUnaryPairIndexTM.unarySourcePairWord first second ++ suffix) = CNFUnaryPairIndexTM.unarySourcePairWord first second

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixPeek (stack : Fin 4) (present absent : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Inspects a source-pair prefix stack and branches on whether a bit is present.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixPop (stack : Fin 4) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Removes the top bit of a source-pair prefix stack.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixPush (stack : Fin 4) (bit : Bool) (continuation : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Pushes the given bit onto a source-pair prefix stack.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixGoto (phase : Fin 6) : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Clears the inspected bit and enters the chosen source-pair prefix phase.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixFirstStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixSecondStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixSuffixStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixSecondRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixFirstRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixFailureStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

abbrev GapCVP.CNFSourcePairPrefixWorkerTM.actualSourcePairPrefixMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixConfiguration (phase : Fin 6) (input first second output : List Bool) : actualSourcePairPrefixMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixConfiguration phase input first second output = { l := some phase, var := none, stk := ![input, first, second, output] }

theorem GapCVP.CNFSourcePairPrefixWorkerTM.actualSourcePairPrefixMachine_init (input : List Bool) : Turing.initList actualSourcePairPrefixMachine input = sourcePairPrefixConfiguration 0 input [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFSourcePairPrefixWorkerTM.tacticSourcePairPrefixStepTac : Lean.ParserDescr

Executes the sourcePairPrefixStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_first_true (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 (true :: input) first second output) = some (sourcePairPrefixConfiguration 0 input (true :: first) second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_first_false (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 (false :: input) first second output) = some (sourcePairPrefixConfiguration 1 input first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_first_missing (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 [] first second output) = some (sourcePairPrefixConfiguration 5 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_second_true (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 (true :: input) first second output) = some (sourcePairPrefixConfiguration 1 input first (true :: second) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_second_false (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 (false :: input) first second output) = some (sourcePairPrefixConfiguration 2 input first second (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_second_missing (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 [] first second output) = some (sourcePairPrefixConfiguration 5 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_suffix_step (bit : Bool) (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 2 (bit :: input) first second output) = some (sourcePairPrefixConfiguration 2 input first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_suffix_finish (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 2 [] first second output) = some (sourcePairPrefixConfiguration 3 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_secondRestore_step (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 3 [] first (true :: second) output) = some (sourcePairPrefixConfiguration 3 [] first second (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_secondRestore_finish (first output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 3 [] first [] output) = some (sourcePairPrefixConfiguration 4 [] first [] (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_firstRestore_step (first output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 4 [] (true :: first) [] output) = some (sourcePairPrefixConfiguration 4 [] first [] (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_firstRestore_finish (output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 4 [] [] [] output) = some (Turing.haltList actualSourcePairPrefixMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_input_step (bit : Bool) (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 (bit :: input) first second output) = some (sourcePairPrefixConfiguration 5 input first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_first_step (bit : Bool) (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] (bit :: first) second output) = some (sourcePairPrefixConfiguration 5 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_second_step (bit : Bool) (second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] (bit :: second) output) = some (sourcePairPrefixConfiguration 5 [] [] second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_output_step (bit : Bool) (output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] [] (bit :: output)) = some (sourcePairPrefixConfiguration 5 [] [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_finish : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] [] []) = some (Turing.haltList actualSourcePairPrefixMachine [])

Internal support shared across GapCVP continuation modules.