OAI/GameTheory/SnakyConditional/Templates/Level17Part04.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_441line 6 - def
OAI.SnakyConditional.envelope_441line 7 - def
OAI.SnakyConditional.childrenC_441line 8 - def
OAI.SnakyConditional.childrenD_441line 9 - theorem
OAI.SnakyConditional.common_sub_441line 10 - theorem
OAI.SnakyConditional.child_required_sub_441line 11 - theorem
OAI.SnakyConditional.child_envelope_sub_441line 12 - theorem
OAI.SnakyConditional.pivot_mem_441line 13 - theorem
OAI.SnakyConditional.children_work_441line 14 - theorem
OAI.SnakyConditional.row_works_441line 19 - def
OAI.SnakyConditional.required_471line 23 - def
OAI.SnakyConditional.envelope_471line 24 - def
OAI.SnakyConditional.childrenC_471line 25 - def
OAI.SnakyConditional.childrenD_471line 26 - theorem
OAI.SnakyConditional.common_sub_471line 27 - theorem
OAI.SnakyConditional.child_required_sub_471line 28 - theorem
OAI.SnakyConditional.child_envelope_sub_471line 29 - theorem
OAI.SnakyConditional.pivot_mem_471line 30 - theorem
OAI.SnakyConditional.children_work_471line 31 - theorem
OAI.SnakyConditional.row_works_471line 36