BT008P

bit_count_bounded

Stable checked-use theorem · independently kernel verified

A zero/one count never exceeds the length of its decoded prefix.

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.

Exact expanded PA statement

forall b c l n. (((exists ff_u_b_sum ff_v_b_sum. ((((exists ff_h_b_sum_start. ff_h_b_sum_start + S (0) = S ((S (0)) * ff_v_b_sum)) /\ exists ff_q_b_sum_start. ff_u_b_sum = ff_q_b_sum_start * S ((S (0)) * ff_v_b_sum) + (0))) /\ ((((exists ff_h_b_sum_terminal. ff_h_b_sum_terminal + S (n) = S ((S (l)) * ff_v_b_sum)) /\ exists ff_q_b_sum_terminal. ff_u_b_sum = ff_q_b_sum_terminal * S ((S (l)) * ff_v_b_sum) + (n))) /\ forall ff_i_b_sum. (exists ff_lt_b_sum_bound. ff_lt_b_sum_bound + S ff_i_b_sum = l) -> exists ff_a_b_sum ff_r_b_sum ff_s_b_sum. ((((exists ff_h_b_sum_summand. ff_h_b_sum_summand + S (ff_a_b_sum) = S ((S (ff_i_b_sum)) * c)) /\ exists ff_q_b_sum_summand. b = ff_q_b_sum_summand * S ((S (ff_i_b_sum)) * c) + (ff_a_b_sum))) /\ ((((exists ff_h_b_sum_partial. ff_h_b_sum_partial + S (ff_r_b_sum) = S ((S (ff_i_b_sum)) * ff_v_b_sum)) /\ exists ff_q_b_sum_partial. ff_u_b_sum = ff_q_b_sum_partial * S ((S (ff_i_b_sum)) * ff_v_b_sum) + (ff_r_b_sum))) /\ ((((exists ff_h_b_sum_successor. ff_h_b_sum_successor + S (ff_s_b_sum) = S ((S (S ff_i_b_sum)) * ff_v_b_sum)) /\ exists ff_q_b_sum_successor. ff_u_b_sum = ff_q_b_sum_successor * S ((S (S ff_i_b_sum)) * ff_v_b_sum) + (ff_s_b_sum))) /\ ff_s_b_sum = ff_r_b_sum + ff_a_b_sum)))))) /\ (forall ff_i_b_bits. (exists ff_lt_b_bits_bound. ff_lt_b_bits_bound + S ff_i_b_bits = l) -> exists ff_bit_b_bits. ((((exists ff_h_b_bits_decoded. ff_h_b_bits_decoded + S (ff_bit_b_bits) = S ((S (ff_i_b_bits)) * c)) /\ exists ff_q_b_bits_decoded. b = ff_q_b_bits_decoded * S ((S (ff_i_b_bits)) * c) + (ff_bit_b_bits))) /\ (ff_bit_b_bits = 0 \/ ff_bit_b_bits = 1))))) -> exists h. h + n = l

Structural proof guide

A zero/one count never exceeds the length of its decoded prefix.

Direct prerequisites: bit_count_zero, bit_count_succ_decompose, add_succ_left, add_assoc. The authored body proceeds by structural induction (1), case analysis (7), intermediate claims (3), equality transport (10).

Proof neighborhood

Direct dependencies

BT008N bit_count_zero BT008O bit_count_succ_decompose BT0001 add_succ_left BT0003 add_assoc

Direct dependents

BT00Y1 bit_count_positive_last_one

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

58 script commands · 20 reading checkpoints · 3 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.

Named ingredients (4)
bit count zerobit count succ decomposeadd succ leftadd assoc

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–5

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

  1. L3
    induction l
  2. L4
    intro n
  3. L5
    intro hcount
03Establish hnL6–13

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

  1. L6
    have hn : n = 0
  2. L7
    specialize bit_count_zero b
  3. L8
    specialize bit_count_zero c
  4. L9
    specialize bit_count_zero 0
  5. L10
    specialize bit_count_zero n
  6. L11
    apply bit_count_zero
  7. L12
    refl
  8. L13
    exact hcount
04Construct an explicit witnessL14–14

Supply the displayed value, then prove that it has the required property.

  1. L14
    exists 0
