OAI/GameTheory/SnakyConditional/Templates/Level24Part03.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_554 line 8
  2. def OAI.SnakyConditional.envelope_554 line 9
  3. def OAI.SnakyConditional.childrenC_554 line 10
  4. def OAI.SnakyConditional.childrenD_554 line 11
  5. theorem OAI.SnakyConditional.common_sub_554 line 12
  6. theorem OAI.SnakyConditional.child_required_sub_554 line 13
  7. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_554_0 line 14
  8. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_554_1 line 16
  9. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_554_2 line 18
  10. theorem OAI.SnakyConditional.child_envelope_sub_554 line 20
  11. theorem OAI.SnakyConditional.pivot_mem_554 line 26
  12. theorem OAI.SnakyConditional.children_work_554 line 27
  13. theorem OAI.SnakyConditional.row_works_554 line 33
  14. def OAI.SnakyConditional.required_561 line 37
  15. def OAI.SnakyConditional.envelope_561 line 38
  16. def OAI.SnakyConditional.childrenC_561 line 39
  17. def OAI.SnakyConditional.childrenD_561 line 40
  18. theorem OAI.SnakyConditional.common_sub_561 line 41
  19. theorem OAI.SnakyConditional.child_required_sub_561 line 42
  20. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_0 line 43
  21. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_1 line 45
  22. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_2 line 47
  23. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_3 line 49
  24. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_4 line 51
  25. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_5 line 53
  26. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_561_6 line 55
  27. theorem OAI.SnakyConditional.child_envelope_sub_561 line 57
  28. theorem OAI.SnakyConditional.pivot_mem_561 line 67
  29. theorem OAI.SnakyConditional.children_work_561 line 68
  30. theorem OAI.SnakyConditional.row_works_561 line 78