OAI/Combinatorics/UniformKServer/RawControl.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniformKServer.RawControl.S line 15
2. def OAI.UniformKServer.RawControl.state line 17
3. def OAI.UniformKServer.RawControl.initial line 19
4. def OAI.UniformKServer.RawControl.trackingLabel line 21
5. def OAI.UniformKServer.RawControl.label line 23
6. def OAI.UniformKServer.RawControl.nextEntry line 28
7. def OAI.UniformKServer.RawControl.step line 31
8. theorem OAI.UniformKServer.RawControl.initial_state line 43
9. theorem OAI.UniformKServer.RawControl.nextEntry_state line 48
10. theorem OAI.UniformKServer.RawControl.label_state line 54

    Source documentation

    Local representation lemma: only the current causal selector value is needed.

    theorem label_state {n k : ℕ} (hk : 0<k) (T coins : List ℕ) (U : EpochShadow.Selector n k)
        (s : EpochControl.State n k) (r : Fin n)
        (hselect : trackingLabel k T coins (state s) r.val=(U s.filter.kept s.virtual.position r).val) :
        label k T coins (state s) r.val=(EpochControl.label hk U s r).val := by
    …

    Mentions: OAI.UniformKServer.EpochShadow.Selector, OAI.UniformKServer.EpochControl.State, OAI.UniformKServer.RawControl.trackingLabel, OAI.UniformKServer.RawControl.state, OAI.UniformKServer.RawControl.label, OAI.UniformKServer.EpochControl.label

11. theorem OAI.UniformKServer.RawControl.step_state line 68
12. theorem OAI.UniformKServer.RawControl.primitive_initial line 100
13. theorem OAI.UniformKServer.RawControl.primitive_tracking line 103
14. theorem OAI.UniformKServer.RawControl.primitive_label line 106
15. theorem OAI.UniformKServer.RawControl.primitive_nextEntry line 112
16. theorem OAI.UniformKServer.RawControl.primitive_step line 118