OAI/GameTheory/SnakyConditional/Templates/Level21Part01.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_438line 6 - def
OAI.SnakyConditional.envelope_438line 7 - def
OAI.SnakyConditional.childrenC_438line 8 - def
OAI.SnakyConditional.childrenD_438line 9 - theorem
OAI.SnakyConditional.common_sub_438line 10 - theorem
OAI.SnakyConditional.child_required_sub_438line 11 - theorem
OAI.SnakyConditional.child_envelope_sub_438line 12 - theorem
OAI.SnakyConditional.pivot_mem_438line 13 - theorem
OAI.SnakyConditional.children_work_438line 14 - theorem
OAI.SnakyConditional.row_works_438line 19 - def
OAI.SnakyConditional.required_445line 23 - def
OAI.SnakyConditional.envelope_445line 24 - def
OAI.SnakyConditional.childrenC_445line 25 - def
OAI.SnakyConditional.childrenD_445line 26 - theorem
OAI.SnakyConditional.common_sub_445line 27 - theorem
OAI.SnakyConditional.child_required_sub_445line 28 - theorem
OAI.SnakyConditional.child_envelope_sub_445line 29 - theorem
OAI.SnakyConditional.pivot_mem_445line 30 - theorem
OAI.SnakyConditional.children_work_445line 31 - theorem
OAI.SnakyConditional.row_works_445line 36