OAI/Computability/BinPacking/PCP/RawInitialMachineLoopData.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.orderedList line 14
2. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.orderedList_cast line 17
3. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.orderedList_prod line 22
4. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.orderedList_sum line 46
5. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.clauseDarts line 60
6. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.orderedList_dartOrder line 65
7. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.rowFor line 78
8. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.rowList_table line 84
9. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.rowWords_incidence line 90
10. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.rowWords_dummy line 110
11. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.clauseDarts_rowWords line 123
12. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.tableWords_eq line 129
13. inductive OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.Tape line 145
14. abbrev OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.Signs line 150
15. abbrev OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.State line 151
16. abbrev OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.Alphabet line 152
17. inductive OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.CopyPhase line 154
18. inductive OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.Label line 162
19. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.initialState line 176
20. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.stateKeys line 178
21. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.stateKeys_complete line 183
22. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.nameField line 189
23. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.copySource line 191
24. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.copyScale line 196
25. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.copyNext line 200
26. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.relationNext line 209
27. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.finalTape line 215
28. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.drain line 218
29. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.headerTape line 221
30. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.relationOutput line 223
31. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.program line 227
32. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineModel.machine line 277
33. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.inputTapes line 294
34. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.firstTapes line 298
35. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.counterTapes line 303
36. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.headerTapes line 309
37. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.startTapes line 316
38. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.initList_eq line 324
39. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.trace_trans line 333
40. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.readCountersTrace line 337
41. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.headersTrace line 370
42. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.initializeIndexTrace line 389
43. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.startTrace line 401
44. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.formulaStartTrace line 411
45. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.startInTime line 421
46. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineStart.formulaStartInTime line 430
47. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_scratch line 446
48. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_reversed line 449
49. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.copyInTime line 452
50. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.relationInTime line 467
51. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.bitWord_head line 480
52. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.loadSigns_step line 484
53. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.loadSignsInTime line 493
54. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.cleanupFieldInTime line 504
55. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachinePhases.cleanupFinalInTime line 512
56. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput line 526
57. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_nil line 529
58. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_cons line 531
59. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput line 535
60. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.mapIdx_ofFn line 539
61. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_nil line 545
62. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_cons line 547
63. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_numbered line 554
64. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.tableWords_decomposition line 564
65. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.loopTapes line 571
66. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.startTapes_eq line 579
67. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.decrement_counter line 585
68. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineLoopData.increment_index line 591