OAI/Computability/PerfectCompleteness/Repetition/CleanPhysicalReplay.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanPhysicalReplay.Exterior line 26
  2. def OAI.PerfectCompleteness.CleanPhysicalReplay.exteriorAt line 29
  3. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.cutSlots_fill line 36
  4. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.childSlots_fill line 41
  5. def OAI.PerfectCompleteness.CleanPhysicalReplay.fillChild line 47
  6. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.fillChild_heq line 55
  7. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.cast_zeroBlock line 61
  8. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.fillChild_zero line 69
  9. def OAI.PerfectCompleteness.CleanPhysicalReplay.retainedAt line 77
  10. def OAI.PerfectCompleteness.CleanPhysicalReplay.assembleAt line 85
  11. def OAI.PerfectCompleteness.CleanPhysicalReplay.physicalTape line 95
  12. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.assembleAt_eq_erase line 103
  13. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.physicalTape_grouped_zero line 120
  14. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.exteriorAt_heq line 142
  15. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.transport_assembleAt line 148
  16. abbrev OAI.PerfectCompleteness.CleanPhysicalReplay.Record line 186
  17. abbrev OAI.PerfectCompleteness.CleanPhysicalReplay.Sample line 189
  18. def OAI.PerfectCompleteness.CleanPhysicalReplay.leftRecord line 192
  19. def OAI.PerfectCompleteness.CleanPhysicalReplay.rightRecord line 202
  20. def OAI.PerfectCompleteness.CleanPhysicalReplay.leftInside line 212
  21. def OAI.PerfectCompleteness.CleanPhysicalReplay.rightInside line 216
  22. def OAI.PerfectCompleteness.CleanPhysicalReplay.leftBlocks line 221
  23. def OAI.PerfectCompleteness.CleanPhysicalReplay.rightBlocks line 227
  24. def OAI.PerfectCompleteness.CleanPhysicalReplay.leftTape line 233
  25. def OAI.PerfectCompleteness.CleanPhysicalReplay.rightTape line 240
  26. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.leftInside_nonclean line 247
  27. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.rightInside_nonclean line 257
  28. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.leftRecord_eq_erase line 267
  29. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.rightRecord_eq_erase line 288
  30. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.rightBlocks_zero line 316
  31. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.leftBlocks_zero line 328
  32. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.rightTape_grouped_zero line 345
  33. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.leftTape_grouped_zero line 358
  34. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.response_of_erase line 370
  35. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.leftRecord_response_eq line 391
  36. theorem OAI.PerfectCompleteness.CleanPhysicalReplay.rightRecord_response_eq line 420
  37. def OAI.PerfectCompleteness.CleanPhysicalReplay.leftReplay line 459
  38. def OAI.PerfectCompleteness.CleanPhysicalReplay.rightReplay line 467