OAI/Computability/Superstring/GroupPoly.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.CollectionCode.poly_foreign line 8
  2. abbrev OAI.Superstring.CollectionCode.ChooseInput line 11
  3. theorem OAI.Superstring.CollectionCode.poly_choose line 12
  4. theorem OAI.Superstring.CollectionCode.poly_hard line 22
  5. theorem OAI.Superstring.CollectionCode.poly_hardPlan line 31
  6. abbrev OAI.Superstring.CollectionCode.CompleteInput line 36
  7. theorem OAI.Superstring.CollectionCode.poly_cond line 37
  8. theorem OAI.Superstring.CollectionCode.poly_decide_and line 41
  9. def OAI.Superstring.CollectionCode.completeRoot line 45
  10. def OAI.Superstring.CollectionCode.completeBand line 47
  11. def OAI.Superstring.CollectionCode.completePick line 49
  12. def OAI.Superstring.CollectionCode.completeHard line 51
  13. def OAI.Superstring.CollectionCode.completeM line 52
  14. def OAI.Superstring.CollectionCode.completeP line 53
  15. def OAI.Superstring.CollectionCode.completeT line 54
  16. def OAI.Superstring.CollectionCode.completeH line 55
  17. def OAI.Superstring.CollectionCode.completeExit line 56
  18. theorem OAI.Superstring.CollectionCode.poly_completeRoot line 57
  19. theorem OAI.Superstring.CollectionCode.poly_completeBand line 62
  20. theorem OAI.Superstring.CollectionCode.poly_completePick line 67
  21. theorem OAI.Superstring.CollectionCode.poly_completeHard line 71
  22. theorem OAI.Superstring.CollectionCode.poly_completeM line 75
  23. theorem OAI.Superstring.CollectionCode.poly_completeP line 77
  24. theorem OAI.Superstring.CollectionCode.poly_completeT line 78
  25. theorem OAI.Superstring.CollectionCode.poly_completeH line 80
  26. theorem OAI.Superstring.CollectionCode.poly_completeExit line 84
  27. theorem OAI.Superstring.CollectionCode.poly_completeTest1 line 89
  28. theorem OAI.Superstring.CollectionCode.poly_completeTest2 line 90
  29. theorem OAI.Superstring.CollectionCode.poly_completeTest3 line 95
  30. theorem OAI.Superstring.CollectionCode.poly_complete line 106
  31. theorem OAI.Superstring.CollectionCode.poly_fibre line 117
  32. theorem OAI.Superstring.CollectionCode.poly_recipients line 122
  33. theorem OAI.Superstring.CollectionCode.poly_incoming line 126
  34. theorem OAI.Superstring.CollectionCode.poly_baseIndex line 135
  35. theorem OAI.Superstring.CollectionCode.poly_holes line 136
  36. theorem OAI.Superstring.CollectionCode.poly_prepare line 139
  37. abbrev OAI.Superstring.CollectionCode.ProcessInput line 156
  38. theorem OAI.Superstring.CollectionCode.poly_process line 157
  39. theorem OAI.Superstring.CollectionCode.complete_extras line 172
  40. def OAI.Superstring.CollectionCode.extraSizes line 179
  41. def OAI.Superstring.CollectionCode.maxExtras line 182
  42. theorem OAI.Superstring.CollectionCode.extras_le line 184
  43. theorem OAI.Superstring.CollectionCode.Model.process_extra_bound line 191
  44. theorem OAI.Superstring.CollectionCode.Model.advance_extra_bound line 203
  45. def OAI.Superstring.CollectionCode.initial line 247
  46. theorem OAI.Superstring.CollectionCode.advance_nil line 248
  47. theorem OAI.Superstring.CollectionCode.Model.initial_invariant line 252
  48. theorem OAI.Superstring.CollectionCode.Model.iterate_advance line 262