OAI/Combinatorics/IndependentSets/PCP/Driver.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.headerPlan line 18
2. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.rowPlan line 19
3. inductive OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.Label line 21
4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.headerEntry line 33
5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.rowEntry line 36
6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.clearNext line 39
7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.program line 42
8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.machine line 76
9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.program_setup line 89
10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.program_guard line 93
11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.program_headLookup line 96
12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.program_compare line 100
13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Driver.program_increment line 103
14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.inputBits line 113
15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords line 116
16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits line 121
17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords line 124
18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits line 127
19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_zero line 130
20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_zero line 136
21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_succ line 142
22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_succ line 155
23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_reverse_succ line 162
24. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixWords_full line 169
25. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.prefixBits_full line 178
26. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_zero line 183
27. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.cursorWords_succ line 188
28. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_succ line 199
29. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.cursorBits_full line 207
30. structure OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready line 215
31. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.of_agree line 233
32. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_scan line 253
33. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.update_indexScan line 260
34. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_succ line 267
35. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_at_end line 274
36. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.cursor_at_end line 279
37. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopState.Ready.reversed_at_end line 283