OAI/Computability/PerfectCompleteness/Foundations/WholeCutGrouping.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeCutGrouping.F2 line 15
  2. def OAI.PerfectCompleteness.WholeCutGrouping.regroupStep line 23
  3. abbrev OAI.PerfectCompleteness.WholeCutGrouping.cutSlots line 51
  4. def OAI.PerfectCompleteness.WholeCutGrouping.Exterior line 56
  5. def OAI.PerfectCompleteness.WholeCutGrouping.exteriorFintypeAux line 66
  6. instance OAI.PerfectCompleteness.WholeCutGrouping.exteriorFintype line 80
  7. def OAI.PerfectCompleteness.WholeCutGrouping.exteriorZero line 84
  8. instance OAI.PerfectCompleteness.WholeCutGrouping.exteriorNonempty line 92
  9. def OAI.PerfectCompleteness.WholeCutGrouping.splitTape line 96
  10. def OAI.PerfectCompleteness.WholeCutGrouping.exteriorLaw line 114
  11. theorem OAI.PerfectCompleteness.WholeCutGrouping.split_tapeLaw line 119