OAI/GameTheory/SnakyConditional/Templates/Level17Part05.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_472line 7 - def
OAI.SnakyConditional.envelope_472line 8 - def
OAI.SnakyConditional.childrenC_472line 9 - def
OAI.SnakyConditional.childrenD_472line 10 - theorem
OAI.SnakyConditional.common_sub_472line 11 - theorem
OAI.SnakyConditional.child_required_sub_472line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_472line 13 - theorem
OAI.SnakyConditional.pivot_mem_472line 14 - theorem
OAI.SnakyConditional.children_work_472line 15 - theorem
OAI.SnakyConditional.row_works_472line 20 - def
OAI.SnakyConditional.required_497line 24 - def
OAI.SnakyConditional.envelope_497line 25 - def
OAI.SnakyConditional.childrenC_497line 26 - def
OAI.SnakyConditional.childrenD_497line 27 - theorem
OAI.SnakyConditional.common_sub_497line 28 - theorem
OAI.SnakyConditional.child_required_sub_497line 29 - theorem
OAI.SnakyConditional.child_envelope_sub_497line 30 - theorem
OAI.SnakyConditional.pivot_mem_497line 31 - theorem
OAI.SnakyConditional.children_work_497line 32 - theorem
OAI.SnakyConditional.row_works_497line 38