OAI/GameTheory/SnakyTwentyOne/Cards/Height01Part01.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_0 line 8
  2. def OAI.SnakyPrototype.Certificate21.envelope_0 line 9
  3. theorem OAI.SnakyPrototype.Certificate21.row_works_0 line 10
  4. def OAI.SnakyPrototype.Certificate21.required_1 line 15
  5. def OAI.SnakyPrototype.Certificate21.envelope_1 line 16
  6. theorem OAI.SnakyPrototype.Certificate21.row_works_1 line 17
  7. def OAI.SnakyPrototype.Certificate21.required_2 line 22
  8. def OAI.SnakyPrototype.Certificate21.envelope_2 line 23
  9. theorem OAI.SnakyPrototype.Certificate21.row_works_2 line 24
  10. def OAI.SnakyPrototype.Certificate21.required_3 line 29
  11. def OAI.SnakyPrototype.Certificate21.envelope_3 line 30
  12. theorem OAI.SnakyPrototype.Certificate21.row_works_3 line 31
  13. def OAI.SnakyPrototype.Certificate21.required_4 line 36
  14. def OAI.SnakyPrototype.Certificate21.envelope_4 line 37
  15. theorem OAI.SnakyPrototype.Certificate21.row_works_4 line 38
  16. def OAI.SnakyPrototype.Certificate21.required_5 line 43
  17. def OAI.SnakyPrototype.Certificate21.envelope_5 line 44
  18. theorem OAI.SnakyPrototype.Certificate21.row_works_5 line 45
  19. def OAI.SnakyPrototype.Certificate21.height_0 line 50
  20. theorem OAI.SnakyPrototype.Certificate21.base_required_exact_0 line 51
  21. theorem OAI.SnakyPrototype.Certificate21.base_envelope_exact_0 line 52
  22. theorem OAI.SnakyPrototype.Certificate21.base_height_exact_0 line 53
  23. def OAI.SnakyPrototype.Certificate21.checked_0 line 54
  24. def OAI.SnakyPrototype.Certificate21.height_1 line 62
  25. theorem OAI.SnakyPrototype.Certificate21.base_required_exact_1 line 63
  26. theorem OAI.SnakyPrototype.Certificate21.base_envelope_exact_1 line 64
  27. theorem OAI.SnakyPrototype.Certificate21.base_height_exact_1 line 65
  28. def OAI.SnakyPrototype.Certificate21.checked_1 line 66
  29. def OAI.SnakyPrototype.Certificate21.height_2 line 74
  30. theorem OAI.SnakyPrototype.Certificate21.base_required_exact_2 line 75
  31. theorem OAI.SnakyPrototype.Certificate21.base_envelope_exact_2 line 76
  32. theorem OAI.SnakyPrototype.Certificate21.base_height_exact_2 line 77
  33. def OAI.SnakyPrototype.Certificate21.checked_2 line 78
  34. def OAI.SnakyPrototype.Certificate21.height_3 line 86
  35. theorem OAI.SnakyPrototype.Certificate21.base_required_exact_3 line 87
  36. theorem OAI.SnakyPrototype.Certificate21.base_envelope_exact_3 line 88
  37. theorem OAI.SnakyPrototype.Certificate21.base_height_exact_3 line 89
  38. def OAI.SnakyPrototype.Certificate21.checked_3 line 90
  39. def OAI.SnakyPrototype.Certificate21.height_4 line 98
  40. theorem OAI.SnakyPrototype.Certificate21.base_required_exact_4 line 99
  41. theorem OAI.SnakyPrototype.Certificate21.base_envelope_exact_4 line 100
  42. theorem OAI.SnakyPrototype.Certificate21.base_height_exact_4 line 101
  43. def OAI.SnakyPrototype.Certificate21.checked_4 line 102
  44. def OAI.SnakyPrototype.Certificate21.height_5 line 110
  45. theorem OAI.SnakyPrototype.Certificate21.base_required_exact_5 line 111
  46. theorem OAI.SnakyPrototype.Certificate21.base_envelope_exact_5 line 112
  47. theorem OAI.SnakyPrototype.Certificate21.base_height_exact_5 line 113
  48. def OAI.SnakyPrototype.Certificate21.checked_5 line 114