OAI/GameTheory/SnakyConditional/Templates/Level23Part01.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_467line 6 - def
OAI.SnakyConditional.envelope_467line 7 - def
OAI.SnakyConditional.childrenC_467line 8 - def
OAI.SnakyConditional.childrenD_467line 9 - theorem
OAI.SnakyConditional.common_sub_467line 10 - theorem
OAI.SnakyConditional.child_required_sub_467line 11 - theorem
OAI.SnakyConditional.child_envelope_sub_467line 12 - theorem
OAI.SnakyConditional.pivot_mem_467line 13 - theorem
OAI.SnakyConditional.children_work_467line 14 - theorem
OAI.SnakyConditional.row_works_467line 20 - def
OAI.SnakyConditional.required_469line 24 - def
OAI.SnakyConditional.envelope_469line 25 - def
OAI.SnakyConditional.childrenC_469line 26 - def
OAI.SnakyConditional.childrenD_469line 27 - theorem
OAI.SnakyConditional.common_sub_469line 28 - theorem
OAI.SnakyConditional.child_required_sub_469line 29 - theorem
OAI.SnakyConditional.child_envelope_sub_469line 30 - theorem
OAI.SnakyConditional.pivot_mem_469line 31 - theorem
OAI.SnakyConditional.children_work_469line 32 - theorem
OAI.SnakyConditional.row_works_469line 38