OAI/Combinatorics/IndependentSets/Expansion/PortTables.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PortTables.Label line 11
2. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.rowIndex line 13
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.rowIndex_val line 16
4. structure OAI.IndependentSetsGames.Foundations.PCP.PortTables.Table line 19
5. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.rotation line 30
6. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.accepts line 33
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.rowIndex_rotation line 36
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.rotation_involutive line 40
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.accepts_rotation line 46
10. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.portGraph line 50
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.portGraph_rot line 58
12. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.baseGraph line 61
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.baseGraph_reverse line 68
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.baseGraph_tail line 71
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.baseGraph_head line 74
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.baseGraph_accepts line 77
17. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.ofPortGraph line 80
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.rotation_ofPortGraph line 97
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.accepts_ofPortGraph line 104
20. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.flatRows line 112
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.reverseAt_flatRows line 116
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.acceptsAt_flatRows line 120
23. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.flatRows_valid line 124
24. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.graphTable line 131
25. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.tableWords line 134
26. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.tableBits line 136
27. abbrev OAI.IndependentSetsGames.Foundations.PCP.PortTables.Input line 138
28. def OAI.IndependentSetsGames.Foundations.PCP.PortTables.inputBits line 140
29. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.tableWords_eq line 142
30. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.tableWords_length line 145
31. theorem OAI.IndependentSetsGames.Foundations.PCP.PortTables.vertices_le_tableBits_length line 149