OAI/Computability/DirectedFeedback/Machines/MachineTuple.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.Reduction.MachineSourceTuple.Tape line 57
  2. inductive OAI.DFVSGames.Reduction.MachineSourceTuple.Label line 64
  3. def OAI.DFVSGames.Reduction.MachineSourceTuple.place line 73
  4. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.place_injective line 77
  5. def OAI.DFVSGames.Reduction.MachineSourceTuple.fill line 81
  6. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.fill_place line 88
  7. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.fill_self line 93
  8. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.fill_update line 103
  9. def OAI.DFVSGames.Reduction.MachineSourceTuple.placedLabel line 112
  10. def OAI.DFVSGames.Reduction.MachineSourceTuple.placedConfiguration line 116
  11. def OAI.DFVSGames.Reduction.MachineSourceTuple.placedStatement line 122
  12. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.placed_stepAux line 134
  13. def OAI.DFVSGames.Reduction.MachineSourceTuple.nextLabel line 159
  14. def OAI.DFVSGames.Reduction.MachineSourceTuple.program line 162
  15. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.placed_step line 173
  16. def OAI.DFVSGames.Reduction.MachineSourceTuple.lookupOutput line 190
  17. def OAI.DFVSGames.Reduction.MachineSourceTuple.placedLookupInTime line 195
  18. def OAI.DFVSGames.Reduction.MachineSourceTuple.copiedTapes line 211
  19. def OAI.DFVSGames.Reduction.MachineSourceTuple.coordinateOutput line 214
  20. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.cleanup_lookupOutput line 222
  21. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.coordinateOutput_savedIndex line 250
  22. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.coordinateOutput_field line 255
  23. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.coordinateOutput_other_field line 262
  24. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.suffix_length_le_input line 267
  25. def OAI.DFVSGames.Reduction.MachineSourceTuple.coordinateInTime line 279
  26. def OAI.DFVSGames.Reduction.MachineSourceTuple.labelAt line 324
  27. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.nextLabel_eq line 327
  28. def OAI.DFVSGames.Reduction.MachineSourceTuple.stageTapes line 329
  29. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.stageTapes_frame line 337
  30. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.stageTapes_clean line 350
  31. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.stageTapes_field line 362
  32. def OAI.DFVSGames.Reduction.MachineSourceTuple.prefixInTime line 387
  33. def OAI.DFVSGames.Reduction.MachineSourceTuple.loadInTime line 430
  34. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.equations_length_le_input line 453
  35. def OAI.DFVSGames.Reduction.MachineSourceTuple.loadUnaryInTime line 458
  36. def OAI.DFVSGames.Reduction.MachineSourceTuple.timePolynomial line 481
  37. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.timePolynomial_eval line 484
  38. def OAI.DFVSGames.Reduction.MachineSourceTuple.tupleBitLength line 490
  39. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.savedIndex_length_le_tupleBitLength line 494
  40. def OAI.DFVSGames.Reduction.MachineSourceTuple.loadTupleInTime line 499
  41. def OAI.DFVSGames.Reduction.MachineSourceTuple.loadTuplePolynomialInTime line 513
  42. def OAI.DFVSGames.Reduction.MachineSourceTuple.nameSlot line 531
  43. def OAI.DFVSGames.Reduction.MachineSourceTuple.nameField line 532
  44. def OAI.DFVSGames.Reduction.MachineSourceTuple.rhsField line 533
  45. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.nameField_ne_rhsField line 536
  46. def OAI.DFVSGames.Reduction.MachineSourceTuple.equationName line 545
  47. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.equationWords_name line 551
  48. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.output_name line 558
  49. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.output_rhs line 565
  50. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.output_savedIndex line 573
  51. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.output_savedIndex_unary line 579
  52. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.output_source line 586
  53. def OAI.DFVSGames.Reduction.MachineSourceTuple.canonicalFields line 591
  54. def OAI.DFVSGames.Reduction.MachineSourceTuple.canonicalWords line 594
  55. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.output_canonicalFields line 598
  56. theorem OAI.DFVSGames.Reduction.MachineSourceTuple.zeroWidthStep line 607
  57. def OAI.DFVSGames.Reduction.MachineSourceTuple.placedLoadUnaryInTime line 611
  58. def OAI.DFVSGames.Reduction.MachineSourceTuple.machine line 628
  59. def OAI.DFVSGames.Reduction.CloneTable.cloneName line 650
  60. theorem OAI.DFVSGames.Reduction.CloneTable.cloneName_value line 656
  61. def OAI.DFVSGames.Reduction.CloneTable.cloneEquation line 660
  62. def OAI.DFVSGames.Reduction.CloneTable.clonedEquations line 665
  63. theorem OAI.DFVSGames.Reduction.CloneTable.length_flatMap_map_inline_CloneTable line 668
  64. theorem OAI.DFVSGames.Reduction.CloneTable.clonedEquations_length line 678
  65. theorem OAI.DFVSGames.Reduction.CloneTable.clonedEquations_nonempty line 682
  66. theorem OAI.DFVSGames.Reduction.CloneTable.cloned_sourceList line 688
  67. theorem OAI.DFVSGames.Reduction.CloneTable.cloned_ofList_sourceList line 702
  68. theorem OAI.DFVSGames.Reduction.CloneTable.source_reconstructed line 707
  69. theorem OAI.DFVSGames.Reduction.CloneTable.ofList_congr_inline_CloneTable line 718
  70. def OAI.DFVSGames.Reduction.CloneTable.eraseEquation line 724
  71. def OAI.DFVSGames.Reduction.CloneTable.natCloneEquation line 727
  72. def OAI.DFVSGames.Reduction.CloneTable.natClonedEquations line 730
  73. theorem OAI.DFVSGames.Reduction.CloneTable.erase_cloneEquation line 733
  74. theorem OAI.DFVSGames.Reduction.CloneTable.erase_clonedEquations line 740
  75. def OAI.DFVSGames.Reduction.CloneTable.cloneEquationWords line 750
  76. def OAI.DFVSGames.Reduction.CloneTable.clonedBodyWords line 754
  77. theorem OAI.DFVSGames.Reduction.CloneTable.cloneEquation_words line 757
  78. theorem OAI.DFVSGames.Reduction.CloneTable.clonedEquations_words line 764
  79. def OAI.DFVSGames.Reduction.CloneTable.clonedInput line 773
  80. def OAI.DFVSGames.Reduction.CloneTable.clonedInputWords line 778
  81. theorem OAI.DFVSGames.Reduction.CloneTable.clonedInput_equations line 782
  82. theorem OAI.DFVSGames.Reduction.CloneTable.clonedInput_source line 787
  83. theorem OAI.DFVSGames.Reduction.CloneTable.clonedInput_words line 795
  84. theorem OAI.DFVSGames.Reduction.CloneTable.clonedInput_decodes line 800
  85. theorem OAI.DFVSGames.Reduction.CloneTable.clonedInput_bits_length_le line 805
  86. inductive OAI.DFVSGames.Reduction.CloneMachineModel.Tape line 828
  87. abbrev OAI.DFVSGames.Reduction.CloneMachineModel.Context line 832
  88. abbrev OAI.DFVSGames.Reduction.CloneMachineModel.State line 833
  89. abbrev OAI.DFVSGames.Reduction.CloneMachineModel.Alphabet line 834
  90. inductive OAI.DFVSGames.Reduction.CloneMachineModel.Label line 836
  91. def OAI.DFVSGames.Reduction.CloneMachineModel.defaultControl line 852
  92. def OAI.DFVSGames.Reduction.CloneMachineModel.initialState line 853
  93. def OAI.DFVSGames.Reduction.CloneMachineModel.headerTape line 855
  94. def OAI.DFVSGames.Reduction.CloneMachineModel.contextSource line 857
  95. def OAI.DFVSGames.Reduction.CloneMachineModel.contextScale line 861
  96. def OAI.DFVSGames.Reduction.CloneMachineModel.tripleField line 865
  97. def OAI.DFVSGames.Reduction.CloneMachineModel.contextOffset line 872
  98. def OAI.DFVSGames.Reduction.CloneMachineModel.affineEmit line 876
  99. def OAI.DFVSGames.Reduction.CloneMachineModel.emission line 880
  100. def OAI.DFVSGames.Reduction.CloneMachineModel.contextNext line 883
  101. def OAI.DFVSGames.Reduction.CloneMachineModel.cleanupNext line 890
  102. def OAI.DFVSGames.Reduction.CloneMachineModel.drain line 893
  103. def OAI.DFVSGames.Reduction.CloneMachineModel.program line 900
  104. def OAI.DFVSGames.Reduction.CloneMachineModel.machine line 923