PA0042 · theorem

bit_count_succ_decompose

Stable checked-use theorem · independently closed

A successor count is its prefix count plus a final zero-or-one bit.

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

∀ b. ∀ c. ∀ l. ∀ sl. ∀ n. sl = S l → BitCount(b,c,sl,n) → ∃ x. ∃ y. BetaAt(b,c,l,x) ∧ (BitCount(b,c,l,y) ∧ ((x = 0 ∨ x = 1) ∧ n = y + x))

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

PD0013 BetaAt PD0017 BitCount

3 occurrences

In local proof propositions

PD0013 BetaAt PD0015 Sum PD0016 AllBits

4 occurrences

Exact expanded native-PA statement
forall b c l sl n. sl = S l -> (((exists ff_u_successor_sum ff_v_successor_sum. ((((exists ff_h_successor_sum_start. ff_h_successor_sum_start + S (0) = S ((S (0)) * ff_v_successor_sum)) /\ exists ff_q_successor_sum_start. ff_u_successor_sum = ff_q_successor_sum_start * S ((S (0)) * ff_v_successor_sum) + (0))) /\ ((((exists ff_h_successor_sum_terminal. ff_h_successor_sum_terminal + S (n) = S ((S (sl)) * ff_v_successor_sum)) /\ exists ff_q_successor_sum_terminal. ff_u_successor_sum = ff_q_successor_sum_terminal * S ((S (sl)) * ff_v_successor_sum) + (n))) /\ forall ff_i_successor_sum. (exists ff_lt_successor_sum_bound. ff_lt_successor_sum_bound + S ff_i_successor_sum = sl) -> exists ff_a_successor_sum ff_r_successor_sum ff_s_successor_sum. ((((exists ff_h_successor_sum_summand. ff_h_successor_sum_summand + S (ff_a_successor_sum) = S ((S (ff_i_successor_sum)) * c)) /\ exists ff_q_successor_sum_summand. b = ff_q_successor_sum_summand * S ((S (ff_i_successor_sum)) * c) + (ff_a_successor_sum))) /\ ((((exists ff_h_successor_sum_partial. ff_h_successor_sum_partial + S (ff_r_successor_sum) = S ((S (ff_i_successor_sum)) * ff_v_successor_sum)) /\ exists ff_q_successor_sum_partial. ff_u_successor_sum = ff_q_successor_sum_partial * S ((S (ff_i_successor_sum)) * ff_v_successor_sum) + (ff_r_successor_sum))) /\ ((((exists ff_h_successor_sum_successor. ff_h_successor_sum_successor + S (ff_s_successor_sum) = S ((S (S ff_i_successor_sum)) * ff_v_successor_sum)) /\ exists ff_q_successor_sum_successor. ff_u_successor_sum = ff_q_successor_sum_successor * S ((S (S ff_i_successor_sum)) * ff_v_successor_sum) + (ff_s_successor_sum))) /\ ff_s_successor_sum = ff_r_successor_sum + ff_a_successor_sum)))))) /\ (forall ff_i_successor_bits. (exists ff_lt_successor_bits_bound. ff_lt_successor_bits_bound + S ff_i_successor_bits = sl) -> exists ff_bit_successor_bits. ((((exists ff_h_successor_bits_decoded. ff_h_successor_bits_decoded + S (ff_bit_successor_bits) = S ((S (ff_i_successor_bits)) * c)) /\ exists ff_q_successor_bits_decoded. b = ff_q_successor_bits_decoded * S ((S (ff_i_successor_bits)) * c) + (ff_bit_successor_bits))) /\ (ff_bit_successor_bits = 0 \/ ff_bit_successor_bits = 1))))) -> 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))

Proof neighborhood

Direct theorem prerequisites

PA003Y beta_sum_succ_decompose PA0040 all_bits_prefix_succ PA0041 all_bits_last_succ PA002F beta_at_unique

Direct theorem dependents

PA007G beta_sign_factor_prefix_exists PA007I beta_sign_factor_product_power PA00DW beta_all_one_bit_count_exact PA00DX eisenstein_initial_segment_bit_count_functional PA00EE complementary_bit_counts_add_length PA00EU eisenstein_successor_row_count_decompose

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

63 script commands · 17 reading checkpoints · 4 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 (4)
beta sum succ decomposeall bits prefix succall bits last succbeta at unique
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro sl
  5. L5
    intro n
  6. L6
    intro hsl
  7. L7
    intro hcount
02Calculate and transport equalitiesL8–11

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

  1. L8
    rewrite hsl at hcount
  2. L9
    rewrite hsl at hcount
  3. L10
    rewrite hsl at hcount
  4. L11
    rewrite hsl at hcount
