OAI/Computability/PerfectCompleteness/Foundations/ExtraCutCall.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ExtraCutCall.splitLast line 17
  2. theorem OAI.PerfectCompleteness.ExtraCutCall.splitLast_law line 32
  3. def OAI.PerfectCompleteness.ExtraCutCall.middleSwap line 43
  4. theorem OAI.PerfectCompleteness.ExtraCutCall.product_assoc_law line 49
  5. theorem OAI.PerfectCompleteness.ExtraCutCall.lift_split_law line 60
  6. def OAI.PerfectCompleteness.ExtraCutCall.splitAssembled line 83
  7. def OAI.PerfectCompleteness.ExtraCutCall.observationLaw line 93
  8. theorem OAI.PerfectCompleteness.ExtraCutCall.observation_split_law line 99
  9. theorem OAI.PerfectCompleteness.ExtraCutCall.uniform_split_law line 122
  10. abbrev OAI.PerfectCompleteness.ExtraCutCall.EnlargedRecord line 131
  11. def OAI.PerfectCompleteness.ExtraCutCall.splitRecord line 136
  12. theorem OAI.PerfectCompleteness.ExtraCutCall.splitRecord_oldCall line 144
  13. theorem OAI.PerfectCompleteness.ExtraCutCall.splitRecord_fresh line 150
  14. theorem OAI.PerfectCompleteness.ExtraCutCall.record_fresh_law line 158
  15. theorem OAI.PerfectCompleteness.ExtraCutCall.uniform_record_fresh_law line 173
  16. def OAI.PerfectCompleteness.ExtraCutCall.arraysAndFresh line 187
  17. theorem OAI.PerfectCompleteness.ExtraCutCall.arrays_fresh_law line 193
  18. theorem OAI.PerfectCompleteness.ExtraCutCall.uniform_arrays_fresh_law line 219