OAI/NumberTheory/Jacobsthal/Paths/MovingStopMargins.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.ActualSourceStopBinding.actual_source_stops_first line 19
  2. theorem OAI.Erdos970.NumberTheoryLean.ActualSourceStopBinding.actual_source_stopped_lower line 33
  3. theorem OAI.Erdos970.NumberTheoryLean.ActualSourceStopBinding.actual_source_stopped_comparison line 42
  4. theorem OAI.Erdos970.NumberTheoryLean.FirstStopFreezing.firstStop_iff_takes line 80
  5. theorem OAI.Erdos970.NumberTheoryLean.FirstStopFreezing.first_source_stop_replacement line 100
  6. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceMembership.reference_cons_iff line 147
  7. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceMembership.stopped_length line 161
  8. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceMembership.stopped_of_reference_first line 178
  9. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceMembership.stopped_iff_reference_first line 200
  10. theorem OAI.Erdos970.NumberTheoryLean.TagBelowStopWindow.source_tag_nonterminal line 216
  11. theorem OAI.Erdos970.NumberTheoryLean.TagBelowStopWindow.moving_window_below_search line 236
  12. theorem OAI.Erdos970.NumberTheoryLean.TagBelowStopWindow.replacement_product line 249
  13. theorem OAI.Erdos970.NumberTheoryLean.TagBelowStopWindow.replacement_last_and_scale line 254
  14. theorem OAI.Erdos970.NumberTheoryLean.StoppedPrefixExistence.reference_length_le_card line 274
  15. theorem OAI.Erdos970.NumberTheoryLean.StoppedPrefixExistence.exists_stopped_prefix line 282
  16. theorem OAI.Erdos970.NumberTheoryLean.StoppedPrefixExistence.reference_candidate_forces_stop line 316
  17. theorem OAI.Erdos970.NumberTheoryLean.ActualFrozenStopFamily.actual_stopped_replacement line 336
  18. theorem OAI.Erdos970.NumberTheoryLean.ActualFrozenStopFamily.stopped_has_full_frozen_group line 401
  19. theorem OAI.Erdos970.NumberTheoryLean.MovingStopMargins.moving_stop_margins line 438