OAI/Computability/DirectedFeedback/Machines/PoweringMachineRelationField.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.Alphabet line 60
  2. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.State line 61
  3. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.Label line 62
  4. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes line 64
  5. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes_injective line 68
  6. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.source_outside_lookup line 74
  7. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.endpoint line 84
  8. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.endpoint_eq_wordEnd line 87
  9. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.bit line 94
  10. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.instruction line 98
  11. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.afterWord line 107
  12. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes line 113
  13. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.steps line 121
  14. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.afterWord_frame line 127
  15. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_frame line 142
  16. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_other line 159
  17. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.fieldTrace line 172
  18. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelationField.steps_le line 229
  19. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.Alphabet line 253
  20. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.Tape line 254
  21. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.State line 255
  22. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.Label line 256
  23. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.entry line 259
  24. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.instruction line 261
  25. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.endpoint line 277
  26. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.resultBit line 281
  27. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes line 285
  28. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes line 291
  29. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.steps line 301
  30. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.steps_le line 308
  31. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_other line 324
  32. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_role line 344
  33. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_other line 365
  34. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_role line 380
  35. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_output line 391
  36. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.joinTrace_inline_PoweringMachineEqualityField line 404
  37. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.fieldTrace line 408
  38. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.fieldInTime line 510
  39. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineEqualityField.machine line 533
  40. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.firstMatch_of_first line 560
  41. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.firstMatch_firstIndex line 570
  42. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.endpointMask line 579
  43. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.firstMatch_endpointMask line 583
  44. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.slotCount line 593
  45. abbrev OAI.DFVSGames.Foundations.PCP.PoweringRowData.RowBuffer line 595
  46. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.fixedLabelAt line 597
  47. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.fixedLabelAt_addressIndex line 601
  48. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.walkData line 609
  49. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.walkBits line 619
  50. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.basePredicate_walkBits line 623
  51. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.leftMatches_walkBits line 630
  52. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rightMatches_walkBits line 637
  53. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_left line 645
  54. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_right line 655
  55. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.edgeAccept_walkBits line 666
  56. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowAccept_walkBits line 679
  57. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.transposeField line 690
  58. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.transposeBits line 695
  59. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.basePredicate_transposeBits line 698
  60. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.leftMatches_transposeBits line 703
  61. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rightMatches_transposeBits line 709
  62. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.edgeAccept_transposeBits line 715
  63. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowAccept_transposeBits line 724
  64. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowBits line 731
  65. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowData line 735
  66. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowBits_packData line 740
  67. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowBits_field line 747
  68. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowAccept_rowBits line 754
  69. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowBlock_at_rowBits line 764
  70. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.dataWords line 772
  71. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.dataTape line 776
  72. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.dataTape_eq line 780
  73. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.dataWords_length line 785
  74. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.dataTape_length_le line 791
  75. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.emittedRelation line 797
  76. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.emittedRelation_eq line 802
  77. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowBlock_unary line 810
  78. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.emittedRelation_table line 822
  79. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowData.rowBlock_unary_table line 849
  80. def OAI.DFVSGames.Foundations.PCP.PoweringRowData.tableRowMachineInTime line 856