Numeric packed-step schedules -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.length_stepFormulaBlock_internal (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (atomIndex : ℕ) (hindex : atomIndex < stepAtomCount stateCount workCount T) : List.length (stepFormulaBlock caseCount stateCount workCount T configBase choiceWire available haltStateIndex kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt atomIndex) = stepFormulaSizeAt caseCount stateCount workCount T kindAt selectedAt choiceAt atomIndex

theorem Complexity.CircuitUnrolling.Serializer.length_stepFormulaGates_internal (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (stepFormulaGates caseCount stateCount workCount T configBase choiceWire available haltStateIndex kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = prefixSize (stepFormulaSizeAt caseCount stateCount workCount T kindAt selectedAt choiceAt) (stepAtomCount stateCount workCount T)

theorem Complexity.CircuitUnrolling.Serializer.length_stepPackedCopies_internal (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : List.length (stepPackedCopies caseCount stateCount workCount T available kindAt selectedAt choiceAt) = stepAtomCount stateCount workCount T

theorem Complexity.CircuitUnrolling.Serializer.getElem_stepPackedCopies_internal (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : Fin (stepAtomCount stateCount workCount T)) : (stepPackedCopies caseCount stateCount workCount T available kindAt selectedAt choiceAt)[↑atomIndex] = stepPackedCopyGate caseCount stateCount workCount T available kindAt selectedAt choiceAt ↑atomIndex

theorem Complexity.CircuitUnrolling.Serializer.length_stepSchedule_internal (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (stepSchedule caseCount stateCount workCount T configBase choiceWire available haltStateIndex kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = stepScheduleSize caseCount stateCount workCount T kindAt selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.stepFragment_eq_stepSchedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepFragment tm T configBase choiceWire available = stepSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (nextHaltStateIndex tm) (stepAtomKindAt tm T) (stepAtomStateIndexAt tm T) (stepAtomTapeIndexAt tm T) (stepAtomPositionAt tm T) (stepAtomSymbolIndexAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

theorem Complexity.CircuitUnrolling.Serializer.stepFragmentSize_eq_stepScheduleSize_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : stepFragmentSize tm T configBase choiceWire = stepScheduleSize (transitionCases tm).length (Fintype.card tm.Q) k T (stepAtomKindAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.stepOutputBase_eq_stepScheduleOutputBase_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepOutputBase tm T configBase choiceWire available = stepScheduleOutputBase (transitionCases tm).length (Fintype.card tm.Q) k T available (stepAtomKindAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.stepScheduleOutputRef_configIndex_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : stepScheduleOutputRef (transitionCases tm).length (Fintype.card tm.Q) k T available (stepAtomKindAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm) (configIndex tm T atom) = configWire tm T (stepOutputBase tm T configBase choiceWire available) atom