OAI/Computability/Superstring/GeoCore.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.PeriodWord.poly_down line 8
  2. theorem OAI.Superstring.PeriodWord.poly_up line 14
  3. theorem OAI.Superstring.PeriodWord.down_fn line 20
  4. theorem OAI.Superstring.PeriodWord.up_fn line 24
  5. theorem OAI.Superstring.PeriodWord.textWord_fn line 28
  6. theorem OAI.Superstring.PeriodWord.poly_route line 32
  7. def OAI.Superstring.GeoCode.exit line 53
  8. def OAI.Superstring.GeoCode.first line 56
  9. theorem OAI.Superstring.GeoCode.poly_exit line 58
  10. theorem OAI.Superstring.GeoCode.poly_first line 64
  11. def OAI.Superstring.GeoCode.passage line 68
  12. def OAI.Superstring.GeoCode.segment line 71
  13. theorem OAI.Superstring.GeoCode.segment_zero line 75
  14. theorem OAI.Superstring.GeoCode.segment_succ line 77
  15. theorem OAI.Superstring.GeoCode.passage_realizes line 82
  16. theorem OAI.Superstring.GeoCode.segment_realizes line 105
  17. theorem OAI.Superstring.GeoCode.poly_passage line 139
  18. theorem OAI.Superstring.GeoCode.poly_segment line 143
  19. def OAI.Superstring.GeoCode.collective line 163
  20. def OAI.Superstring.GeoCode.band line 167
  21. def OAI.Superstring.GeoCode.shortSweep line 173
  22. def OAI.Superstring.GeoCode.individual line 180
  23. theorem OAI.Superstring.GeoCode.collective_link_realizes line 183
  24. theorem OAI.Superstring.GeoCode.join_band_realizes line 234
  25. theorem OAI.Superstring.GeoCode.collective_short_sweep_realizes line 286
  26. theorem OAI.Superstring.GeoCode.individual_link_realizes line 347
  27. theorem OAI.Superstring.WalkCode.join_fn line 393
  28. theorem OAI.Superstring.PeriodWord.route_fn line 399
  29. theorem OAI.Superstring.BitCode.Poly.leInt_fn line 406
  30. theorem OAI.Superstring.BitCode.Poly.maxInt_fn line 408
  31. theorem OAI.Superstring.BitCode.Poly.minInt_fn line 410
  32. theorem OAI.Superstring.GeoCode.exit_fn line 416
  33. theorem OAI.Superstring.GeoCode.poly_collective line 419
  34. theorem OAI.Superstring.GeoCode.poly_band line 424
  35. theorem OAI.Superstring.GeoCode.poly_shortSweep line 441
  36. theorem OAI.Superstring.GeoCode.poly_individual line 446
  37. def OAI.Superstring.WalkCode.root line 458
  38. def OAI.Superstring.WalkCode.rootAt line 459
  39. theorem OAI.Superstring.WalkCode.root_spec line 463
  40. theorem OAI.Superstring.WalkCode.rootAt_spec line 474
  41. theorem OAI.Superstring.WalkCode.poly_root line 494
  42. theorem OAI.Superstring.WalkCode.poly_rootAt line 495
  43. def OAI.Superstring.WalkCode.edgeCheck line 507
  44. theorem OAI.Superstring.WalkCode.edgeCheck_eq line 510
  45. def OAI.Superstring.WalkCode.check line 522
  46. theorem OAI.Superstring.WalkCode.chain_zip line 527
  47. theorem OAI.Superstring.WalkCode.check_eq line 542
  48. theorem OAI.Superstring.WalkCode.poly_edgeCheck line 553
  49. theorem OAI.Superstring.WalkCode.poly_check line 560
  50. theorem OAI.Superstring.GeoCode.full_turn_realizes line 575