OAI/Combinatorics/UniformKServer/RawFallback.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RawFallback.endpoint line 14
  2. def OAI.UniformKServer.RawFallback.choose line 16
  3. def OAI.UniformKServer.RawFallback.label line 18
  4. def OAI.UniformKServer.RawFallback.nextMarked line 20
  5. def OAI.UniformKServer.RawFallback.nextSeen line 22
  6. theorem OAI.UniformKServer.RawFallback.endpoint_bits line 25
  7. theorem OAI.UniformKServer.RawFallback.choose_bits line 29
  8. theorem OAI.UniformKServer.RawFallback.label_bits line 36
  9. theorem OAI.UniformKServer.RawFallback.nextSeen_bits line 47
  10. theorem OAI.UniformKServer.RawFallback.step_bits line 52
  11. theorem OAI.UniformKServer.RawFallback.primitive_endpoint line 72
  12. theorem OAI.UniformKServer.RawFallback.primitive_choose line 75
  13. theorem OAI.UniformKServer.RawFallback.primitive_label line 80
  14. theorem OAI.UniformKServer.RawFallback.primitive_nextMarked line 85
  15. theorem OAI.UniformKServer.RawFallback.primitive_nextSeen line 90