OAI/Computability/Superstring/LayerCode.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.ThreadArray.aligned line 9
  2. theorem OAI.Superstring.ThreadArray.poly_aligned line 12
  3. theorem OAI.Superstring.ThreadArray.countP_range line 19
  4. theorem OAI.Superstring.ThreadArray.aligned_length line 26
  5. def OAI.Superstring.ThreadArray.atLength line 39
  6. theorem OAI.Superstring.ThreadArray.poly_atLength line 43
  7. theorem OAI.Superstring.ThreadArray.atLength_eq line 49
  8. theorem OAI.Superstring.ThreadArray.atLength_bound line 56
  9. def OAI.Superstring.ThreadArray.rankLength line 68
  10. theorem OAI.Superstring.ThreadArray.poly_rankLength line 72
  11. def OAI.Superstring.ThreadArray.lengthValues line 87
  12. theorem OAI.Superstring.ThreadArray.count_rank line 93
  13. theorem OAI.Superstring.ThreadArray.rankLength_eq line 116
  14. theorem OAI.Superstring.ThreadArray.sortedExit_eq_rank line 137
  15. def OAI.Superstring.ThreadArray.exit line 170
  16. theorem OAI.Superstring.ThreadArray.poly_exit line 173
  17. theorem OAI.Superstring.ThreadArray.exit_eq line 182
  18. def OAI.Superstring.WindowCode.down line 206
  19. def OAI.Superstring.WindowCode.up line 209
  20. def OAI.Superstring.WindowCode.route line 212
  21. theorem OAI.Superstring.WindowCode.down_realizes line 216
  22. theorem OAI.Superstring.WindowCode.up_realizes line 239
  23. theorem OAI.Superstring.WindowCode.route_realizes line 263
  24. theorem OAI.Superstring.BitCode.Poly.leInt line 300
  25. theorem OAI.Superstring.BitCode.Poly.ltInt line 306
  26. theorem OAI.Superstring.BitCode.Poly.maxInt line 314
  27. theorem OAI.Superstring.BitCode.Poly.minInt line 321
  28. def OAI.Superstring.PeriodWord.text line 334
  29. def OAI.Superstring.PeriodWord.window line 336
  30. theorem OAI.Superstring.PeriodWord.window_eq line 339
  31. theorem OAI.Superstring.PeriodWord.periodic line 345
  32. theorem OAI.Superstring.PeriodWord.eq_of_prefix line 349
  33. theorem OAI.Superstring.PeriodWord.poly_text line 361
  34. theorem OAI.Superstring.PeriodWord.poly_window line 367
  35. theorem OAI.Superstring.PeriodWord.poly_textWord line 373