OAI/GameTheory/SnakyConditional/Templates/Level17Part03.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_439line 7 - def
OAI.SnakyConditional.envelope_439line 8 - def
OAI.SnakyConditional.childrenC_439line 9 - def
OAI.SnakyConditional.childrenD_439line 10 - theorem
OAI.SnakyConditional.common_sub_439line 11 - theorem
OAI.SnakyConditional.child_required_sub_439line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_439line 13 - theorem
OAI.SnakyConditional.pivot_mem_439line 14 - theorem
OAI.SnakyConditional.children_work_439line 15 - theorem
OAI.SnakyConditional.row_works_439line 23 - def
OAI.SnakyConditional.required_440line 27 - def
OAI.SnakyConditional.envelope_440line 28 - def
OAI.SnakyConditional.childrenC_440line 29 - def
OAI.SnakyConditional.childrenD_440line 30 - theorem
OAI.SnakyConditional.common_sub_440line 31 - theorem
OAI.SnakyConditional.child_required_sub_440line 32 - theorem
OAI.SnakyConditional.child_envelope_sub_440line 33 - theorem
OAI.SnakyConditional.pivot_mem_440line 34 - theorem
OAI.SnakyConditional.children_work_440line 35 - theorem
OAI.SnakyConditional.row_works_440line 40