OAI/GameTheory/SnakyConditional/Templates/Level20Part01.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_432line 6 - def
OAI.SnakyConditional.envelope_432line 7 - def
OAI.SnakyConditional.childrenC_432line 8 - def
OAI.SnakyConditional.childrenD_432line 9 - theorem
OAI.SnakyConditional.common_sub_432line 10 - theorem
OAI.SnakyConditional.child_required_sub_432line 11 - theorem
OAI.SnakyConditional.child_envelope_sub_432line 12 - theorem
OAI.SnakyConditional.pivot_mem_432line 13 - theorem
OAI.SnakyConditional.children_work_432line 14 - theorem
OAI.SnakyConditional.row_works_432line 20 - def
OAI.SnakyConditional.required_436line 24 - def
OAI.SnakyConditional.envelope_436line 25 - def
OAI.SnakyConditional.childrenC_436line 26 - def
OAI.SnakyConditional.childrenD_436line 27 - theorem
OAI.SnakyConditional.common_sub_436line 28 - theorem
OAI.SnakyConditional.child_required_sub_436line 29 - theorem
OAI.SnakyConditional.child_envelope_sub_436line 30 - theorem
OAI.SnakyConditional.pivot_mem_436line 31 - theorem
OAI.SnakyConditional.children_work_436line 32 - theorem
OAI.SnakyConditional.row_works_436line 39