PA00DJ

eisenstein_rectangle_row_count_prefix_exists

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

Every finite family of semantic row counts has an outer beta prefix.

Exact expanded PA statement

forall p q k l. (forall erc_row_rectangle_count_exists_all. (exists erc_lt_gap_rectangle_count_exists_all_bound. erc_lt_gap_rectangle_count_exists_all_bound + S (erc_row_rectangle_count_exists_all) = l) -> exists erc_count_rectangle_count_exists_all. (exists erc_row_code_rectangle_count_exists_all_witness erc_row_scale_rectangle_count_exists_all_witness. ((forall eri_column_erc_rectangle_count_exists_all_witness_row. (exists eri_gap_erc_rectangle_count_exists_all_witness_row_bound. eri_gap_erc_rectangle_count_exists_all_witness_row_bound + S (eri_column_erc_rectangle_count_exists_all_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_all_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_all_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_all_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_all_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_all_witness_row)) * erc_row_scale_rectangle_count_exists_all_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_all_witness_row_decoded. erc_row_code_rectangle_count_exists_all_witness = ff_q_eri_erc_rectangle_count_exists_all_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_all_witness_row)) * erc_row_scale_rectangle_count_exists_all_witness) + (eri_bit_erc_rectangle_count_exists_all_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_all_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_all) = p * S eri_column_erc_rectangle_count_exists_all_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_all_witness_row) = q * S erc_row_rectangle_count_exists_all))) \/ (eri_bit_erc_rectangle_count_exists_all_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_all_witness_row) = q * S erc_row_rectangle_count_exists_all) /\ ~(exists eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_all_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_all) = p * S eri_column_erc_rectangle_count_exists_all_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_all_witness_count_sum ff_v_erc_rectangle_count_exists_all_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_start. ff_h_erc_rectangle_count_exists_all_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_start. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_all_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_all) = S ((S (k)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (erc_count_rectangle_count_exists_all))) /\ forall ff_i_erc_rectangle_count_exists_all_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_all_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_all_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_all_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_all_witness_count_sum ff_r_erc_rectangle_count_exists_all_witness_count_sum ff_s_erc_rectangle_count_exists_all_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_all_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_all_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * erc_row_scale_rectangle_count_exists_all_witness)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_summand. erc_row_code_rectangle_count_exists_all_witness = ff_q_erc_rectangle_count_exists_all_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * erc_row_scale_rectangle_count_exists_all_witness) + (ff_a_erc_rectangle_count_exists_all_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_all_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_all_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (ff_r_erc_rectangle_count_exists_all_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_all_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_all_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_all_witness_count_sum = ff_q_erc_rectangle_count_exists_all_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_all_witness_count_sum)) * ff_v_erc_rectangle_count_exists_all_witness_count_sum) + (ff_s_erc_rectangle_count_exists_all_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_all_witness_count_sum = ff_r_erc_rectangle_count_exists_all_witness_count_sum + ff_a_erc_rectangle_count_exists_all_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_all_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_all_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_all_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_all_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_all_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_all_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_all_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_all_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_bits)) * erc_row_scale_rectangle_count_exists_all_witness)) /\ exists ff_q_erc_rectangle_count_exists_all_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_all_witness = ff_q_erc_rectangle_count_exists_all_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_all_witness_count_bits)) * erc_row_scale_rectangle_count_exists_all_witness) + (ff_bit_erc_rectangle_count_exists_all_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_all_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_all_witness_count_bits = 1)))))))) -> (exists cb cc. (forall erc_row_rectangle_count_exists_result. (exists erc_lt_gap_rectangle_count_exists_result_bound. erc_lt_gap_rectangle_count_exists_result_bound + S (erc_row_rectangle_count_exists_result) = l) -> exists erc_count_rectangle_count_exists_result. ((((exists ff_h_erc_rectangle_count_exists_result_decoded. ff_h_erc_rectangle_count_exists_result_decoded + S (erc_count_rectangle_count_exists_result) = S ((S (erc_row_rectangle_count_exists_result)) * cc)) /\ exists ff_q_erc_rectangle_count_exists_result_decoded. cb = ff_q_erc_rectangle_count_exists_result_decoded * S ((S (erc_row_rectangle_count_exists_result)) * cc) + (erc_count_rectangle_count_exists_result))) /\ (exists erc_row_code_rectangle_count_exists_result_witness erc_row_scale_rectangle_count_exists_result_witness. ((forall eri_column_erc_rectangle_count_exists_result_witness_row. (exists eri_gap_erc_rectangle_count_exists_result_witness_row_bound. eri_gap_erc_rectangle_count_exists_result_witness_row_bound + S (eri_column_erc_rectangle_count_exists_result_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_result_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_result_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_result_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_result_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_result_witness_row)) * erc_row_scale_rectangle_count_exists_result_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_result_witness_row_decoded. erc_row_code_rectangle_count_exists_result_witness = ff_q_eri_erc_rectangle_count_exists_result_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_result_witness_row)) * erc_row_scale_rectangle_count_exists_result_witness) + (eri_bit_erc_rectangle_count_exists_result_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_result_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_result) = p * S eri_column_erc_rectangle_count_exists_result_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_result_witness_row) = q * S erc_row_rectangle_count_exists_result))) \/ (eri_bit_erc_rectangle_count_exists_result_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_result_witness_row) = q * S erc_row_rectangle_count_exists_result) /\ ~(exists eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_result_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_result) = p * S eri_column_erc_rectangle_count_exists_result_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_result_witness_count_sum ff_v_erc_rectangle_count_exists_result_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_start. ff_h_erc_rectangle_count_exists_result_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_start. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_result_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_result) = S ((S (k)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (erc_count_rectangle_count_exists_result))) /\ forall ff_i_erc_rectangle_count_exists_result_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_result_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_result_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_result_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_result_witness_count_sum ff_r_erc_rectangle_count_exists_result_witness_count_sum ff_s_erc_rectangle_count_exists_result_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_result_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_result_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * erc_row_scale_rectangle_count_exists_result_witness)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_summand. erc_row_code_rectangle_count_exists_result_witness = ff_q_erc_rectangle_count_exists_result_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * erc_row_scale_rectangle_count_exists_result_witness) + (ff_a_erc_rectangle_count_exists_result_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_result_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_result_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (ff_r_erc_rectangle_count_exists_result_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_result_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_result_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_result_witness_count_sum = ff_q_erc_rectangle_count_exists_result_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_result_witness_count_sum)) * ff_v_erc_rectangle_count_exists_result_witness_count_sum) + (ff_s_erc_rectangle_count_exists_result_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_result_witness_count_sum = ff_r_erc_rectangle_count_exists_result_witness_count_sum + ff_a_erc_rectangle_count_exists_result_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_result_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_result_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_result_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_result_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_result_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_result_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_result_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_result_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_bits)) * erc_row_scale_rectangle_count_exists_result_witness)) /\ exists ff_q_erc_rectangle_count_exists_result_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_result_witness = ff_q_erc_rectangle_count_exists_result_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_result_witness_count_bits)) * erc_row_scale_rectangle_count_exists_result_witness) + (ff_bit_erc_rectangle_count_exists_result_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_result_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_result_witness_count_bits = 1))))))))))

