PA00ES

eisenstein_zero_width_rectangle_sum_zero

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

Every semantic zero-width rectangle has relational outer Sum zero.

Exact expanded PA statement

forall p q z bb bc l T. z = 0 -> (forall erc_row_fubini_zero_width_prefix. (exists erc_lt_gap_fubini_zero_width_prefix_bound. erc_lt_gap_fubini_zero_width_prefix_bound + S (erc_row_fubini_zero_width_prefix) = l) -> exists erc_count_fubini_zero_width_prefix. ((((exists ff_h_erc_fubini_zero_width_prefix_decoded. ff_h_erc_fubini_zero_width_prefix_decoded + S (erc_count_fubini_zero_width_prefix) = S ((S (erc_row_fubini_zero_width_prefix)) * bc)) /\ exists ff_q_erc_fubini_zero_width_prefix_decoded. bb = ff_q_erc_fubini_zero_width_prefix_decoded * S ((S (erc_row_fubini_zero_width_prefix)) * bc) + (erc_count_fubini_zero_width_prefix))) /\ (exists erc_row_code_fubini_zero_width_prefix_witness erc_row_scale_fubini_zero_width_prefix_witness. ((forall eri_column_erc_fubini_zero_width_prefix_witness_row. (exists eri_gap_erc_fubini_zero_width_prefix_witness_row_bound. eri_gap_erc_fubini_zero_width_prefix_witness_row_bound + S (eri_column_erc_fubini_zero_width_prefix_witness_row) = z) -> exists eri_bit_erc_fubini_zero_width_prefix_witness_row. ((((exists ff_h_eri_erc_fubini_zero_width_prefix_witness_row_decoded. ff_h_eri_erc_fubini_zero_width_prefix_witness_row_decoded + S (eri_bit_erc_fubini_zero_width_prefix_witness_row) = S ((S (eri_column_erc_fubini_zero_width_prefix_witness_row)) * erc_row_scale_fubini_zero_width_prefix_witness)) /\ exists ff_q_eri_erc_fubini_zero_width_prefix_witness_row_decoded. erc_row_code_fubini_zero_width_prefix_witness = ff_q_eri_erc_fubini_zero_width_prefix_witness_row_decoded * S ((S (eri_column_erc_fubini_zero_width_prefix_witness_row)) * erc_row_scale_fubini_zero_width_prefix_witness) + (eri_bit_erc_fubini_zero_width_prefix_witness_row))) /\ (((eri_bit_erc_fubini_zero_width_prefix_witness_row = 0 /\ ((exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left + S (q * S erc_row_fubini_zero_width_prefix) = p * S eri_column_erc_fubini_zero_width_prefix_witness_row) /\ ~(exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_prefix_witness_row) = q * S erc_row_fubini_zero_width_prefix))) \/ (eri_bit_erc_fubini_zero_width_prefix_witness_row = 1 /\ ((exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_prefix_witness_row) = q * S erc_row_fubini_zero_width_prefix) /\ ~(exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left + S (q * S erc_row_fubini_zero_width_prefix) = p * S eri_column_erc_fubini_zero_width_prefix_witness_row))))))) /\ (((exists ff_u_erc_fubini_zero_width_prefix_witness_count_sum ff_v_erc_fubini_zero_width_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_start. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_start. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_terminal. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_terminal + S (erc_count_fubini_zero_width_prefix) = S ((S (z)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_terminal. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_terminal * S ((S (z)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (erc_count_fubini_zero_width_prefix))) /\ forall ff_i_erc_fubini_zero_width_prefix_witness_count_sum. (exists ff_lt_erc_fubini_zero_width_prefix_witness_count_sum_bound. ff_lt_erc_fubini_zero_width_prefix_witness_count_sum_bound + S ff_i_erc_fubini_zero_width_prefix_witness_count_sum = z) -> exists ff_a_erc_fubini_zero_width_prefix_witness_count_sum ff_r_erc_fubini_zero_width_prefix_witness_count_sum ff_s_erc_fubini_zero_width_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_summand. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_summand + S (ff_a_erc_fubini_zero_width_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * erc_row_scale_fubini_zero_width_prefix_witness)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_summand. erc_row_code_fubini_zero_width_prefix_witness = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_summand * S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * erc_row_scale_fubini_zero_width_prefix_witness) + (ff_a_erc_fubini_zero_width_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_partial. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_partial + S (ff_r_erc_fubini_zero_width_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_partial. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_partial * S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (ff_r_erc_fubini_zero_width_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_successor. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_successor + S (ff_s_erc_fubini_zero_width_prefix_witness_count_sum) = S ((S (S ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_successor. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (ff_s_erc_fubini_zero_width_prefix_witness_count_sum))) /\ ff_s_erc_fubini_zero_width_prefix_witness_count_sum = ff_r_erc_fubini_zero_width_prefix_witness_count_sum + ff_a_erc_fubini_zero_width_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_zero_width_prefix_witness_count_bits. (exists ff_lt_erc_fubini_zero_width_prefix_witness_count_bits_bound. ff_lt_erc_fubini_zero_width_prefix_witness_count_bits_bound + S ff_i_erc_fubini_zero_width_prefix_witness_count_bits = z) -> exists ff_bit_erc_fubini_zero_width_prefix_witness_count_bits. ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_bits_decoded. ff_h_erc_fubini_zero_width_prefix_witness_count_bits_decoded + S (ff_bit_erc_fubini_zero_width_prefix_witness_count_bits) = S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_bits)) * erc_row_scale_fubini_zero_width_prefix_witness)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_bits_decoded. erc_row_code_fubini_zero_width_prefix_witness = ff_q_erc_fubini_zero_width_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_bits)) * erc_row_scale_fubini_zero_width_prefix_witness) + (ff_bit_erc_fubini_zero_width_prefix_witness_count_bits))) /\ (ff_bit_erc_fubini_zero_width_prefix_witness_count_bits = 0 \/ ff_bit_erc_fubini_zero_width_prefix_witness_count_bits = 1))))))))) -> (exists ff_u_fubini_zero_width_sum ff_v_fubini_zero_width_sum. ((((exists ff_h_fubini_zero_width_sum_start. ff_h_fubini_zero_width_sum_start + S (0) = S ((S (0)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_start. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_start * S ((S (0)) * ff_v_fubini_zero_width_sum) + (0))) /\ ((((exists ff_h_fubini_zero_width_sum_terminal. ff_h_fubini_zero_width_sum_terminal + S (T) = S ((S (l)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_terminal. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_terminal * S ((S (l)) * ff_v_fubini_zero_width_sum) + (T))) /\ forall ff_i_fubini_zero_width_sum. (exists ff_lt_fubini_zero_width_sum_bound. ff_lt_fubini_zero_width_sum_bound + S ff_i_fubini_zero_width_sum = l) -> exists ff_a_fubini_zero_width_sum ff_r_fubini_zero_width_sum ff_s_fubini_zero_width_sum. ((((exists ff_h_fubini_zero_width_sum_summand. ff_h_fubini_zero_width_sum_summand + S (ff_a_fubini_zero_width_sum) = S ((S (ff_i_fubini_zero_width_sum)) * bc)) /\ exists ff_q_fubini_zero_width_sum_summand. bb = ff_q_fubini_zero_width_sum_summand * S ((S (ff_i_fubini_zero_width_sum)) * bc) + (ff_a_fubini_zero_width_sum))) /\ ((((exists ff_h_fubini_zero_width_sum_partial. ff_h_fubini_zero_width_sum_partial + S (ff_r_fubini_zero_width_sum) = S ((S (ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_partial. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_partial * S ((S (ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum) + (ff_r_fubini_zero_width_sum))) /\ ((((exists ff_h_fubini_zero_width_sum_successor. ff_h_fubini_zero_width_sum_successor + S (ff_s_fubini_zero_width_sum) = S ((S (S ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_successor. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_successor * S ((S (S ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum) + (ff_s_fubini_zero_width_sum))) /\ ff_s_fubini_zero_width_sum = ff_r_fubini_zero_width_sum + ff_a_fubini_zero_width_sum)))))) -> T = 0

Structural proof guide

Generated structural guide

Every semantic zero-width rectangle has relational outer Sum zero.

Use the direct prerequisites beta_repeat_exists, eisenstein_rectangle_decoded_row_count, bit_count_zero, beta_sum_transport_prefix, beta_repeat_sum_exact, mul_comm, mul_zero_left as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (7), equality transport (5).

Referenced ingredients

PA0045 beta_repeat_exists PA00E6 eisenstein_rectangle_decoded_row_count PA0048 bit_count_zero PA00CT beta_sum_transport_prefix PA00EK beta_repeat_sum_exact PA000H mul_comm PA000D mul_zero_left

Proof neighborhood

Direct dependencies

PA0045 beta_repeat_exists PA00E6 eisenstein_rectangle_decoded_row_count PA0048 bit_count_zero PA00CT beta_sum_transport_prefix PA00EK beta_repeat_sum_exact PA000H mul_comm PA000D mul_zero_left

Direct dependents

PA00FC eisenstein_fubini_universal

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 p
  2. 0002intro q
  3. 0003intro z
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro l
  7. 0007intro T
  8. 0008intro hz
  9. 0009intro hprefix
  10. 0010intro hsum
  11. 0011have hrepeat : exists rb rc. (forall ff_i_fubini_zero_width_repeat. (exists ff_lt_fubini_zero_width_repeat_bound. ff_lt_fubini_zero_width_repeat_bound + S ff_i_fubini_zero_width_repeat = l) -> (((exists ff_h_fubini_zero_width_repeat_decoded. ff_h_fubini_zero_width_repeat_decoded + S (z) = S ((S (ff_i_fubini_zero_width_repeat)) * rc)) /\ exists ff_q_fubini_zero_width_repeat_decoded. rb = ff_q_fubini_zero_width_repeat_decoded * S ((S (ff_i_fubini_zero_width_repeat)) * rc) + (z))))
  12. 0012specialize beta_repeat_exists z
  13. 0013specialize beta_repeat_exists l
  14. 0014exact beta_repeat_exists
  15. 0015cases hrepeat
  16. 0016cases hrepeat_witness
  17. 0017have hpreserve : forall i n. (exists efrd_lt_gap_fubini_zero_width_preserve_bound. efrd_lt_gap_fubini_zero_width_preserve_bound + S (i) = l) -> (((exists ff_h_fubini_zero_width_preserve_source. ff_h_fubini_zero_width_preserve_source + S (n) = S ((S (i)) * bc)) /\ exists ff_q_fubini_zero_width_preserve_source. bb = ff_q_fubini_zero_width_preserve_source * S ((S (i)) * bc) + (n))) -> (((exists ff_h_fubini_zero_width_preserve_target. ff_h_fubini_zero_width_preserve_target + S (n) = S ((S (i)) * x1)) /\ exists ff_q_fubini_zero_width_preserve_target. x = ff_q_fubini_zero_width_preserve_target * S ((S (i)) * x1) + (n)))
  18. 0018intro i
  19. 0019intro n
  20. 0020intro hi
  21. 0021intro hn
  22. 0022have hwitness : exists erc_row_code_fubini_zero_width_decoded_witness erc_row_scale_fubini_zero_width_decoded_witness. ((forall eri_column_erc_fubini_zero_width_decoded_witness_row. (exists eri_gap_erc_fubini_zero_width_decoded_witness_row_bound. eri_gap_erc_fubini_zero_width_decoded_witness_row_bound + S (eri_column_erc_fubini_zero_width_decoded_witness_row) = z) -> exists eri_bit_erc_fubini_zero_width_decoded_witness_row. ((((exists ff_h_eri_erc_fubini_zero_width_decoded_witness_row_decoded. ff_h_eri_erc_fubini_zero_width_decoded_witness_row_decoded + S (eri_bit_erc_fubini_zero_width_decoded_witness_row) = S ((S (eri_column_erc_fubini_zero_width_decoded_witness_row)) * erc_row_scale_fubini_zero_width_decoded_witness)) /\ exists ff_q_eri_erc_fubini_zero_width_decoded_witness_row_decoded. erc_row_code_fubini_zero_width_decoded_witness = ff_q_eri_erc_fubini_zero_width_decoded_witness_row_decoded * S ((S (eri_column_erc_fubini_zero_width_decoded_witness_row)) * erc_row_scale_fubini_zero_width_decoded_witness) + (eri_bit_erc_fubini_zero_width_decoded_witness_row))) /\ (((eri_bit_erc_fubini_zero_width_decoded_witness_row = 0 /\ ((exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_zero_width_decoded_witness_row) /\ ~(exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_decoded_witness_row) = q * S i))) \/ (eri_bit_erc_fubini_zero_width_decoded_witness_row = 1 /\ ((exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_decoded_witness_row) = q * S i) /\ ~(exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_zero_width_decoded_witness_row))))))) /\ (((exists ff_u_erc_fubini_zero_width_decoded_witness_count_sum ff_v_erc_fubini_zero_width_decoded_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_start. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_start. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_terminal. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_terminal + S (n) = S ((S (z)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_terminal. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_terminal * S ((S (z)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (n))) /\ forall ff_i_erc_fubini_zero_width_decoded_witness_count_sum. (exists ff_lt_erc_fubini_zero_width_decoded_witness_count_sum_bound. ff_lt_erc_fubini_zero_width_decoded_witness_count_sum_bound + S ff_i_erc_fubini_zero_width_decoded_witness_count_sum = z) -> exists ff_a_erc_fubini_zero_width_decoded_witness_count_sum ff_r_erc_fubini_zero_width_decoded_witness_count_sum ff_s_erc_fubini_zero_width_decoded_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_summand. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_summand + S (ff_a_erc_fubini_zero_width_decoded_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * erc_row_scale_fubini_zero_width_decoded_witness)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_summand. erc_row_code_fubini_zero_width_decoded_witness = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_summand * S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * erc_row_scale_fubini_zero_width_decoded_witness) + (ff_a_erc_fubini_zero_width_decoded_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_partial. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_partial + S (ff_r_erc_fubini_zero_width_decoded_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_partial. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_partial * S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (ff_r_erc_fubini_zero_width_decoded_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_successor. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_successor + S (ff_s_erc_fubini_zero_width_decoded_witness_count_sum) = S ((S (S ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_successor. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (ff_s_erc_fubini_zero_width_decoded_witness_count_sum))) /\ ff_s_erc_fubini_zero_width_decoded_witness_count_sum = ff_r_erc_fubini_zero_width_decoded_witness_count_sum + ff_a_erc_fubini_zero_width_decoded_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_zero_width_decoded_witness_count_bits. (exists ff_lt_erc_fubini_zero_width_decoded_witness_count_bits_bound. ff_lt_erc_fubini_zero_width_decoded_witness_count_bits_bound + S ff_i_erc_fubini_zero_width_decoded_witness_count_bits = z) -> exists ff_bit_erc_fubini_zero_width_decoded_witness_count_bits. ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_bits_decoded. ff_h_erc_fubini_zero_width_decoded_witness_count_bits_decoded + S (ff_bit_erc_fubini_zero_width_decoded_witness_count_bits) = S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_bits)) * erc_row_scale_fubini_zero_width_decoded_witness)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_bits_decoded. erc_row_code_fubini_zero_width_decoded_witness = ff_q_erc_fubini_zero_width_decoded_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_bits)) * erc_row_scale_fubini_zero_width_decoded_witness) + (ff_bit_erc_fubini_zero_width_decoded_witness_count_bits))) /\ (ff_bit_erc_fubini_zero_width_decoded_witness_count_bits = 0 \/ ff_bit_erc_fubini_zero_width_decoded_witness_count_bits = 1))))))
  23. 0023specialize eisenstein_rectangle_decoded_row_count p
  24. 0024specialize eisenstein_rectangle_decoded_row_count q
  25. 0025specialize eisenstein_rectangle_decoded_row_count z
  26. 0026specialize eisenstein_rectangle_decoded_row_count bb
  27. 0027specialize eisenstein_rectangle_decoded_row_count bc
  28. 0028specialize eisenstein_rectangle_decoded_row_count l
  29. 0029specialize eisenstein_rectangle_decoded_row_count i
  30. 0030specialize eisenstein_rectangle_decoded_row_count n
  31. 0031apply eisenstein_rectangle_decoded_row_count
  32. 0032exact hprefix
  33. 0033exact hi
  34. 0034exact hn
  35. 0035cases hwitness
  36. 0036cases hwitness_witness
  37. 0037cases hwitness_witness_witness
  38. 0038have hnzero : n = 0
  39. 0039specialize bit_count_zero x2
  40. 0040specialize bit_count_zero x3
  41. 0041specialize bit_count_zero z
  42. 0042specialize bit_count_zero n
  43. 0043apply bit_count_zero
  44. 0044exact hz
  45. 0045exact hwitness_witness_witness_right
  46. 0046have hzero_entry : ((exists ff_h_fubini_zero_width_repeat_entry. ff_h_fubini_zero_width_repeat_entry + S (z) = S ((S (i)) * x1)) /\ exists ff_q_fubini_zero_width_repeat_entry. x = ff_q_fubini_zero_width_repeat_entry * S ((S (i)) * x1) + (z))
  47. 0047specialize hrepeat_witness_witness i
  48. 0048apply hrepeat_witness_witness
  49. 0049exact hi
  50. 0050rewrite hz at hzero_entry
  51. 0051rewrite hz at hzero_entry
  52. 0052rewrite hnzero
  53. 0053rewrite hnzero
  54. 0054exact hzero_entry
  55. 0055have hrepeat_sum : exists ff_u_fubini_zero_width_transport_sum ff_v_fubini_zero_width_transport_sum. ((((exists ff_h_fubini_zero_width_transport_sum_start. ff_h_fubini_zero_width_transport_sum_start + S (0) = S ((S (0)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_start. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_start * S ((S (0)) * ff_v_fubini_zero_width_transport_sum) + (0))) /\ ((((exists ff_h_fubini_zero_width_transport_sum_terminal. ff_h_fubini_zero_width_transport_sum_terminal + S (T) = S ((S (l)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_terminal. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_terminal * S ((S (l)) * ff_v_fubini_zero_width_transport_sum) + (T))) /\ forall ff_i_fubini_zero_width_transport_sum. (exists ff_lt_fubini_zero_width_transport_sum_bound. ff_lt_fubini_zero_width_transport_sum_bound + S ff_i_fubini_zero_width_transport_sum = l) -> exists ff_a_fubini_zero_width_transport_sum ff_r_fubini_zero_width_transport_sum ff_s_fubini_zero_width_transport_sum. ((((exists ff_h_fubini_zero_width_transport_sum_summand. ff_h_fubini_zero_width_transport_sum_summand + S (ff_a_fubini_zero_width_transport_sum) = S ((S (ff_i_fubini_zero_width_transport_sum)) * x1)) /\ exists ff_q_fubini_zero_width_transport_sum_summand. x = ff_q_fubini_zero_width_transport_sum_summand * S ((S (ff_i_fubini_zero_width_transport_sum)) * x1) + (ff_a_fubini_zero_width_transport_sum))) /\ ((((exists ff_h_fubini_zero_width_transport_sum_partial. ff_h_fubini_zero_width_transport_sum_partial + S (ff_r_fubini_zero_width_transport_sum) = S ((S (ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_partial. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_partial * S ((S (ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum) + (ff_r_fubini_zero_width_transport_sum))) /\ ((((exists ff_h_fubini_zero_width_transport_sum_successor. ff_h_fubini_zero_width_transport_sum_successor + S (ff_s_fubini_zero_width_transport_sum) = S ((S (S ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_successor. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_successor * S ((S (S ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum) + (ff_s_fubini_zero_width_transport_sum))) /\ ff_s_fubini_zero_width_transport_sum = ff_r_fubini_zero_width_transport_sum + ff_a_fubini_zero_width_transport_sum)))))
  56. 0056specialize beta_sum_transport_prefix bb
  57. 0057specialize beta_sum_transport_prefix bc
  58. 0058specialize beta_sum_transport_prefix x
  59. 0059specialize beta_sum_transport_prefix x1
  60. 0060specialize beta_sum_transport_prefix l
  61. 0061specialize beta_sum_transport_prefix T
  62. 0062apply beta_sum_transport_prefix
  63. 0063exact hsum
  64. 0064exact hpreserve
  65. 0065have hproduct : T = l * z
  66. 0066specialize beta_repeat_sum_exact x
  67. 0067specialize beta_repeat_sum_exact x1
  68. 0068specialize beta_repeat_sum_exact z
  69. 0069specialize beta_repeat_sum_exact l
  70. 0070specialize beta_repeat_sum_exact T
  71. 0071apply beta_repeat_sum_exact
  72. 0072exact hrepeat_witness_witness
  73. 0073exact hrepeat_sum
  74. 0074rewrite hz at hproduct
  75. 0075trans l * 0
  76. 0076exact hproduct
  77. 0077trans 0 * l
  78. 0078specialize mul_comm l
  79. 0079specialize mul_comm 0
  80. 0080exact mul_comm
  81. 0081specialize mul_zero_left l
  82. 0082exact mul_zero_left