03Separate the logical casesL12–12

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

  1. L12
    cases hcount
04Establish hsumL13–19

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

  1. L13
    have hsum : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ n = r + a)Definitions: BetaAt(b,c,l,a)Sum(b,c,l,r)Original native command in the exact edition
  2. L14
    specialize beta_sum_succ_decompose b
  3. L15
    specialize beta_sum_succ_decompose c
  4. L16
    specialize beta_sum_succ_decompose l
  5. L17
    specialize beta_sum_succ_decompose n
  6. L18
    apply beta_sum_succ_decompose
  7. L19
    exact hcount_left
05Separate the logical casesL20–23

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

  1. L20
    cases hsum
  2. L21
    cases hsum_witness
  3. L22
    cases hsum_witness_witness
  4. L23
    cases hsum_witness_witness_right
06Establish hlastL24–31

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

  1. L24
    have hlast : ∃ a. BetaAt(b,c,l,a) ∧ (a = 0 ∨ a = 1)Definitions: BetaAt(b,c,l,a)Original native command in the exact edition
  2. L25
    specialize all_bits_last_succ b
  3. L26
    specialize all_bits_last_succ c
  4. L27
    specialize all_bits_last_succ l
  5. L28
    specialize all_bits_last_succ (S l)
  6. L29
    apply all_bits_last_succ
  7. L30
    refl
  8. L31
    exact hcount_right
07Separate the logical casesL32–33

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

  1. L32
    cases hlast
  2. L33
    cases hlast_witness
08Establish haL34–42

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

  1. L34
    have ha : x = x2
  2. L35
    specialize beta_at_unique b
  3. L36
    specialize beta_at_unique c
  4. L37
    specialize beta_at_unique l
  5. L38
    specialize beta_at_unique x
  6. L39
    specialize beta_at_unique x2
  7. L40
    apply beta_at_unique
  8. L41
    exact hsum_witness_witness_left
  9. L42
    exact hlast_witness_left
09Establish hprefixL43–50

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

  1. L43
    have hprefix : AllBits(b,c,l)Definitions: AllBits(b,c,l)Original native command in the exact edition
  2. L44
    specialize all_bits_prefix_succ b
  3. L45
    specialize all_bits_prefix_succ c
  4. L46
    specialize all_bits_prefix_succ l
  5. L47
    specialize all_bits_prefix_succ (S l)
  6. L48
    apply all_bits_prefix_succ
  7. L49
    refl
  8. L50
    exact hcount_right
10Construct an explicit witnessL51–52

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

  1. L51
    exists x
  2. L52
    exists x1
11Separate the logical casesL53–53

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

  1. L53
    split
12Use earlier factsL54–54

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

  1. L54
    exact hsum_witness_witness_left
13Separate the logical casesL55–56

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

  1. L55
    split
  2. L56
    split
14Use earlier factsL57–58

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

  1. L57
    exact hsum_witness_witness_right_left
  2. L58
    exact hprefix
15Separate the logical casesL59–59

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

  1. L59
    split
16Calculate and transport equalitiesL60–61

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

  1. L60
    rewrite ha
  2. L61
    rewrite ha
