OAI/GameTheory/SnakyConditional/Templates/Level21Part03.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_454line 7 - def
OAI.SnakyConditional.envelope_454line 8 - def
OAI.SnakyConditional.childrenC_454line 9 - def
OAI.SnakyConditional.childrenD_454line 10 - theorem
OAI.SnakyConditional.common_sub_454line 11 - theorem
OAI.SnakyConditional.child_required_sub_454line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_454line 13 - theorem
OAI.SnakyConditional.pivot_mem_454line 14 - theorem
OAI.SnakyConditional.children_work_454line 15 - theorem
OAI.SnakyConditional.row_works_454line 20 - def
OAI.SnakyConditional.required_462line 24 - def
OAI.SnakyConditional.envelope_462line 25 - def
OAI.SnakyConditional.childrenC_462line 26 - def
OAI.SnakyConditional.childrenD_462line 27 - theorem
OAI.SnakyConditional.common_sub_462line 28 - theorem
OAI.SnakyConditional.child_required_sub_462line 29 - theorem
OAI.SnakyConditional.child_envelope_sub_462line 30 - theorem
OAI.SnakyConditional.pivot_mem_462line 31 - theorem
OAI.SnakyConditional.children_work_462line 32 - theorem
OAI.SnakyConditional.row_works_462line 38