OAI/Computability/PerfectCompleteness/Decoding/UpperScalarCutLaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.scalarLaw_cast line 18
  2. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.cutSpaceEquiv_scalarLaw line 28
  3. def OAI.PerfectCompleteness.UpperScalarCutLaw.freshExteriorLaw line 38
  4. def OAI.PerfectCompleteness.UpperScalarCutLaw.freshValuesLaw line 43
  5. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.readFresh_law line 50
  6. def OAI.PerfectCompleteness.UpperScalarCutLaw.exteriorLaw line 98
  7. def OAI.PerfectCompleteness.UpperScalarCutLaw.valuesLaw line 104
  8. def OAI.PerfectCompleteness.UpperScalarCutLaw.assembledEquiv line 112
  9. def OAI.PerfectCompleteness.UpperScalarCutLaw.assembledLaw line 119
  10. def OAI.PerfectCompleteness.UpperScalarCutLaw.recordLaw line 136
  11. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.pack_law line 144
  12. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.read_law line 174
  13. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.numberRecord_law line 210
  14. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.numbered_read_law line 242
  15. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.observe_law line 257
  16. theorem OAI.PerfectCompleteness.UpperScalarCutLaw.numberedObserve_law line 291