OAI/GameTheory/SnakyConditional/Templates/Level29Part01.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SnakyConditional.required_571 line 7
2. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_4 line 8
3. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_5 line 9
4. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_3 line 10
5. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_7 line 12
6. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_8 line 13
7. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_6 line 14
8. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_2 line 16
9. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_11 line 18
10. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_12 line 19
11. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_10 line 20
12. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_14 line 22
13. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_15 line 23
14. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_13 line 24
15. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_9 line 26
16. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_1 line 28
17. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_19 line 30
18. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_20 line 31
19. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_18 line 32
20. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_22 line 34
21. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_23 line 35
22. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_21 line 36
23. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_17 line 38
24. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_26 line 40
25. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_27 line 41
26. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_25 line 42
27. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_29 line 44
28. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_30 line 45
29. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_28 line 46
30. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_24 line 48
31. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_16 line 50
32. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_chain_0 line 52
33. theorem OAI.SnakyConditional.Internal.SnakyRows008.cf17_envelope_571_nodup line 54
34. def OAI.SnakyConditional.envelope_571 line 56
35. def OAI.SnakyConditional.childrenC_571 line 57
36. def OAI.SnakyConditional.childrenD_571 line 58
37. theorem OAI.SnakyConditional.common_sub_571 line 59
38. theorem OAI.SnakyConditional.child_required_sub_571 line 60
39. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_571_0 line 61
40. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_571_1 line 63
41. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_571_2 line 65
42. theorem OAI.SnakyConditional.Internal.SnakyRows008.containment_571_3 line 67
43. theorem OAI.SnakyConditional.child_envelope_sub_571 line 69
44. theorem OAI.SnakyConditional.pivot_mem_571 line 76
45. theorem OAI.SnakyConditional.children_work_571 line 77
46. theorem OAI.SnakyConditional.row_works_571 line 84