OAI/Computability/DirectedFeedback/Machines/MachineLazyTable.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.Tape line 56
  2. instance OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.(instance at line 61) line 61
  3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.State line 63
  4. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.clean line 65
  5. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.clean_pair line 68
  6. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.splitRoles line 71
  7. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.splitView line 72
  8. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.dummyRoles line 76
  9. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.dummyView line 77
  10. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.oldRoles line 81
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.splitRoles_left line 85
  12. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.splitRoles_right line 88
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.dummyRoles_left line 91
  14. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.dummyRoles_right line 94
  15. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.oldRoles_injective line 97
  16. inductive OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.Label line 99
  17. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.program line 109
  18. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.frame line 146
  19. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.initialTapes line 151
  20. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.loopTapes line 153
  21. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.finalTapes line 158
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.joinTrace_inline_MachineLazyTable line 160
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.dummyTrace line 164
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.oldTrace line 193
  25. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.prefixSteps line 225
  26. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.prefixTrace line 228
  27. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.vertexBlock line 310
  28. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.bodySteps line 314
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.frame_old_empty line 320
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.bodyTrace line 325
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.drainPhase line 437
  32. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.finishSteps line 448
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.finishTrace line 450
  34. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.remaining line 505
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.remaining_zero line 507
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.remaining_done line 508
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.remaining_cons line 510
  38. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.inputBlocks line 516
  39. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.outputBlocks line 519
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.vertexBlock_codec line 522
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.encodeWords_flatMap_inline_MachineLazyTable line 528
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.inputBlocks_codec line 534
  43. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.outputBlocks_codec line 541
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.input_table_codec line 547
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.output_table_codec line 558
  46. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.loopSteps line 570
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.loopTrace line 578
  48. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.totalSteps line 619
  49. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.tableTrace line 623
  50. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.dummyRows_length_le_inline_MachineLazyTable line 638
  51. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.bodySteps_le line 649
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.output_length_le line 770
  53. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.loopSteps_le line 787
  54. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.timePolynomial line 819
  55. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.timePolynomial_eval line 822
  56. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.totalSteps_le line 826
  57. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.machine line 857
  58. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.machine_alphabet_finite line 868
  59. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.initial_configuration line 874
  60. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.finalTapes_input line 882
  61. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.finalTapes_output line 883
  62. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.finalTapes_work_empty line 885
  63. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTable.machineInTime line 889