OAI/Combinatorics/UniformKServer/ControllerEpoch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.TapeController.cut_expected line 20

   Source documentation

   Deterministic evolution under the already loaded epoch tape, up to the next raw-block boundary. No future requests are needed by the controller.

   theorem cut_expected (z : State n k M R b) (s : Configuration n k)
       (coins : Tape k M b) (w : List (Fin n)) :
       let parts := cut k R z.localState.val.seen z.completed.val w
   …

   Mentions: OAI.UniformKServer.TapeController.State, OAI.UniformKServer.Configuration, OAI.UniformKServer.TapeController.Tape