OAI/GameTheory/SnakyTwentyOne/Cards/Height19Part01.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_694_i0 line 21
  2. def OAI.SnakyPrototype.Certificate21.envelope_694_i0 line 22
  3. def OAI.SnakyPrototype.Certificate21.childrenC_694_i0 line 23
  4. def OAI.SnakyPrototype.Certificate21.childrenD_694_i0 line 24
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_694_i0 line 25
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_694_i0 line 26
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_694_i0 line 27
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_694_i0 line 28
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_694_i0 line 29
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_694_i0 line 37
  11. def OAI.SnakyPrototype.Certificate21.required_694_i1 line 42
  12. def OAI.SnakyPrototype.Certificate21.envelope_694_i1 line 43
  13. def OAI.SnakyPrototype.Certificate21.childrenC_694_i1 line 44
  14. def OAI.SnakyPrototype.Certificate21.childrenD_694_i1 line 45
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_694_i1 line 46
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_694_i1 line 47
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_694_i1 line 48
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_694_i1 line 49
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_694_i1 line 50
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_694_i1 line 57
  21. def OAI.SnakyPrototype.Certificate21.required_694 line 62
  22. def OAI.SnakyPrototype.Certificate21.envelope_694 line 63
  23. def OAI.SnakyPrototype.Certificate21.childrenC_694 line 64
  24. def OAI.SnakyPrototype.Certificate21.childrenD_694 line 65
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_694 line 66
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_694 line 67
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_694 line 68
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_694 line 69
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_694 line 70
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_694 line 80
  31. def OAI.SnakyPrototype.Certificate21.height_694_i0 line 85
  32. def OAI.SnakyPrototype.Certificate21.childrenH_694_i0 line 86
  33. theorem OAI.SnakyPrototype.Certificate21.height_exact_694_i0 line 87
  34. theorem OAI.SnakyPrototype.Certificate21.required_origin_694_i0 line 88
  35. theorem OAI.SnakyPrototype.Certificate21.required_exact_694_i0 line 90
  36. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_694_i0 line 94
  37. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_694_i0 line 96
  38. def OAI.SnakyPrototype.Certificate21.checked_694_i0 line 100
  39. def OAI.SnakyPrototype.Certificate21.height_694_i1 line 108
  40. def OAI.SnakyPrototype.Certificate21.childrenH_694_i1 line 109
  41. theorem OAI.SnakyPrototype.Certificate21.height_exact_694_i1 line 110
  42. theorem OAI.SnakyPrototype.Certificate21.required_origin_694_i1 line 111
  43. theorem OAI.SnakyPrototype.Certificate21.required_exact_694_i1 line 113
  44. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_694_i1 line 117
  45. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_694_i1 line 119
  46. def OAI.SnakyPrototype.Certificate21.checked_694_i1 line 123
  47. def OAI.SnakyPrototype.Certificate21.height_694 line 131
  48. def OAI.SnakyPrototype.Certificate21.childrenH_694 line 132
  49. theorem OAI.SnakyPrototype.Certificate21.height_exact_694 line 133
  50. theorem OAI.SnakyPrototype.Certificate21.required_origin_694 line 134
  51. theorem OAI.SnakyPrototype.Certificate21.required_exact_694 line 136
  52. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_694 line 140
  53. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_694 line 142
  54. def OAI.SnakyPrototype.Certificate21.checked_694 line 146