OAI/Computability/PerfectCompleteness/Foundations/WholeCutReplayGroupingTransport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.F2 line 14
  2. abbrev OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.ChildBlock line 22
  3. def OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.castChildren line 26
  4. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.castChildren_apply_heq line 36
  5. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.blockCast_calls line 45
  6. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.blockCast_arrays line 53
  7. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.castChildren_calls line 61
  8. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.castChildren_arrays line 72
  9. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.blockCast_reindex line 83
  10. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.blockTransport_eq_cast line 92
  11. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.arraysTransport_eq_cast line 111
  12. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.cast_exterior_parts line 123
  13. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.exterior_equiv_step line 134
  14. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.castChildren_tail line 153
  15. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.transport_assemble line 169
  16. theorem OAI.PerfectCompleteness.WholeCutReplayGroupingTransport.transportTape_target_eq line 243