GapCVP proof, part 05, continuation 04

noncomputable def GapCVP.SourceCanonicalUnaryGridIndexTM.sourceCanonicalUnaryGridIndexComputable : BitTM sourceCanonicalUnaryGridIndexOutput

GapCVP reduction support.

Equations

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

def GapCVP.SourceOriginalSourcePreservingTM.originalSourcePreservingOutput (f : List Bool → List Bool) (input : List Bool) : List Bool

Append the original input after the computed output, separated by a false bit.

Equations

• GapCVP.SourceOriginalSourcePreservingTM.originalSourcePreservingOutput f input = f input ++ false :: input

def GapCVP.SourceOriginalSourcePreservingTM.tacticOriginalSourcePreservationStepTac : Lean.ParserDescr

Executes the originalSourcePreservationStepTac machine-step simplifier.

Equations

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

noncomputable def GapCVP.SourceOriginalSourcePreservingTM.originalSourcePreservingComputable {f : List Bool → List Bool} (computer : BitTM f) : BitTM (originalSourcePreservingOutput f)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFGuardedSourceDescriptorRotationBoundedFoldTM.guardedRotation_readUnaryPrefix_some_reconstruct (input : List Bool) (count : ℕ) (tail : List Bool) (hread : BinaryEncoding.readUnaryPrefix input = some (count, tail)) : input = List.replicate count true ++ false :: tail

theorem GapCVP.CNFGuardedSourceDescriptorRotationBoundedFoldTM.guardedRotation_readLengthPrefixedWord_some_reconstruct (input payload suffix : List Bool) (hread : BinaryEncoding.readLengthPrefixedWord input = some (payload, suffix)) : input = BinaryEncoding.lengthPrefixedWord payload ++ suffix

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSwapOutput (input : List Bool) : List Bool

Swap the first two length-prefixed records while preserving the suffix.

Equations

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

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSwapOutput_records (first second suffix : List Bool) : flatAdjacentRecordSwapOutput (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = BinaryEncoding.lengthPrefixedWord second ++ BinaryEncoding.lengthPrefixedWord first ++ suffix

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSwapOutput_length_le (input : List Bool) : (flatAdjacentRecordSwapOutput input).length ≤ input.length

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordFirstPrefixStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordFirstPayloadStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSecondPrefixStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSecondPayloadStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordRestoreFirstStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordRestoreSecondStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordFailureStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 7) (Option Bool)

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.CNFFlatAdjacentRecordSwapTM.actualFlatAdjacentRecordSwapMachine : Turing.FinTM2

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordConfiguration (phase : Fin 7) (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.Cfg

GapCVP reduction support.

Equations

• GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordConfiguration phase input first second counter = { l := some phase, var := none, stk := ![input, first, second, counter] }

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.actualFlatAdjacentRecordSwapMachine_init (input : List Bool) : Turing.initList actualFlatAdjacentRecordSwapMachine input = flatAdjacentRecordConfiguration 0 input [] [] []

def GapCVP.CNFFlatAdjacentRecordSwapTM.tacticFlatAdjacentRecordStepTac : Lean.ParserDescr

Executes the flatAdjacentRecordStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_firstPrefix_true (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 0 (true :: input) first second counter) = some (flatAdjacentRecordConfiguration 0 input (true :: first) second (true :: counter))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_firstPrefix_false (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 0 (false :: input) first second counter) = some (flatAdjacentRecordConfiguration 1 input (false :: first) second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_firstPrefix_missing (first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 0 [] first second counter) = some (flatAdjacentRecordConfiguration 6 [] first second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_firstPayload_step (bit : Bool) (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 1 (bit :: input) first second (true :: counter)) = some (flatAdjacentRecordConfiguration 1 input (bit :: first) second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_firstPayload_missing (first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 1 [] first second (true :: counter)) = some (flatAdjacentRecordConfiguration 6 [] first second (true :: counter))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_firstPayload_finish (input first second : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 1 input first second []) = some (flatAdjacentRecordConfiguration 2 input first second [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_secondPrefix_true (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 2 (true :: input) first second counter) = some (flatAdjacentRecordConfiguration 2 input first (true :: second) (true :: counter))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_secondPrefix_false (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 2 (false :: input) first second counter) = some (flatAdjacentRecordConfiguration 3 input first (false :: second) counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_secondPrefix_missing (first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 2 [] first second counter) = some (flatAdjacentRecordConfiguration 6 [] first second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_secondPayload_step (bit : Bool) (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 3 (bit :: input) first second (true :: counter)) = some (flatAdjacentRecordConfiguration 3 input first (bit :: second) counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_secondPayload_missing (first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 3 [] first second (true :: counter)) = some (flatAdjacentRecordConfiguration 6 [] first second (true :: counter))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_secondPayload_finish (input first second : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 3 input first second []) = some (flatAdjacentRecordConfiguration 4 input first second [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_restoreFirst_step (bit : Bool) (input first second : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 4 input (bit :: first) second []) = some (flatAdjacentRecordConfiguration 4 (bit :: input) first second [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_restoreFirst_finish (input second : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 4 input [] second []) = some (flatAdjacentRecordConfiguration 5 input [] second [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_restoreSecond_step (bit : Bool) (input second : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 5 input [] (bit :: second) []) = some (flatAdjacentRecordConfiguration 5 (bit :: input) [] second [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_restoreSecond_finish (input : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 5 input [] [] []) = some (Turing.haltList actualFlatAdjacentRecordSwapMachine input)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_failure_input (bit : Bool) (input first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 6 (bit :: input) first second counter) = some (flatAdjacentRecordConfiguration 6 input first second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_failure_first (bit : Bool) (first second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 6 [] (bit :: first) second counter) = some (flatAdjacentRecordConfiguration 6 [] first second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_failure_second (bit : Bool) (second counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 6 [] [] (bit :: second) counter) = some (flatAdjacentRecordConfiguration 6 [] [] second counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_failure_counter (bit : Bool) (counter : List Bool) : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 6 [] [] [] (bit :: counter)) = some (flatAdjacentRecordConfiguration 6 [] [] [] counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecord_failure_finish : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 6 [] [] [] []) = some (Turing.haltList actualFlatAdjacentRecordSwapMachine [])

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFFlatAdjacentRecordSwapTotalCert.flatAdjacent_readLengthPrefixedWord_missing (count : ℕ) : BinaryEncoding.readLengthPrefixedWord (List.replicate count true) = none

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFFlatAdjacentRecordSwapTotalCert.flatAdjacent_readLengthPrefixedWord_short (payload : List Bool) (extra : ℕ) : BinaryEncoding.readLengthPrefixedWord (List.replicate (payload.length + extra + 1) true ++ false :: payload) = none

Internal support shared across GapCVP continuation modules.