OAI/Computability/PerfectCompleteness/Foundations/WholeArrayComposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.WholeArrayComposition.collapseRoot line 19
  2. theorem OAI.PerfectCompleteness.WholeArrayComposition.evaluate_collapseRoot line 25
  3. def OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix line 43
  4. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix_refl line 55
  5. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix_root line 60
  6. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix_selected line 67
  7. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix_ordinary line 74
  8. theorem OAI.PerfectCompleteness.WholeArrayComposition.evaluate_collapseSuffix line 81
  9. def OAI.PerfectCompleteness.WholeArrayComposition.collapsedRootLaw line 96
  10. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseRoot_tapeLaw line 102
  11. def OAI.PerfectCompleteness.WholeArrayComposition.collapsedTapeLaw line 118
  12. def OAI.PerfectCompleteness.WholeArrayComposition.collapseField line 139
  13. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix_step line 153
  14. theorem OAI.PerfectCompleteness.WholeArrayComposition.collapseSuffix_tapeLaw line 166
  15. theorem OAI.PerfectCompleteness.WholeArrayComposition.law_append line 204