OAI/GroupTheory/PeriodicGroups/Machines/TimedExecution.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SourceBurnside.OneTape.Coding line 11
  2. def OAI.SourceBurnside.OneTape.Coding.oneHotEncode line 21
  3. lemma OAI.SourceBurnside.OneTape.Coding.oneHotEncode_injective line 24
  4. def OAI.SourceBurnside.OneTape.Coding.oneHot line 31
  5. lemma OAI.SourceBurnside.OneTape.Coding.encode_injective line 43
  6. def OAI.SourceBurnside.OneTape.Coding.transition line 45
  7. structure OAI.SourceBurnside.OneTape.Coding.Realization line 49
  8. def OAI.SourceBurnside.OneTape.Coding.realization line 55
  9. def OAI.SourceBurnside.OneTape.Coding.trace line 60
  10. theorem OAI.SourceBurnside.OneTape.Coding.local_trace line 63
  11. lemma OAI.SourceBurnside.OneTape.far_cell line 80
  12. lemma OAI.SourceBurnside.OneTape.Coding.boundary_trace line 97
  13. theorem OAI.SourceBurnside.OneTape.Coding.rectangle_valid line 112
  14. theorem OAI.SourceBurnside.OneTape.Coding.rectangle_run line 129
  15. def OAI.SourceBurnside.Addressable.InputBit.mapBool line 144
  16. lemma OAI.SourceBurnside.Addressable.InputBit.eval_mapBool line 152
  17. structure OAI.SourceBurnside.OneTape.Input line 166
  18. def OAI.SourceBurnside.OneTape.Input.symbol line 175
  19. def OAI.SourceBurnside.OneTape.Input.config line 181
  20. def OAI.SourceBurnside.OneTape.Input.reading line 183
  21. lemma OAI.SourceBurnside.OneTape.Input.reading_eval line 190
  22. lemma OAI.SourceBurnside.OneTape.Input.left_blank line 200
  23. lemma OAI.SourceBurnside.OneTape.Input.right_blank line 207
  24. def OAI.SourceBurnside.OneTape.Input.initialBits line 214
  25. lemma OAI.SourceBurnside.OneTape.Input.initialBits_eval line 217
  26. theorem OAI.SourceBurnside.OneTape.Input.addressed_rectangle line 222
  27. theorem OAI.SourceBurnside.OneTape.Input.certificate_machine_iff line 237
  28. def OAI.SourceBurnside.OneTape.Frozen line 257
  29. lemma OAI.SourceBurnside.OneTape.step_of_frozen line 260
  30. lemma OAI.SourceBurnside.OneTape.run_of_step_eq line 268
  31. lemma OAI.SourceBurnside.OneTape.run_eq_of_frozen line 274
  32. theorem OAI.SourceBurnside.OneTape.final_accept_iff line 280
  33. lemma OAI.SourceBurnside.ExponentialThreshold.polynomial_lt line 301
  34. lemma OAI.SourceBurnside.ExponentialThreshold.scaled line 312
  35. lemma OAI.SourceBurnside.RawFit.eventually_fits line 330
  36. opaque OAI.SourceBurnside.SourceMachine.coding line 394
  37. opaque OAI.SourceBurnside.SourceMachine.localCircuit line 395
  38. abbrev OAI.SourceBurnside.SourceMachine.β line 396
  39. abbrev OAI.SourceBurnside.SourceMachine.g line 397
  40. def OAI.SourceBurnside.SourceMachine.blankBits line 398
  41. def OAI.SourceBurnside.SourceMachine.initialBits line 399
  42. def OAI.SourceBurnside.SourceMachine.acceptBits line 400
  43. def OAI.SourceBurnside.SourceMachine.bitEncoding line 401
  44. def OAI.SourceBurnside.SourceMachine.body line 402
  45. lemma OAI.SourceBurnside.SourceMachine.bit_positive line 404
  46. theorem OAI.SourceBurnside.SourceMachine.timed_selfpoint line 406
  47. abbrev OAI.SourceBurnside.TimedTape.addressedInput line 447
  48. lemma OAI.SourceBurnside.TimedTape.initial_store line 449
  49. lemma OAI.SourceBurnside.TimedTape.raw_symbol_zero line 459
  50. lemma OAI.SourceBurnside.TimedTape.raw_symbol_pos line 460
  51. lemma OAI.SourceBurnside.TimedTape.raw_symbol_far line 469
  52. lemma OAI.SourceBurnside.TimedTape.addressed_config line 479
  53. def OAI.SourceBurnside.SourceMachine.candidateBits line 504
  54. lemma OAI.SourceBurnside.SourceMachine.candidate_length line 508
  55. lemma OAI.SourceBurnside.SourceMachine.candidate_length_le line 512
  56. lemma OAI.SourceBurnside.SourceMachine.source_input_eval line 517
  57. lemma OAI.SourceBurnside.SourceMachine.small_arity line 524
  58. lemma OAI.SourceBurnside.SourceMachine.source_input_length line 526
  59. lemma OAI.SourceBurnside.SourceMachine.source_config line 537
  60. def OAI.SourceBurnside.SourceMachine.layout line 544
  61. lemma OAI.SourceBurnside.SourceMachine.layout_origin line 551
  62. lemma OAI.SourceBurnside.SourceMachine.input_short line 552
  63. theorem OAI.SourceBurnside.SourceMachine.tableau_selfpoint line 563
  64. lemma OAI.SourceBurnside.TimedTape.initialBits_row line 608
  65. lemma OAI.SourceBurnside.FiniteTable.Codec.field_of_bits line 639
  66. def OAI.SourceBurnside.SourceMachine.candidateWord line 655
  67. lemma OAI.SourceBurnside.SourceMachine.candidate_bit line 658
  68. lemma OAI.SourceBurnside.SourceMachine.candidate_field line 690
  69. lemma OAI.SourceBurnside.SourceMachine.candidate_lengthOK line 701
  70. lemma OAI.SourceBurnside.SourceMachine.candidate_piece line 707
  71. lemma OAI.SourceBurnside.SourceMachine.candidate_body_eq line 728
  72. lemma OAI.SourceBurnside.SourceMachine.sourceBody_boolean line 741
  73. lemma OAI.SourceBurnside.SourceMachine.sourceBody_eq_one_iff_ne_zero line 743
  74. def OAI.SourceBurnside.SourceMachine.sourceInitial line 752
  75. def OAI.SourceBurnside.SourceMachine.sourceSchedule line 755
  76. lemma OAI.SourceBurnside.SourceMachine.sourceInitial_input line 759
  77. lemma OAI.SourceBurnside.SourceMachine.physical_represents line 765
  78. lemma OAI.SourceBurnside.SourceMachine.local_zero_one line 779
  79. lemma OAI.SourceBurnside.SourceMachine.local_zero_two line 791
  80. lemma OAI.SourceBurnside.SourceMachine.local_rep_one line 804
  81. lemma OAI.SourceBurnside.SourceMachine.local_rep_two line 817
  82. lemma OAI.SourceBurnside.SourceMachine.candidate_entry line 839
  83. theorem OAI.SourceBurnside.SourceMachine.fixed_table_certificate line 901