OAI/Computability/PerfectCompleteness/Decoding/UpperScalarCutErasure.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.UpperScalarCutErasure.assocTapeEquiv line 18
  2. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.evaluate_cast line 26
  3. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.evaluate_assocTapeEquiv line 36
  4. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.cast_step_selected line 45
  5. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.assocTapeEquiv_selected line 57
  6. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.extract_assocTapeEquiv line 65
  7. def OAI.PerfectCompleteness.UpperScalarCutErasure.upperReadRecord line 79
  8. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.upperReadRecord_reconstruct line 90
  9. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.ownValues_readRecord line 103
  10. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.upperReadRecord_ownValues line 122
  11. def OAI.PerfectCompleteness.UpperScalarCutErasure.upperPairRecord line 138
  12. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.originalPairRecord_numberRecord line 148
  13. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.upperBuckets_eq_ownValues line 164
  14. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.pairRecord_read_eq_upper line 176
  15. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.enlargedPairRecord_read_eq_upper line 197
  16. theorem OAI.PerfectCompleteness.UpperScalarCutErasure.numberedPairRecord_read_eq_upper line 213