OAI/Computability/Superstring/LocalCode.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Superstring.LayerArray.exits line 9
  2. def OAI.Superstring.LayerArray.covered line 10
  3. def OAI.Superstring.LayerArray.collective line 12
  4. def OAI.Superstring.LayerArray.band line 15
  5. def OAI.Superstring.LayerArray.shortSweep line 18
  6. def OAI.Superstring.LayerArray.individual line 21
  7. theorem OAI.Superstring.LayerArray.covered_eq line 25
  8. theorem OAI.Superstring.LayerArray.filled_realized line 37
  9. theorem OAI.Superstring.LayerArray.collective_spec line 56
  10. theorem OAI.Superstring.LayerArray.band_spec line 83
  11. theorem OAI.Superstring.LayerArray.poly_exits line 109
  12. theorem OAI.Superstring.LayerArray.poly_covered line 112
  13. theorem OAI.Superstring.LayerArray.saturate_fn line 119
  14. theorem OAI.Superstring.LayerArray.poly_collective line 124
  15. theorem OAI.Superstring.LayerArray.poly_band line 131
  16. theorem OAI.Superstring.LayerArray.poly_shortSweep line 138
  17. theorem OAI.Superstring.LayerArray.poly_individual line 145
  18. theorem OAI.Superstring.LayerArray.individual_spec line 159
  19. theorem OAI.Superstring.LayerArray.shortSweep_spec line 184
  20. theorem OAI.Superstring.LayerArray.collective_contact line 210
  21. theorem OAI.Superstring.WalkCode.root_prefix line 247
  22. def OAI.Superstring.LayerArray.rootContent line 260
  23. def OAI.Superstring.LayerArray.shortPool line 262
  24. def OAI.Superstring.LayerArray.rootUpper line 264
  25. theorem OAI.Superstring.LayerArray.rootContent_spec line 267
  26. theorem OAI.Superstring.LayerArray.shortPool_spec line 281
  27. theorem OAI.Superstring.LayerArray.rootUpper_spec line 298
  28. theorem OAI.Superstring.LayerArray.poly_rootContent line 322
  29. theorem OAI.Superstring.LayerArray.poly_shortPool line 324
  30. theorem OAI.Superstring.LayerArray.poly_rootUpper line 329
  31. def OAI.Superstring.WalkCode.rootShort line 341
  32. theorem OAI.Superstring.WalkCode.rootShort_spec line 344
  33. theorem OAI.Superstring.WalkCode.poly_rootShort line 360