OAI/Combinatorics/UniformKServer/SideFiniteInput.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Actual posterior/core inputs in a finite reveal law. Conditions describe the held, measurable data, not a movement conclusion. Empty and null-fiber cases still use the zero conventions of the conditional kernel.

  1. structure OAI.UniformKServer.SideFiniteInput.Data line 19
  2. def OAI.UniformKServer.SideFiniteInput.post line 40
  3. def OAI.UniformKServer.SideFiniteInput.activeFlag line 43
  4. def OAI.UniformKServer.SideFiniteInput.input line 45
  5. def OAI.UniformKServer.SideFiniteInput.star line 48
  6. def OAI.UniformKServer.SideFiniteInput.oldMask line 52
  7. def OAI.UniformKServer.SideFiniteInput.changes line 55
  8. def OAI.UniformKServer.SideFiniteInput.tracker line 58
  9. def OAI.UniformKServer.SideFiniteInput.prepared line 62
  10. theorem OAI.UniformKServer.SideFiniteInput.post_range line 66
  11. theorem OAI.UniformKServer.SideFiniteInput.flag_supported line 71
  12. theorem OAI.UniformKServer.SideFiniteInput.input_nonneg line 76
  13. theorem OAI.UniformKServer.SideFiniteInput.input_supported line 79
  14. theorem OAI.UniformKServer.SideFiniteInput.star_supported_old line 84
  15. theorem OAI.UniformKServer.SideFiniteInput.star_supported_new line 89
  16. theorem OAI.UniformKServer.SideFiniteInput.valid_input line 94
  17. theorem OAI.UniformKServer.SideFiniteInput.errors line 104
  18. theorem OAI.UniformKServer.SideFiniteInput.tracker_state line 112
  19. theorem OAI.UniformKServer.SideFiniteInput.step line 115
  20. theorem OAI.UniformKServer.SideFiniteInput.refining line 120
  21. theorem OAI.UniformKServer.SideFiniteInput.input_measurable line 126
  22. theorem OAI.UniformKServer.SideFiniteInput.star_measurable line 135
  23. theorem OAI.UniformKServer.SideFiniteInput.tracker_measurable line 144