OAI/Combinatorics/UniformKServer/RawTable.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RawTable.history line 13
  2. def OAI.UniformKServer.RawTable.key line 15
  3. def OAI.UniformKServer.RawTable.entry line 16
  4. def OAI.UniformKServer.RawTable.dist line 17
  5. abbrev OAI.UniformKServer.RawTable.PathState line 18
  6. def OAI.UniformKServer.RawTable.pathStep line 19
  7. def OAI.UniformKServer.RawTable.path line 23
  8. def OAI.UniformKServer.RawTable.term line 25
  9. def OAI.UniformKServer.RawTable.total line 29
  10. def OAI.UniformKServer.RawTable.expected line 31
  11. def OAI.UniformKServer.RawTable.cost line 33
  12. theorem OAI.UniformKServer.RawTable.primitive_natural line 38
  13. theorem OAI.UniformKServer.RawTable.primitive_add line 40
  14. theorem OAI.UniformKServer.RawTable.primitive_mul line 42
  15. theorem OAI.UniformKServer.RawTable.primitive_divide line 44
  16. theorem OAI.UniformKServer.RawTable.primitive_words line 46
  17. theorem OAI.UniformKServer.RawTable.primitive_upto line 48
  18. theorem OAI.UniformKServer.RawTable.primitive_sum line 50
  19. theorem OAI.UniformKServer.RawTable.primitive_history line 53
  20. theorem OAI.UniformKServer.RawTable.primitive_key line 55
  21. theorem OAI.UniformKServer.RawTable.primitive_entry line 58
  22. theorem OAI.UniformKServer.RawTable.primitive_dist line 61
  23. theorem OAI.UniformKServer.RawTable.primitive_pathStep line 64
  24. theorem OAI.UniformKServer.RawTable.primitive_path line 68
  25. theorem OAI.UniformKServer.RawTable.primitive_term line 79
  26. theorem OAI.UniformKServer.RawTable.primitive_total line 85
  27. theorem OAI.UniformKServer.RawTable.primitive_expected line 92
  28. theorem OAI.UniformKServer.RawTable.primitive_cost line 98