OAI/Computability/VertexCover/PCP/PoweringEnumeration.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.addressCount line 13
2. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.reverseWordEquiv line 15
3. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.wordEquiv line 21
4. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.wordEquiv_val line 24
5. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.addressEquiv line 27
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.addressEquiv_val line 31
7. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv line 39
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv_val line 44
9. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.orientationEquiv line 49
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_false line 51
11. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_true line 52
12. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv line 54
13. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv_val line 59
14. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.dartVertexEquiv line 65
15. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.dartEquiv line 73
16. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.dartEquiv_val line 82
17. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.dartEquiv_true_eq_false_add_one line 91
18. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeWord line 98
19. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeWord line 99
20. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeWord_encodeWord line 101
21. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeWord_decodeWord line 104
22. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeAddress line 107
23. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeAddress line 110
24. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeAddress_encodeAddress line 113
25. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeAddress_decodeAddress line 116
26. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeLabel line 119
27. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeLabel line 122
28. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeLabel_encodeLabel line 126
29. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeLabel_decodeLabel line 129
30. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeLabel_apply line 132
31. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeDart line 136
32. def OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeDart line 140
33. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.decodeDart_encodeDart line 144
34. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.encodeDart_decodeDart line 149
35. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.card_words line 154
36. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.card_addresses line 157
37. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.card_labels line 161
38. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.card_darts line 165
39. theorem OAI.UniqueGames.Foundations.PCP.PoweringEnumeration.length_allAddresses line 170