OAI/NumberTheory/Jacobsthal/Paths/ActualTagFreezing.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.Vertex line 20
  2. def OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.child line 27
  3. def OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.includedPrimes line 34
  4. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.included_subset line 37
  5. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.included_even line 40
  6. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.child_rank_lt line 43
  7. def OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.countMass line 47
  8. def OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.countSurvivors line 50
  9. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.countSurvivors_nonneg line 53
  10. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.count_partition line 56
  11. def OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.referenceValue line 63
  12. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.reference_partition line 66
  13. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.count_leaf line 78
  14. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountVertex.reference_leaf line 82
  15. def OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.lowerStop line 95
  16. def OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.evaluate line 98
  17. theorem OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.evaluate_sub line 104
  18. theorem OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.evaluate_add line 117
  19. theorem OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.evaluate_reference line 130
  20. def OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.stoppedCount line 152
  21. theorem OAI.Erdos970.NumberTheoryLean.StoppedEvaluation.stopped_count_reference_difference line 156
  22. def OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after line 178
  23. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after_node line 182
  24. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after_past line 188
  25. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after_required line 197
  26. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after_available line 208
  27. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after_scale line 217
  28. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.prefixWeight_product line 227
  29. theorem OAI.Erdos970.NumberTheoryLean.StoppedVertexHistory.after_scale_product line 235
  30. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountLowerBound.actual_stopped_bounds line 249
  31. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountLowerBound.actual_stopped_lower_bound line 298
  32. def OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.childrenTraces line 313
  33. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.nil_not_childrenTraces line 316
  34. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.sum_childrenTraces line 319
  35. def OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.traces line 335
  36. def OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.expanded line 342
  37. def OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.stopped line 345
  38. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.stopped_lower line 348
  39. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceSets.signed_childrenTraces line 370
  40. def OAI.Erdos970.NumberTheoryLean.FirstStopSemantics.FirstStop line 393
  41. theorem OAI.Erdos970.NumberTheoryLean.FirstStopSemantics.firstStop_nil line 397
  42. theorem OAI.Erdos970.NumberTheoryLean.FirstStopSemantics.stopped_first line 403
  43. theorem OAI.Erdos970.NumberTheoryLean.FirstStopSemantics.stopped_prefix_free line 435
  44. theorem OAI.Erdos970.NumberTheoryLean.FlatStoppedIdentity.flat_evaluate line 454
  45. def OAI.Erdos970.NumberTheoryLean.FlatStoppedIdentity.sideSign line 476
  46. theorem OAI.Erdos970.NumberTheoryLean.FlatStoppedIdentity.sideSign_after line 480
  47. theorem OAI.Erdos970.NumberTheoryLean.FlatStoppedIdentity.stopped_sign_one line 490
  48. theorem OAI.Erdos970.NumberTheoryLean.FlatStoppedIdentity.literal_stopped_difference line 497
  49. theorem OAI.Erdos970.NumberTheoryLean.FlatStoppedIdentity.actual_reference_error_lower_bound line 514
  50. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceAdmission.reference_nil_mem line 539
  51. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceAdmission.reference_child_cons line 544
  52. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceAdmission.trace_reference_member line 557
  53. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceAdmission.trace_nodup line 586
  54. theorem OAI.Erdos970.NumberTheoryLean.StoppedTraceAdmission.trace_primes line 591
  55. def OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.rootVertex line 609
  56. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.countMass_eq_tree_mass line 612
  57. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.countSurvivors_eq_tree_survivors line 616
  58. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.root_after_mass line 621
  59. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.root_after_survivors line 628
  60. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.root_after_reference line 635
  61. theorem OAI.Erdos970.NumberTheoryLean.StoppedCountAdapters.literal_root_lower_comparison line 642
  62. def OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.sourceClass line 668
  63. def OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.representative line 670
  64. def OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.boxed line 673
  65. def OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.representativeSafe line 676
  66. def OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.representativeWindow line 680
  67. def OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.stopCandidate line 685
  68. theorem OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.empty_not_candidate line 693
  69. theorem OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.finite_safe_admits line 698
  70. theorem OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.candidate_admitted line 709
  71. theorem OAI.Erdos970.NumberTheoryLean.SourceStopPredicate.candidate_owner_witness line 720
  72. theorem OAI.Erdos970.NumberTheoryLean.ActualTagFreezing.sourceTag_replacement line 743
  73. theorem OAI.Erdos970.NumberTheoryLean.ActualTagFreezing.all_prefix_tags_replacement line 753
  74. theorem OAI.Erdos970.NumberTheoryLean.ActualTagFreezing.replacement_labels line 764
  75. theorem OAI.Erdos970.NumberTheoryLean.ActualTagFreezing.replacement_representatives line 768
  76. theorem OAI.Erdos970.NumberTheoryLean.ActualTagFreezing.forall_mem_replacement_iff line 774