GapCVP proof, part 06, continuation 02

noncomputable def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationComputable : BitTM sourceUnaryIntegerMultiplicationOutput

GapCVP reduction support.

Equations

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

def GapCVP.SourceMixedRadixPreservedFourFamilyRecordTM.sourcePreservedPhysicalAtomicDescriptorOutput (atom : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceMixedRadixPreservedFourFamilyRecordTM.sourcePreservedPhysicalAtomicDescriptorComputable {atom : List Bool → List Bool} (computer : BitTM atom) : BitTM (sourcePreservedPhysicalAtomicDescriptorOutput atom)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceMixedRadixPreservedFourFamilyRecordTM.sourcePreservedPhysicalAtomicDescriptorOutput_eq (atom : List Bool → List Bool) (input : List Bool) : sourcePreservedPhysicalAtomicDescriptorOutput atom input = SourceWholeOutputValidBranchRecordTM.sourceFlatAtomicDescriptor (atom input) ++ false :: input

structure GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.SourceUnaryDivisionState : Type

Internal support shared across GapCVP continuation modules.

• valid : Bool

  Whether the encoded division input is valid.

• current : Option Bool

  The current scanned bit, when present.

@[instance_reducible]

instance GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.instFintypeSourceUnaryDivisionState : Fintype SourceUnaryDivisionState

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionDividendStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionModulusStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionArchiveSuffixStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionRestoreSourceStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionDispatchStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionMatchStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionRestoreModulusStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionEmitRemainderStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionEmitQuotientStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionCleanupModulusStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionCleanupScratchStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionCleanupDividendStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionCleanupPartialStatement : Turing.TM2.Stmt (fun (x : Fin 8) => Bool) (Fin 13) SourceUnaryDivisionState

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionConfiguration (phase : Fin 13) (valid : Bool) (input archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionMachine_init (input : List Bool) : Turing.initList sourceUnaryDivisionMachine input = sourceUnaryDivisionConfiguration 0 true input [] [] [] [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.tacticSourceUnaryDivisionStepTac : Lean.ParserDescr

Executes the sourceUnaryDivisionStepTac machine-step simplifier.

Equations

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

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_dividend_true (valid : Bool) (input archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 0 valid (true :: input) archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 0 valid input (true :: archive) (true :: dividend) modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_dividend_false (valid : Bool) (input archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 0 valid (false :: input) archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 1 valid input (false :: archive) dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_dividend_missing (valid : Bool) (archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 0 valid [] archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 2 false [] archive dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_modulus_true (valid : Bool) (input archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 1 valid (true :: input) archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 1 valid input (true :: archive) dividend (true :: modulus) modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_modulus_false (valid : Bool) (input archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 1 valid (false :: input) archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 2 valid input (false :: archive) dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_modulus_missing (valid : Bool) (archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 1 valid [] archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 2 false [] archive dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_suffix_step (valid bit : Bool) (input archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 2 valid (bit :: input) archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 2 valid input (bit :: archive) dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_suffix_finish (valid : Bool) (archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 2 valid [] archive dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 3 valid [] archive dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_restoreSource_step (valid bit : Bool) (archive dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 3 valid [] (bit :: archive) dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 3 valid [] archive dividend modulus modulusScratch quotient residueStack (bit :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_restoreSource_finish (valid : Bool) (dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 3 valid [] [] dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 4 valid [] [] dividend modulus modulusScratch quotient residueStack (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_dispatch_valid (modulusTail dividend modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 4 true [] [] dividend (true :: modulusTail) modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 5 true [] [] dividend (true :: modulusTail) modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_dispatch_zero (dividend modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 4 true [] [] dividend [] modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 9 true [] [] dividend [] modulusScratch quotient residueStack (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_dispatch_invalid (dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 4 false [] [] dividend modulus modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 9 false [] [] dividend modulus modulusScratch quotient residueStack (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_match_step (valid : Bool) (dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 5 valid [] [] (true :: dividend) (true :: modulus) modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 5 valid [] [] dividend modulus (true :: modulusScratch) quotient (true :: residueStack) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_match_full (valid : Bool) (dividend modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 5 valid [] [] dividend [] modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 6 valid [] [] dividend [] modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_match_partial (valid : Bool) (modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 5 valid [] [] [] (true :: modulus) modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 7 valid [] [] [] (true :: modulus) modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_restoreModulus_step (valid : Bool) (dividend modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 6 valid [] [] dividend modulus (true :: modulusScratch) quotient (true :: residueStack) output) = some (sourceUnaryDivisionConfiguration 6 valid [] [] dividend (true :: modulus) modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_restoreModulus_finish (valid : Bool) (dividend modulus quotient output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 6 valid [] [] dividend modulus [] quotient [] output) = some (sourceUnaryDivisionConfiguration 5 valid [] [] dividend modulus [] (true :: quotient) [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_emitRemainder_step (valid : Bool) (modulus modulusScratch quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 7 valid [] [] [] modulus modulusScratch quotient (true :: residueStack) output) = some (sourceUnaryDivisionConfiguration 7 valid [] [] [] modulus modulusScratch quotient residueStack (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_emitRemainder_finish (valid : Bool) (modulus modulusScratch quotient output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 7 valid [] [] [] modulus modulusScratch quotient [] output) = some (sourceUnaryDivisionConfiguration 8 valid [] [] [] modulus modulusScratch quotient [] (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_emitQuotient_step (valid : Bool) (modulus modulusScratch quotient output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 8 valid [] [] [] modulus modulusScratch (true :: quotient) [] output) = some (sourceUnaryDivisionConfiguration 8 valid [] [] [] modulus modulusScratch quotient [] (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_emitQuotient_finish (valid : Bool) (modulus modulusScratch output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 8 valid [] [] [] modulus modulusScratch [] [] output) = some (sourceUnaryDivisionConfiguration 9 valid [] [] [] modulus modulusScratch [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupModulus_step (valid : Bool) (modulus modulusScratch dividend quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 9 valid [] [] dividend (true :: modulus) modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 9 valid [] [] dividend modulus modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupModulus_finish (valid : Bool) (modulusScratch dividend quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 9 valid [] [] dividend [] modulusScratch quotient residueStack output) = some (sourceUnaryDivisionConfiguration 10 valid [] [] dividend [] modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupScratch_step (valid : Bool) (modulusScratch dividend quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 10 valid [] [] dividend [] (true :: modulusScratch) quotient residueStack output) = some (sourceUnaryDivisionConfiguration 10 valid [] [] dividend [] modulusScratch quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupScratch_finish (valid : Bool) (dividend quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 10 valid [] [] dividend [] [] quotient residueStack output) = some (sourceUnaryDivisionConfiguration 11 valid [] [] dividend [] [] quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupDividend_step (valid : Bool) (dividend quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 11 valid [] [] (true :: dividend) [] [] quotient residueStack output) = some (sourceUnaryDivisionConfiguration 11 valid [] [] dividend [] [] quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupDividend_finish (valid : Bool) (quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 11 valid [] [] [] [] [] quotient residueStack output) = some (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupPartial_step (valid : Bool) (quotient residueStack output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] quotient (true :: residueStack) output) = some (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] quotient residueStack output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivision_cleanupPartial_finish (valid : Bool) (output : List Bool) : sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] [] [] output) = some (Turing.haltList sourceUnaryDivisionMachine output)

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionQuery (dividend modulus : ℕ) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionQuery dividend modulus source = List.replicate dividend true ++ false :: (List.replicate modulus true ++ false :: source)

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionOutput_valid (dividend modulus : ℕ) (source : List Bool) (hmodulus : 0 < modulus) : sourceUnaryDivisionOutput (sourceUnaryDivisionQuery dividend modulus source) = List.replicate (dividend / modulus) true ++ false :: (List.replicate (dividend % modulus) true ++ false :: sourceUnaryDivisionQuery dividend modulus source)