OAI/GameTheory/SnakyConditional/Templates/Level17Part06.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SnakyConditional.required_535line 7 - def
OAI.SnakyConditional.envelope_535line 8 - def
OAI.SnakyConditional.childrenC_535line 9 - def
OAI.SnakyConditional.childrenD_535line 10 - theorem
OAI.SnakyConditional.common_sub_535line 11 - theorem
OAI.SnakyConditional.child_required_sub_535line 12 - theorem
OAI.SnakyConditional.child_envelope_sub_535line 13 - theorem
OAI.SnakyConditional.pivot_mem_535line 14 - theorem
OAI.SnakyConditional.children_work_535line 15 - theorem
OAI.SnakyConditional.row_works_535line 22 - def
OAI.SnakyConditional.required_548line 26 - def
OAI.SnakyConditional.envelope_548line 27 - def
OAI.SnakyConditional.childrenC_548line 28 - def
OAI.SnakyConditional.childrenD_548line 29 - theorem
OAI.SnakyConditional.common_sub_548line 30 - theorem
OAI.SnakyConditional.child_required_sub_548line 31 - theorem
OAI.SnakyConditional.Internal.SnakyRows008C.containment_548_0line 32 - theorem
OAI.SnakyConditional.Internal.SnakyRows008C.containment_548_1line 34 - theorem
OAI.SnakyConditional.Internal.SnakyRows008C.containment_548_2line 36 - theorem
OAI.SnakyConditional.Internal.SnakyRows008C.containment_548_3line 38 - theorem
OAI.SnakyConditional.child_envelope_sub_548line 40 - theorem
OAI.SnakyConditional.pivot_mem_548line 47 - theorem
OAI.SnakyConditional.children_work_548line 48 - theorem
OAI.SnakyConditional.row_works_548line 55