05Calculate and transport equalitiesL15–17

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

  1. L15
    rewrite hn
  2. L16
    rewrite PA3
  3. L17
    refl
06Fix variables and assumptionsL18–19

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

  1. L18
    intro n
  2. L19
    intro hcount
07Establish hdecompL20–28

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

  1. L20
    have hdecomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (BitCount(b,c,l,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))Definitions: BetaAtBitCount
  2. L21
    specialize bit_count_succ_decompose b
  3. L22
    specialize bit_count_succ_decompose c
  4. L23
    specialize bit_count_succ_decompose l
  5. L24
    specialize bit_count_succ_decompose (S l)
  6. L25
    specialize bit_count_succ_decompose n
  7. L26
    apply bit_count_succ_decompose
  8. L27
    refl
  9. L28
    exact hcount
08Separate the logical casesL29–33

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

  1. L29
    cases hdecomp
  2. L30
    cases hdecomp_witness
  3. L31
    cases hdecomp_witness_witness
  4. L32
    cases hdecomp_witness_witness_right
  5. L33
    cases hdecomp_witness_witness_right_right
09Establish hrL34–37

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

  1. L34
    have hr : exists h. h + x1 = l
  2. L35
    specialize IH x1
  3. L36
    apply IH
  4. L37
    exact hdecomp_witness_witness_right_left
10Separate the logical casesL38–39

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

  1. L38
    cases hr
  2. L39
    cases hdecomp_witness_witness_right_right_left
11Construct an explicit witnessL40–40

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists S x2
12Calculate and transport equalitiesL41–43

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

  1. L41
    rewrite hdecomp_witness_witness_right_right_right
  2. L42
    rewrite hdecomp_witness_witness_right_right_left_left
  3. L43
    rewrite PA3
13Use earlier factsL44–45

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

  1. L44
    specialize add_succ_left x2
  2. L45
    specialize add_succ_left x1
14Calculate and transport equalitiesL46–47

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

  1. L46
    rewrite add_succ_left
  2. L47
    congr
15Use earlier factsL48–48

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

  1. L48
    exact hr_witness
16Construct an explicit witnessL49–49

Supply the displayed value, then prove that it has the required property.

  1. L49
    exists x2
17Calculate and transport equalitiesL50–53

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

  1. L50
    rewrite hdecomp_witness_witness_right_right_right
  2. L51
    rewrite hdecomp_witness_witness_right_right_left_right
  3. L52
    trans (x2 + x1) + 1
  4. L53
    symm
18Use earlier factsL54–54

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

  1. L54
    apply add_assoc
19Calculate and transport equalitiesL55–57

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

  1. L55
    rewrite PA4
  2. L56
    rewrite PA3
  3. L57
    congr
20Use earlier factsL58–58

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

  1. L58
    exact hr_witness

Library-wide reading audit

