GapCVP proof, part 06, continuation 03

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionDividendPrefixTrace (count : ℕ) (valid : Bool) (remaining archive dividend modulus modulusScratch quotient residueStack output : List Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 0 valid (List.replicate count true ++ false :: remaining) archive dividend modulus modulusScratch quotient residueStack output) (some (sourceUnaryDivisionConfiguration 1 valid remaining (false :: (List.replicate count true ++ archive)) (List.replicate count true ++ dividend) modulus modulusScratch quotient residueStack output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionDividendMissingTrace (count : ℕ) (valid : Bool) (archive dividend modulus modulusScratch quotient residueStack output : List Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 0 valid (List.replicate count true) archive dividend modulus modulusScratch quotient residueStack output) (some (sourceUnaryDivisionConfiguration 2 false [] (List.replicate count true ++ archive) (List.replicate count true ++ dividend) modulus modulusScratch quotient residueStack output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionModulusPrefixTrace (count : ℕ) (valid : Bool) (remaining archive dividend modulus modulusScratch quotient residueStack output : List Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 1 valid (List.replicate count true ++ false :: remaining) archive dividend modulus modulusScratch quotient residueStack output) (some (sourceUnaryDivisionConfiguration 2 valid remaining (false :: (List.replicate count true ++ archive)) dividend (List.replicate count true ++ modulus) modulusScratch quotient residueStack output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionModulusMissingTrace (count : ℕ) (valid : Bool) (archive dividend modulus modulusScratch quotient residueStack output : List Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 1 valid (List.replicate count true) archive dividend modulus modulusScratch quotient residueStack output) (some (sourceUnaryDivisionConfiguration 2 false [] (List.replicate count true ++ archive) dividend (List.replicate count true ++ modulus) modulusScratch quotient residueStack output)) (count + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionSuffixTrace (source archive dividend modulus modulusScratch quotient residueStack output : List Bool) (valid : Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 2 valid source archive dividend modulus modulusScratch quotient residueStack output) (some (sourceUnaryDivisionConfiguration 3 valid [] (source.reverse ++ archive) dividend modulus modulusScratch quotient residueStack output)) (source.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionRestoreSourceTrace (archive dividend modulus modulusScratch quotient residueStack output : List Bool) (valid : Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 3 valid [] archive dividend modulus modulusScratch quotient residueStack output) (some (sourceUnaryDivisionConfiguration 4 valid [] [] dividend modulus modulusScratch quotient residueStack (false :: (archive.reverse ++ output)))) (archive.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionCleanupTrace (modulusCount scratchCount dividendCount residueCount : ℕ) (valid : Bool) (output : List Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 9 valid [] [] (List.replicate dividendCount true) (List.replicate modulusCount true) (List.replicate scratchCount true) [] (List.replicate residueCount true) output) (some (Turing.haltList sourceUnaryDivisionMachine output)) (modulusCount + scratchCount + dividendCount + residueCount + 4)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionModuloTrace (modulus quotientCount remainder previous : ℕ) (hremainder : remainder < modulus) (output : List Bool) : StateTransition.EvalsToInTime sourceUnaryDivisionMachine.step (sourceUnaryDivisionConfiguration 5 true [] [] (List.replicate (modulus * quotientCount + remainder) true) (List.replicate modulus true) [] (List.replicate previous true) [] output) (some (Turing.haltList sourceUnaryDivisionMachine (List.replicate (quotientCount + previous) true ++ false :: (List.replicate remainder true ++ output)))) (quotientCount * (2 * modulus + 3) + 4 * modulus + previous + 12)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionQuery_reverse (dividend modulus : ℕ) (source : List Bool) : (sourceUnaryDivisionQuery dividend modulus source).reverse = source.reverse ++ false :: (List.replicate modulus true ++ false :: List.replicate dividend true)

Internal support shared across GapCVP continuation modules.