OAI/Combinatorics/UniformKServer/PrimitiveRules.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Composition rules for the explicit primitive-recursive constructor. fun_prop only builds terms from the listed proved closure lemmas.

  1. theorem OAI.UniformKServer.PrimitiveRules.add line 17
  2. theorem OAI.UniformKServer.PrimitiveRules.mul line 19
  3. theorem OAI.UniformKServer.PrimitiveRules.sub line 21
  4. theorem OAI.UniformKServer.PrimitiveRules.pow line 23
  5. theorem OAI.UniformKServer.PrimitiveRules.div line 25
  6. theorem OAI.UniformKServer.PrimitiveRules.eqs line 27
  7. theorem OAI.UniformKServer.PrimitiveRules.les line 29
  8. theorem OAI.UniformKServer.PrimitiveRules.lts line 31
  9. theorem OAI.UniformKServer.PrimitiveRules.encoded line 33
  10. theorem OAI.UniformKServer.PrimitiveRules.decoded line 35
  11. theorem OAI.UniformKServer.PrimitiveRules.length line 37
  12. theorem OAI.UniformKServer.PrimitiveRules.range line 39
  13. theorem OAI.UniformKServer.PrimitiveRules.getD line 41
  14. theorem OAI.UniformKServer.PrimitiveRules.set line 43
  15. theorem OAI.UniformKServer.PrimitiveRules.append line 46
  16. theorem OAI.UniformKServer.PrimitiveRules.cons line 48
  17. theorem OAI.UniformKServer.PrimitiveRules.map line 50
  18. theorem OAI.UniformKServer.PrimitiveRules.flatMap line 53
  19. theorem OAI.UniformKServer.PrimitiveRules.foldl line 56
  20. theorem OAI.UniformKServer.PrimitiveRules.bool_and line 59
  21. theorem OAI.UniformKServer.PrimitiveRules.bool_or line 61
  22. theorem OAI.UniformKServer.PrimitiveRules.bool_not line 63
  23. theorem OAI.UniformKServer.PrimitiveRules.bool_all line 65
  24. example OAI.UniformKServer.PrimitiveRules.(example at line 74) line 74
  25. example OAI.UniformKServer.PrimitiveRules.(example at line 75) line 75