OAI/Combinatorics/UniformKServer/RawArithmetic.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

A primitive-recursive nonnegative rational presentation for the uniform finite certificate search. Denominators are stored minus one, so every bit string denotes a valid nonnegative rational; there is no division oracle.

  1. abbrev OAI.UniformKServer.RawArithmetic.Q line 12
  2. def OAI.UniformKServer.RawArithmetic.value line 14
  3. def OAI.UniformKServer.RawArithmetic.natural line 15
  4. def OAI.UniformKServer.RawArithmetic.add line 16
  5. def OAI.UniformKServer.RawArithmetic.mul line 17
  6. def OAI.UniformKServer.RawArithmetic.divide line 18
  7. def OAI.UniformKServer.RawArithmetic.le line 19
  8. instance OAI.UniformKServer.RawArithmetic.(instance at line 20) line 20
  9. theorem OAI.UniformKServer.RawArithmetic.denominator line 22
  10. theorem OAI.UniformKServer.RawArithmetic.value_natural line 26
  11. theorem OAI.UniformKServer.RawArithmetic.value_nonneg line 27
  12. theorem OAI.UniformKServer.RawArithmetic.value_add line 28
  13. theorem OAI.UniformKServer.RawArithmetic.value_mul line 35
  14. theorem OAI.UniformKServer.RawArithmetic.value_divide line 39
  15. theorem OAI.UniformKServer.RawArithmetic.le_iff line 43
  16. theorem OAI.UniformKServer.RawArithmetic.eq_present line 48
  17. theorem OAI.UniformKServer.RawArithmetic.primitive_natural line 59
  18. theorem OAI.UniformKServer.RawArithmetic.primitive_add line 60
  19. theorem OAI.UniformKServer.RawArithmetic.primitive_mul line 65
  20. theorem OAI.UniformKServer.RawArithmetic.primitive_divide line 69
  21. theorem OAI.UniformKServer.RawArithmetic.primitive_le line 73