OAI/Combinatorics/IndependentSets/Expansion/PreprocessingInternalRows.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.localStep line 13
2. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.destination line 17
3. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.rowIndex line 21
4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row line 26
5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation line 30
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation_apply line 33
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.cloud_rotation line 37
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.source_rotation line 46
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.rotation_internal line 58
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.reverseIndex_internal line 65
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.relation_ext line 75
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.relations_internal line 84
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row_tail line 91
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row_reverse line 96
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row_relation line 103
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.localStep_original line 108
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.localStep_dummy line 113
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row_tail_original line 117
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row_tail_dummy line 123
20. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex line 129
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_eq line 134
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_old line 158
23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_dummy line 163
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.row_reverse_selectedIndex line 169
25. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingInternalRows.rowWords_eq line 177