OAI/Computability/PerfectCompleteness/Construction/OriginalChildBlocks.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalChildBlocks.uniform_product line 20
  2. def OAI.PerfectCompleteness.OriginalChildBlocks.rawEquiv line 31
  3. def OAI.PerfectCompleteness.OriginalChildBlocks.arrayComponent line 36
  4. def OAI.PerfectCompleteness.OriginalChildBlocks.specialLaw line 42
  5. def OAI.PerfectCompleteness.OriginalChildBlocks.componentLaw line 53
  6. theorem OAI.PerfectCompleteness.OriginalChildBlocks.callComponent_uniform line 64
  7. theorem OAI.PerfectCompleteness.OriginalChildBlocks.componentLaw_eq line 75
  8. abbrev OAI.PerfectCompleteness.OriginalChildBlocks.SourceTape line 101
  9. def OAI.PerfectCompleteness.OriginalChildBlocks.sourceLaw line 106
  10. def OAI.PerfectCompleteness.OriginalChildBlocks.rawMap line 112
  11. theorem OAI.PerfectCompleteness.OriginalChildBlocks.rawMap_call line 120
  12. theorem OAI.PerfectCompleteness.OriginalChildBlocks.rawMap_array line 127
  13. theorem OAI.PerfectCompleteness.OriginalChildBlocks.rawMap_product_law line 135
  14. theorem OAI.PerfectCompleteness.OriginalChildBlocks.rawMap_law line 164
  15. def OAI.PerfectCompleteness.OriginalChildBlocks.observed line 177
  16. theorem OAI.PerfectCompleteness.OriginalChildBlocks.assemble_rawMap line 184
  17. theorem OAI.PerfectCompleteness.OriginalChildBlocks.observed_law line 196