OAI/Computability/PerfectCompleteness/Sampling/WholeCutSampler.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeCutSampler.F2 line 16
  2. abbrev OAI.PerfectCompleteness.WholeCutSampler.RootTape line 22
  3. def OAI.PerfectCompleteness.WholeCutSampler.Tape line 27
  4. def OAI.PerfectCompleteness.WholeCutSampler.tapeFintypeAux line 38
  5. instance OAI.PerfectCompleteness.WholeCutSampler.tapeFintype line 53
  6. def OAI.PerfectCompleteness.WholeCutSampler.zeroTape line 57
  7. instance OAI.PerfectCompleteness.WholeCutSampler.tapeNonempty line 67
  8. def OAI.PerfectCompleteness.WholeCutSampler.stepEquiv line 71
  9. def OAI.PerfectCompleteness.WholeCutSampler.assembleArrays line 90
  10. theorem OAI.PerfectCompleteness.WholeCutSampler.assembleArrays_surjective line 103
  11. def OAI.PerfectCompleteness.WholeCutSampler.collapseRoot line 114
  12. def OAI.PerfectCompleteness.WholeCutSampler.collapse line 119
  13. def OAI.PerfectCompleteness.WholeCutSampler.rootLaw line 133
  14. def OAI.PerfectCompleteness.WholeCutSampler.tapeLaw line 139
  15. theorem OAI.PerfectCompleteness.WholeCutSampler.uniform_product line 152
  16. theorem OAI.PerfectCompleteness.WholeCutSampler.rootLaw_eq_uniform line 161
  17. theorem OAI.PerfectCompleteness.WholeCutSampler.tapeLaw_eq_uniform line 167
  18. def OAI.PerfectCompleteness.WholeCutSampler.stepComponent line 195
  19. theorem OAI.PerfectCompleteness.WholeCutSampler.stepEquiv_law line 206
  20. theorem OAI.PerfectCompleteness.WholeCutSampler.collapseRoot_law line 224
  21. theorem OAI.PerfectCompleteness.WholeCutSampler.terminal_law line 233
  22. theorem OAI.PerfectCompleteness.WholeCutSampler.collapse_tapeLaw line 249
  23. def OAI.PerfectCompleteness.WholeCutSampler.evaluate line 301
  24. def OAI.PerfectCompleteness.WholeCutSampler.law line 306
  25. theorem OAI.PerfectCompleteness.WholeCutSampler.evaluate_law line 311