OAI/Computability/PerfectCompleteness/Repetition/CleanRecordChildBlocks.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanRecordChildBlocks.Record line 21
  2. abbrev OAI.PerfectCompleteness.CleanRecordChildBlocks.Sample line 26
  3. abbrev OAI.PerfectCompleteness.CleanRecordChildBlocks.Row line 28
  4. def OAI.PerfectCompleteness.CleanRecordChildBlocks.clean line 32
  5. def OAI.PerfectCompleteness.CleanRecordChildBlocks.visible line 37
  6. def OAI.PerfectCompleteness.CleanRecordChildBlocks.projected line 42
  7. def OAI.PerfectCompleteness.CleanRecordChildBlocks.event line 47
  8. abbrev OAI.PerfectCompleteness.CleanRecordChildBlocks.Nonclean line 53
  9. def OAI.PerfectCompleteness.CleanRecordChildBlocks.extract line 56
  10. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.record_extract line 63
  11. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.extract_eq line 74
  12. def OAI.PerfectCompleteness.CleanRecordChildBlocks.source line 97
  13. def OAI.PerfectCompleteness.CleanRecordChildBlocks.raw line 102
  14. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.visible_nonclean line 107
  15. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.projected_nonclean line 123
  16. def OAI.PerfectCompleteness.CleanRecordChildBlocks.leftRef line 135
  17. def OAI.PerfectCompleteness.CleanRecordChildBlocks.rightRef line 140
  18. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.leftRef_childSlots line 145
  19. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.rightRef_childSlots line 157
  20. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.leftRef_childSlots_event line 174
  21. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.rightRef_childSlots_event line 186
  22. def OAI.PerfectCompleteness.CleanRecordChildBlocks.physicalRight line 199
  23. def OAI.PerfectCompleteness.CleanRecordChildBlocks.physicalLeft line 204
  24. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.physicalLeft_eq_leftChildren line 213
  25. def OAI.PerfectCompleteness.CleanRecordChildBlocks.rightChild line 221
  26. def OAI.PerfectCompleteness.CleanRecordChildBlocks.leftChild line 227
  27. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.rightChild_heq line 233
  28. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.leftChild_heq line 239
  29. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.dependent_congr line 245
  30. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.rightChild_event_heq line 250
  31. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.leftChild_event_heq line 261
  32. theorem OAI.PerfectCompleteness.CleanRecordChildBlocks.childClean_of_clean line 277