OAI/GameTheory/SnakyConditional/Templates/Level08Part08.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_293line 7 - def
OAI.SnakyConditional.envelope_293line 8 - def
OAI.SnakyConditional.childrenC_293line 9 - def
OAI.SnakyConditional.childrenD_293line 10 - theorem
OAI.SnakyConditional.common_sub_293line 11 - theorem
OAI.SnakyConditional.child_required_sub_293line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_293line 13 - theorem
OAI.SnakyConditional.pivot_mem_293line 14 - theorem
OAI.SnakyConditional.children_work_293line 15 - theorem
OAI.SnakyConditional.row_works_293line 20 - def
OAI.SnakyConditional.required_429line 24 - def
OAI.SnakyConditional.envelope_429line 25 - def
OAI.SnakyConditional.childrenC_429line 26 - def
OAI.SnakyConditional.childrenD_429line 27 - theorem
OAI.SnakyConditional.common_sub_429line 28 - theorem
OAI.SnakyConditional.child_required_sub_429line 29 - theorem
OAI.SnakyConditional.child_envelope_sub_429line 30 - theorem
OAI.SnakyConditional.pivot_mem_429line 31 - theorem
OAI.SnakyConditional.children_work_429line 32 - theorem
OAI.SnakyConditional.row_works_429line 37