OAI/GameTheory/SnakyConditional/Templates/Level23Part07.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_558 line 8
  2. def OAI.SnakyConditional.envelope_558 line 9
  3. def OAI.SnakyConditional.childrenC_558 line 10
  4. def OAI.SnakyConditional.childrenD_558 line 11
  5. theorem OAI.SnakyConditional.common_sub_558 line 12
  6. theorem OAI.SnakyConditional.child_required_sub_558 line 13
  7. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_558_0 line 14
  8. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_558_1 line 16
  9. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_558_2 line 18
  10. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_558_3 line 20
  11. theorem OAI.SnakyConditional.child_envelope_sub_558 line 22
  12. theorem OAI.SnakyConditional.pivot_mem_558 line 29
  13. theorem OAI.SnakyConditional.children_work_558 line 30
  14. theorem OAI.SnakyConditional.row_works_558 line 37
  15. def OAI.SnakyConditional.required_577 line 41
  16. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_3 line 42
  17. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_3_chain line 43
  18. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_3_head line 44
  19. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_3_last line 45
  20. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_4 line 46
  21. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_4_chain line 47
  22. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_4_head line 48
  23. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_4_last line 49
  24. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_2 line 50
  25. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_2_chain line 51
  26. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_2_head line 54
  27. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_2_last line 56
  28. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_6 line 58
  29. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_6_chain line 59
  30. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_6_head line 60
  31. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_6_last line 61
  32. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_7 line 62
  33. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_7_chain line 63
  34. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_7_head line 64
  35. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_7_last line 65
  36. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_5 line 66
  37. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_5_chain line 67
  38. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_5_head line 70
  39. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_5_last line 72
  40. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_1 line 74
  41. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_1_chain line 75
  42. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_1_head line 78
  43. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_1_last line 80
  44. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_10 line 82
  45. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_10_chain line 83
  46. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_10_head line 84
  47. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_10_last line 85
  48. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_11 line 86
  49. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_11_chain line 87
  50. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_11_head line 88
  51. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_11_last line 89
  52. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_9 line 90
  53. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_9_chain line 91
  54. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_9_head line 94
  55. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_9_last line 96
  56. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_13 line 98
  57. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_13_chain line 99
  58. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_13_head line 100
  59. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_13_last line 101
  60. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_14 line 102
  61. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_14_chain line 103
  62. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_14_head line 104
  63. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_14_last line 105
  64. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_12 line 106
  65. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_12_chain line 107
  66. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_12_head line 110
  67. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_12_last line 112
  68. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_8 line 114
  69. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_8_chain line 115
  70. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_8_head line 118
  71. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_8_last line 120
  72. def OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_0 line 122
  73. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_0_chain line 123
  74. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_0_head line 126
  75. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_0_last line 128
  76. theorem OAI.SnakyConditional.Internal.SnakyRows009.named_envelope_577_nodup line 130
  77. def OAI.SnakyConditional.envelope_577 line 132
  78. def OAI.SnakyConditional.childrenC_577 line 133
  79. def OAI.SnakyConditional.childrenD_577 line 134
  80. theorem OAI.SnakyConditional.common_sub_577 line 135
  81. theorem OAI.SnakyConditional.child_required_sub_577 line 136
  82. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_577_0 line 137
  83. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_577_1 line 139
  84. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_577_2 line 141
  85. theorem OAI.SnakyConditional.Internal.SnakyRows009.containment_577_3 line 143
  86. theorem OAI.SnakyConditional.child_envelope_sub_577 line 145
  87. theorem OAI.SnakyConditional.pivot_mem_577 line 152
  88. theorem OAI.SnakyConditional.children_work_577 line 153
  89. theorem OAI.SnakyConditional.row_works_577 line 160