Original exact command ledger · 58 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro hcount
  6. 0006have hn : n = 0
  7. 0007specialize bit_count_zero b
  8. 0008specialize bit_count_zero c
  9. 0009specialize bit_count_zero 0
  10. 0010specialize bit_count_zero n
  11. 0011apply bit_count_zero
  12. 0012refl
  13. 0013exact hcount
  14. 0014exists 0
  15. 0015rewrite hn
  16. 0016rewrite PA3
  17. 0017refl
  18. 0018intro n
  19. 0019intro hcount
  20. 0020have hdecomp : exists a r. (((exists ff_h_last. ff_h_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_last. b = ff_q_last * S ((S (l)) * c) + (a))) /\ ((((exists ff_u_prefix_sum ff_v_prefix_sum. ((((exists ff_h_prefix_sum_start. ff_h_prefix_sum_start + S (0) = S ((S (0)) * ff_v_prefix_sum)) /\ exists ff_q_prefix_sum_start. ff_u_prefix_sum = ff_q_prefix_sum_start * S ((S (0)) * ff_v_prefix_sum) + (0))) /\ ((((exists ff_h_prefix_sum_terminal. ff_h_prefix_sum_terminal + S (r) = S ((S (l)) * ff_v_prefix_sum)) /\ exists ff_q_prefix_sum_terminal. ff_u_prefix_sum = ff_q_prefix_sum_terminal * S ((S (l)) * ff_v_prefix_sum) + (r))) /\ forall ff_i_prefix_sum. (exists ff_lt_prefix_sum_bound. ff_lt_prefix_sum_bound + S ff_i_prefix_sum = l) -> exists ff_a_prefix_sum ff_r_prefix_sum ff_s_prefix_sum. ((((exists ff_h_prefix_sum_summand. ff_h_prefix_sum_summand + S (ff_a_prefix_sum) = S ((S (ff_i_prefix_sum)) * c)) /\ exists ff_q_prefix_sum_summand. b = ff_q_prefix_sum_summand * S ((S (ff_i_prefix_sum)) * c) + (ff_a_prefix_sum))) /\ ((((exists ff_h_prefix_sum_partial. ff_h_prefix_sum_partial + S (ff_r_prefix_sum) = S ((S (ff_i_prefix_sum)) * ff_v_prefix_sum)) /\ exists ff_q_prefix_sum_partial. ff_u_prefix_sum = ff_q_prefix_sum_partial * S ((S (ff_i_prefix_sum)) * ff_v_prefix_sum) + (ff_r_prefix_sum))) /\ ((((exists ff_h_prefix_sum_successor. ff_h_prefix_sum_successor + S (ff_s_prefix_sum) = S ((S (S ff_i_prefix_sum)) * ff_v_prefix_sum)) /\ exists ff_q_prefix_sum_successor. ff_u_prefix_sum = ff_q_prefix_sum_successor * S ((S (S ff_i_prefix_sum)) * ff_v_prefix_sum) + (ff_s_prefix_sum))) /\ ff_s_prefix_sum = ff_r_prefix_sum + ff_a_prefix_sum)))))) /\ (forall ff_i_prefix_bits. (exists ff_lt_prefix_bits_bound. ff_lt_prefix_bits_bound + S ff_i_prefix_bits = l) -> exists ff_bit_prefix_bits. ((((exists ff_h_prefix_bits_decoded. ff_h_prefix_bits_decoded + S (ff_bit_prefix_bits) = S ((S (ff_i_prefix_bits)) * c)) /\ exists ff_q_prefix_bits_decoded. b = ff_q_prefix_bits_decoded * S ((S (ff_i_prefix_bits)) * c) + (ff_bit_prefix_bits))) /\ (ff_bit_prefix_bits = 0 \/ ff_bit_prefix_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  21. 0021specialize bit_count_succ_decompose b
  22. 0022specialize bit_count_succ_decompose c
  23. 0023specialize bit_count_succ_decompose l
  24. 0024specialize bit_count_succ_decompose (S l)
  25. 0025specialize bit_count_succ_decompose n
  26. 0026apply bit_count_succ_decompose
  27. 0027refl
  28. 0028exact hcount
  29. 0029cases hdecomp
  30. 0030cases hdecomp_witness
  31. 0031cases hdecomp_witness_witness
  32. 0032cases hdecomp_witness_witness_right
  33. 0033cases hdecomp_witness_witness_right_right
  34. 0034have hr : exists h. h + x1 = l
  35. 0035specialize IH x1
  36. 0036apply IH
  37. 0037exact hdecomp_witness_witness_right_left
  38. 0038cases hr
  39. 0039cases hdecomp_witness_witness_right_right_left
  40. 0040exists S x2
  41. 0041rewrite hdecomp_witness_witness_right_right_right
  42. 0042rewrite hdecomp_witness_witness_right_right_left_left
  43. 0043rewrite PA3
  44. 0044specialize add_succ_left x2
  45. 0045specialize add_succ_left x1
  46. 0046rewrite add_succ_left
  47. 0047congr
  48. 0048exact hr_witness
  49. 0049exists x2
  50. 0050rewrite hdecomp_witness_witness_right_right_right
  51. 0051rewrite hdecomp_witness_witness_right_right_left_right
  52. 0052trans (x2 + x1) + 1
  53. 0053symm
  54. 0054apply add_assoc
  55. 0055rewrite PA4
  56. 0056rewrite PA3
  57. 0057congr
  58. 0058exact hr_witness