OAI/GameTheory/SnakyConditional/Templates/Level19Part04.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_549 line 8
  2. def OAI.SnakyConditional.envelope_549 line 9
  3. def OAI.SnakyConditional.childrenC_549 line 10
  4. def OAI.SnakyConditional.childrenD_549 line 11
  5. theorem OAI.SnakyConditional.common_sub_549 line 12
  6. theorem OAI.SnakyConditional.child_required_sub_549 line 13
  7. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_549_0 line 14
  8. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_549_1 line 16
  9. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_549_2 line 18
  10. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_549_3 line 20
  11. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_549_4 line 22
  12. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_549_5 line 24
  13. theorem OAI.SnakyConditional.child_envelope_sub_549 line 26
  14. theorem OAI.SnakyConditional.pivot_mem_549 line 35
  15. theorem OAI.SnakyConditional.children_work_549 line 36
  16. theorem OAI.SnakyConditional.row_works_549 line 45
  17. def OAI.SnakyConditional.required_553 line 49
  18. def OAI.SnakyConditional.envelope_553 line 50
  19. def OAI.SnakyConditional.childrenC_553 line 51
  20. def OAI.SnakyConditional.childrenD_553 line 52
  21. theorem OAI.SnakyConditional.common_sub_553 line 53
  22. theorem OAI.SnakyConditional.child_required_sub_553 line 54
  23. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_553_0 line 55
  24. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_553_1 line 57
  25. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_553_2 line 59
  26. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_553_3 line 61
  27. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_553_4 line 63
  28. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_553_5 line 65
  29. theorem OAI.SnakyConditional.child_envelope_sub_553 line 67
  30. theorem OAI.SnakyConditional.pivot_mem_553 line 76
  31. theorem OAI.SnakyConditional.children_work_553 line 77
  32. theorem OAI.SnakyConditional.row_works_553 line 86