OAI/NumberTheory/Jacobsthal/Renewal/RawHitRegeneration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawMarkedWord_cons_ae line 15
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnAnchor line 36
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnAnchor_measurable line 39
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturn_anchor_regenerates line 45
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedCycleAnchor line 62
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedCycleAnchor_measurable line 65
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle_anchor_regenerates line 70
8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitAnchor line 99
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitAnchor_measurable line 102
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstHit_anchor_regenerates line 109
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRegFirstHit_anchor_regenerates line 122
12. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitAnchor line 130
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitAnchor_measurable line 133
14. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_anchor_regenerates line 136