Numeric schedules for atomic transition formulas -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_headAtCellFormula_eq_gate_internal {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (tape : TapeSlot k) (position : Fin (T + 2)) : BoolFormula.compileRaw available (headAtCellFormula tm T configBase tape position) = [headAtCellFormulaGate (Fintype.card tm.Q) T configBase ↑tape.index ↑position]

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_haltedOrFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (oldValue nextValue : BoolFormula) : BoolFormula.compileRaw available (haltedOrFormula tm T configBase oldValue nextValue) = haltedOrSchedule (configWire tm T configBase (ConfigAtom.state tm.qhalt)) available (BoolFormula.compileRaw (available + 1) oldValue) (BoolFormula.compileRaw (available + oldValue.size + 4) nextValue)