OAI/GameTheory/SnakyConditional/Templates/Level23Part06.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.required_552 line 9
  2. def OAI.SnakyConditional.envelope_552 line 10
  3. def OAI.SnakyConditional.childrenC_552 line 11
  4. def OAI.SnakyConditional.childrenD_552 line 12
  5. theorem OAI.SnakyConditional.common_sub_552 line 13
  6. theorem OAI.SnakyConditional.child_required_sub_552 line 14
  7. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_552_0 line 15
  8. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_552_1 line 17
  9. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_552_2 line 19
  10. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_552_3 line 21
  11. theorem OAI.SnakyConditional.child_envelope_sub_552 line 23
  12. theorem OAI.SnakyConditional.pivot_mem_552 line 30
  13. theorem OAI.SnakyConditional.children_work_552 line 31
  14. theorem OAI.SnakyConditional.row_works_552 line 38
  15. def OAI.SnakyConditional.required_555 line 42
  16. def OAI.SnakyConditional.envelope_555 line 43
  17. def OAI.SnakyConditional.childrenC_555 line 44
  18. def OAI.SnakyConditional.childrenD_555 line 45
  19. theorem OAI.SnakyConditional.common_sub_555 line 46
  20. theorem OAI.SnakyConditional.child_required_sub_555 line 47
  21. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_555_0 line 48
  22. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_555_1 line 50
  23. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_555_2 line 52
  24. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_555_3 line 54
  25. theorem OAI.SnakyConditional.Internal.SnakyRows008C.containment_555_4 line 56
  26. theorem OAI.SnakyConditional.child_envelope_sub_555 line 58
  27. theorem OAI.SnakyConditional.pivot_mem_555 line 66
  28. theorem OAI.SnakyConditional.children_work_555 line 67
  29. theorem OAI.SnakyConditional.row_works_555 line 75