Structural proof guide

Generated structural guide

Every finite family of semantic row counts has an outer beta prefix.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, le_succ, le_refl, eisenstein_rectangle_row_count_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (3), intermediate claims (5).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00DI eisenstein_rectangle_row_count_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00DI eisenstein_rectangle_row_count_prefix_extend

Direct dependents

PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded

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 k
  4. 0004induction l
  5. 0005intro hchoices
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro hi
  10. 0010exfalso
  11. 0011cases hi
  12. 0012have hsi : S i = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S i)
  15. 0015apply add_eq_zero_right
  16. 0016exact hi_witness
  17. 0017specialize succ_ne_zero i
  18. 0018apply succ_ne_zero
  19. 0019exact hsi
  20. 0020intro hchoices
  21. 0021have hprevious_choices : forall erc_row_rectangle_count_exists_previous_choices. (exists erc_lt_gap_rectangle_count_exists_previous_choices_bound. erc_lt_gap_rectangle_count_exists_previous_choices_bound + S (erc_row_rectangle_count_exists_previous_choices) = l) -> exists erc_count_rectangle_count_exists_previous_choices. (exists erc_row_code_rectangle_count_exists_previous_choices_witness erc_row_scale_rectangle_count_exists_previous_choices_witness. ((forall eri_column_erc_rectangle_count_exists_previous_choices_witness_row. (exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_bound. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_bound + S (eri_column_erc_rectangle_count_exists_previous_choices_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_previous_choices_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_previous_choices_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_previous_choices_witness_row)) * erc_row_scale_rectangle_count_exists_previous_choices_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded. erc_row_code_rectangle_count_exists_previous_choices_witness = ff_q_eri_erc_rectangle_count_exists_previous_choices_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_previous_choices_witness_row)) * erc_row_scale_rectangle_count_exists_previous_choices_witness) + (eri_bit_erc_rectangle_count_exists_previous_choices_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_previous_choices_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_choices) = p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row) = q * S erc_row_rectangle_count_exists_previous_choices))) \/ (eri_bit_erc_rectangle_count_exists_previous_choices_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row) = q * S erc_row_rectangle_count_exists_previous_choices) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_choices) = p * S eri_column_erc_rectangle_count_exists_previous_choices_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_start. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_start. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_previous_choices) = S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (erc_count_rectangle_count_exists_previous_choices))) /\ forall ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_choices_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand. erc_row_code_rectangle_count_exists_previous_choices_witness = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_choices_witness) + (ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_choices_witness_count_sum) + (ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_previous_choices_witness_count_sum = ff_r_erc_rectangle_count_exists_previous_choices_witness_count_sum + ff_a_erc_rectangle_count_exists_previous_choices_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_previous_choices_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_choices_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_previous_choices_witness = ff_q_erc_rectangle_count_exists_previous_choices_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_previous_choices_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_choices_witness) + (ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_previous_choices_witness_count_bits = 1)))))))
  22. 0022intro i
  23. 0023intro hi
  24. 0024specialize hchoices i
  25. 0025apply hchoices
  26. 0026specialize le_succ (S i)
  27. 0027specialize le_succ l
  28. 0028apply le_succ
  29. 0029exact hi
  30. 0030have hprevious : exists cb cc. (forall erc_row_rectangle_count_exists_previous_prefix. (exists erc_lt_gap_rectangle_count_exists_previous_prefix_bound. erc_lt_gap_rectangle_count_exists_previous_prefix_bound + S (erc_row_rectangle_count_exists_previous_prefix) = l) -> exists erc_count_rectangle_count_exists_previous_prefix. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_decoded. ff_h_erc_rectangle_count_exists_previous_prefix_decoded + S (erc_count_rectangle_count_exists_previous_prefix) = S ((S (erc_row_rectangle_count_exists_previous_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_decoded. cb = ff_q_erc_rectangle_count_exists_previous_prefix_decoded * S ((S (erc_row_rectangle_count_exists_previous_prefix)) * cc) + (erc_count_rectangle_count_exists_previous_prefix))) /\ (exists erc_row_code_rectangle_count_exists_previous_prefix_witness erc_row_scale_rectangle_count_exists_previous_prefix_witness. ((forall eri_column_erc_rectangle_count_exists_previous_prefix_witness_row. (exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_bound. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_previous_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded. erc_row_code_rectangle_count_exists_previous_prefix_witness = ff_q_eri_erc_rectangle_count_exists_previous_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_previous_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness) + (eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_prefix) = p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) = q * S erc_row_rectangle_count_exists_previous_prefix))) \/ (eri_bit_erc_rectangle_count_exists_previous_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row) = q * S erc_row_rectangle_count_exists_previous_prefix) /\ ~(exists eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_previous_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_previous_prefix) = p * S eri_column_erc_rectangle_count_exists_previous_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_previous_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (erc_count_rectangle_count_exists_previous_prefix))) /\ forall ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_exists_previous_prefix_witness = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness) + (ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_previous_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_previous_prefix_witness_count_sum = ff_r_erc_rectangle_count_exists_previous_prefix_witness_count_sum + ff_a_erc_rectangle_count_exists_previous_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_previous_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_previous_prefix_witness = ff_q_erc_rectangle_count_exists_previous_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_previous_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_previous_prefix_witness) + (ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_previous_prefix_witness_count_bits = 1)))))))))
  31. 0031apply IH
  32. 0032exact hprevious_choices
  33. 0033cases hprevious
  34. 0034cases hprevious_witness
  35. 0035have hlast : exists n. (exists erc_row_code_rectangle_count_exists_last erc_row_scale_rectangle_count_exists_last. ((forall eri_column_erc_rectangle_count_exists_last_row. (exists eri_gap_erc_rectangle_count_exists_last_row_bound. eri_gap_erc_rectangle_count_exists_last_row_bound + S (eri_column_erc_rectangle_count_exists_last_row) = k) -> exists eri_bit_erc_rectangle_count_exists_last_row. ((((exists ff_h_eri_erc_rectangle_count_exists_last_row_decoded. ff_h_eri_erc_rectangle_count_exists_last_row_decoded + S (eri_bit_erc_rectangle_count_exists_last_row) = S ((S (eri_column_erc_rectangle_count_exists_last_row)) * erc_row_scale_rectangle_count_exists_last)) /\ exists ff_q_eri_erc_rectangle_count_exists_last_row_decoded. erc_row_code_rectangle_count_exists_last = ff_q_eri_erc_rectangle_count_exists_last_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_last_row)) * erc_row_scale_rectangle_count_exists_last) + (eri_bit_erc_rectangle_count_exists_last_row))) /\ (((eri_bit_erc_rectangle_count_exists_last_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_last_row_choice_left. eri_gap_erc_rectangle_count_exists_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_exists_last_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_last_row_choice_right. eri_gap_erc_rectangle_count_exists_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_last_row) = q * S l))) \/ (eri_bit_erc_rectangle_count_exists_last_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_last_row_choice_right. eri_gap_erc_rectangle_count_exists_last_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_last_row) = q * S l) /\ ~(exists eri_gap_erc_rectangle_count_exists_last_row_choice_left. eri_gap_erc_rectangle_count_exists_last_row_choice_left + S (q * S l) = p * S eri_column_erc_rectangle_count_exists_last_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_last_count_sum ff_v_erc_rectangle_count_exists_last_count_sum. ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_start. ff_h_erc_rectangle_count_exists_last_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_start. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_terminal. ff_h_erc_rectangle_count_exists_last_count_sum_terminal + S (n) = S ((S (k)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_terminal. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (n))) /\ forall ff_i_erc_rectangle_count_exists_last_count_sum. (exists ff_lt_erc_rectangle_count_exists_last_count_sum_bound. ff_lt_erc_rectangle_count_exists_last_count_sum_bound + S ff_i_erc_rectangle_count_exists_last_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_last_count_sum ff_r_erc_rectangle_count_exists_last_count_sum ff_s_erc_rectangle_count_exists_last_count_sum. ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_summand. ff_h_erc_rectangle_count_exists_last_count_sum_summand + S (ff_a_erc_rectangle_count_exists_last_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * erc_row_scale_rectangle_count_exists_last)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_summand. erc_row_code_rectangle_count_exists_last = ff_q_erc_rectangle_count_exists_last_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * erc_row_scale_rectangle_count_exists_last) + (ff_a_erc_rectangle_count_exists_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_partial. ff_h_erc_rectangle_count_exists_last_count_sum_partial + S (ff_r_erc_rectangle_count_exists_last_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_partial. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (ff_r_erc_rectangle_count_exists_last_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_last_count_sum_successor. ff_h_erc_rectangle_count_exists_last_count_sum_successor + S (ff_s_erc_rectangle_count_exists_last_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_last_count_sum_successor. ff_u_erc_rectangle_count_exists_last_count_sum = ff_q_erc_rectangle_count_exists_last_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_last_count_sum)) * ff_v_erc_rectangle_count_exists_last_count_sum) + (ff_s_erc_rectangle_count_exists_last_count_sum))) /\ ff_s_erc_rectangle_count_exists_last_count_sum = ff_r_erc_rectangle_count_exists_last_count_sum + ff_a_erc_rectangle_count_exists_last_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_last_count_bits. (exists ff_lt_erc_rectangle_count_exists_last_count_bits_bound. ff_lt_erc_rectangle_count_exists_last_count_bits_bound + S ff_i_erc_rectangle_count_exists_last_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_last_count_bits. ((((exists ff_h_erc_rectangle_count_exists_last_count_bits_decoded. ff_h_erc_rectangle_count_exists_last_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_last_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_last_count_bits)) * erc_row_scale_rectangle_count_exists_last)) /\ exists ff_q_erc_rectangle_count_exists_last_count_bits_decoded. erc_row_code_rectangle_count_exists_last = ff_q_erc_rectangle_count_exists_last_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_last_count_bits)) * erc_row_scale_rectangle_count_exists_last) + (ff_bit_erc_rectangle_count_exists_last_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_last_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_last_count_bits = 1)))))))
  36. 0036specialize hchoices l
  37. 0037apply hchoices
  38. 0038specialize le_refl (S l)
  39. 0039exact le_refl
  40. 0040have hnext : exists cb cc. (forall erc_row_rectangle_count_exists_successor_prefix. (exists erc_lt_gap_rectangle_count_exists_successor_prefix_bound. erc_lt_gap_rectangle_count_exists_successor_prefix_bound + S (erc_row_rectangle_count_exists_successor_prefix) = S l) -> exists erc_count_rectangle_count_exists_successor_prefix. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_decoded. ff_h_erc_rectangle_count_exists_successor_prefix_decoded + S (erc_count_rectangle_count_exists_successor_prefix) = S ((S (erc_row_rectangle_count_exists_successor_prefix)) * cc)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_decoded. cb = ff_q_erc_rectangle_count_exists_successor_prefix_decoded * S ((S (erc_row_rectangle_count_exists_successor_prefix)) * cc) + (erc_count_rectangle_count_exists_successor_prefix))) /\ (exists erc_row_code_rectangle_count_exists_successor_prefix_witness erc_row_scale_rectangle_count_exists_successor_prefix_witness. ((forall eri_column_erc_rectangle_count_exists_successor_prefix_witness_row. (exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_bound. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_bound + S (eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) = k) -> exists eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row. ((((exists ff_h_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded. ff_h_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded + S (eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row) = S ((S (eri_column_erc_rectangle_count_exists_successor_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness)) /\ exists ff_q_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded. erc_row_code_rectangle_count_exists_successor_prefix_witness = ff_q_eri_erc_rectangle_count_exists_successor_prefix_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_exists_successor_prefix_witness_row)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness) + (eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row))) /\ (((eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_successor_prefix) = p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) = q * S erc_row_rectangle_count_exists_successor_prefix))) \/ (eri_bit_erc_rectangle_count_exists_successor_prefix_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row) = q * S erc_row_rectangle_count_exists_successor_prefix) /\ ~(exists eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left. eri_gap_erc_rectangle_count_exists_successor_prefix_witness_row_choice_left + S (q * S erc_row_rectangle_count_exists_successor_prefix) = p * S eri_column_erc_rectangle_count_exists_successor_prefix_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal + S (erc_count_rectangle_count_exists_successor_prefix) = S ((S (k)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (erc_count_rectangle_count_exists_successor_prefix))) /\ forall ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum. (exists ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_sum_bound. ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_sum_bound + S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand + S (ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand. erc_row_code_rectangle_count_exists_successor_prefix_witness = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness) + (ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial + S (ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor + S (ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor. ff_u_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_sum)) * ff_v_erc_rectangle_count_exists_successor_prefix_witness_count_sum) + (ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum))) /\ ff_s_erc_rectangle_count_exists_successor_prefix_witness_count_sum = ff_r_erc_rectangle_count_exists_successor_prefix_witness_count_sum + ff_a_erc_rectangle_count_exists_successor_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits. (exists ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_bits_bound. ff_lt_erc_rectangle_count_exists_successor_prefix_witness_count_bits_bound + S ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits. ((((exists ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded. ff_h_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness)) /\ exists ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded. erc_row_code_rectangle_count_exists_successor_prefix_witness = ff_q_erc_rectangle_count_exists_successor_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_exists_successor_prefix_witness_count_bits)) * erc_row_scale_rectangle_count_exists_successor_prefix_witness) + (ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_exists_successor_prefix_witness_count_bits = 1)))))))))
  41. 0041specialize eisenstein_rectangle_row_count_prefix_extend p
  42. 0042specialize eisenstein_rectangle_row_count_prefix_extend q
  43. 0043specialize eisenstein_rectangle_row_count_prefix_extend k
  44. 0044specialize eisenstein_rectangle_row_count_prefix_extend x
  45. 0045specialize eisenstein_rectangle_row_count_prefix_extend x1
  46. 0046specialize eisenstein_rectangle_row_count_prefix_extend l
  47. 0047apply eisenstein_rectangle_row_count_prefix_extend
  48. 0048exact hprevious_witness_witness
  49. 0049exact hlast
  50. 0050exact hnext