OAI/GameTheory/SnakyConditional/Templates/Level24Part01.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_483line 8 - def
OAI.SnakyConditional.envelope_483line 9 - def
OAI.SnakyConditional.childrenC_483line 10 - def
OAI.SnakyConditional.childrenD_483line 11 - theorem
OAI.SnakyConditional.common_sub_483line 12 - theorem
OAI.SnakyConditional.child_required_sub_483line 13 - theorem
OAI.SnakyConditional.child_envelope_sub_483line 14 - theorem
OAI.SnakyConditional.pivot_mem_483line 15 - theorem
OAI.SnakyConditional.children_work_483line 16 - theorem
OAI.SnakyConditional.row_works_483line 24 - def
OAI.SnakyConditional.required_490line 28 - def
OAI.SnakyConditional.envelope_490line 29 - def
OAI.SnakyConditional.childrenC_490line 30 - def
OAI.SnakyConditional.childrenD_490line 31 - theorem
OAI.SnakyConditional.common_sub_490line 32 - theorem
OAI.SnakyConditional.child_required_sub_490line 33 - theorem
OAI.SnakyConditional.child_envelope_sub_490line 34 - theorem
OAI.SnakyConditional.pivot_mem_490line 35 - theorem
OAI.SnakyConditional.children_work_490line 36 - theorem
OAI.SnakyConditional.row_works_490line 43