OAI/Combinatorics/IndependentSets/Expansion/PoweringEnumeration.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.addressCount line 11
2. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.reverseWordEquiv line 13
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.wordEquiv line 19
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.wordEquiv_val line 22
5. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.addressEquiv line 25
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.addressEquiv_val line 29
7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv line 37
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv_val line 42
9. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.orientationEquiv line 47
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_false line 49
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_true line 50
12. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv line 52
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv_val line 57
14. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.dartVertexEquiv line 63
15. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.dartEquiv line 71
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.dartEquiv_val line 80
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.dartEquiv_true_eq_false_add_one line 89
18. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeWord line 96
19. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeWord line 97
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeWord_encodeWord line 99
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeWord_decodeWord line 102
22. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeAddress line 105
23. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeAddress line 108
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeAddress_encodeAddress line 111
25. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeAddress_decodeAddress line 114
26. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeLabel line 117
27. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeLabel line 120
28. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeLabel_encodeLabel line 124
29. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeLabel_decodeLabel line 127
30. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeLabel_apply line 130
31. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeDart line 134
32. def OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeDart line 138
33. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.decodeDart_encodeDart line 142
34. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.encodeDart_decodeDart line 147
35. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.card_words line 152
36. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.card_addresses line 155
37. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.card_labels line 159
38. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.card_darts line 163
39. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringEnumeration.length_allAddresses line 168