BT008P

bit_count_bounded

Stable · empty-context checked

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

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 this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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