OAI/GameTheory/SnakyConditional/Templates/Level23Part04.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_479line 7 - def
OAI.SnakyConditional.envelope_479line 8 - def
OAI.SnakyConditional.childrenC_479line 9 - def
OAI.SnakyConditional.childrenD_479line 10 - theorem
OAI.SnakyConditional.common_sub_479line 11 - theorem
OAI.SnakyConditional.child_required_sub_479line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_479line 13 - theorem
OAI.SnakyConditional.pivot_mem_479line 14 - theorem
OAI.SnakyConditional.children_work_479line 15 - theorem
OAI.SnakyConditional.row_works_479line 21 - def
OAI.SnakyConditional.required_514line 25 - def
OAI.SnakyConditional.envelope_514line 26 - def
OAI.SnakyConditional.childrenC_514line 27 - def
OAI.SnakyConditional.childrenD_514line 28 - theorem
OAI.SnakyConditional.common_sub_514line 29 - theorem
OAI.SnakyConditional.child_required_sub_514line 30 - theorem
OAI.SnakyConditional.child_envelope_sub_514line 31 - theorem
OAI.SnakyConditional.pivot_mem_514line 32 - theorem
OAI.SnakyConditional.children_work_514line 33 - theorem
OAI.SnakyConditional.row_works_514line 39