GapCVP proof, part 05, continuation 02

noncomputable def GapCVP.CNFSourcePairPrefixWorkerTotalCert.actualSourcePairPrefixComputable : BitTM CNFSourcePairPrefixWorkerTM.sourcePairPrefixOutput

GapCVP reduction support.

Equations

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

def GapCVP.SourceLatticeFormulaPreservation.tacticFormulaPreservationStepTac : Lean.ParserDescr

Executes the formulaPreservationStepTac machine-step simplifier.

Equations

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

def GapCVP.SourceLatticeFormulaPreservation.formulaPreservedOutput (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceLatticeFormulaPreservation.formulaPreservedOutput input = input ++ GapCVP.FormulaTotalCert.canonicalMachineOutput input

theorem GapCVP.SourceLatticeFormulaPreservation.formulaPreservedOutput_eq_expected (input : List Bool) : formulaPreservedOutput input = input ++ FormulaTotalCert.canonicalFormulaExpected input

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceLatticeDependentSectionComputation.tacticSourceMarkerStepTac : Lean.ParserDescr

Executes the sourceMarkerStepTac machine-step simplifier.

Equations

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

def GapCVP.SourceLatticeDependentSectionComputation.sourceMarkerRotatedOutput (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceLatticeDependentSectionComputation.sourceMarkerRotatedOutput input = match input.reverse with | [] => [false] | marker :: formula => marker :: formula.reverse

@[simp]

theorem GapCVP.SourceLatticeDependentSectionComputation.sourceMarkerRotatedOutput_append_marker (input : List Bool) (marker : Bool) : sourceMarkerRotatedOutput (input ++ [marker]) = marker :: input

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceLatticeDependentSectionComputation.validatedPreservedFormulaOutput : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.SourceLatticeDependentSectionComputation.validatedPreservedFormulaComputable : BitTM validatedPreservedFormulaOutput

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceLatticeNormalizedSectionSynthesis.normalizedRadiusPeek (stack : Fin 5) (present absent : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceLatticeNormalizedSectionSynthesis.normalizedRadiusPop (stack : Fin 5) (continuation : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceLatticeNormalizedSectionSynthesis.normalizedRadiusPop stack continuation = Turing.TM2.Stmt.pop stack (fun (x x_1 : Option Bool) => none) continuation

def GapCVP.SourceLatticeNormalizedSectionSynthesis.normalizedRadiusPush (stack : Fin 5) (continuation : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceLatticeNormalizedSectionSynthesis.normalizedRadiusPush stack continuation = Turing.TM2.Stmt.push stack (fun (x : Option Bool) => true) continuation

def GapCVP.SourceLatticeNormalizedSectionSynthesis.normalizedRadiusGoto (phase : Fin 7) : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceLatticeStructuralRadiusNumerator.tacticRadiusMarkerTailStepTac : Lean.ParserDescr

Executes the radiusMarkerTailStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.SourceLatticeStructuralRadiusNumerator.radiusMarkerTailComputable : Turing.TM2ComputableInPolyTime bitEncoding bitEncoding fun (input : List Bool) => input.tail

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceLatticeStructuralRationalRadius.sourceRationalNatCast_atomic (number : ℕ) : BinaryEncoding.encodeAtomic ↑number = BinaryEncoding.lengthPrefixedWord (Computability.encodeNat (4 * number ^ 2 + 2 * number + 1))

def GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusFailureStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 7) (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.SourceLatticeStructuralRationalRadiusTM.rationalRadiusMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusConfiguration (phase : Fin 7) (input base outer restore output : List Bool) : rationalRadiusMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusConfiguration phase input base outer restore output = { l := some phase, var := none, stk := ![input, base, outer, restore, output] }

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadiusMachine_init (input : List Bool) : Turing.initList rationalRadiusMachine input = rationalRadiusConfiguration 0 input [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceLatticeStructuralRationalRadiusTM.tacticRationalRadiusStepTac : Lean.ParserDescr

Executes the rationalRadiusStepTac machine-step simplifier.

Equations

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

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_marker_true_step (input base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 0 (true :: input) base outer restore output) = some (rationalRadiusConfiguration 1 input base outer restore (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_marker_false_step (input base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 0 (false :: input) base outer restore output) = some (rationalRadiusConfiguration 6 input base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_marker_missing_step (base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 0 [] base outer restore output) = some (rationalRadiusConfiguration 6 [] base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_scan_true_step (input base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 1 (true :: input) base outer restore output) = some (rationalRadiusConfiguration 1 input (true :: true :: base) (true :: true :: outer) restore (true :: true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_scan_false_step (input base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 1 (false :: input) base outer restore output) = some (rationalRadiusConfiguration 6 input base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_scan_finish (base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 1 [] base outer restore output) = some (rationalRadiusConfiguration 2 [] base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_outer_step (base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 2 [] base (true :: outer) restore output) = some (rationalRadiusConfiguration 3 [] base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_outer_finish (base restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 2 [] base [] restore output) = some (rationalRadiusConfiguration 5 [] base [] restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_copy_step (base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 3 [] (true :: base) outer restore output) = some (rationalRadiusConfiguration 3 [] base outer (true :: restore) (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_copy_finish (outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 3 [] [] outer restore output) = some (rationalRadiusConfiguration 4 [] [] outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_restore_step (base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 4 [] base outer (true :: restore) output) = some (rationalRadiusConfiguration 4 [] (true :: base) outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_restore_finish (base outer output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 4 [] base outer [] output) = some (rationalRadiusConfiguration 2 [] base outer [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_cleanup_base_step (base output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 5 [] (true :: base) [] [] output) = some (rationalRadiusConfiguration 5 [] base [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_cleanup_finish (output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 5 [] [] [] [] output) = some (Turing.haltList rationalRadiusMachine (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_failure_input_step (bit : Bool) (input base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 6 (bit :: input) base outer restore output) = some (rationalRadiusConfiguration 6 input base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_failure_base_step (bit : Bool) (base outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 6 [] (bit :: base) outer restore output) = some (rationalRadiusConfiguration 6 [] base outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_failure_outer_step (bit : Bool) (outer restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 6 [] [] (bit :: outer) restore output) = some (rationalRadiusConfiguration 6 [] [] outer restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_failure_restore_step (bit : Bool) (restore output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 6 [] [] [] (bit :: restore) output) = some (rationalRadiusConfiguration 6 [] [] [] restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_failure_output_step (bit : Bool) (output : List Bool) : rationalRadiusMachine.step (rationalRadiusConfiguration 6 [] [] [] [] (bit :: output)) = some (rationalRadiusConfiguration 6 [] [] [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceLatticeStructuralRationalRadiusTM.rationalRadius_failure_finish : rationalRadiusMachine.step (rationalRadiusConfiguration 6 [] [] [] [] []) = some (Turing.haltList rationalRadiusMachine [false])

Internal support shared across GapCVP continuation modules.