OAI/Computability/PerfectCompleteness/Repetition/CleanNativeReplay.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CleanNativeReplay.transport_target_heq line 20
  2. theorem OAI.PerfectCompleteness.CleanNativeReplay.evaluateArrays_heq line 32
  3. abbrev OAI.PerfectCompleteness.CleanNativeReplay.context line 50
  4. abbrev OAI.PerfectCompleteness.CleanNativeReplay.leftOwn line 51
  5. abbrev OAI.PerfectCompleteness.CleanNativeReplay.rightOwn line 52
  6. abbrev OAI.PerfectCompleteness.CleanNativeReplay.leftSlots line 54
  7. abbrev OAI.PerfectCompleteness.CleanNativeReplay.rightSlots line 58
  8. abbrev OAI.PerfectCompleteness.CleanNativeReplay.leftTape line 62
  9. abbrev OAI.PerfectCompleteness.CleanNativeReplay.rightTape line 66
  10. theorem OAI.PerfectCompleteness.CleanNativeReplay.leftSlots_eq line 70
  11. theorem OAI.PerfectCompleteness.CleanNativeReplay.rightSlots_eq line 76
  12. theorem OAI.PerfectCompleteness.CleanNativeReplay.leftReplay_heq line 82
  13. theorem OAI.PerfectCompleteness.CleanNativeReplay.rightReplay_heq line 106
  14. theorem OAI.PerfectCompleteness.CleanNativeReplay.left_grouped_zero line 137
  15. theorem OAI.PerfectCompleteness.CleanNativeReplay.right_grouped_zero line 151
  16. theorem OAI.PerfectCompleteness.CleanNativeReplay.leftArrays_heq line 165
  17. theorem OAI.PerfectCompleteness.CleanNativeReplay.rightArrays_heq line 177