Numeric next-atom schedules -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.length_nextHaltedOrSchedule_internal (haltWire available oldWire : ℕ) (nextSchedule : CircuitCode.RawCircuit) : List.length (nextHaltedOrSchedule haltWire available oldWire nextSchedule) = nextHaltedOrScheduleSize (List.length nextSchedule)

theorem Complexity.CircuitUnrolling.Serializer.length_nextStateFormulaSchedule_internal (caseCount stateCount workCount T configBase choiceWire available stateIndex haltStateIndex : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextStateFormulaSchedule caseCount stateCount workCount T configBase choiceWire available stateIndex haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextStateFormulaScheduleSize caseCount workCount T selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.length_nextHeadFormulaSchedule_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target haltStateIndex : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextHeadFormulaSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex target haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextHeadFormulaScheduleSize caseCount workCount T selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.length_nextCellCopySchedule_internal (stateCount tapeCount T configBase tapeIndex position symbolIndex : ℕ) : List.length (nextCellCopySchedule stateCount tapeCount T configBase tapeIndex position symbolIndex) = nextCellCopyScheduleSize

theorem Complexity.CircuitUnrolling.Serializer.length_nextWrittenCellFormulaSchedule_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex haltStateIndex : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextWrittenCellFormulaSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextWrittenCellFormulaScheduleSize caseCount workCount T selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.length_nextFormulaSchedule_internal (caseCount stateCount workCount T configBase choiceWire available atomKind stateIndex tapeIndex position symbolIndex haltStateIndex : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextFormulaSchedule caseCount stateCount workCount T configBase choiceWire available atomKind stateIndex tapeIndex position symbolIndex haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextFormulaScheduleSize caseCount workCount T atomKind selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextStateFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (state : tm.Q) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.state state)) = nextStateFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (stateIndex tm state) (nextHaltStateIndex tm) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextHeadFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.head tape target)) = nextHeadFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (↑tape.index) (↑target) (nextHaltStateIndex tm) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextInputCellFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (position : Fin (T + 2)) (symbol : Γ) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.cell TapeSlot.input position symbol)) = nextCellCopySchedule (Fintype.card tm.Q) (k + 2) T configBase ↑TapeSlot.input.index ↑position ↑(symbolIndex symbol)

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextWritableMarkerFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) (hposition : ↑position = 0) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.cell tape.toTapeSlot position symbol)) = nextCellCopySchedule (Fintype.card tm.Q) (k + 2) T configBase ↑tape.toTapeSlot.index ↑position ↑(symbolIndex symbol)

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextWrittenCellFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) (hposition : ↑position ≠ 0) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.cell tape.toTapeSlot position symbol)) = nextWrittenCellFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (↑tape.toTapeSlot.index) (↑position) (↑(symbolIndex symbol)) (nextHaltStateIndex tm) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire atom) = nextFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (nextAtomKind atom) (nextAtomStateIndex tm atom) (nextAtomTapeIndex atom) (nextAtomPosition atom) (nextAtomSymbolIndex atom) (nextHaltStateIndex tm) (nextAtomEffectSelectedAt tm atom) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

theorem Complexity.CircuitUnrolling.Serializer.size_nextFormula_eq_scheduleSize_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) (atom : ConfigAtom tm T) : (nextFormula tm T configBase choiceWire atom).size = nextFormulaScheduleSize (transitionCases tm).length k T (nextAtomKind atom) (nextAtomEffectSelectedAt tm atom) (effectCaseChoiceAt tm)