OAI/Combinatorics/UniformKServer/RuntimeCertificate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.RuntimeCertificate.Cert line 12
  2. def OAI.UniformKServer.RuntimeCertificate.has line 14
  3. def OAI.UniformKServer.RuntimeCertificate.B line 15
  4. def OAI.UniformKServer.RuntimeCertificate.item line 17
  5. def OAI.UniformKServer.RuntimeCertificate.row line 23
  6. def OAI.UniformKServer.RuntimeCertificate.node line 27
  7. def OAI.UniformKServer.RuntimeCertificate.verify line 30
  8. theorem OAI.UniformKServer.RuntimeCertificate.primitive_has line 36
  9. theorem OAI.UniformKServer.RuntimeCertificate.primitive_B line 38
  10. theorem OAI.UniformKServer.RuntimeCertificate.primitive_requestToken line 40
  11. theorem OAI.UniformKServer.RuntimeCertificate.primitive_initial line 42
  12. theorem OAI.UniformKServer.RuntimeCertificate.primitive_finishes line 45
  13. theorem OAI.UniformKServer.RuntimeCertificate.primitive_item line 49
  14. theorem OAI.UniformKServer.RuntimeCertificate.primitive_row line 64
  15. theorem OAI.UniformKServer.RuntimeCertificate.primitive_node line 67
  16. theorem OAI.UniformKServer.RuntimeCertificate.primitive_verify line 70
  17. theorem OAI.UniformKServer.RuntimeCertificate.has_iff line 91
  18. theorem OAI.UniformKServer.RuntimeCertificate.verify_iff line 94