OAI/Computability/DirectedFeedback/RankGraph/MachineClone100Cleanup.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_eq_flatMap line 58
  2. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_append line 67
  3. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.affineEmit_replicate_true line 74
  4. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.affineEmit_word line 81
  5. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.affineEmit_word_append line 88
  6. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.affineEmit_words line 93
  7. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_word line 101
  8. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_word_append line 108
  9. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_words line 115
  10. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_header_variables line 122
  11. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_header_count line 127
  12. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_field line 132
  13. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_first_field line 138
  14. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_second_field line 144
  15. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_third_field line 150
  16. theorem OAI.DFVSGames.Explicit.MachineClone100Affine.output_rhs_field line 156
  17. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.drainStep_cons line 177
  18. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.drainStep_nil line 190
  19. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.drainTrace line 202
  20. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.drainTrace_base line 222
  21. def OAI.DFVSGames.Explicit.MachineClone100Cleanup.drainInTime line 232
  22. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearHeaderTrace line 246
  23. def OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearHeaderInTime line 254
  24. def OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields line 263
  25. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_field line 267
  26. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_other line 271
  27. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_input line 275
  28. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_header line 277
  29. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_counter line 279
  30. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_scratch line 281
  31. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_reversed line 283
  32. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_output line 285
  33. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_eq_self line 288
  34. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.clearFields_idempotent line 293
  35. def OAI.DFVSGames.Explicit.MachineClone100Cleanup.cleanupSteps line 297
  36. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.cleanupTrace line 301
  37. theorem OAI.DFVSGames.Explicit.MachineClone100Cleanup.cleanupFourTrace line 311
  38. def OAI.DFVSGames.Explicit.MachineClone100Cleanup.cleanupFourInTime line 350
  39. def OAI.DFVSGames.Explicit.MachineClone100Headers.parsedTapes line 377
  40. def OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes line 384
  41. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_input line 392
  42. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_header line 394
  43. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_counter line 396
  44. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_reversed line 398
  45. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_scratch line 401
  46. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_field line 403
  47. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.resultTapes_output line 405
  48. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.twoFieldsTapes_inline_MachineClone100Headers line 408
  49. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.firstContextTapes_inline_MachineClone100Headers line 417
  50. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.secondContextTapes_inline_MachineClone100Headers line 425
  51. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.clearHeaderTapes_inline_MachineClone100Headers line 435
  52. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.headersTrace line 444
  53. def OAI.DFVSGames.Explicit.MachineClone100Headers.headersInTime line 519
  54. theorem OAI.DFVSGames.Explicit.MachineClone100Headers.headersTime_linear line 532
  55. def OAI.DFVSGames.Explicit.MachineClone100Triples.rowOutput line 547
  56. def OAI.DFVSGames.Explicit.MachineClone100Triples.rowSteps line 553
  57. def OAI.DFVSGames.Explicit.MachineClone100Triples.startAt line 557
  58. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.contextTapes_field line 560
  59. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.rowOutput_update line 565
  60. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.rowSteps_update line 570
  61. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.chain_inline_MachineClone100Triples line 574
  62. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.fourContexts_tapes line 578
  63. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.rowTrace line 589
  64. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.tailTrace_inline_MachineClone100Triples line 624
  65. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.tableTrace_raw line 664
  66. def OAI.DFVSGames.Explicit.MachineClone100Triples.affineRecord line 675
  67. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.rowOutput_words line 678
  68. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.tableOutput_words line 686
  69. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.tableTrace line 698
  70. theorem OAI.DFVSGames.Explicit.MachineClone100Triples.tableTapes_other line 712
  71. structure OAI.DFVSGames.Explicit.MachineClone100Loop.Record line 732
  72. def OAI.DFVSGames.Explicit.MachineClone100Loop.recordWords line 738
  73. def OAI.DFVSGames.Explicit.MachineClone100Loop.recordBits line 739
  74. def OAI.DFVSGames.Explicit.MachineClone100Loop.recordsBits line 740
  75. def OAI.DFVSGames.Explicit.MachineClone100Loop.clonedRecordBits line 742
  76. def OAI.DFVSGames.Explicit.MachineClone100Loop.clonedRecordsBits line 745
  77. def OAI.DFVSGames.Explicit.MachineClone100Loop.recordFields line 748
  78. def OAI.DFVSGames.Explicit.MachineClone100Loop.tapes line 751
  79. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.update_reversed line 761
  80. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.counterTapes_eq line 768
  81. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.fourTapes_eq line 776
  82. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.clearFields_eq line 791
  83. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.cleanupSteps_eq line 798
  84. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.recordBits_length line 805
  85. def OAI.DFVSGames.Explicit.MachineClone100Loop.bodyCost line 810
  86. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.bodyCost_eq_inline_MachineClone100Loop line 813
  87. def OAI.DFVSGames.Explicit.MachineClone100Loop.bodyInTime line 820
  88. def OAI.DFVSGames.Explicit.MachineClone100Loop.loopCost line 869
  89. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.loopCost_eq line 873
  90. def OAI.DFVSGames.Explicit.MachineClone100Loop.loopInTime line 883
  91. def OAI.DFVSGames.Explicit.MachineClone100Loop.loopInTime_linear line 917
  92. def OAI.DFVSGames.Explicit.MachineClone100Loop.recordOfEquation line 929
  93. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.recordsBits_equations line 932
  94. theorem OAI.DFVSGames.Explicit.MachineClone100Loop.clonedRecordsBits_equations_table line 942
  95. def OAI.DFVSGames.Explicit.MachineClone100Loop.sourceLoopInTime_table line 953