OAI/GameTheory/SnakyConditional/Templates/Level23Part02.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_470line 7 - def
OAI.SnakyConditional.envelope_470line 8 - def
OAI.SnakyConditional.childrenC_470line 9 - def
OAI.SnakyConditional.childrenD_470line 10 - theorem
OAI.SnakyConditional.common_sub_470line 11 - theorem
OAI.SnakyConditional.child_required_sub_470line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_470line 13 - theorem
OAI.SnakyConditional.pivot_mem_470line 14 - theorem
OAI.SnakyConditional.children_work_470line 15 - theorem
OAI.SnakyConditional.row_works_470line 20 - def
OAI.SnakyConditional.required_474line 24 - def
OAI.SnakyConditional.envelope_474line 25 - def
OAI.SnakyConditional.childrenC_474line 26 - def
OAI.SnakyConditional.childrenD_474line 27 - theorem
OAI.SnakyConditional.common_sub_474line 28 - theorem
OAI.SnakyConditional.child_required_sub_474line 29 - theorem
OAI.SnakyConditional.child_envelope_sub_474line 30 - theorem
OAI.SnakyConditional.pivot_mem_474line 31 - theorem
OAI.SnakyConditional.children_work_474line 32 - theorem
OAI.SnakyConditional.row_works_474line 38