OAI/Computability/MinUncut/Machines/MachineRegularVertexBlock.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.PortLabel line 15
  2. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portEntry line 17
  3. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portInstruction line 21
  4. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits line 27
  5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_eq line 31
  6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_all line 41
  7. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits line 45
  8. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps line 50
  9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.joinTrace line 58
  10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portPrefixTrace line 62
  11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portTrace line 91
  12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalTapes line 107
  13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalView line 110
  14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_left line 115
  15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_right line 118
  16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalStateEquiv line 123
  17. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction line 131
  18. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory line 138
  19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_input line 142
  20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_update line 146
  21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalFrame line 150
  22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreTrace line 156
  23. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTapes line 188
  24. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView line 190
  25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_left line 195
  26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_right line 198
  27. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreInstruction line 203
  28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMemory_update line 209
  29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyFrame line 214
  30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreTrace line 220
  31. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.Label line 249
  32. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry line 256
  33. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry line 259
  34. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.instruction line 262
  35. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.oldCloud line 271
  36. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps line 274
  37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps_eq line 278
  38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_flatMap line 289
  39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_pair line 295
  40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.vertexBits_split line 298
  41. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps line 311
  42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalTraceAt line 318
  43. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps line 361
  44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTraceAt line 368
  45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.rowSizeBound line 410
  46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits_length_le line 412
  47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_length_le line 418
  48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.allRowBits_length_le line 432
  49. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portTimeBound line 440
  50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps_le line 444
  51. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalTimeBound line 476
  52. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTimeBound line 481
  53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps_le line 485
  54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps_le line 515
  55. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachine line 533
  56. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine line 544
  57. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachineInTime line 555
  58. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachineInTime line 575