BT00JC

beta_all_one_bit_count_exact

Alpha body-checked · checked-use disabled

A length-k beta prefix consisting only of ones has BitCount k.

Exact expanded PA statement

forall b c k n. (forall eis_one_index_initial_segment_all_one_source. (exists eis_lt_gap_initial_segment_all_one_source_bound. eis_lt_gap_initial_segment_all_one_source_bound + S (eis_one_index_initial_segment_all_one_source) = k) -> (((exists ff_h_eis_initial_segment_all_one_source_decoded. ff_h_eis_initial_segment_all_one_source_decoded + S (1) = S ((S (eis_one_index_initial_segment_all_one_source)) * c)) /\ exists ff_q_eis_initial_segment_all_one_source_decoded. b = ff_q_eis_initial_segment_all_one_source_decoded * S ((S (eis_one_index_initial_segment_all_one_source)) * c) + (1)))) -> (((exists ff_u_initial_segment_all_one_count_sum ff_v_initial_segment_all_one_count_sum. ((((exists ff_h_initial_segment_all_one_count_sum_start. ff_h_initial_segment_all_one_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_start. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_start * S ((S (0)) * ff_v_initial_segment_all_one_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_all_one_count_sum_terminal. ff_h_initial_segment_all_one_count_sum_terminal + S (n) = S ((S (k)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_terminal. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_all_one_count_sum) + (n))) /\ forall ff_i_initial_segment_all_one_count_sum. (exists ff_lt_initial_segment_all_one_count_sum_bound. ff_lt_initial_segment_all_one_count_sum_bound + S ff_i_initial_segment_all_one_count_sum = k) -> exists ff_a_initial_segment_all_one_count_sum ff_r_initial_segment_all_one_count_sum ff_s_initial_segment_all_one_count_sum. ((((exists ff_h_initial_segment_all_one_count_sum_summand. ff_h_initial_segment_all_one_count_sum_summand + S (ff_a_initial_segment_all_one_count_sum) = S ((S (ff_i_initial_segment_all_one_count_sum)) * c)) /\ exists ff_q_initial_segment_all_one_count_sum_summand. b = ff_q_initial_segment_all_one_count_sum_summand * S ((S (ff_i_initial_segment_all_one_count_sum)) * c) + (ff_a_initial_segment_all_one_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_count_sum_partial. ff_h_initial_segment_all_one_count_sum_partial + S (ff_r_initial_segment_all_one_count_sum) = S ((S (ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_partial. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_partial * S ((S (ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum) + (ff_r_initial_segment_all_one_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_count_sum_successor. ff_h_initial_segment_all_one_count_sum_successor + S (ff_s_initial_segment_all_one_count_sum) = S ((S (S ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_successor. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_successor * S ((S (S ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum) + (ff_s_initial_segment_all_one_count_sum))) /\ ff_s_initial_segment_all_one_count_sum = ff_r_initial_segment_all_one_count_sum + ff_a_initial_segment_all_one_count_sum)))))) /\ (forall ff_i_initial_segment_all_one_count_bits. (exists ff_lt_initial_segment_all_one_count_bits_bound. ff_lt_initial_segment_all_one_count_bits_bound + S ff_i_initial_segment_all_one_count_bits = k) -> exists ff_bit_initial_segment_all_one_count_bits. ((((exists ff_h_initial_segment_all_one_count_bits_decoded. ff_h_initial_segment_all_one_count_bits_decoded + S (ff_bit_initial_segment_all_one_count_bits) = S ((S (ff_i_initial_segment_all_one_count_bits)) * c)) /\ exists ff_q_initial_segment_all_one_count_bits_decoded. b = ff_q_initial_segment_all_one_count_bits_decoded * S ((S (ff_i_initial_segment_all_one_count_bits)) * c) + (ff_bit_initial_segment_all_one_count_bits))) /\ (ff_bit_initial_segment_all_one_count_bits = 0 \/ ff_bit_initial_segment_all_one_count_bits = 1))))) -> n = k

Structural proof guide

A length-k beta prefix consisting only of ones has BitCount k.

Direct prerequisites: bit_count_zero, bit_count_succ_decompose, all_bits_prefix_succ, beta_at_unique, le_succ, le_refl. The authored body proceeds by structural induction (1), case analysis (5), intermediate claims (5), equality transport (3).

Proof neighborhood

Direct dependencies

BT008N bit_count_zero BT008O bit_count_succ_decompose BT008J all_bits_prefix_succ BT0042 beta_at_unique BT0018 le_succ BT000E le_refl

Direct dependents

BT00JD eisenstein_initial_segment_bit_count_functional

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro b
  2. 0002intro c
  3. 0003induction k
  4. 0004intro n
  5. 0005intro hone
  6. 0006intro hcount
  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. 0014intro n
  15. 0015intro hone
  16. 0016intro hcount
  17. 0017have hdecomp : exists a r. (((exists ff_h_initial_segment_all_one_last. ff_h_initial_segment_all_one_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_all_one_last. b = ff_q_initial_segment_all_one_last * S ((S (k)) * c) + (a))) /\ ((((exists ff_u_initial_segment_all_one_prefix_count_sum ff_v_initial_segment_all_one_prefix_count_sum. ((((exists ff_h_initial_segment_all_one_prefix_count_sum_start. ff_h_initial_segment_all_one_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_start. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_start * S ((S (0)) * ff_v_initial_segment_all_one_prefix_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_all_one_prefix_count_sum_terminal. ff_h_initial_segment_all_one_prefix_count_sum_terminal + S (r) = S ((S (k)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_terminal. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_all_one_prefix_count_sum) + (r))) /\ forall ff_i_initial_segment_all_one_prefix_count_sum. (exists ff_lt_initial_segment_all_one_prefix_count_sum_bound. ff_lt_initial_segment_all_one_prefix_count_sum_bound + S ff_i_initial_segment_all_one_prefix_count_sum = k) -> exists ff_a_initial_segment_all_one_prefix_count_sum ff_r_initial_segment_all_one_prefix_count_sum ff_s_initial_segment_all_one_prefix_count_sum. ((((exists ff_h_initial_segment_all_one_prefix_count_sum_summand. ff_h_initial_segment_all_one_prefix_count_sum_summand + S (ff_a_initial_segment_all_one_prefix_count_sum) = S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * c)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_summand. b = ff_q_initial_segment_all_one_prefix_count_sum_summand * S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * c) + (ff_a_initial_segment_all_one_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_prefix_count_sum_partial. ff_h_initial_segment_all_one_prefix_count_sum_partial + S (ff_r_initial_segment_all_one_prefix_count_sum) = S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_partial. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_partial * S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum) + (ff_r_initial_segment_all_one_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_prefix_count_sum_successor. ff_h_initial_segment_all_one_prefix_count_sum_successor + S (ff_s_initial_segment_all_one_prefix_count_sum) = S ((S (S ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_successor. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_successor * S ((S (S ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum) + (ff_s_initial_segment_all_one_prefix_count_sum))) /\ ff_s_initial_segment_all_one_prefix_count_sum = ff_r_initial_segment_all_one_prefix_count_sum + ff_a_initial_segment_all_one_prefix_count_sum)))))) /\ (forall ff_i_initial_segment_all_one_prefix_count_bits. (exists ff_lt_initial_segment_all_one_prefix_count_bits_bound. ff_lt_initial_segment_all_one_prefix_count_bits_bound + S ff_i_initial_segment_all_one_prefix_count_bits = k) -> exists ff_bit_initial_segment_all_one_prefix_count_bits. ((((exists ff_h_initial_segment_all_one_prefix_count_bits_decoded. ff_h_initial_segment_all_one_prefix_count_bits_decoded + S (ff_bit_initial_segment_all_one_prefix_count_bits) = S ((S (ff_i_initial_segment_all_one_prefix_count_bits)) * c)) /\ exists ff_q_initial_segment_all_one_prefix_count_bits_decoded. b = ff_q_initial_segment_all_one_prefix_count_bits_decoded * S ((S (ff_i_initial_segment_all_one_prefix_count_bits)) * c) + (ff_bit_initial_segment_all_one_prefix_count_bits))) /\ (ff_bit_initial_segment_all_one_prefix_count_bits = 0 \/ ff_bit_initial_segment_all_one_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  18. 0018specialize bit_count_succ_decompose b
  19. 0019specialize bit_count_succ_decompose c
  20. 0020specialize bit_count_succ_decompose k
  21. 0021specialize bit_count_succ_decompose (S k)
  22. 0022specialize bit_count_succ_decompose n
  23. 0023apply bit_count_succ_decompose
  24. 0024refl
  25. 0025exact hcount
  26. 0026cases hdecomp
  27. 0027cases hdecomp_witness
  28. 0028cases hdecomp_witness_witness
  29. 0029cases hdecomp_witness_witness_right
  30. 0030cases hdecomp_witness_witness_right_right
  31. 0031have hone_previous : forall eis_one_index_initial_segment_all_one_previous. (exists eis_lt_gap_initial_segment_all_one_previous_bound. eis_lt_gap_initial_segment_all_one_previous_bound + S (eis_one_index_initial_segment_all_one_previous) = k) -> (((exists ff_h_eis_initial_segment_all_one_previous_decoded. ff_h_eis_initial_segment_all_one_previous_decoded + S (1) = S ((S (eis_one_index_initial_segment_all_one_previous)) * c)) /\ exists ff_q_eis_initial_segment_all_one_previous_decoded. b = ff_q_eis_initial_segment_all_one_previous_decoded * S ((S (eis_one_index_initial_segment_all_one_previous)) * c) + (1)))
  32. 0032intro j
  33. 0033intro hj
  34. 0034specialize hone j
  35. 0035apply hone
  36. 0036specialize le_succ (S j)
  37. 0037specialize le_succ k
  38. 0038apply le_succ
  39. 0039exact hj
  40. 0040have hr : x1 = k
  41. 0041specialize IH x1
  42. 0042apply IH
  43. 0043exact hone_previous
  44. 0044exact hdecomp_witness_witness_right_left
  45. 0045have hlast_one : ((exists ff_h_initial_segment_all_one_terminal. ff_h_initial_segment_all_one_terminal + S (1) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_all_one_terminal. b = ff_q_initial_segment_all_one_terminal * S ((S (k)) * c) + (1))
  46. 0046specialize hone k
  47. 0047apply hone
  48. 0048specialize le_refl (S k)
  49. 0049exact le_refl
  50. 0050have ha : x = 1
  51. 0051specialize beta_at_unique b
  52. 0052specialize beta_at_unique c
  53. 0053specialize beta_at_unique k
  54. 0054specialize beta_at_unique x
  55. 0055specialize beta_at_unique 1
  56. 0056apply beta_at_unique
  57. 0057exact hdecomp_witness_witness_left
  58. 0058exact hlast_one
  59. 0059rewrite hdecomp_witness_witness_right_right_right
  60. 0060rewrite hr
  61. 0061rewrite ha
  62. 0062simp