OAI/GameTheory/SnakyConditional/Templates/Level20Part03.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_531line 9 - def
OAI.SnakyConditional.envelope_531line 10 - def
OAI.SnakyConditional.childrenC_531line 11 - def
OAI.SnakyConditional.childrenD_531line 12 - theorem
OAI.SnakyConditional.common_sub_531line 13 - theorem
OAI.SnakyConditional.child_required_sub_531line 14 - theorem
OAI.SnakyConditional.child_envelope_sub_531line 15 - theorem
OAI.SnakyConditional.pivot_mem_531line 16 - theorem
OAI.SnakyConditional.children_work_531line 17 - theorem
OAI.SnakyConditional.row_works_531line 28 - def
OAI.SnakyConditional.required_539line 32 - def
OAI.SnakyConditional.envelope_539line 33 - def
OAI.SnakyConditional.childrenC_539line 34 - def
OAI.SnakyConditional.childrenD_539line 35 - theorem
OAI.SnakyConditional.common_sub_539line 36 - theorem
OAI.SnakyConditional.child_required_sub_539line 37 - theorem
OAI.SnakyConditional.child_envelope_sub_539line 38 - theorem
OAI.SnakyConditional.pivot_mem_539line 39 - theorem
OAI.SnakyConditional.children_work_539line 40 - theorem
OAI.SnakyConditional.row_works_539line 47