Packed-step generator soundness

Soundness proofs for the compositional formula and delayed-copy routines used by one direct-unrolling transition step.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateFormulas_sound_internal {k : ℕ} (tm : NTM k) : (emitStepStateFormulas tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeFormulas_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitStepHeadTapeFormulas tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellPosition_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitStepImmutableCellPosition tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellPosition_sound_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) : (emitStepWritableCellPosition tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeFormulas_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitStepCellTapeFormulas tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepFormulas_sound_internal {k : ℕ} (tm : NTM k) : (emitStepFormulas tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateCopies_sound_internal {k : ℕ} (tm : NTM k) : (emitStepStateCopies tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeCopies_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitStepHeadTapeCopies tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellCopies_sound_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) : (emitStepWritableCellCopies tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeCopies_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitStepCellTapeCopies tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepPackedCopies_sound_internal {k : ℕ} (tm : NTM k) : (emitStepPackedCopies tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_sound_internal {k : ℕ} (tm : TM k) : (emitStep tm).Sound