OAI/Computability/PerfectCompleteness/Decoding/UpperCutOldRecord.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UpperCutOldRecord.product_swap line 20
  2. theorem OAI.PerfectCompleteness.UpperCutOldRecord.product_fst line 28
  3. abbrev OAI.PerfectCompleteness.UpperCutOldRecord.OldRecord line 47
  4. def OAI.PerfectCompleteness.UpperCutOldRecord.oldView line 52
  5. def OAI.PerfectCompleteness.UpperCutOldRecord.arrayView line 57
  6. def OAI.PerfectCompleteness.UpperCutOldRecord.oldCall line 63
  7. theorem OAI.PerfectCompleteness.UpperCutOldRecord.oldCall_injective line 70
  8. def OAI.PerfectCompleteness.UpperCutOldRecord.restrictedRecord line 77
  9. theorem OAI.PerfectCompleteness.UpperCutOldRecord.number_oldRecord line 85
  10. theorem OAI.PerfectCompleteness.UpperCutOldRecord.oldView_numberedPairRecord line 95
  11. def OAI.PerfectCompleteness.UpperCutOldRecord.arrayLaw line 114
  12. theorem OAI.PerfectCompleteness.UpperCutOldRecord.restrictedRecord_law line 127
  13. theorem OAI.PerfectCompleteness.UpperCutOldRecord.pairLaw_oldView line 154
  14. def OAI.PerfectCompleteness.UpperCutOldRecord.modifiedArrayLaw line 212
  15. theorem OAI.PerfectCompleteness.UpperCutOldRecord.modifiedPair_oldView line 227