OAI/GameTheory/SnakyConditional/Templates/Level23Part03.lean
20 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_475line 7 - def
OAI.SnakyConditional.envelope_475line 8 - def
OAI.SnakyConditional.childrenC_475line 9 - def
OAI.SnakyConditional.childrenD_475line 10 - theorem
OAI.SnakyConditional.common_sub_475line 11 - theorem
OAI.SnakyConditional.child_required_sub_475line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_475line 13 - theorem
OAI.SnakyConditional.pivot_mem_475line 14 - theorem
OAI.SnakyConditional.children_work_475line 15 - theorem
OAI.SnakyConditional.row_works_475line 22 - def
OAI.SnakyConditional.required_476line 26 - def
OAI.SnakyConditional.envelope_476line 27 - def
OAI.SnakyConditional.childrenC_476line 28 - def
OAI.SnakyConditional.childrenD_476line 29 - theorem
OAI.SnakyConditional.common_sub_476line 30 - theorem
OAI.SnakyConditional.child_required_sub_476line 31 - theorem
OAI.SnakyConditional.child_envelope_sub_476line 32 - theorem
OAI.SnakyConditional.pivot_mem_476line 33 - theorem
OAI.SnakyConditional.children_work_476line 34 - theorem
OAI.SnakyConditional.row_works_476line 39