OAI/Combinatorics/UniformKServer/EpochFinite.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.EpochControl.Bounded line 13
2. theorem OAI.UniformKServer.EpochControl.bounded_initial line 17
3. theorem OAI.UniformKServer.EpochControl.bounded_step line 23
4. abbrev OAI.UniformKServer.EpochControl.BList line 46
5. instance OAI.UniformKServer.EpochControl.(instance at line 47) line 47
6. abbrev OAI.UniformKServer.EpochControl.Packed line 50
7. def OAI.UniformKServer.EpochControl.pack line 55
8. def OAI.UniformKServer.EpochControl.unpack line 66
9. theorem OAI.UniformKServer.EpochControl.unpack_pack line 70
10. instance OAI.UniformKServer.EpochControl.(instance at line 80) line 80
11. def OAI.UniformKServer.EpochControl.boundedStep line 88

    Source documentation

    A bounded-state one-epoch transducer. Neither its state bound nor its transition function contains a raw word or a request horizon.

    def boundedStep {n k : ℕ} (hk : 0 < k) (M : ℕ) (T : Selector n k)
        (s : {s : State n k // Bounded M s}) (r : Fin n) : {s : State n k // Bounded M s} :=
    …

    Mentions: OAI.UniformKServer.EpochControl.State, OAI.UniformKServer.EpochControl.Bounded