PA00FE

eisenstein_rectangle_floor_sum_identity

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

The two semantic Eisenstein row totals add exactly to the rectangle area.

Exact expanded PA statement

forall p q h k ab ac bb bc N T. (forall erc_row_fubini_total_identity_first_outer. (exists erc_lt_gap_fubini_total_identity_first_outer_bound. erc_lt_gap_fubini_total_identity_first_outer_bound + S (erc_row_fubini_total_identity_first_outer) = h) -> exists erc_count_fubini_total_identity_first_outer. ((((exists ff_h_erc_fubini_total_identity_first_outer_decoded. ff_h_erc_fubini_total_identity_first_outer_decoded + S (erc_count_fubini_total_identity_first_outer) = S ((S (erc_row_fubini_total_identity_first_outer)) * ac)) /\ exists ff_q_erc_fubini_total_identity_first_outer_decoded. ab = ff_q_erc_fubini_total_identity_first_outer_decoded * S ((S (erc_row_fubini_total_identity_first_outer)) * ac) + (erc_count_fubini_total_identity_first_outer))) /\ (exists erc_row_code_fubini_total_identity_first_outer_witness erc_row_scale_fubini_total_identity_first_outer_witness. ((forall eri_column_erc_fubini_total_identity_first_outer_witness_row. (exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_bound. eri_gap_erc_fubini_total_identity_first_outer_witness_row_bound + S (eri_column_erc_fubini_total_identity_first_outer_witness_row) = k) -> exists eri_bit_erc_fubini_total_identity_first_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_identity_first_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_identity_first_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_identity_first_outer_witness_row) = S ((S (eri_column_erc_fubini_total_identity_first_outer_witness_row)) * erc_row_scale_fubini_total_identity_first_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_identity_first_outer_witness_row_decoded. erc_row_code_fubini_total_identity_first_outer_witness = ff_q_eri_erc_fubini_total_identity_first_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_identity_first_outer_witness_row)) * erc_row_scale_fubini_total_identity_first_outer_witness) + (eri_bit_erc_fubini_total_identity_first_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_identity_first_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left + S (q * S erc_row_fubini_total_identity_first_outer) = p * S eri_column_erc_fubini_total_identity_first_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right + S (p * S eri_column_erc_fubini_total_identity_first_outer_witness_row) = q * S erc_row_fubini_total_identity_first_outer))) \/ (eri_bit_erc_fubini_total_identity_first_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_right + S (p * S eri_column_erc_fubini_total_identity_first_outer_witness_row) = q * S erc_row_fubini_total_identity_first_outer) /\ ~(exists eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_first_outer_witness_row_choice_left + S (q * S erc_row_fubini_total_identity_first_outer) = p * S eri_column_erc_fubini_total_identity_first_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_identity_first_outer_witness_count_sum ff_v_erc_fubini_total_identity_first_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_start. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_start. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_terminal + S (erc_count_fubini_total_identity_first_outer) = S ((S (k)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (erc_count_fubini_total_identity_first_outer))) /\ forall ff_i_erc_fubini_total_identity_first_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_identity_first_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_identity_first_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_identity_first_outer_witness_count_sum = k) -> exists ff_a_erc_fubini_total_identity_first_outer_witness_count_sum ff_r_erc_fubini_total_identity_first_outer_witness_count_sum ff_s_erc_fubini_total_identity_first_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_summand. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_identity_first_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_first_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_summand. erc_row_code_fubini_total_identity_first_outer_witness = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_first_outer_witness) + (ff_a_erc_fubini_total_identity_first_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_partial. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_identity_first_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_partial. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (ff_r_erc_fubini_total_identity_first_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_successor. ff_h_erc_fubini_total_identity_first_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_identity_first_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_successor. ff_u_erc_fubini_total_identity_first_outer_witness_count_sum = ff_q_erc_fubini_total_identity_first_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_identity_first_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_first_outer_witness_count_sum) + (ff_s_erc_fubini_total_identity_first_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_identity_first_outer_witness_count_sum = ff_r_erc_fubini_total_identity_first_outer_witness_count_sum + ff_a_erc_fubini_total_identity_first_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_identity_first_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_identity_first_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_identity_first_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_identity_first_outer_witness_count_bits = k) -> exists ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_identity_first_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_identity_first_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_first_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_first_outer_witness_count_bits_decoded. erc_row_code_fubini_total_identity_first_outer_witness = ff_q_erc_fubini_total_identity_first_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_identity_first_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_first_outer_witness) + (ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_identity_first_outer_witness_count_bits = 1))))))))) -> (forall erc_row_fubini_total_identity_second_outer. (exists erc_lt_gap_fubini_total_identity_second_outer_bound. erc_lt_gap_fubini_total_identity_second_outer_bound + S (erc_row_fubini_total_identity_second_outer) = k) -> exists erc_count_fubini_total_identity_second_outer. ((((exists ff_h_erc_fubini_total_identity_second_outer_decoded. ff_h_erc_fubini_total_identity_second_outer_decoded + S (erc_count_fubini_total_identity_second_outer) = S ((S (erc_row_fubini_total_identity_second_outer)) * bc)) /\ exists ff_q_erc_fubini_total_identity_second_outer_decoded. bb = ff_q_erc_fubini_total_identity_second_outer_decoded * S ((S (erc_row_fubini_total_identity_second_outer)) * bc) + (erc_count_fubini_total_identity_second_outer))) /\ (exists erc_row_code_fubini_total_identity_second_outer_witness erc_row_scale_fubini_total_identity_second_outer_witness. ((forall eri_column_erc_fubini_total_identity_second_outer_witness_row. (exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_bound. eri_gap_erc_fubini_total_identity_second_outer_witness_row_bound + S (eri_column_erc_fubini_total_identity_second_outer_witness_row) = h) -> exists eri_bit_erc_fubini_total_identity_second_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_identity_second_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_identity_second_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_identity_second_outer_witness_row) = S ((S (eri_column_erc_fubini_total_identity_second_outer_witness_row)) * erc_row_scale_fubini_total_identity_second_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_identity_second_outer_witness_row_decoded. erc_row_code_fubini_total_identity_second_outer_witness = ff_q_eri_erc_fubini_total_identity_second_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_identity_second_outer_witness_row)) * erc_row_scale_fubini_total_identity_second_outer_witness) + (eri_bit_erc_fubini_total_identity_second_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_identity_second_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_identity_second_outer) = q * S eri_column_erc_fubini_total_identity_second_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_identity_second_outer_witness_row) = p * S erc_row_fubini_total_identity_second_outer))) \/ (eri_bit_erc_fubini_total_identity_second_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_identity_second_outer_witness_row) = p * S erc_row_fubini_total_identity_second_outer) /\ ~(exists eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left. eri_gap_erc_fubini_total_identity_second_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_identity_second_outer) = q * S eri_column_erc_fubini_total_identity_second_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_identity_second_outer_witness_count_sum ff_v_erc_fubini_total_identity_second_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_start. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_start. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_terminal + S (erc_count_fubini_total_identity_second_outer) = S ((S (h)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (erc_count_fubini_total_identity_second_outer))) /\ forall ff_i_erc_fubini_total_identity_second_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_identity_second_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_identity_second_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_identity_second_outer_witness_count_sum = h) -> exists ff_a_erc_fubini_total_identity_second_outer_witness_count_sum ff_r_erc_fubini_total_identity_second_outer_witness_count_sum ff_s_erc_fubini_total_identity_second_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_summand. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_identity_second_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_second_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_summand. erc_row_code_fubini_total_identity_second_outer_witness = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * erc_row_scale_fubini_total_identity_second_outer_witness) + (ff_a_erc_fubini_total_identity_second_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_partial. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_identity_second_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_partial. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (ff_r_erc_fubini_total_identity_second_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_successor. ff_h_erc_fubini_total_identity_second_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_identity_second_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_successor. ff_u_erc_fubini_total_identity_second_outer_witness_count_sum = ff_q_erc_fubini_total_identity_second_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_identity_second_outer_witness_count_sum)) * ff_v_erc_fubini_total_identity_second_outer_witness_count_sum) + (ff_s_erc_fubini_total_identity_second_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_identity_second_outer_witness_count_sum = ff_r_erc_fubini_total_identity_second_outer_witness_count_sum + ff_a_erc_fubini_total_identity_second_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_identity_second_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_identity_second_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_identity_second_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_identity_second_outer_witness_count_bits = h) -> exists ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_identity_second_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_identity_second_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_second_outer_witness)) /\ exists ff_q_erc_fubini_total_identity_second_outer_witness_count_bits_decoded. erc_row_code_fubini_total_identity_second_outer_witness = ff_q_erc_fubini_total_identity_second_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_identity_second_outer_witness_count_bits)) * erc_row_scale_fubini_total_identity_second_outer_witness) + (ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_identity_second_outer_witness_count_bits = 1))))))))) -> (exists ff_u_fubini_total_identity_first_sum ff_v_fubini_total_identity_first_sum. ((((exists ff_h_fubini_total_identity_first_sum_start. ff_h_fubini_total_identity_first_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_start. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_start * S ((S (0)) * ff_v_fubini_total_identity_first_sum) + (0))) /\ ((((exists ff_h_fubini_total_identity_first_sum_terminal. ff_h_fubini_total_identity_first_sum_terminal + S (N) = S ((S (h)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_terminal. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_terminal * S ((S (h)) * ff_v_fubini_total_identity_first_sum) + (N))) /\ forall ff_i_fubini_total_identity_first_sum. (exists ff_lt_fubini_total_identity_first_sum_bound. ff_lt_fubini_total_identity_first_sum_bound + S ff_i_fubini_total_identity_first_sum = h) -> exists ff_a_fubini_total_identity_first_sum ff_r_fubini_total_identity_first_sum ff_s_fubini_total_identity_first_sum. ((((exists ff_h_fubini_total_identity_first_sum_summand. ff_h_fubini_total_identity_first_sum_summand + S (ff_a_fubini_total_identity_first_sum) = S ((S (ff_i_fubini_total_identity_first_sum)) * ac)) /\ exists ff_q_fubini_total_identity_first_sum_summand. ab = ff_q_fubini_total_identity_first_sum_summand * S ((S (ff_i_fubini_total_identity_first_sum)) * ac) + (ff_a_fubini_total_identity_first_sum))) /\ ((((exists ff_h_fubini_total_identity_first_sum_partial. ff_h_fubini_total_identity_first_sum_partial + S (ff_r_fubini_total_identity_first_sum) = S ((S (ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_partial. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_partial * S ((S (ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum) + (ff_r_fubini_total_identity_first_sum))) /\ ((((exists ff_h_fubini_total_identity_first_sum_successor. ff_h_fubini_total_identity_first_sum_successor + S (ff_s_fubini_total_identity_first_sum) = S ((S (S ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum)) /\ exists ff_q_fubini_total_identity_first_sum_successor. ff_u_fubini_total_identity_first_sum = ff_q_fubini_total_identity_first_sum_successor * S ((S (S ff_i_fubini_total_identity_first_sum)) * ff_v_fubini_total_identity_first_sum) + (ff_s_fubini_total_identity_first_sum))) /\ ff_s_fubini_total_identity_first_sum = ff_r_fubini_total_identity_first_sum + ff_a_fubini_total_identity_first_sum)))))) -> (exists ff_u_fubini_total_identity_second_sum ff_v_fubini_total_identity_second_sum. ((((exists ff_h_fubini_total_identity_second_sum_start. ff_h_fubini_total_identity_second_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_start. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_start * S ((S (0)) * ff_v_fubini_total_identity_second_sum) + (0))) /\ ((((exists ff_h_fubini_total_identity_second_sum_terminal. ff_h_fubini_total_identity_second_sum_terminal + S (T) = S ((S (k)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_terminal. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_terminal * S ((S (k)) * ff_v_fubini_total_identity_second_sum) + (T))) /\ forall ff_i_fubini_total_identity_second_sum. (exists ff_lt_fubini_total_identity_second_sum_bound. ff_lt_fubini_total_identity_second_sum_bound + S ff_i_fubini_total_identity_second_sum = k) -> exists ff_a_fubini_total_identity_second_sum ff_r_fubini_total_identity_second_sum ff_s_fubini_total_identity_second_sum. ((((exists ff_h_fubini_total_identity_second_sum_summand. ff_h_fubini_total_identity_second_sum_summand + S (ff_a_fubini_total_identity_second_sum) = S ((S (ff_i_fubini_total_identity_second_sum)) * bc)) /\ exists ff_q_fubini_total_identity_second_sum_summand. bb = ff_q_fubini_total_identity_second_sum_summand * S ((S (ff_i_fubini_total_identity_second_sum)) * bc) + (ff_a_fubini_total_identity_second_sum))) /\ ((((exists ff_h_fubini_total_identity_second_sum_partial. ff_h_fubini_total_identity_second_sum_partial + S (ff_r_fubini_total_identity_second_sum) = S ((S (ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_partial. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_partial * S ((S (ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum) + (ff_r_fubini_total_identity_second_sum))) /\ ((((exists ff_h_fubini_total_identity_second_sum_successor. ff_h_fubini_total_identity_second_sum_successor + S (ff_s_fubini_total_identity_second_sum) = S ((S (S ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum)) /\ exists ff_q_fubini_total_identity_second_sum_successor. ff_u_fubini_total_identity_second_sum = ff_q_fubini_total_identity_second_sum_successor * S ((S (S ff_i_fubini_total_identity_second_sum)) * ff_v_fubini_total_identity_second_sum) + (ff_s_fubini_total_identity_second_sum))) /\ ff_s_fubini_total_identity_second_sum = ff_r_fubini_total_identity_second_sum + ff_a_fubini_total_identity_second_sum)))))) -> N + T = h * k

Structural proof guide

Generated structural guide

The two semantic Eisenstein row totals add exactly to the rectangle area.

Use the direct prerequisites eisenstein_rectangle_plus_column_count_total, eisenstein_constructed_column_total_equals_swapped_total as previously established PA formulas.

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

Referenced ingredients

PA00EQ eisenstein_rectangle_plus_column_count_total PA00FD eisenstein_constructed_column_total_equals_swapped_total

Proof neighborhood

Direct dependencies

PA00EQ eisenstein_rectangle_plus_column_count_total PA00FD eisenstein_constructed_column_total_equals_swapped_total

Direct dependents

PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity

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 ab
  6. 0006intro ac
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro N
  10. 0010intro T
  11. 0011intro hfirst
  12. 0012intro hsecond
  13. 0013intro hfirstsum
  14. 0014intro hsecondsum
  15. 0015have hpartition : exists db dc M. ((forall etcc_row_index_fubini_total_identity_partition_prefix. (exists edt_lt_gap_fubini_total_identity_partition_prefix_bound. edt_lt_gap_fubini_total_identity_partition_prefix_bound + S (etcc_row_index_fubini_total_identity_partition_prefix) = h) -> exists etcc_count_fubini_total_identity_partition_prefix. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_decoded. ff_h_etcc_fubini_total_identity_partition_prefix_decoded + S (etcc_count_fubini_total_identity_partition_prefix) = S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * dc)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_decoded. db = ff_q_etcc_fubini_total_identity_partition_prefix_decoded * S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * dc) + (etcc_count_fubini_total_identity_partition_prefix))) /\ (exists etcc_row_count_fubini_total_identity_partition_prefix_witness etcc_column_code_fubini_total_identity_partition_prefix_witness etcc_column_scale_fubini_total_identity_partition_prefix_witness. ((((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_first_entry. ff_h_etcc_fubini_total_identity_partition_prefix_witness_first_entry + S (etcc_row_count_fubini_total_identity_partition_prefix_witness) = S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * ac)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_first_entry. ab = ff_q_etcc_fubini_total_identity_partition_prefix_witness_first_entry * S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * ac) + (etcc_row_count_fubini_total_identity_partition_prefix_witness))) /\ (exists erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics. ((forall eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row. (exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_bound. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_bound + S (eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded. erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics = ff_q_eri_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics) + (eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_fubini_total_identity_partition_prefix) = p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = q * S etcc_row_index_fubini_total_identity_partition_prefix))) \/ (eri_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row) = q * S etcc_row_index_fubini_total_identity_partition_prefix) /\ ~(exists eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_fubini_total_identity_partition_prefix) = p * S eri_column_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal + S (etcc_row_count_fubini_total_identity_partition_prefix_witness) = S ((S (k)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (etcc_row_count_fubini_total_identity_partition_prefix_witness))) /\ forall ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand. erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics) + (ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum) + (ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum = ff_r_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum + ff_a_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_fubini_total_identity_partition_prefix_witness_row_semantics = ff_q_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_row_semantics) + (ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_fubini_total_identity_partition_prefix_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column. (exists edt_lt_gap_etcc_fubini_total_identity_partition_prefix_witness_column_bound. edt_lt_gap_etcc_fubini_total_identity_partition_prefix_witness_column_bound + S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) = k) -> exists etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded + S (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column) = S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded. etcc_column_code_fubini_total_identity_partition_prefix_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_decoded * S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness) + (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column))) /\ (exists etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness. ((((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry + S (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness) = S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * bc)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column)) * bc) + (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness))) /\ (forall eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row. (exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_bound. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_bound + S (eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = S ((S (eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_eri_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) = q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column))) \/ (eri_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) /\ ~(exists eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_fubini_total_identity_partition_prefix_witness_column) = q * S eri_column_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (etc_count_etcc_fubini_total_identity_partition_prefix_witness_column_witness))) /\ forall ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum = ff_r_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum + ff_a_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry. ff_h_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry + S (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column) = S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry. etc_row_code_etcc_fubini_total_identity_partition_prefix_witness_column_witness = ff_q_etc_etcc_fubini_total_identity_partition_prefix_witness_column_witness_inner_entry * S ((S (etcc_row_index_fubini_total_identity_partition_prefix)) * etc_row_scale_etcc_fubini_total_identity_partition_prefix_witness_column_witness) + (etc_bit_etcc_fubini_total_identity_partition_prefix_witness_column)))))))) /\ ((((exists ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal + S (etcc_count_fubini_total_identity_partition_prefix) = S ((S (k)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (etcc_count_fubini_total_identity_partition_prefix))) /\ forall ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum. (exists ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_bound. ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_bound + S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = k) -> exists ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand + S (ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand. etcc_column_code_fubini_total_identity_partition_prefix_witness = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_summand * S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness) + (ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial + S (ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_partial * S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor + S (ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) = S ((S (S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor. ff_u_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum_successor * S ((S (S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)) * ff_v_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum) + (ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum))) /\ ff_s_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum = ff_r_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum + ff_a_etcc_fubini_total_identity_partition_prefix_witness_column_count_sum)))))) /\ (forall ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits. (exists ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_bound. ff_lt_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_bound + S ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits = k) -> exists ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits. ((((exists ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded. ff_h_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded + S (ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits) = S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness)) /\ exists ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded. etcc_column_code_fubini_total_identity_partition_prefix_witness = ff_q_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits_decoded * S ((S (ff_i_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits)) * etcc_column_scale_fubini_total_identity_partition_prefix_witness) + (ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits))) /\ (ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits = 0 \/ ff_bit_etcc_fubini_total_identity_partition_prefix_witness_column_count_bits = 1))))) /\ etcc_row_count_fubini_total_identity_partition_prefix_witness + etcc_count_fubini_total_identity_partition_prefix = k))))) /\ ((exists ff_u_fubini_total_identity_partition_sum ff_v_fubini_total_identity_partition_sum. ((((exists ff_h_fubini_total_identity_partition_sum_start. ff_h_fubini_total_identity_partition_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_start. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_start * S ((S (0)) * ff_v_fubini_total_identity_partition_sum) + (0))) /\ ((((exists ff_h_fubini_total_identity_partition_sum_terminal. ff_h_fubini_total_identity_partition_sum_terminal + S (M) = S ((S (h)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_terminal. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_terminal * S ((S (h)) * ff_v_fubini_total_identity_partition_sum) + (M))) /\ forall ff_i_fubini_total_identity_partition_sum. (exists ff_lt_fubini_total_identity_partition_sum_bound. ff_lt_fubini_total_identity_partition_sum_bound + S ff_i_fubini_total_identity_partition_sum = h) -> exists ff_a_fubini_total_identity_partition_sum ff_r_fubini_total_identity_partition_sum ff_s_fubini_total_identity_partition_sum. ((((exists ff_h_fubini_total_identity_partition_sum_summand. ff_h_fubini_total_identity_partition_sum_summand + S (ff_a_fubini_total_identity_partition_sum) = S ((S (ff_i_fubini_total_identity_partition_sum)) * dc)) /\ exists ff_q_fubini_total_identity_partition_sum_summand. db = ff_q_fubini_total_identity_partition_sum_summand * S ((S (ff_i_fubini_total_identity_partition_sum)) * dc) + (ff_a_fubini_total_identity_partition_sum))) /\ ((((exists ff_h_fubini_total_identity_partition_sum_partial. ff_h_fubini_total_identity_partition_sum_partial + S (ff_r_fubini_total_identity_partition_sum) = S ((S (ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_partial. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_partial * S ((S (ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum) + (ff_r_fubini_total_identity_partition_sum))) /\ ((((exists ff_h_fubini_total_identity_partition_sum_successor. ff_h_fubini_total_identity_partition_sum_successor + S (ff_s_fubini_total_identity_partition_sum) = S ((S (S ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum)) /\ exists ff_q_fubini_total_identity_partition_sum_successor. ff_u_fubini_total_identity_partition_sum = ff_q_fubini_total_identity_partition_sum_successor * S ((S (S ff_i_fubini_total_identity_partition_sum)) * ff_v_fubini_total_identity_partition_sum) + (ff_s_fubini_total_identity_partition_sum))) /\ ff_s_fubini_total_identity_partition_sum = ff_r_fubini_total_identity_partition_sum + ff_a_fubini_total_identity_partition_sum)))))) /\ N + M = h * k))
  16. 0016specialize eisenstein_rectangle_plus_column_count_total p
  17. 0017specialize eisenstein_rectangle_plus_column_count_total q
  18. 0018specialize eisenstein_rectangle_plus_column_count_total h
  19. 0019specialize eisenstein_rectangle_plus_column_count_total k
  20. 0020specialize eisenstein_rectangle_plus_column_count_total ab
  21. 0021specialize eisenstein_rectangle_plus_column_count_total ac
  22. 0022specialize eisenstein_rectangle_plus_column_count_total bb
  23. 0023specialize eisenstein_rectangle_plus_column_count_total bc
  24. 0024specialize eisenstein_rectangle_plus_column_count_total N
  25. 0025apply eisenstein_rectangle_plus_column_count_total
  26. 0026exact hfirst
  27. 0027exact hsecond
  28. 0028exact hfirstsum
  29. 0029cases hpartition
  30. 0030cases hpartition_witness
  31. 0031cases hpartition_witness_witness
  32. 0032cases hpartition_witness_witness_witness
  33. 0033cases hpartition_witness_witness_witness_right
  34. 0034have heq : x2 = T
  35. 0035specialize eisenstein_constructed_column_total_equals_swapped_total p
  36. 0036specialize eisenstein_constructed_column_total_equals_swapped_total q
  37. 0037specialize eisenstein_constructed_column_total_equals_swapped_total h
  38. 0038specialize eisenstein_constructed_column_total_equals_swapped_total k
  39. 0039specialize eisenstein_constructed_column_total_equals_swapped_total ab
  40. 0040specialize eisenstein_constructed_column_total_equals_swapped_total ac
  41. 0041specialize eisenstein_constructed_column_total_equals_swapped_total bb
  42. 0042specialize eisenstein_constructed_column_total_equals_swapped_total bc
  43. 0043specialize eisenstein_constructed_column_total_equals_swapped_total x
  44. 0044specialize eisenstein_constructed_column_total_equals_swapped_total x1
  45. 0045specialize eisenstein_constructed_column_total_equals_swapped_total T
  46. 0046specialize eisenstein_constructed_column_total_equals_swapped_total x2
  47. 0047apply eisenstein_constructed_column_total_equals_swapped_total
  48. 0048exact hsecond
  49. 0049exact hpartition_witness_witness_witness_left
  50. 0050exact hsecondsum
  51. 0051exact hpartition_witness_witness_witness_right_left
  52. 0052rewrite heq at hpartition_witness_witness_witness_right_right
  53. 0053exact hpartition_witness_witness_witness_right_right