OAI/GameTheory/SnakyConditional/Templates/Level17Part01.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_385line 7 - def
OAI.SnakyConditional.envelope_385line 8 - def
OAI.SnakyConditional.childrenC_385line 9 - def
OAI.SnakyConditional.childrenD_385line 10 - theorem
OAI.SnakyConditional.common_sub_385line 11 - theorem
OAI.SnakyConditional.child_required_sub_385line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_385line 13 - theorem
OAI.SnakyConditional.pivot_mem_385line 14 - theorem
OAI.SnakyConditional.children_work_385line 15 - theorem
OAI.SnakyConditional.row_works_385line 22 - def
OAI.SnakyConditional.required_433line 26 - def
OAI.SnakyConditional.envelope_433line 27 - def
OAI.SnakyConditional.childrenC_433line 28 - def
OAI.SnakyConditional.childrenD_433line 29 - theorem
OAI.SnakyConditional.common_sub_433line 30 - theorem
OAI.SnakyConditional.child_required_sub_433line 31 - theorem
OAI.SnakyConditional.child_envelope_sub_433line 32 - theorem
OAI.SnakyConditional.pivot_mem_433line 33 - theorem
OAI.SnakyConditional.children_work_433line 34 - theorem
OAI.SnakyConditional.row_works_433line 41