OAI/Combinatorics/IndependentSets/Machines/MachineRegularVertexBlock.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.PortLabel line 16
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portEntry line 18
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portInstruction line 22
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portBits line 28
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_eq line 32
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_all line 42
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits line 46
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps line 51
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.joinTrace line 59
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portPrefixTrace line 63
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portTrace line 92
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalTapes line 108
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalView line 111
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_left line 116
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_right line 119
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalStateEquiv line 124
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction line 132
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory line 139
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_input line 143
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_update line 147
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalFrame line 151
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreTrace line 157
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTapes line 189
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView line 191
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_left line 196
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_right line 199
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreInstruction line 204
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMemory_update line 210
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyFrame line 215
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreTrace line 221
  31. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.Label line 250
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry line 257
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry line 260
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.instruction line 263
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.oldCloud line 272
  36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps line 275
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps_eq line 279
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_flatMap line 290
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_pair line 296
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.vertexBits_split line 299
  41. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps line 312
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalTraceAt line 319
  43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps line 362
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTraceAt line 369
  45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.rowSizeBound line 411
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits_length_le line 413
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_length_le line 419
  48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.allRowBits_length_le line 433
  49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portTimeBound line 441
  50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps_le line 445
  51. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalTimeBound line 477
  52. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTimeBound line 482
  53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps_le line 486
  54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps_le line 516
  55. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachine line 534
  56. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine line 545
  57. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachineInTime line 556
  58. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachineInTime line 576