PA00EE

complementary_bit_counts_add_length

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

Complementary decoded bit prefixes have counts summing to their length.

Exact expanded PA statement

forall b c z e l n m. (((exists ff_u_complement_left_sum ff_v_complement_left_sum. ((((exists ff_h_complement_left_sum_start. ff_h_complement_left_sum_start + S (0) = S ((S (0)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_start. ff_u_complement_left_sum = ff_q_complement_left_sum_start * S ((S (0)) * ff_v_complement_left_sum) + (0))) /\ ((((exists ff_h_complement_left_sum_terminal. ff_h_complement_left_sum_terminal + S (n) = S ((S (l)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_terminal. ff_u_complement_left_sum = ff_q_complement_left_sum_terminal * S ((S (l)) * ff_v_complement_left_sum) + (n))) /\ forall ff_i_complement_left_sum. (exists ff_lt_complement_left_sum_bound. ff_lt_complement_left_sum_bound + S ff_i_complement_left_sum = l) -> exists ff_a_complement_left_sum ff_r_complement_left_sum ff_s_complement_left_sum. ((((exists ff_h_complement_left_sum_summand. ff_h_complement_left_sum_summand + S (ff_a_complement_left_sum) = S ((S (ff_i_complement_left_sum)) * c)) /\ exists ff_q_complement_left_sum_summand. b = ff_q_complement_left_sum_summand * S ((S (ff_i_complement_left_sum)) * c) + (ff_a_complement_left_sum))) /\ ((((exists ff_h_complement_left_sum_partial. ff_h_complement_left_sum_partial + S (ff_r_complement_left_sum) = S ((S (ff_i_complement_left_sum)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_partial. ff_u_complement_left_sum = ff_q_complement_left_sum_partial * S ((S (ff_i_complement_left_sum)) * ff_v_complement_left_sum) + (ff_r_complement_left_sum))) /\ ((((exists ff_h_complement_left_sum_successor. ff_h_complement_left_sum_successor + S (ff_s_complement_left_sum) = S ((S (S ff_i_complement_left_sum)) * ff_v_complement_left_sum)) /\ exists ff_q_complement_left_sum_successor. ff_u_complement_left_sum = ff_q_complement_left_sum_successor * S ((S (S ff_i_complement_left_sum)) * ff_v_complement_left_sum) + (ff_s_complement_left_sum))) /\ ff_s_complement_left_sum = ff_r_complement_left_sum + ff_a_complement_left_sum)))))) /\ (forall ff_i_complement_left_bits. (exists ff_lt_complement_left_bits_bound. ff_lt_complement_left_bits_bound + S ff_i_complement_left_bits = l) -> exists ff_bit_complement_left_bits. ((((exists ff_h_complement_left_bits_decoded. ff_h_complement_left_bits_decoded + S (ff_bit_complement_left_bits) = S ((S (ff_i_complement_left_bits)) * c)) /\ exists ff_q_complement_left_bits_decoded. b = ff_q_complement_left_bits_decoded * S ((S (ff_i_complement_left_bits)) * c) + (ff_bit_complement_left_bits))) /\ (ff_bit_complement_left_bits = 0 \/ ff_bit_complement_left_bits = 1))))) -> (((exists ff_u_complement_right_sum ff_v_complement_right_sum. ((((exists ff_h_complement_right_sum_start. ff_h_complement_right_sum_start + S (0) = S ((S (0)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_start. ff_u_complement_right_sum = ff_q_complement_right_sum_start * S ((S (0)) * ff_v_complement_right_sum) + (0))) /\ ((((exists ff_h_complement_right_sum_terminal. ff_h_complement_right_sum_terminal + S (m) = S ((S (l)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_terminal. ff_u_complement_right_sum = ff_q_complement_right_sum_terminal * S ((S (l)) * ff_v_complement_right_sum) + (m))) /\ forall ff_i_complement_right_sum. (exists ff_lt_complement_right_sum_bound. ff_lt_complement_right_sum_bound + S ff_i_complement_right_sum = l) -> exists ff_a_complement_right_sum ff_r_complement_right_sum ff_s_complement_right_sum. ((((exists ff_h_complement_right_sum_summand. ff_h_complement_right_sum_summand + S (ff_a_complement_right_sum) = S ((S (ff_i_complement_right_sum)) * e)) /\ exists ff_q_complement_right_sum_summand. z = ff_q_complement_right_sum_summand * S ((S (ff_i_complement_right_sum)) * e) + (ff_a_complement_right_sum))) /\ ((((exists ff_h_complement_right_sum_partial. ff_h_complement_right_sum_partial + S (ff_r_complement_right_sum) = S ((S (ff_i_complement_right_sum)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_partial. ff_u_complement_right_sum = ff_q_complement_right_sum_partial * S ((S (ff_i_complement_right_sum)) * ff_v_complement_right_sum) + (ff_r_complement_right_sum))) /\ ((((exists ff_h_complement_right_sum_successor. ff_h_complement_right_sum_successor + S (ff_s_complement_right_sum) = S ((S (S ff_i_complement_right_sum)) * ff_v_complement_right_sum)) /\ exists ff_q_complement_right_sum_successor. ff_u_complement_right_sum = ff_q_complement_right_sum_successor * S ((S (S ff_i_complement_right_sum)) * ff_v_complement_right_sum) + (ff_s_complement_right_sum))) /\ ff_s_complement_right_sum = ff_r_complement_right_sum + ff_a_complement_right_sum)))))) /\ (forall ff_i_complement_right_bits. (exists ff_lt_complement_right_bits_bound. ff_lt_complement_right_bits_bound + S ff_i_complement_right_bits = l) -> exists ff_bit_complement_right_bits. ((((exists ff_h_complement_right_bits_decoded. ff_h_complement_right_bits_decoded + S (ff_bit_complement_right_bits) = S ((S (ff_i_complement_right_bits)) * e)) /\ exists ff_q_complement_right_bits_decoded. z = ff_q_complement_right_bits_decoded * S ((S (ff_i_complement_right_bits)) * e) + (ff_bit_complement_right_bits))) /\ (ff_bit_complement_right_bits = 0 \/ ff_bit_complement_right_bits = 1))))) -> (forall i a d. (exists h. h + S i = l) -> (((exists ff_h_complement_left_entry. ff_h_complement_left_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_complement_left_entry. b = ff_q_complement_left_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_complement_right_entry. ff_h_complement_right_entry + S (d) = S ((S (i)) * e)) /\ exists ff_q_complement_right_entry. z = ff_q_complement_right_entry * S ((S (i)) * e) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))) -> n + m = l

Structural proof guide

Generated structural guide

Complementary decoded bit prefixes have counts summing to their length.

Use the direct prerequisites bit_count_zero, bit_count_succ_decompose, le_succ, le_refl, add_succ_left as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (13), intermediate claims (7), equality transport (9), certified simplification (3).

Referenced ingredients

PA0048 bit_count_zero PA0042 bit_count_succ_decompose PA002O le_succ PA001A le_refl PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0048 bit_count_zero PA0042 bit_count_succ_decompose PA002O le_succ PA001A le_refl PA000E add_succ_left

Direct dependents

PA00EF eisenstein_row_transposed_column_count_partition

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro e
  5. 0005induction l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010intro hcomplement
  11. 0011have hn : n = 0
  12. 0012specialize bit_count_zero b
  13. 0013specialize bit_count_zero c
  14. 0014specialize bit_count_zero 0
  15. 0015specialize bit_count_zero n
  16. 0016apply bit_count_zero
  17. 0017refl
  18. 0018exact hleft
  19. 0019have hm : m = 0
  20. 0020specialize bit_count_zero z
  21. 0021specialize bit_count_zero e
  22. 0022specialize bit_count_zero 0
  23. 0023specialize bit_count_zero m
  24. 0024apply bit_count_zero
  25. 0025refl
  26. 0026exact hright
  27. 0027rewrite hn
  28. 0028rewrite hm
  29. 0029simp
  30. 0030intro n
  31. 0031intro m
  32. 0032intro hleft
  33. 0033intro hright
  34. 0034intro hcomplement
  35. 0035have hleft_decomp : exists a r. (((exists ff_h_complement_left_last. ff_h_complement_left_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_complement_left_last. b = ff_q_complement_left_last * S ((S (l)) * c) + (a))) /\ ((((exists ff_u_complement_left_prefix_sum ff_v_complement_left_prefix_sum. ((((exists ff_h_complement_left_prefix_sum_start. ff_h_complement_left_prefix_sum_start + S (0) = S ((S (0)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_start. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_start * S ((S (0)) * ff_v_complement_left_prefix_sum) + (0))) /\ ((((exists ff_h_complement_left_prefix_sum_terminal. ff_h_complement_left_prefix_sum_terminal + S (r) = S ((S (l)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_terminal. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_terminal * S ((S (l)) * ff_v_complement_left_prefix_sum) + (r))) /\ forall ff_i_complement_left_prefix_sum. (exists ff_lt_complement_left_prefix_sum_bound. ff_lt_complement_left_prefix_sum_bound + S ff_i_complement_left_prefix_sum = l) -> exists ff_a_complement_left_prefix_sum ff_r_complement_left_prefix_sum ff_s_complement_left_prefix_sum. ((((exists ff_h_complement_left_prefix_sum_summand. ff_h_complement_left_prefix_sum_summand + S (ff_a_complement_left_prefix_sum) = S ((S (ff_i_complement_left_prefix_sum)) * c)) /\ exists ff_q_complement_left_prefix_sum_summand. b = ff_q_complement_left_prefix_sum_summand * S ((S (ff_i_complement_left_prefix_sum)) * c) + (ff_a_complement_left_prefix_sum))) /\ ((((exists ff_h_complement_left_prefix_sum_partial. ff_h_complement_left_prefix_sum_partial + S (ff_r_complement_left_prefix_sum) = S ((S (ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_partial. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_partial * S ((S (ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum) + (ff_r_complement_left_prefix_sum))) /\ ((((exists ff_h_complement_left_prefix_sum_successor. ff_h_complement_left_prefix_sum_successor + S (ff_s_complement_left_prefix_sum) = S ((S (S ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum)) /\ exists ff_q_complement_left_prefix_sum_successor. ff_u_complement_left_prefix_sum = ff_q_complement_left_prefix_sum_successor * S ((S (S ff_i_complement_left_prefix_sum)) * ff_v_complement_left_prefix_sum) + (ff_s_complement_left_prefix_sum))) /\ ff_s_complement_left_prefix_sum = ff_r_complement_left_prefix_sum + ff_a_complement_left_prefix_sum)))))) /\ (forall ff_i_complement_left_prefix_bits. (exists ff_lt_complement_left_prefix_bits_bound. ff_lt_complement_left_prefix_bits_bound + S ff_i_complement_left_prefix_bits = l) -> exists ff_bit_complement_left_prefix_bits. ((((exists ff_h_complement_left_prefix_bits_decoded. ff_h_complement_left_prefix_bits_decoded + S (ff_bit_complement_left_prefix_bits) = S ((S (ff_i_complement_left_prefix_bits)) * c)) /\ exists ff_q_complement_left_prefix_bits_decoded. b = ff_q_complement_left_prefix_bits_decoded * S ((S (ff_i_complement_left_prefix_bits)) * c) + (ff_bit_complement_left_prefix_bits))) /\ (ff_bit_complement_left_prefix_bits = 0 \/ ff_bit_complement_left_prefix_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  36. 0036specialize bit_count_succ_decompose b
  37. 0037specialize bit_count_succ_decompose c
  38. 0038specialize bit_count_succ_decompose l
  39. 0039specialize bit_count_succ_decompose (S l)
  40. 0040specialize bit_count_succ_decompose n
  41. 0041apply bit_count_succ_decompose
  42. 0042refl
  43. 0043exact hleft
  44. 0044cases hleft_decomp
  45. 0045cases hleft_decomp_witness
  46. 0046cases hleft_decomp_witness_witness
  47. 0047cases hleft_decomp_witness_witness_right
  48. 0048cases hleft_decomp_witness_witness_right_right
  49. 0049have hright_decomp : exists d s. (((exists ff_h_complement_right_last. ff_h_complement_right_last + S (d) = S ((S (l)) * e)) /\ exists ff_q_complement_right_last. z = ff_q_complement_right_last * S ((S (l)) * e) + (d))) /\ ((((exists ff_u_complement_right_prefix_sum ff_v_complement_right_prefix_sum. ((((exists ff_h_complement_right_prefix_sum_start. ff_h_complement_right_prefix_sum_start + S (0) = S ((S (0)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_start. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_start * S ((S (0)) * ff_v_complement_right_prefix_sum) + (0))) /\ ((((exists ff_h_complement_right_prefix_sum_terminal. ff_h_complement_right_prefix_sum_terminal + S (s) = S ((S (l)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_terminal. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_terminal * S ((S (l)) * ff_v_complement_right_prefix_sum) + (s))) /\ forall ff_i_complement_right_prefix_sum. (exists ff_lt_complement_right_prefix_sum_bound. ff_lt_complement_right_prefix_sum_bound + S ff_i_complement_right_prefix_sum = l) -> exists ff_a_complement_right_prefix_sum ff_r_complement_right_prefix_sum ff_s_complement_right_prefix_sum. ((((exists ff_h_complement_right_prefix_sum_summand. ff_h_complement_right_prefix_sum_summand + S (ff_a_complement_right_prefix_sum) = S ((S (ff_i_complement_right_prefix_sum)) * e)) /\ exists ff_q_complement_right_prefix_sum_summand. z = ff_q_complement_right_prefix_sum_summand * S ((S (ff_i_complement_right_prefix_sum)) * e) + (ff_a_complement_right_prefix_sum))) /\ ((((exists ff_h_complement_right_prefix_sum_partial. ff_h_complement_right_prefix_sum_partial + S (ff_r_complement_right_prefix_sum) = S ((S (ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_partial. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_partial * S ((S (ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum) + (ff_r_complement_right_prefix_sum))) /\ ((((exists ff_h_complement_right_prefix_sum_successor. ff_h_complement_right_prefix_sum_successor + S (ff_s_complement_right_prefix_sum) = S ((S (S ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum)) /\ exists ff_q_complement_right_prefix_sum_successor. ff_u_complement_right_prefix_sum = ff_q_complement_right_prefix_sum_successor * S ((S (S ff_i_complement_right_prefix_sum)) * ff_v_complement_right_prefix_sum) + (ff_s_complement_right_prefix_sum))) /\ ff_s_complement_right_prefix_sum = ff_r_complement_right_prefix_sum + ff_a_complement_right_prefix_sum)))))) /\ (forall ff_i_complement_right_prefix_bits. (exists ff_lt_complement_right_prefix_bits_bound. ff_lt_complement_right_prefix_bits_bound + S ff_i_complement_right_prefix_bits = l) -> exists ff_bit_complement_right_prefix_bits. ((((exists ff_h_complement_right_prefix_bits_decoded. ff_h_complement_right_prefix_bits_decoded + S (ff_bit_complement_right_prefix_bits) = S ((S (ff_i_complement_right_prefix_bits)) * e)) /\ exists ff_q_complement_right_prefix_bits_decoded. z = ff_q_complement_right_prefix_bits_decoded * S ((S (ff_i_complement_right_prefix_bits)) * e) + (ff_bit_complement_right_prefix_bits))) /\ (ff_bit_complement_right_prefix_bits = 0 \/ ff_bit_complement_right_prefix_bits = 1))))) /\ ((d = 0 \/ d = 1) /\ m = s + d))
  50. 0050specialize bit_count_succ_decompose z
  51. 0051specialize bit_count_succ_decompose e
  52. 0052specialize bit_count_succ_decompose l
  53. 0053specialize bit_count_succ_decompose (S l)
  54. 0054specialize bit_count_succ_decompose m
  55. 0055apply bit_count_succ_decompose
  56. 0056refl
  57. 0057exact hright
  58. 0058cases hright_decomp
  59. 0059cases hright_decomp_witness
  60. 0060cases hright_decomp_witness_witness
  61. 0061cases hright_decomp_witness_witness_right
  62. 0062cases hright_decomp_witness_witness_right_right
  63. 0063have hprefix_complement : forall i a d. (exists h. h + S i = l) -> (((exists ff_h_complement_prefix_left. ff_h_complement_prefix_left + S (a) = S ((S (i)) * c)) /\ exists ff_q_complement_prefix_left. b = ff_q_complement_prefix_left * S ((S (i)) * c) + (a))) -> (((exists ff_h_complement_prefix_right. ff_h_complement_prefix_right + S (d) = S ((S (i)) * e)) /\ exists ff_q_complement_prefix_right. z = ff_q_complement_prefix_right * S ((S (i)) * e) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))
  64. 0064intro i
  65. 0065intro a
  66. 0066intro d
  67. 0067intro hi
  68. 0068intro ha
  69. 0069intro hd
  70. 0070specialize hcomplement i
  71. 0071specialize hcomplement a
  72. 0072specialize hcomplement d
  73. 0073apply hcomplement
  74. 0074specialize le_succ (S i)
  75. 0075specialize le_succ l
  76. 0076apply le_succ
  77. 0077exact hi
  78. 0078exact ha
  79. 0079exact hd
  80. 0080have hprefix : x1 + x3 = l
  81. 0081specialize IH x1
  82. 0082specialize IH x3
  83. 0083apply IH
  84. 0084exact hleft_decomp_witness_witness_right_left
  85. 0085exact hright_decomp_witness_witness_right_left
  86. 0086exact hprefix_complement
  87. 0087have hlast : ((x = 0 /\ x2 = 1) \/ (x = 1 /\ x2 = 0))
  88. 0088specialize hcomplement l
  89. 0089specialize hcomplement x
  90. 0090specialize hcomplement x2
  91. 0091apply hcomplement
  92. 0092specialize le_refl (S l)
  93. 0093exact le_refl
  94. 0094exact hleft_decomp_witness_witness_left
  95. 0095exact hright_decomp_witness_witness_left
  96. 0096rewrite hleft_decomp_witness_witness_right_right_right
  97. 0097rewrite hright_decomp_witness_witness_right_right_right
  98. 0098cases hlast
  99. 0099cases hlast_left
  100. 0100rewrite hlast_left_left
  101. 0101rewrite hlast_left_right
  102. 0102simp
  103. 0103cases hlast_right
  104. 0104rewrite hlast_right_left
  105. 0105rewrite hlast_right_right
  106. 0106simp
  107. 0107specialize add_succ_left x1
  108. 0108specialize add_succ_left x3
  109. 0109trans S (x1 + x3)
  110. 0110exact add_succ_left
  111. 0111rewrite hprefix
  112. 0112refl