PA00DX · theorem

eisenstein_initial_segment_bit_count_functional

Alpha v34 checked-use theorem · independently closed; not Stable

The BitCount of a bounded exact initial segment is its threshold.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ q. ∀ b. ∀ c. ∀ k. ∀ n. (∀ x. Lt(x,k) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 1 ∧ Lt(x,q) ∨ y = 0 ∧ Lt(q,S x))) → Le(q,k) → BitCount(b,c,k,n) → n = q

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0013 BetaAt PD0017 BitCount

6 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt PD0017 BitCount PD0019 Repeat

14 occurrences

Exact expanded native-PA statement
forall q b c k n. (forall eis_index_initial_segment_exact_source. (exists eis_lt_gap_initial_segment_exact_source_bound. eis_lt_gap_initial_segment_exact_source_bound + S (eis_index_initial_segment_exact_source) = k) -> exists eis_bit_initial_segment_exact_source. ((((exists ff_h_eis_initial_segment_exact_source_decoded. ff_h_eis_initial_segment_exact_source_decoded + S (eis_bit_initial_segment_exact_source) = S ((S (eis_index_initial_segment_exact_source)) * c)) /\ exists ff_q_eis_initial_segment_exact_source_decoded. b = ff_q_eis_initial_segment_exact_source_decoded * S ((S (eis_index_initial_segment_exact_source)) * c) + (eis_bit_initial_segment_exact_source))) /\ (((eis_bit_initial_segment_exact_source = 1 /\ (exists eis_le_gap_initial_segment_exact_source_choice_inside. eis_le_gap_initial_segment_exact_source_choice_inside + (S eis_index_initial_segment_exact_source) = q)) \/ (eis_bit_initial_segment_exact_source = 0 /\ (exists eis_lt_gap_initial_segment_exact_source_choice_outside. eis_lt_gap_initial_segment_exact_source_choice_outside + S (q) = S eis_index_initial_segment_exact_source)))))) -> (exists eis_le_gap_initial_segment_exact_threshold. eis_le_gap_initial_segment_exact_threshold + (q) = k) -> (((exists ff_u_initial_segment_exact_count_sum ff_v_initial_segment_exact_count_sum. ((((exists ff_h_initial_segment_exact_count_sum_start. ff_h_initial_segment_exact_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_start. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_start * S ((S (0)) * ff_v_initial_segment_exact_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_exact_count_sum_terminal. ff_h_initial_segment_exact_count_sum_terminal + S (n) = S ((S (k)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_terminal. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_exact_count_sum) + (n))) /\ forall ff_i_initial_segment_exact_count_sum. (exists ff_lt_initial_segment_exact_count_sum_bound. ff_lt_initial_segment_exact_count_sum_bound + S ff_i_initial_segment_exact_count_sum = k) -> exists ff_a_initial_segment_exact_count_sum ff_r_initial_segment_exact_count_sum ff_s_initial_segment_exact_count_sum. ((((exists ff_h_initial_segment_exact_count_sum_summand. ff_h_initial_segment_exact_count_sum_summand + S (ff_a_initial_segment_exact_count_sum) = S ((S (ff_i_initial_segment_exact_count_sum)) * c)) /\ exists ff_q_initial_segment_exact_count_sum_summand. b = ff_q_initial_segment_exact_count_sum_summand * S ((S (ff_i_initial_segment_exact_count_sum)) * c) + (ff_a_initial_segment_exact_count_sum))) /\ ((((exists ff_h_initial_segment_exact_count_sum_partial. ff_h_initial_segment_exact_count_sum_partial + S (ff_r_initial_segment_exact_count_sum) = S ((S (ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_partial. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_partial * S ((S (ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum) + (ff_r_initial_segment_exact_count_sum))) /\ ((((exists ff_h_initial_segment_exact_count_sum_successor. ff_h_initial_segment_exact_count_sum_successor + S (ff_s_initial_segment_exact_count_sum) = S ((S (S ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum)) /\ exists ff_q_initial_segment_exact_count_sum_successor. ff_u_initial_segment_exact_count_sum = ff_q_initial_segment_exact_count_sum_successor * S ((S (S ff_i_initial_segment_exact_count_sum)) * ff_v_initial_segment_exact_count_sum) + (ff_s_initial_segment_exact_count_sum))) /\ ff_s_initial_segment_exact_count_sum = ff_r_initial_segment_exact_count_sum + ff_a_initial_segment_exact_count_sum)))))) /\ (forall ff_i_initial_segment_exact_count_bits. (exists ff_lt_initial_segment_exact_count_bits_bound. ff_lt_initial_segment_exact_count_bits_bound + S ff_i_initial_segment_exact_count_bits = k) -> exists ff_bit_initial_segment_exact_count_bits. ((((exists ff_h_initial_segment_exact_count_bits_decoded. ff_h_initial_segment_exact_count_bits_decoded + S (ff_bit_initial_segment_exact_count_bits) = S ((S (ff_i_initial_segment_exact_count_bits)) * c)) /\ exists ff_q_initial_segment_exact_count_bits_decoded. b = ff_q_initial_segment_exact_count_bits_decoded * S ((S (ff_i_initial_segment_exact_count_bits)) * c) + (ff_bit_initial_segment_exact_count_bits))) /\ (ff_bit_initial_segment_exact_count_bits = 0 \/ ff_bit_initial_segment_exact_count_bits = 1))))) -> n = q

Proof neighborhood

Direct theorem prerequisites

PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA002O le_succ PA001A le_refl PA003A lt_not_le PA0048 bit_count_zero PA0042 bit_count_succ_decompose PA00DV eisenstein_initial_segment_decoded_choice PA00DW beta_all_one_bit_count_exact

Direct theorem dependents

PA00DY eisenstein_initial_segment_bit_count_exact

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

129 script commands · 29 reading checkpoints · 12 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (10)
le zerole eq or ltle of succ le succle succle refllt not lebit count zerobit count succ decomposeeisenstein initial segment decoded choicebeta all one bit count exact
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro q
  2. L2
    intro b
  3. L3
    intro c
02Induction on kL4–8

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction k
  2. L5
    intro n
  3. L6
    intro hprefix
  4. L7
    intro hqk
  5. L8
    intro hcount
03Establish hq0L9–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le zero.

  1. L9
    have hq0 : q = 0
  2. L10
    specialize le_zero q
  3. L11
    apply le_zero
  4. L12
    exact hqk
04Establish hn0L13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count zero.

  1. L13
    have hn0 : n = 0
  2. L14
    specialize bit_count_zero b
  3. L15
    specialize bit_count_zero c
  4. L16
    specialize bit_count_zero 0
  5. L17
    specialize bit_count_zero n
  6. L18
    apply bit_count_zero
  7. L19
    refl
  8. L20
    exact hcount
  9. L21
    trans 0
  10. L22
    exact hn0
05Calculate and transport equalitiesL23–23

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L23
    symm
06Use earlier factsL24–24

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    exact hq0
07Fix variables and assumptionsL25–28

Work with arbitrary variables or the premises of the current implication.

  1. L25
    intro n
  2. L26
    intro hprefix
  3. L27
    intro hqk
  4. L28
    intro hcount
08Establish hsplitL29–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L29
    have hsplit : q = S k ∨ Lt(q,S k)Definitions: Lt(q,S k)Original native command in the exact edition
  2. L30
    specialize le_eq_or_lt q
  3. L31
    specialize le_eq_or_lt (S k)
  4. L32
    apply le_eq_or_lt
  5. L33
    exact hqk
09Separate the logical casesL34–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L34
    cases hsplit
10Establish halloneL35–37

Establish this local claim before using it. It is not an additional assumption.

  1. L35
    have hallone : Repeat(b,c,1,S k)Definitions: Repeat(b,c,1,S k)Original native command in the exact edition
  2. L36
    intro j
  3. L37
    intro hj
11Establish hstoredL38–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L38
    have hstored : ∃ bit. BetaAt(b,c,j,bit) ∧ (bit = 1 ∧ Lt(j,q) ∨ bit = 0 ∧ Lt(q,S j))Definitions: BetaAt(b,c,j,bit)Lt(j,q)Lt(q,S j)Original native command in the exact edition
  2. L39
    specialize hprefix j
  3. L40
    apply hprefix
  4. L41
    exact hj
12Separate the logical casesL42–45

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L42
    cases hstored
  2. L43
    cases hstored_witness
  3. L44
    cases hstored_witness_right
  4. L45
    cases hstored_witness_right_left
13Establish hbit_oneL46–50

Establish this local claim before using it. It is not an additional assumption.

  1. L46
    have hbit_one : x = 1
  2. L47
    exact hstored_witness_right_left_left
  3. L48
    rewrite hbit_one at hstored_witness_left
  4. L49
    rewrite hbit_one at hstored_witness_left
  5. L50
    exact hstored_witness_left
14Separate the logical casesL51–52

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L51
    cases hstored_witness_right_right
  2. L52
    exfalso
15Calculate and transport equalitiesL53–53

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L53
    rewrite hsplit_left at hstored_witness_right_right_right
16Use earlier factsL54–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L54
    specialize lt_not_le (S k)
  2. L55
    specialize lt_not_le (S j)
  3. L56
    apply lt_not_le
  4. L57
    exact hstored_witness_right_right_right
  5. L58
    exact hj
17Establish hnL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta all one bit count exact.

  1. L59
    have hn : n = S k
  2. L60
    specialize beta_all_one_bit_count_exact b
  3. L61
    specialize beta_all_one_bit_count_exact c
  4. L62
    specialize beta_all_one_bit_count_exact (S k)
  5. L63
    specialize beta_all_one_bit_count_exact n
  6. L64
    apply beta_all_one_bit_count_exact
  7. L65
    exact hallone
  8. L66
    exact hcount
  9. L67
    trans S k
  10. L68
    exact hn
18Calculate and transport equalitiesL69–69

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L69
    symm
19Use earlier factsL70–70

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L70
    exact hsplit_left
20Establish hqk_previousL71–75

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L71
    have hqk_previous : Le(q,k)Definitions: Le(q,k)Original native command in the exact edition
  2. L72
    specialize le_of_succ_le_succ q
  3. L73
    specialize le_of_succ_le_succ k
  4. L74
    apply le_of_succ_le_succ
  5. L75
    exact hsplit_right
21Establish hpreviousL76–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L76
    have hprevious : ∀ eis_index_initial_segment_functional_previous. Lt(eis_index_initial_segment_functional_previous,k) → ∃ x. BetaAt(b,c,eis_index_initial_segment_functional_previous,x) ∧ (x = 1 ∧ Lt(eis_index_initial_segment_functional_previous,q) ∨ x = 0 ∧ Lt(q,S eis_index_initial_segment_functional_previous))Definitions: Lt(eis_index_initial_segment_functional_previous,k)BetaAt(b,c,eis_index_initial_segment_functional_previous,x)Lt(eis_index_initial_segment_functional_previous,q)Lt(q,S eis_index_initial_segment_functional_previous)Original native command in the exact edition
  2. L77
    intro j
  3. L78
    intro hj
  4. L79
    specialize hprefix j
  5. L80
    apply hprefix
  6. L81
    specialize le_succ (S j)
  7. L82
    specialize le_succ k
  8. L83
    apply le_succ
  9. L84
    exact hj
22Establish hdecompL85–93

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count succ decompose.

  1. L85
    have hdecomp : ∃ a. ∃ r. BetaAt(b,c,k,a) ∧ (BitCount(b,c,k,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))Definitions: BetaAt(b,c,k,a)BitCount(b,c,k,r)Original native command in the exact edition
  2. L86
    specialize bit_count_succ_decompose b
  3. L87
    specialize bit_count_succ_decompose c
  4. L88
    specialize bit_count_succ_decompose k
  5. L89
    specialize bit_count_succ_decompose (S k)
  6. L90
    specialize bit_count_succ_decompose n
  7. L91
    apply bit_count_succ_decompose
  8. L92
    refl
  9. L93
    exact hcount
23Separate the logical casesL94–98

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L94
    cases hdecomp
  2. L95
    cases hdecomp_witness
  3. L96
    cases hdecomp_witness_witness
  4. L97
    cases hdecomp_witness_witness_right
  5. L98
    cases hdecomp_witness_witness_right_right
24Establish hlast_choiceL99–108

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein initial segment decoded choice.

  1. L99
    have hlast_choice : x = 1 ∧ Lt(k,q) ∨ x = 0 ∧ Lt(q,S k)Definitions: Lt(k,q)Lt(q,S k)Original native command in the exact edition
  2. L100
    specialize eisenstein_initial_segment_decoded_choice q
  3. L101
    specialize eisenstein_initial_segment_decoded_choice b
  4. L102
    specialize eisenstein_initial_segment_decoded_choice c
  5. L103
    specialize eisenstein_initial_segment_decoded_choice (S k)
  6. L104
    specialize eisenstein_initial_segment_decoded_choice k
  7. L105
    specialize eisenstein_initial_segment_decoded_choice x
  8. L106
    apply eisenstein_initial_segment_decoded_choice
  9. L107
    exact hprefix
  10. L108
    specialize le_refl (S k)
25Use earlier factsL109–110

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L109
    exact le_refl
  2. L110
    exact hdecomp_witness_witness_left
26Separate the logical casesL111–113

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L111
    cases hlast_choice
  2. L112
    cases hlast_choice_left
  3. L113
    exfalso
27Use earlier factsL114–118

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L114
    specialize lt_not_le q
  2. L115
    specialize lt_not_le (S k)
  3. L116
    apply lt_not_le
  4. L117
    exact hsplit_right
  5. L118
    exact hlast_choice_left_right
28Separate the logical casesL119–119

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L119
    cases hlast_choice_right
29Establish hrqL120–129

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L120
    have hrq : x1 = q
  2. L121
    specialize IH x1
  3. L122
    apply IH
  4. L123
    exact hprevious
  5. L124
    exact hqk_previous
  6. L125
    exact hdecomp_witness_witness_right_left
  7. L126
    rewrite hdecomp_witness_witness_right_right_right
  8. L127
    rewrite hrq
  9. L128
    rewrite hlast_choice_right_left
  10. L129
    apply PA3

Library-wide reading audit

Original defined command ledger · 129 lines
  1. 0001intro q
  2. 0002intro b
  3. 0003intro c
  4. 0004induction k
  5. 0005intro n
  6. 0006intro hprefix
  7. 0007intro hqk
  8. 0008intro hcount
  9. 0009have hq0 : q = 0
  10. 0010specialize le_zero q
  11. 0011apply le_zero
  12. 0012exact hqk
  13. 0013have hn0 : n = 0
  14. 0014specialize bit_count_zero b
  15. 0015specialize bit_count_zero c
  16. 0016specialize bit_count_zero 0
  17. 0017specialize bit_count_zero n
  18. 0018apply bit_count_zero
  19. 0019refl
  20. 0020exact hcount
  21. 0021trans 0
  22. 0022exact hn0
  23. 0023symm
  24. 0024exact hq0
  25. 0025intro n
  26. 0026intro hprefix
  27. 0027intro hqk
  28. 0028intro hcount
  29. 0029have hsplit : q = S k ∨ Lt(q,S k)
    Exact native replay linehave hsplit : q = S k \/ exists gap. gap + S q = S k
  30. 0030specialize le_eq_or_lt q
  31. 0031specialize le_eq_or_lt (S k)
  32. 0032apply le_eq_or_lt
  33. 0033exact hqk
  34. 0034cases hsplit
  35. 0035have hallone : Repeat(b,c,1,S k)
    Exact native replay linehave hallone : forall eis_one_index_initial_segment_functional_all_one. (exists eis_lt_gap_initial_segment_functional_all_one_bound. eis_lt_gap_initial_segment_functional_all_one_bound + S (eis_one_index_initial_segment_functional_all_one) = S k) -> (((exists ff_h_eis_initial_segment_functional_all_one_decoded. ff_h_eis_initial_segment_functional_all_one_decoded + S (1) = S ((S (eis_one_index_initial_segment_functional_all_one)) * c)) /\ exists ff_q_eis_initial_segment_functional_all_one_decoded. b = ff_q_eis_initial_segment_functional_all_one_decoded * S ((S (eis_one_index_initial_segment_functional_all_one)) * c) + (1)))
  36. 0036intro j
  37. 0037intro hj
  38. 0038have hstored : ∃ bit. BetaAt(b,c,j,bit) ∧ (bit = 1 ∧ Lt(j,q) ∨ bit = 0 ∧ Lt(q,S j))
    Exact native replay linehave hstored : exists bit. ((((exists ff_h_initial_segment_functional_stored. ff_h_initial_segment_functional_stored + S (bit) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_functional_stored. b = ff_q_initial_segment_functional_stored * S ((S (j)) * c) + (bit))) /\ (((bit = 1 /\ (exists eis_le_gap_initial_segment_functional_stored_choice_inside. eis_le_gap_initial_segment_functional_stored_choice_inside + (S j) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_functional_stored_choice_outside. eis_lt_gap_initial_segment_functional_stored_choice_outside + S (q) = S j)))))
  39. 0039specialize hprefix j
  40. 0040apply hprefix
  41. 0041exact hj
  42. 0042cases hstored
  43. 0043cases hstored_witness
  44. 0044cases hstored_witness_right
  45. 0045cases hstored_witness_right_left
  46. 0046have hbit_one : x = 1
  47. 0047exact hstored_witness_right_left_left
  48. 0048rewrite hbit_one at hstored_witness_left
  49. 0049rewrite hbit_one at hstored_witness_left
  50. 0050exact hstored_witness_left
  51. 0051cases hstored_witness_right_right
  52. 0052exfalso
  53. 0053rewrite hsplit_left at hstored_witness_right_right_right
  54. 0054specialize lt_not_le (S k)
  55. 0055specialize lt_not_le (S j)
  56. 0056apply lt_not_le
  57. 0057exact hstored_witness_right_right_right
  58. 0058exact hj
  59. 0059have hn : n = S k
  60. 0060specialize beta_all_one_bit_count_exact b
  61. 0061specialize beta_all_one_bit_count_exact c
  62. 0062specialize beta_all_one_bit_count_exact (S k)
  63. 0063specialize beta_all_one_bit_count_exact n
  64. 0064apply beta_all_one_bit_count_exact
  65. 0065exact hallone
  66. 0066exact hcount
  67. 0067trans S k
  68. 0068exact hn
  69. 0069symm
  70. 0070exact hsplit_left
  71. 0071have hqk_previous : Le(q,k)
    Exact native replay linehave hqk_previous : exists gap. gap + q = k
  72. 0072specialize le_of_succ_le_succ q
  73. 0073specialize le_of_succ_le_succ k
  74. 0074apply le_of_succ_le_succ
  75. 0075exact hsplit_right
  76. 0076have hprevious : ∀ eis_index_initial_segment_functional_previous. Lt(eis_index_initial_segment_functional_previous,k) → ∃ x. BetaAt(b,c,eis_index_initial_segment_functional_previous,x) ∧ (x = 1 ∧ Lt(eis_index_initial_segment_functional_previous,q) ∨ x = 0 ∧ Lt(q,S eis_index_initial_segment_functional_previous))
    Exact native replay linehave hprevious : forall eis_index_initial_segment_functional_previous. (exists eis_lt_gap_initial_segment_functional_previous_bound. eis_lt_gap_initial_segment_functional_previous_bound + S (eis_index_initial_segment_functional_previous) = k) -> exists eis_bit_initial_segment_functional_previous. ((((exists ff_h_eis_initial_segment_functional_previous_decoded. ff_h_eis_initial_segment_functional_previous_decoded + S (eis_bit_initial_segment_functional_previous) = S ((S (eis_index_initial_segment_functional_previous)) * c)) /\ exists ff_q_eis_initial_segment_functional_previous_decoded. b = ff_q_eis_initial_segment_functional_previous_decoded * S ((S (eis_index_initial_segment_functional_previous)) * c) + (eis_bit_initial_segment_functional_previous))) /\ (((eis_bit_initial_segment_functional_previous = 1 /\ (exists eis_le_gap_initial_segment_functional_previous_choice_inside. eis_le_gap_initial_segment_functional_previous_choice_inside + (S eis_index_initial_segment_functional_previous) = q)) \/ (eis_bit_initial_segment_functional_previous = 0 /\ (exists eis_lt_gap_initial_segment_functional_previous_choice_outside. eis_lt_gap_initial_segment_functional_previous_choice_outside + S (q) = S eis_index_initial_segment_functional_previous)))))
  77. 0077intro j
  78. 0078intro hj
  79. 0079specialize hprefix j
  80. 0080apply hprefix
  81. 0081specialize le_succ (S j)
  82. 0082specialize le_succ k
  83. 0083apply le_succ
  84. 0084exact hj
  85. 0085have hdecomp : ∃ a. ∃ r. BetaAt(b,c,k,a) ∧ (BitCount(b,c,k,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))
    Exact native replay linehave hdecomp : exists a r. (((exists ff_h_initial_segment_functional_last. ff_h_initial_segment_functional_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_functional_last. b = ff_q_initial_segment_functional_last * S ((S (k)) * c) + (a))) /\ ((((exists ff_u_initial_segment_functional_prefix_count_sum ff_v_initial_segment_functional_prefix_count_sum. ((((exists ff_h_initial_segment_functional_prefix_count_sum_start. ff_h_initial_segment_functional_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_start. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_start * S ((S (0)) * ff_v_initial_segment_functional_prefix_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_terminal. ff_h_initial_segment_functional_prefix_count_sum_terminal + S (r) = S ((S (k)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_terminal. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_functional_prefix_count_sum) + (r))) /\ forall ff_i_initial_segment_functional_prefix_count_sum. (exists ff_lt_initial_segment_functional_prefix_count_sum_bound. ff_lt_initial_segment_functional_prefix_count_sum_bound + S ff_i_initial_segment_functional_prefix_count_sum = k) -> exists ff_a_initial_segment_functional_prefix_count_sum ff_r_initial_segment_functional_prefix_count_sum ff_s_initial_segment_functional_prefix_count_sum. ((((exists ff_h_initial_segment_functional_prefix_count_sum_summand. ff_h_initial_segment_functional_prefix_count_sum_summand + S (ff_a_initial_segment_functional_prefix_count_sum) = S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * c)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_summand. b = ff_q_initial_segment_functional_prefix_count_sum_summand * S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * c) + (ff_a_initial_segment_functional_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_partial. ff_h_initial_segment_functional_prefix_count_sum_partial + S (ff_r_initial_segment_functional_prefix_count_sum) = S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_partial. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_partial * S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum) + (ff_r_initial_segment_functional_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_successor. ff_h_initial_segment_functional_prefix_count_sum_successor + S (ff_s_initial_segment_functional_prefix_count_sum) = S ((S (S ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_successor. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_successor * S ((S (S ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum) + (ff_s_initial_segment_functional_prefix_count_sum))) /\ ff_s_initial_segment_functional_prefix_count_sum = ff_r_initial_segment_functional_prefix_count_sum + ff_a_initial_segment_functional_prefix_count_sum)))))) /\ (forall ff_i_initial_segment_functional_prefix_count_bits. (exists ff_lt_initial_segment_functional_prefix_count_bits_bound. ff_lt_initial_segment_functional_prefix_count_bits_bound + S ff_i_initial_segment_functional_prefix_count_bits = k) -> exists ff_bit_initial_segment_functional_prefix_count_bits. ((((exists ff_h_initial_segment_functional_prefix_count_bits_decoded. ff_h_initial_segment_functional_prefix_count_bits_decoded + S (ff_bit_initial_segment_functional_prefix_count_bits) = S ((S (ff_i_initial_segment_functional_prefix_count_bits)) * c)) /\ exists ff_q_initial_segment_functional_prefix_count_bits_decoded. b = ff_q_initial_segment_functional_prefix_count_bits_decoded * S ((S (ff_i_initial_segment_functional_prefix_count_bits)) * c) + (ff_bit_initial_segment_functional_prefix_count_bits))) /\ (ff_bit_initial_segment_functional_prefix_count_bits = 0 \/ ff_bit_initial_segment_functional_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  86. 0086specialize bit_count_succ_decompose b
  87. 0087specialize bit_count_succ_decompose c
  88. 0088specialize bit_count_succ_decompose k
  89. 0089specialize bit_count_succ_decompose (S k)
  90. 0090specialize bit_count_succ_decompose n
  91. 0091apply bit_count_succ_decompose
  92. 0092refl
  93. 0093exact hcount
  94. 0094cases hdecomp
  95. 0095cases hdecomp_witness
  96. 0096cases hdecomp_witness_witness
  97. 0097cases hdecomp_witness_witness_right
  98. 0098cases hdecomp_witness_witness_right_right
  99. 0099have hlast_choice : x = 1 ∧ Lt(k,q) ∨ x = 0 ∧ Lt(q,S k)
    Exact native replay linehave hlast_choice : ((x = 1 /\ (exists eis_le_gap_initial_segment_functional_last_choice_inside. eis_le_gap_initial_segment_functional_last_choice_inside + (S k) = q)) \/ (x = 0 /\ (exists eis_lt_gap_initial_segment_functional_last_choice_outside. eis_lt_gap_initial_segment_functional_last_choice_outside + S (q) = S k)))
  100. 0100specialize eisenstein_initial_segment_decoded_choice q
  101. 0101specialize eisenstein_initial_segment_decoded_choice b
  102. 0102specialize eisenstein_initial_segment_decoded_choice c
  103. 0103specialize eisenstein_initial_segment_decoded_choice (S k)
  104. 0104specialize eisenstein_initial_segment_decoded_choice k
  105. 0105specialize eisenstein_initial_segment_decoded_choice x
  106. 0106apply eisenstein_initial_segment_decoded_choice
  107. 0107exact hprefix
  108. 0108specialize le_refl (S k)
  109. 0109exact le_refl
  110. 0110exact hdecomp_witness_witness_left
  111. 0111cases hlast_choice
  112. 0112cases hlast_choice_left
  113. 0113exfalso
  114. 0114specialize lt_not_le q
  115. 0115specialize lt_not_le (S k)
  116. 0116apply lt_not_le
  117. 0117exact hsplit_right
  118. 0118exact hlast_choice_left_right
  119. 0119cases hlast_choice_right
  120. 0120have hrq : x1 = q
  121. 0121specialize IH x1
  122. 0122apply IH
  123. 0123exact hprevious
  124. 0124exact hqk_previous
  125. 0125exact hdecomp_witness_witness_right_left
  126. 0126rewrite hdecomp_witness_witness_right_right_right
  127. 0127rewrite hrq
  128. 0128rewrite hlast_choice_right_left
  129. 0129apply PA3