PA00DM

distinct_odd_prime_half_rectangle_total_exists

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

The nested row counts have a native beta-sum rectangle total.

Exact expanded PA statement

forall p q h k. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_rectangle_count_prime_p frp_prime_right_rectangle_count_prime_p. p = frp_prime_left_rectangle_count_prime_p * frp_prime_right_rectangle_count_prime_p -> frp_prime_left_rectangle_count_prime_p = 1 \/ frp_prime_right_rectangle_count_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_rectangle_count_prime_q frp_prime_right_rectangle_count_prime_q. q = frp_prime_left_rectangle_count_prime_q * frp_prime_right_rectangle_count_prime_q -> frp_prime_left_rectangle_count_prime_q = 1 \/ frp_prime_right_rectangle_count_prime_q = 1)) -> ~(p = q) -> (exists cb cc total. ((forall erc_row_rectangle_count_total_prefix. (exists erc_lt_gap_rectangle_count_total_prefix_bound. erc_lt_gap_rectangle_count_total_prefix_bound + S (erc_row_rectangle_count_total_prefix) = h) -> exists erc_count_rectangle_count_total_prefix. ((((exists ff_h_erc_rectangle_count_total_prefix_decoded. ff_h_erc_rectangle_count_total_prefix_decoded + S (erc_count_rectangle_count_total_prefix) = S ((S (erc_row_rectangle_count_total_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_total_prefix_decoded. cb = ff_q_erc_rectangle_count_total_prefix_decoded * S ((S (erc_row_rectangle_count_total_prefix)) * cc) + (erc_count_rectangle_count_total_prefix))) /\ (exists erc_row_code_rectangle_count_total_prefix_witness erc_row_scale_rectangle_count_total_prefix_witness. ((forall eri_column_erc_rectangle_count_total_prefix_witness_row. (exists eri_gap_erc_rectangle_count_total_prefix_witness_row_bound. eri_gap_erc_rectangle_count_total_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_total_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_total_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_total_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_total_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_total_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_total_prefix_witness_row)) * erc_row_scale_rectangle_count_total_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_total_prefix_witness_row_decoded. erc_row_code_rectangle_count_total_prefix_witness = ff_q_eri_erc_rectangle_count_total_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_total_prefix_witness_row)) * erc_row_scale_rectangle_count_total_prefix_witness) + (eri_bit_erc_rectangle_count_total_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_total_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_total_prefix) = p * S eri_column_erc_rectangle_count_total_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_total_prefix_witness_row) = q * S erc_row_rectangle_count_total_prefix))) \/ (eri_bit_erc_rectangle_count_total_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_total_prefix_witness_row) = q * S erc_row_rectangle_count_total_prefix) /\ ~(exists eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_total_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_total_prefix) = p * S eri_column_erc_rectangle_count_total_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_total_prefix_witness_count_sum ff_v_erc_rectangle_count_total_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_total_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (erc_count_rectangle_count_total_prefix))) /\ forall ff_i_erc_rectangle_count_total_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_total_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_total_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_total_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_total_prefix_witness_count_sum ff_r_erc_rectangle_count_total_prefix_witness_count_sum ff_s_erc_rectangle_count_total_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_total_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_total_prefix_witness)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_total_prefix_witness = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_total_prefix_witness) + (ff_a_erc_rectangle_count_total_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_total_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_total_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_total_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_total_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_total_prefix_witness_count_sum = ff_q_erc_rectangle_count_total_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_total_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_total_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_total_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_total_prefix_witness_count_sum = ff_r_erc_rectangle_count_total_prefix_witness_count_sum + ff_a_erc_rectangle_count_total_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_total_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_total_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_total_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_total_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_total_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_total_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_total_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_total_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_total_prefix_witness)) /\ exists ff_q_erc_rectangle_count_total_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_total_prefix_witness = ff_q_erc_rectangle_count_total_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_total_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_total_prefix_witness) + (ff_bit_erc_rectangle_count_total_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_total_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_total_prefix_witness_count_bits = 1))))))))) /\ (exists ff_u_rectangle_count_total_sum ff_v_rectangle_count_total_sum. ((((exists ff_h_rectangle_count_total_sum_start. ff_h_rectangle_count_total_sum_start + S (0) = S ((S (0)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_start. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_start * S ((S (0)) * ff_v_rectangle_count_total_sum) + (0))) /\ ((((exists ff_h_rectangle_count_total_sum_terminal. ff_h_rectangle_count_total_sum_terminal + S (total) = S ((S (h)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_terminal. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_terminal * S ((S (h)) * ff_v_rectangle_count_total_sum) + (total))) /\ forall ff_i_rectangle_count_total_sum. (exists ff_lt_rectangle_count_total_sum_bound. ff_lt_rectangle_count_total_sum_bound + S ff_i_rectangle_count_total_sum = h) -> exists ff_a_rectangle_count_total_sum ff_r_rectangle_count_total_sum ff_s_rectangle_count_total_sum. ((((exists ff_h_rectangle_count_total_sum_summand. ff_h_rectangle_count_total_sum_summand + S (ff_a_rectangle_count_total_sum) = S ((S (ff_i_rectangle_count_total_sum)) * cc)) /\ exists ff_q_rectangle_count_total_sum_summand. cb = ff_q_rectangle_count_total_sum_summand * S ((S (ff_i_rectangle_count_total_sum)) * cc) + (ff_a_rectangle_count_total_sum))) /\ ((((exists ff_h_rectangle_count_total_sum_partial. ff_h_rectangle_count_total_sum_partial + S (ff_r_rectangle_count_total_sum) = S ((S (ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_partial. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_partial * S ((S (ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum) + (ff_r_rectangle_count_total_sum))) /\ ((((exists ff_h_rectangle_count_total_sum_successor. ff_h_rectangle_count_total_sum_successor + S (ff_s_rectangle_count_total_sum) = S ((S (S ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum)) /\ exists ff_q_rectangle_count_total_sum_successor. ff_u_rectangle_count_total_sum = ff_q_rectangle_count_total_sum_successor * S ((S (S ff_i_rectangle_count_total_sum)) * ff_v_rectangle_count_total_sum) + (ff_s_rectangle_count_total_sum))) /\ ff_s_rectangle_count_total_sum = ff_r_rectangle_count_total_sum + ff_a_rectangle_count_total_sum))))))))

Structural proof guide

Generated structural guide

The nested row counts have a native beta-sum rectangle total.

Use the direct prerequisites distinct_odd_prime_half_row_count_prefix_exists, beta_sum_exists as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (2).

Referenced ingredients

PA00DL distinct_odd_prime_half_row_count_prefix_exists PA003H beta_sum_exists

Proof neighborhood

Direct dependencies

PA00DL distinct_odd_prime_half_row_count_prefix_exists PA003H beta_sum_exists

Direct dependents

PA00FG distinct_odd_primes_gauss_eisenstein_data_exists

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 h
  4. 0004intro k
  5. 0005intro hpodd
  6. 0006intro hqodd
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro hpq
  10. 0010have hprefix : exists cb cc. (forall erc_row_rectangle_count_full_prefix. (exists erc_lt_gap_rectangle_count_full_prefix_bound. erc_lt_gap_rectangle_count_full_prefix_bound + S (erc_row_rectangle_count_full_prefix) = h) -> exists erc_count_rectangle_count_full_prefix. ((((exists ff_h_erc_rectangle_count_full_prefix_decoded. ff_h_erc_rectangle_count_full_prefix_decoded + S (erc_count_rectangle_count_full_prefix) = S ((S (erc_row_rectangle_count_full_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_full_prefix_decoded. cb = ff_q_erc_rectangle_count_full_prefix_decoded * S ((S (erc_row_rectangle_count_full_prefix)) * cc) + (erc_count_rectangle_count_full_prefix))) /\ (exists erc_row_code_rectangle_count_full_prefix_witness erc_row_scale_rectangle_count_full_prefix_witness. ((forall eri_column_erc_rectangle_count_full_prefix_witness_row. (exists eri_gap_erc_rectangle_count_full_prefix_witness_row_bound. eri_gap_erc_rectangle_count_full_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_full_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_full_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_full_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_full_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_full_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_full_prefix_witness_row)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_full_prefix_witness_row_decoded. erc_row_code_rectangle_count_full_prefix_witness = ff_q_eri_erc_rectangle_count_full_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_full_prefix_witness_row)) * erc_row_scale_rectangle_count_full_prefix_witness) + (eri_bit_erc_rectangle_count_full_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_full_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_full_prefix) = p * S eri_column_erc_rectangle_count_full_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_full_prefix_witness_row) = q * S erc_row_rectangle_count_full_prefix))) \/ (eri_bit_erc_rectangle_count_full_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_full_prefix_witness_row) = q * S erc_row_rectangle_count_full_prefix) /\ ~(exists eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_full_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_full_prefix) = p * S eri_column_erc_rectangle_count_full_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_full_prefix_witness_count_sum ff_v_erc_rectangle_count_full_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_full_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (erc_count_rectangle_count_full_prefix))) /\ forall ff_i_erc_rectangle_count_full_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_full_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_full_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_full_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_full_prefix_witness_count_sum ff_r_erc_rectangle_count_full_prefix_witness_count_sum ff_s_erc_rectangle_count_full_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_full_prefix_witness = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_full_prefix_witness) + (ff_a_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_full_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_full_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_full_prefix_witness_count_sum = ff_q_erc_rectangle_count_full_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_full_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_full_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_full_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_full_prefix_witness_count_sum = ff_r_erc_rectangle_count_full_prefix_witness_count_sum + ff_a_erc_rectangle_count_full_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_full_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_full_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_full_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_full_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_full_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_full_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_full_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_full_prefix_witness)) /\ exists ff_q_erc_rectangle_count_full_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_full_prefix_witness = ff_q_erc_rectangle_count_full_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_full_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_full_prefix_witness) + (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_full_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_full_prefix_witness_count_bits = 1)))))))))
  11. 0011specialize distinct_odd_prime_half_row_count_prefix_exists p
  12. 0012specialize distinct_odd_prime_half_row_count_prefix_exists q
  13. 0013specialize distinct_odd_prime_half_row_count_prefix_exists h
  14. 0014specialize distinct_odd_prime_half_row_count_prefix_exists k
  15. 0015apply distinct_odd_prime_half_row_count_prefix_exists
  16. 0016exact hpodd
  17. 0017exact hqodd
  18. 0018exact hp
  19. 0019exact hq
  20. 0020exact hpq
  21. 0021cases hprefix
  22. 0022cases hprefix_witness
  23. 0023have hsum : exists total. (exists ff_u_rectangle_count_total_witness_sum ff_v_rectangle_count_total_witness_sum. ((((exists ff_h_rectangle_count_total_witness_sum_start. ff_h_rectangle_count_total_witness_sum_start + S (0) = S ((S (0)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_start. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_start * S ((S (0)) * ff_v_rectangle_count_total_witness_sum) + (0))) /\ ((((exists ff_h_rectangle_count_total_witness_sum_terminal. ff_h_rectangle_count_total_witness_sum_terminal + S (total) = S ((S (h)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_terminal. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_terminal * S ((S (h)) * ff_v_rectangle_count_total_witness_sum) + (total))) /\ forall ff_i_rectangle_count_total_witness_sum. (exists ff_lt_rectangle_count_total_witness_sum_bound. ff_lt_rectangle_count_total_witness_sum_bound + S ff_i_rectangle_count_total_witness_sum = h) -> exists ff_a_rectangle_count_total_witness_sum ff_r_rectangle_count_total_witness_sum ff_s_rectangle_count_total_witness_sum. ((((exists ff_h_rectangle_count_total_witness_sum_summand. ff_h_rectangle_count_total_witness_sum_summand + S (ff_a_rectangle_count_total_witness_sum) = S ((S (ff_i_rectangle_count_total_witness_sum)) * x1)) /\ exists ff_q_rectangle_count_total_witness_sum_summand. x = ff_q_rectangle_count_total_witness_sum_summand * S ((S (ff_i_rectangle_count_total_witness_sum)) * x1) + (ff_a_rectangle_count_total_witness_sum))) /\ ((((exists ff_h_rectangle_count_total_witness_sum_partial. ff_h_rectangle_count_total_witness_sum_partial + S (ff_r_rectangle_count_total_witness_sum) = S ((S (ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_partial. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_partial * S ((S (ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum) + (ff_r_rectangle_count_total_witness_sum))) /\ ((((exists ff_h_rectangle_count_total_witness_sum_successor. ff_h_rectangle_count_total_witness_sum_successor + S (ff_s_rectangle_count_total_witness_sum) = S ((S (S ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum)) /\ exists ff_q_rectangle_count_total_witness_sum_successor. ff_u_rectangle_count_total_witness_sum = ff_q_rectangle_count_total_witness_sum_successor * S ((S (S ff_i_rectangle_count_total_witness_sum)) * ff_v_rectangle_count_total_witness_sum) + (ff_s_rectangle_count_total_witness_sum))) /\ ff_s_rectangle_count_total_witness_sum = ff_r_rectangle_count_total_witness_sum + ff_a_rectangle_count_total_witness_sum))))))
  24. 0024specialize beta_sum_exists x
  25. 0025specialize beta_sum_exists x1
  26. 0026specialize beta_sum_exists h
  27. 0027exact beta_sum_exists
  28. 0028cases hsum
  29. 0029exists x
  30. 0030exists x1
  31. 0031exists x2
  32. 0032split
  33. 0033exact hprefix_witness_witness
  34. 0034exact hsum_witness