OAI/Computability/BinPacking/Computation/MachineCanonicalOutput.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.Label line 12
2. instance OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.labelFintype line 16
3. instance OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.labelDecidableEq line 24
4. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.entry line 35
5. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.instruction line 42
6. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.resultOf line 53
7. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.steps line 57
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFiniteSequence.trace line 63
9. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.Alphabet line 109
10. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.Tapes line 110
11. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.LocalLabel line 111
12. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.Label line 112
13. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.Data line 113
14. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.entry line 115
15. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.localInstruction line 118
16. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.instruction line 122
17. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.result line 127
18. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.cost line 130
19. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalTapes line 132
20. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalRegister line 136
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalRegister_none line 141
22. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.steps line 144
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.sequence_result line 149
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.sequence_steps line 159
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalTapes_apply line 166
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalTapes_mem line 177
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalTapes_not_mem line 180
28. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.lengthSum line 183
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.lengthSum_mono line 187
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.steps_le line 196
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.steps_le_uniform line 212
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.trace line 227
33. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.execution line 248
34. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.workTapes line 260
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.mem_workTapes line 263
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.workTapes_length_le line 270
37. def OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.haltTapes line 275
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.finalTapes_workTapes line 278
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrainMany.cleanupTrace line 288
40. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.Alphabet line 308
41. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.Label line 310
42. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.copyInstruction line 314
43. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.instruction line 321
44. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.program line 333
45. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.afterD line 338
46. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders line 341
47. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_output line 344
48. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_other line 348
49. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.copySteps line 352
50. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.copySteps_eq line 354
51. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.steps line 358
52. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.budget line 362
53. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.trace_trans line 366
54. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.traceAt line 370
55. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.trace line 419
56. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.steps_le_budget line 435
57. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_length_le line 441
58. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.steps_le_uniform line 454
59. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineFinish.execution line 468
60. structure OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.Program line 491
61. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.extendedLabel line 502
62. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.extendedCfg line 506
63. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.extendedStmt line 511
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.stepAux_extended line 529
65. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.sourceMachine line 553
66. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.Label line 564
67. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.cleanupLabel line 566
68. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.resetLabel line 569
69. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry line 571
70. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.completedProgram line 574
71. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine line 581
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.finiteAlphabet line 592
73. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.embeddedCfg line 597
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.step_simulation line 601
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.embedded_init line 617
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.finalTapes_eq line 622
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.haltList_eq line 633
78. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.cleanupExecution line 638
79. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.outputsInTime line 669
80. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.completedTime line 694
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.completedTime_eval line 699
82. structure OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun line 706
83. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime line 713
84. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime_finite_alphabet line 732
85. def OAI.BinPackingGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTimeOfEnumeration line 743