OAI/GameTheory/SnakyConditional/Templates/Level20Part02.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_452line 7 - def
OAI.SnakyConditional.envelope_452line 8 - def
OAI.SnakyConditional.childrenC_452line 9 - def
OAI.SnakyConditional.childrenD_452line 10 - theorem
OAI.SnakyConditional.common_sub_452line 11 - theorem
OAI.SnakyConditional.child_required_sub_452line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_452line 13 - theorem
OAI.SnakyConditional.pivot_mem_452line 14 - theorem
OAI.SnakyConditional.children_work_452line 15 - theorem
OAI.SnakyConditional.row_works_452line 21 - def
OAI.SnakyConditional.required_461line 25 - def
OAI.SnakyConditional.envelope_461line 26 - def
OAI.SnakyConditional.childrenC_461line 27 - def
OAI.SnakyConditional.childrenD_461line 28 - theorem
OAI.SnakyConditional.common_sub_461line 29 - theorem
OAI.SnakyConditional.child_required_sub_461line 30 - theorem
OAI.SnakyConditional.child_envelope_sub_461line 31 - theorem
OAI.SnakyConditional.pivot_mem_461line 32 - theorem
OAI.SnakyConditional.children_work_461line 33 - theorem
OAI.SnakyConditional.row_works_461line 38