OAI/Combinatorics/IndependentSets/Fourier/NumberedStorage.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 16
2. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 34
3. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 49
4. def OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.honestGlobal line 81
5. def OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.honestBits line 87
6. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.honestBits_code line 92
7. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.honestBits_dummy line 100
8. def OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.honestValidJ line 106
9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 112
10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.leftResponse_honest line 118
11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.rightResponse_honest line 126
12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 149
13. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 163
14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 173
15. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 192
16. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 202
17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 216
18. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 226