GapCVP proof, part 05, continuation 05

noncomputable def GapCVP.CNFFlatAdjacentRecordSwapTotalCert.flatAdjacentRecordSwapTimePolynomial : Polynomial ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFFlatAdjacentRecordSwapTotalCert.flatAdjacentRecordSwapTimePolynomial = 16 * Polynomial.X + 32

noncomputable def GapCVP.CNFFlatAdjacentRecordSwapTotalCert.flatAdjacentRecordTotalTrace (input : List Bool) : StateTransition.EvalsToInTime CNFFlatAdjacentRecordSwapTM.actualFlatAdjacentRecordSwapMachine.step (CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordConfiguration 0 input [] [] []) (some (Turing.haltList CNFFlatAdjacentRecordSwapTM.actualFlatAdjacentRecordSwapMachine (CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSwapOutput input))) (Polynomial.eval input.length flatAdjacentRecordSwapTimePolynomial)

GapCVP reduction support.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.CNFFlatAdjacentRecordSwapTotalCert.flatAdjacentRecordSwapComputable : BitTM CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSwapOutput

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatPhysicalBinaryAppendTM.flatPhysicalPrependComputedRecordOutput (worker : List Bool → List 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.CNFFlatPhysicalBinaryAppendTM.flatPhysicalPrependComputedRecordComputable {worker : List Bool → List Bool} (computer : BitTM worker) : BitTM (flatPhysicalPrependComputedRecordOutput worker)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFlatPhysicalBinaryAppendTM.flatPhysicalPrependComputedRecordOutput_eq (worker : List Bool → List Bool) (input : List Bool) : flatPhysicalPrependComputedRecordOutput worker input = BinaryEncoding.lengthPrefixedWord (worker input) ++ input

noncomputable def GapCVP.CNFFlatPhysicalBinaryAppendTM.pointwiseAppendComputable {first second : List Bool → List Bool} (firstComputer : BitTM first) (secondComputer : BitTM second) : BitTM fun (input : List Bool) => first input ++ second input

GapCVP reduction support.

Equations

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

def GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimumOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimumOutput_pair (first second : ℕ) (suffix : List Bool) : cappedUnaryMinimumOutput (CNFUnaryPairIndexTM.unarySourcePairWord first second ++ suffix) = List.replicate (min first second) true

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

Internal support shared across GapCVP continuation modules.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimumFailureStatement : Turing.TM2.Stmt (fun (x : Fin 3) => Bool) (Fin 4) (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.CNFCappedUnaryMinimumTM.actualCappedUnaryMinimumMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimumConfiguration (phase : Fin 4) (input first output : List Bool) : actualCappedUnaryMinimumMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFCappedUnaryMinimumTM.actualCappedUnaryMinimumMachine_init (input : List Bool) : Turing.initList actualCappedUnaryMinimumMachine input = cappedUnaryMinimumConfiguration 0 input [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFCappedUnaryMinimumTM.tacticCappedUnaryMinimumStepTac : Lean.ParserDescr

Executes the cappedUnaryMinimumStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_first_true (input first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 0 (true :: input) first output) = some (cappedUnaryMinimumConfiguration 0 input (true :: first) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_first_false (input first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 0 (false :: input) first output) = some (cappedUnaryMinimumConfiguration 1 input first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_first_missing (first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 0 [] first output) = some (cappedUnaryMinimumConfiguration 3 [] first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_second_true_counter (input first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 1 (true :: input) (true :: first) output) = some (cappedUnaryMinimumConfiguration 1 input first (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_second_true_empty (input output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 1 (true :: input) [] output) = some (cappedUnaryMinimumConfiguration 1 input [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_second_false (input first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 1 (false :: input) first output) = some (cappedUnaryMinimumConfiguration 2 input first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_second_missing (first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 1 [] first output) = some (cappedUnaryMinimumConfiguration 3 [] first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_success_input (bit : Bool) (input first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 2 (bit :: input) first output) = some (cappedUnaryMinimumConfiguration 2 input first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_success_first (bit : Bool) (first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 2 [] (bit :: first) output) = some (cappedUnaryMinimumConfiguration 2 [] first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_success_finish (output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 2 [] [] output) = some (Turing.haltList actualCappedUnaryMinimumMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_failure_input (bit : Bool) (input first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 3 (bit :: input) first output) = some (cappedUnaryMinimumConfiguration 3 input first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_failure_first (bit : Bool) (first output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 3 [] (bit :: first) output) = some (cappedUnaryMinimumConfiguration 3 [] first output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_failure_output (bit : Bool) (output : List Bool) : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 3 [] [] (bit :: output)) = some (cappedUnaryMinimumConfiguration 3 [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFCappedUnaryMinimumTM.cappedUnaryMinimum_failure_finish : actualCappedUnaryMinimumMachine.step (cappedUnaryMinimumConfiguration 3 [] [] []) = some (Turing.haltList actualCappedUnaryMinimumMachine [])

Internal support shared across GapCVP continuation modules.