OAI/Computability/PerfectCompleteness/Decoding/UpperScalarCutReconstructionLemmas.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UpperScalarCutReconstruction.cutSlots_append line 20
  2. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.cutSpaceEquiv line 26
  3. abbrev OAI.PerfectCompleteness.UpperScalarCutReconstruction.FreshExterior line 32
  4. abbrev OAI.PerfectCompleteness.UpperScalarCutReconstruction.FreshValues line 36
  5. abbrev OAI.PerfectCompleteness.UpperScalarCutReconstruction.FreshRecord line 40
  6. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.readFresh line 44
  7. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.reconstructFresh line 54
  8. theorem OAI.PerfectCompleteness.UpperScalarCutReconstruction.reconstructFresh_readFresh line 60
  9. abbrev OAI.PerfectCompleteness.UpperScalarCutReconstruction.Exterior line 70
  10. abbrev OAI.PerfectCompleteness.UpperScalarCutReconstruction.Record line 75
  11. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.pack line 81
  12. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.oldRecord line 87
  13. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.freshRecord line 93
  14. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.packEquiv line 98
  15. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.observe line 113
  16. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.read line 121
  17. theorem OAI.PerfectCompleteness.UpperScalarCutReconstruction.observe_read line 131
  18. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.reconstruct line 145
  19. theorem OAI.PerfectCompleteness.UpperScalarCutReconstruction.reconstruct_read line 152
  20. abbrev OAI.PerfectCompleteness.UpperScalarCutReconstruction.NumberedRecord line 165
  21. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.numberRecordEquiv line 172
  22. def OAI.PerfectCompleteness.UpperScalarCutReconstruction.numberedObserve line 179
  23. theorem OAI.PerfectCompleteness.UpperScalarCutReconstruction.numberedObserve_numberRecord line 185
  24. def OAI.PerfectCompleteness.UpperScalarCutBucket.descendRecord line 209
  25. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.restrictArrays_reconstruct line 219
  26. def OAI.PerfectCompleteness.UpperScalarCutBucket.rootBuckets line 247
  27. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.rootRows_reconstruct line 257
  28. def OAI.PerfectCompleteness.UpperScalarCutBucket.upperBuckets line 266
  29. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.selectedRows_reconstruct line 273
  30. def OAI.PerfectCompleteness.UpperScalarCutBucket.descendTape line 285
  31. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.descendRecord_readRecord line 296
  32. def OAI.PerfectCompleteness.UpperScalarCutBucket.continuedRootTape line 312
  33. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.rootBuckets_readRecord line 321
  34. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.upperBuckets_readRecord line 335
  35. def OAI.PerfectCompleteness.UpperScalarCutBucket.replaceArrays line 348
  36. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.replaceArrays_rankOne line 359
  37. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.replaceArrays_outside line 374
  38. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.matrix_reconstruct line 384
  39. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.matrix_replaceArrays line 396
  40. def OAI.PerfectCompleteness.UpperScalarCutBucket.pairRecord line 412
  41. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.pairRecord_eq line 424
  42. def OAI.PerfectCompleteness.UpperScalarCutBucket.enlargedPairRecord line 441
  43. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.enlargedPairRecord_read line 452
  44. def OAI.PerfectCompleteness.UpperScalarCutBucket.numberedPairRecord line 470
  45. theorem OAI.PerfectCompleteness.UpperScalarCutBucket.numberedPairRecord_numberRecord line 479