OAI/Computability/PerfectCompleteness/Machines/OriginalWholeCutTape.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.OriginalWholeCutTape.regroupStep line 22
  2. def OAI.PerfectCompleteness.OriginalWholeCutTape.prependUnit line 43
  3. abbrev OAI.PerfectCompleteness.OriginalWholeCutTape.cutSlots line 53
  4. def OAI.PerfectCompleteness.OriginalWholeCutTape.Exterior line 58
  5. def OAI.PerfectCompleteness.OriginalWholeCutTape.exteriorFintypeAux line 68
  6. instance OAI.PerfectCompleteness.OriginalWholeCutTape.exteriorFintype line 82
  7. def OAI.PerfectCompleteness.OriginalWholeCutTape.exteriorZero line 86
  8. instance OAI.PerfectCompleteness.OriginalWholeCutTape.exteriorNonempty line 94
  9. abbrev OAI.PerfectCompleteness.OriginalWholeCutTape.BelowTape line 98
  10. abbrev OAI.PerfectCompleteness.OriginalWholeCutTape.Calls line 103
  11. def OAI.PerfectCompleteness.OriginalWholeCutTape.splitTape line 109
  12. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.splitTape_refl line 133
  13. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.splitTape_step_exterior line 139
  14. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.splitTape_step_rootCall line 149
  15. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.splitTape_step_lowerCall line 160
  16. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.splitTape_step_below line 169
  17. def OAI.PerfectCompleteness.OriginalWholeCutTape.exteriorLaw line 176
  18. def OAI.PerfectCompleteness.OriginalWholeCutTape.callsLaw line 180
  19. def OAI.PerfectCompleteness.OriginalWholeCutTape.belowLaw line 187
  20. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.callsLaw_uniform line 194
  21. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.belowLaw_uniform line 201
  22. theorem OAI.PerfectCompleteness.OriginalWholeCutTape.split_tapeLaw line 211