OAI/Computability/DirectedFeedback/Machines/MachinePreservingLookupClean.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet line 15
  2. inductive OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.Label line 17
  3. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.statement line 22
  4. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.program line 28
  5. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.steps line 32
  6. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.remaining_length_le line 36
  7. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le line 43
  8. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.timePolynomial line 51
  9. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le_timePolynomial line 53
  10. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt line 59
  11. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt line 115
  12. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.initialTapes_eq line 136
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt_fromTapes line 145
  14. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.machine line 166
  15. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookupClean.machineInTime line 177
  16. abbrev OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.Alphabet line 200
  17. def OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendTapes line 202
  18. theorem OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendTapes_source line 206
  19. theorem OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendTapes_destination line 211
  20. theorem OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendTapes_other line 215
  21. theorem OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendTapes_scratch line 220
  22. def OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.firstTapes_inline_MachineAppendAt line 227
  23. def OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.secondTapes_inline_MachineAppendAt line 230
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.finalTapes_eq_inline_MachineAppendAt line 234
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendTrace line 256
  26. def OAI.DFVSGames.Foundations.Complexity.MachineAppendAt.appendInTime line 326
  27. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Lift.statement line 362
  28. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Lift.configuration line 368
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Lift.stepAux line 376
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Lift.step line 389
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Lift.trace line 411
  32. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.update_memory_spare line 438
  33. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.RankLabel line 443
  34. def OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankSkip line 449
  35. def OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankProgram line 452
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankProgram_skip line 471
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rowGuard_succ line 476
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rowGuard_zero line 487
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.zeroRowsTrace line 495
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankRowTrace line 509
  41. def OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.prefixTime line 545
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.prefixTrace line 549
  43. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.prefixTime_le line 576
  44. def OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.queryWord line 586
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.encoded_rows_split line 589
  46. def OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankSteps line 597
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankTrace line 602
  48. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.rankSteps_le line 660
  49. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.idxOf_filter_prefix line 673
  50. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.tableRows_length line 692
  51. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.cloudRank_eq_prefix_count line 695
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.cloudRankTrace line 708
  53. def OAI.DFVSGames.Foundations.Complexity.MachineCloudRank.cloudRankInTime line 731