17Use earlier factsL62–63

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

  1. L62
    exact hlast_witness_right
  2. L63
    exact hsum_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro sl
  5. 0005intro n
  6. 0006intro hsl
  7. 0007intro hcount
  8. 0008rewrite hsl at hcount
  9. 0009rewrite hsl at hcount
  10. 0010rewrite hsl at hcount
  11. 0011rewrite hsl at hcount
  12. 0012cases hcount
  13. 0013have hsum : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ n = r + a)
    Exact native replay linehave hsum : exists a r. (((exists ff_h_sum_last. ff_h_sum_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_sum_last. b = ff_q_sum_last * S ((S (l)) * c) + (a))) /\ ((exists ff_u_sum_prefix ff_v_sum_prefix. ((((exists ff_h_sum_prefix_start. ff_h_sum_prefix_start + S (0) = S ((S (0)) * ff_v_sum_prefix)) /\ exists ff_q_sum_prefix_start. ff_u_sum_prefix = ff_q_sum_prefix_start * S ((S (0)) * ff_v_sum_prefix) + (0))) /\ ((((exists ff_h_sum_prefix_terminal. ff_h_sum_prefix_terminal + S (r) = S ((S (l)) * ff_v_sum_prefix)) /\ exists ff_q_sum_prefix_terminal. ff_u_sum_prefix = ff_q_sum_prefix_terminal * S ((S (l)) * ff_v_sum_prefix) + (r))) /\ forall ff_i_sum_prefix. (exists ff_lt_sum_prefix_bound. ff_lt_sum_prefix_bound + S ff_i_sum_prefix = l) -> exists ff_a_sum_prefix ff_r_sum_prefix ff_s_sum_prefix. ((((exists ff_h_sum_prefix_summand. ff_h_sum_prefix_summand + S (ff_a_sum_prefix) = S ((S (ff_i_sum_prefix)) * c)) /\ exists ff_q_sum_prefix_summand. b = ff_q_sum_prefix_summand * S ((S (ff_i_sum_prefix)) * c) + (ff_a_sum_prefix))) /\ ((((exists ff_h_sum_prefix_partial. ff_h_sum_prefix_partial + S (ff_r_sum_prefix) = S ((S (ff_i_sum_prefix)) * ff_v_sum_prefix)) /\ exists ff_q_sum_prefix_partial. ff_u_sum_prefix = ff_q_sum_prefix_partial * S ((S (ff_i_sum_prefix)) * ff_v_sum_prefix) + (ff_r_sum_prefix))) /\ ((((exists ff_h_sum_prefix_successor. ff_h_sum_prefix_successor + S (ff_s_sum_prefix) = S ((S (S ff_i_sum_prefix)) * ff_v_sum_prefix)) /\ exists ff_q_sum_prefix_successor. ff_u_sum_prefix = ff_q_sum_prefix_successor * S ((S (S ff_i_sum_prefix)) * ff_v_sum_prefix) + (ff_s_sum_prefix))) /\ ff_s_sum_prefix = ff_r_sum_prefix + ff_a_sum_prefix)))))) /\ n = r + a)
  14. 0014specialize beta_sum_succ_decompose b
  15. 0015specialize beta_sum_succ_decompose c
  16. 0016specialize beta_sum_succ_decompose l
  17. 0017specialize beta_sum_succ_decompose n
  18. 0018apply beta_sum_succ_decompose
  19. 0019exact hcount_left
  20. 0020cases hsum
  21. 0021cases hsum_witness
  22. 0022cases hsum_witness_witness
  23. 0023cases hsum_witness_witness_right
  24. 0024have hlast : ∃ a. BetaAt(b,c,l,a) ∧ (a = 0 ∨ a = 1)
    Exact native replay linehave hlast : exists a. ((((exists ff_h_bits_last. ff_h_bits_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_bits_last. b = ff_q_bits_last * S ((S (l)) * c) + (a))) /\ (a = 0 \/ a = 1))
  25. 0025specialize all_bits_last_succ b
  26. 0026specialize all_bits_last_succ c
  27. 0027specialize all_bits_last_succ l
  28. 0028specialize all_bits_last_succ (S l)
  29. 0029apply all_bits_last_succ
  30. 0030refl
  31. 0031exact hcount_right
  32. 0032cases hlast
  33. 0033cases hlast_witness
  34. 0034have ha : x = x2
  35. 0035specialize beta_at_unique b
  36. 0036specialize beta_at_unique c
  37. 0037specialize beta_at_unique l
  38. 0038specialize beta_at_unique x
  39. 0039specialize beta_at_unique x2
  40. 0040apply beta_at_unique
  41. 0041exact hsum_witness_witness_left
  42. 0042exact hlast_witness_left
  43. 0043have hprefix : AllBits(b,c,l)
    Exact native replay linehave hprefix : forall ff_i_kept_prefix. (exists ff_lt_kept_prefix_bound. ff_lt_kept_prefix_bound + S ff_i_kept_prefix = l) -> exists ff_bit_kept_prefix. ((((exists ff_h_kept_prefix_decoded. ff_h_kept_prefix_decoded + S (ff_bit_kept_prefix) = S ((S (ff_i_kept_prefix)) * c)) /\ exists ff_q_kept_prefix_decoded. b = ff_q_kept_prefix_decoded * S ((S (ff_i_kept_prefix)) * c) + (ff_bit_kept_prefix))) /\ (ff_bit_kept_prefix = 0 \/ ff_bit_kept_prefix = 1))
  44. 0044specialize all_bits_prefix_succ b
  45. 0045specialize all_bits_prefix_succ c
  46. 0046specialize all_bits_prefix_succ l
  47. 0047specialize all_bits_prefix_succ (S l)
  48. 0048apply all_bits_prefix_succ
  49. 0049refl
  50. 0050exact hcount_right
  51. 0051exists x
  52. 0052exists x1
  53. 0053split
  54. 0054exact hsum_witness_witness_left
  55. 0055split
  56. 0056split
  57. 0057exact hsum_witness_witness_right_left
  58. 0058exact hprefix
  59. 0059split
  60. 0060rewrite ha
  61. 0061rewrite ha
  62. 0062exact hlast_witness_right
  63. 0063exact hsum_witness_witness_right_right