PA00FC — eisenstein_fubini

Exact expanded PA statement

forall h p q k bb bc db dc T M. (forall erc_row_fubini_total_general_outer. (exists erc_lt_gap_fubini_total_general_outer_bound. erc_lt_gap_fubini_total_general_outer_bound + S (erc_row_fubini_total_general_outer) = k) -> exists erc_count_fubini_total_general_outer. ((((exists ff_h_erc_fubini_total_general_outer_decoded. ff_h_erc_fubini_total_general_outer_decoded + S (erc_count_fubini_total_general_outer) = S ((S (erc_row_fubini_total_general_outer)) * bc)) /\ exists ff_q_erc_fubini_total_general_outer_decoded. bb = ff_q_erc_fubini_total_general_outer_decoded * S ((S (erc_row_fubini_total_general_outer)) * bc) + (erc_count_fubini_total_general_outer))) /\ (exists erc_row_code_fubini_total_general_outer_witness erc_row_scale_fubini_total_general_outer_witness. ((forall eri_column_erc_fubini_total_general_outer_witness_row. (exists eri_gap_erc_fubini_total_general_outer_witness_row_bound. eri_gap_erc_fubini_total_general_outer_witness_row_bound + S (eri_column_erc_fubini_total_general_outer_witness_row) = h) -> exists eri_bit_erc_fubini_total_general_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_general_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_general_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_general_outer_witness_row) = S ((S (eri_column_erc_fubini_total_general_outer_witness_row)) * erc_row_scale_fubini_total_general_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_general_outer_witness_row_decoded. erc_row_code_fubini_total_general_outer_witness = ff_q_eri_erc_fubini_total_general_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_general_outer_witness_row)) * erc_row_scale_fubini_total_general_outer_witness) + (eri_bit_erc_fubini_total_general_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_general_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_left. eri_gap_erc_fubini_total_general_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_general_outer) = q * S eri_column_erc_fubini_total_general_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_right. eri_gap_erc_fubini_total_general_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_general_outer_witness_row) = p * S erc_row_fubini_total_general_outer))) \/ (eri_bit_erc_fubini_total_general_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_right. eri_gap_erc_fubini_total_general_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_general_outer_witness_row) = p * S erc_row_fubini_total_general_outer) /\ ~(exists eri_gap_erc_fubini_total_general_outer_witness_row_choice_left. eri_gap_erc_fubini_total_general_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_general_outer) = q * S eri_column_erc_fubini_total_general_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_general_outer_witness_count_sum ff_v_erc_fubini_total_general_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_start. ff_h_erc_fubini_total_general_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_start. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_general_outer_witness_count_sum_terminal + S (erc_count_fubini_total_general_outer) = S ((S (h)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (erc_count_fubini_total_general_outer))) /\ forall ff_i_erc_fubini_total_general_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_general_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_general_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_general_outer_witness_count_sum = h) -> exists ff_a_erc_fubini_total_general_outer_witness_count_sum ff_r_erc_fubini_total_general_outer_witness_count_sum ff_s_erc_fubini_total_general_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_summand. ff_h_erc_fubini_total_general_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_general_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * erc_row_scale_fubini_total_general_outer_witness)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_summand. erc_row_code_fubini_total_general_outer_witness = ff_q_erc_fubini_total_general_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * erc_row_scale_fubini_total_general_outer_witness) + (ff_a_erc_fubini_total_general_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_partial. ff_h_erc_fubini_total_general_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_general_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_partial. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (ff_r_erc_fubini_total_general_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_general_outer_witness_count_sum_successor. ff_h_erc_fubini_total_general_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_general_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_sum_successor. ff_u_erc_fubini_total_general_outer_witness_count_sum = ff_q_erc_fubini_total_general_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_general_outer_witness_count_sum)) * ff_v_erc_fubini_total_general_outer_witness_count_sum) + (ff_s_erc_fubini_total_general_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_general_outer_witness_count_sum = ff_r_erc_fubini_total_general_outer_witness_count_sum + ff_a_erc_fubini_total_general_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_general_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_general_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_general_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_general_outer_witness_count_bits = h) -> exists ff_bit_erc_fubini_total_general_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_general_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_general_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_general_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_general_outer_witness_count_bits)) * erc_row_scale_fubini_total_general_outer_witness)) /\ exists ff_q_erc_fubini_total_general_outer_witness_count_bits_decoded. erc_row_code_fubini_total_general_outer_witness = ff_q_erc_fubini_total_general_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_general_outer_witness_count_bits)) * erc_row_scale_fubini_total_general_outer_witness) + (ff_bit_erc_fubini_total_general_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_general_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_general_outer_witness_count_bits = 1))))))))) -> (forall eft_fixed_index_fubini_total_general_columns. (exists edt_lt_gap_eft_fubini_total_general_columns_bound. edt_lt_gap_eft_fubini_total_general_columns_bound + S (eft_fixed_index_fubini_total_general_columns) = h) -> exists eft_count_fubini_total_general_columns. ((((exists ff_h_eft_fubini_total_general_columns_decoded. ff_h_eft_fubini_total_general_columns_decoded + S (eft_count_fubini_total_general_columns) = S ((S (eft_fixed_index_fubini_total_general_columns)) * dc)) /\ exists ff_q_eft_fubini_total_general_columns_decoded. db = ff_q_eft_fubini_total_general_columns_decoded * S ((S (eft_fixed_index_fubini_total_general_columns)) * dc) + (eft_count_fubini_total_general_columns))) /\ (exists eft_column_code_fubini_total_general_columns_witness eft_column_scale_fubini_total_general_columns_witness. ((forall etc_row_index_eft_fubini_total_general_columns_witness_column. (exists edt_lt_gap_eft_fubini_total_general_columns_witness_column_bound. edt_lt_gap_eft_fubini_total_general_columns_witness_column_bound + S (etc_row_index_eft_fubini_total_general_columns_witness_column) = k) -> exists etc_bit_eft_fubini_total_general_columns_witness_column. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_decoded. ff_h_etc_eft_fubini_total_general_columns_witness_column_decoded + S (etc_bit_eft_fubini_total_general_columns_witness_column) = S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * eft_column_scale_fubini_total_general_columns_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_decoded. eft_column_code_fubini_total_general_columns_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * eft_column_scale_fubini_total_general_columns_witness) + (etc_bit_eft_fubini_total_general_columns_witness_column))) /\ (exists etc_count_eft_fubini_total_general_columns_witness_column_witness etc_row_code_eft_fubini_total_general_columns_witness_column_witness etc_row_scale_eft_fubini_total_general_columns_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_general_columns_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * bc)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry. bb = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_general_columns_witness_column)) * bc) + (etc_count_eft_fubini_total_general_columns_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) = h) -> exists eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_eri_etc_eft_fubini_total_general_columns_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_general_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_general_columns_witness_column))) \/ (eri_bit_etc_eft_fubini_total_general_columns_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_general_columns_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_general_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_general_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_general_columns_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_general_columns_witness_column_witness) = S ((S (h)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_general_columns_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_general_columns_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_general_columns_witness_column) = S ((S (eft_fixed_index_fubini_total_general_columns)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_general_columns_witness_column_witness = ff_q_etc_eft_fubini_total_general_columns_witness_column_witness_inner_entry * S ((S (eft_fixed_index_fubini_total_general_columns)) * etc_row_scale_eft_fubini_total_general_columns_witness_column_witness) + (etc_bit_eft_fubini_total_general_columns_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_general_columns_witness_count_sum ff_v_eft_fubini_total_general_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_start. ff_h_eft_fubini_total_general_columns_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_start. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_terminal. ff_h_eft_fubini_total_general_columns_witness_count_sum_terminal + S (eft_count_fubini_total_general_columns) = S ((S (k)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_terminal. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (eft_count_fubini_total_general_columns))) /\ forall ff_i_eft_fubini_total_general_columns_witness_count_sum. (exists ff_lt_eft_fubini_total_general_columns_witness_count_sum_bound. ff_lt_eft_fubini_total_general_columns_witness_count_sum_bound + S ff_i_eft_fubini_total_general_columns_witness_count_sum = k) -> exists ff_a_eft_fubini_total_general_columns_witness_count_sum ff_r_eft_fubini_total_general_columns_witness_count_sum ff_s_eft_fubini_total_general_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_summand. ff_h_eft_fubini_total_general_columns_witness_count_sum_summand + S (ff_a_eft_fubini_total_general_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * eft_column_scale_fubini_total_general_columns_witness)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_summand. eft_column_code_fubini_total_general_columns_witness = ff_q_eft_fubini_total_general_columns_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * eft_column_scale_fubini_total_general_columns_witness) + (ff_a_eft_fubini_total_general_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_partial. ff_h_eft_fubini_total_general_columns_witness_count_sum_partial + S (ff_r_eft_fubini_total_general_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_partial. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (ff_r_eft_fubini_total_general_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_general_columns_witness_count_sum_successor. ff_h_eft_fubini_total_general_columns_witness_count_sum_successor + S (ff_s_eft_fubini_total_general_columns_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_sum_successor. ff_u_eft_fubini_total_general_columns_witness_count_sum = ff_q_eft_fubini_total_general_columns_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_general_columns_witness_count_sum)) * ff_v_eft_fubini_total_general_columns_witness_count_sum) + (ff_s_eft_fubini_total_general_columns_witness_count_sum))) /\ ff_s_eft_fubini_total_general_columns_witness_count_sum = ff_r_eft_fubini_total_general_columns_witness_count_sum + ff_a_eft_fubini_total_general_columns_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_general_columns_witness_count_bits. (exists ff_lt_eft_fubini_total_general_columns_witness_count_bits_bound. ff_lt_eft_fubini_total_general_columns_witness_count_bits_bound + S ff_i_eft_fubini_total_general_columns_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_general_columns_witness_count_bits. ((((exists ff_h_eft_fubini_total_general_columns_witness_count_bits_decoded. ff_h_eft_fubini_total_general_columns_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_general_columns_witness_count_bits) = S ((S (ff_i_eft_fubini_total_general_columns_witness_count_bits)) * eft_column_scale_fubini_total_general_columns_witness)) /\ exists ff_q_eft_fubini_total_general_columns_witness_count_bits_decoded. eft_column_code_fubini_total_general_columns_witness = ff_q_eft_fubini_total_general_columns_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_general_columns_witness_count_bits)) * eft_column_scale_fubini_total_general_columns_witness) + (ff_bit_eft_fubini_total_general_columns_witness_count_bits))) /\ (ff_bit_eft_fubini_total_general_columns_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_general_columns_witness_count_bits = 1))))))))) -> (exists ff_u_fubini_total_general_outer_sum ff_v_fubini_total_general_outer_sum. ((((exists ff_h_fubini_total_general_outer_sum_start. ff_h_fubini_total_general_outer_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_start. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_start * S ((S (0)) * ff_v_fubini_total_general_outer_sum) + (0))) /\ ((((exists ff_h_fubini_total_general_outer_sum_terminal. ff_h_fubini_total_general_outer_sum_terminal + S (T) = S ((S (k)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_terminal. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_terminal * S ((S (k)) * ff_v_fubini_total_general_outer_sum) + (T))) /\ forall ff_i_fubini_total_general_outer_sum. (exists ff_lt_fubini_total_general_outer_sum_bound. ff_lt_fubini_total_general_outer_sum_bound + S ff_i_fubini_total_general_outer_sum = k) -> exists ff_a_fubini_total_general_outer_sum ff_r_fubini_total_general_outer_sum ff_s_fubini_total_general_outer_sum. ((((exists ff_h_fubini_total_general_outer_sum_summand. ff_h_fubini_total_general_outer_sum_summand + S (ff_a_fubini_total_general_outer_sum) = S ((S (ff_i_fubini_total_general_outer_sum)) * bc)) /\ exists ff_q_fubini_total_general_outer_sum_summand. bb = ff_q_fubini_total_general_outer_sum_summand * S ((S (ff_i_fubini_total_general_outer_sum)) * bc) + (ff_a_fubini_total_general_outer_sum))) /\ ((((exists ff_h_fubini_total_general_outer_sum_partial. ff_h_fubini_total_general_outer_sum_partial + S (ff_r_fubini_total_general_outer_sum) = S ((S (ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_partial. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_partial * S ((S (ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum) + (ff_r_fubini_total_general_outer_sum))) /\ ((((exists ff_h_fubini_total_general_outer_sum_successor. ff_h_fubini_total_general_outer_sum_successor + S (ff_s_fubini_total_general_outer_sum) = S ((S (S ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum)) /\ exists ff_q_fubini_total_general_outer_sum_successor. ff_u_fubini_total_general_outer_sum = ff_q_fubini_total_general_outer_sum_successor * S ((S (S ff_i_fubini_total_general_outer_sum)) * ff_v_fubini_total_general_outer_sum) + (ff_s_fubini_total_general_outer_sum))) /\ ff_s_fubini_total_general_outer_sum = ff_r_fubini_total_general_outer_sum + ff_a_fubini_total_general_outer_sum)))))) -> (exists ff_u_fubini_total_general_column_sum ff_v_fubini_total_general_column_sum. ((((exists ff_h_fubini_total_general_column_sum_start. ff_h_fubini_total_general_column_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_start. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_start * S ((S (0)) * ff_v_fubini_total_general_column_sum) + (0))) /\ ((((exists ff_h_fubini_total_general_column_sum_terminal. ff_h_fubini_total_general_column_sum_terminal + S (M) = S ((S (h)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_terminal. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_terminal * S ((S (h)) * ff_v_fubini_total_general_column_sum) + (M))) /\ forall ff_i_fubini_total_general_column_sum. (exists ff_lt_fubini_total_general_column_sum_bound. ff_lt_fubini_total_general_column_sum_bound + S ff_i_fubini_total_general_column_sum = h) -> exists ff_a_fubini_total_general_column_sum ff_r_fubini_total_general_column_sum ff_s_fubini_total_general_column_sum. ((((exists ff_h_fubini_total_general_column_sum_summand. ff_h_fubini_total_general_column_sum_summand + S (ff_a_fubini_total_general_column_sum) = S ((S (ff_i_fubini_total_general_column_sum)) * dc)) /\ exists ff_q_fubini_total_general_column_sum_summand. db = ff_q_fubini_total_general_column_sum_summand * S ((S (ff_i_fubini_total_general_column_sum)) * dc) + (ff_a_fubini_total_general_column_sum))) /\ ((((exists ff_h_fubini_total_general_column_sum_partial. ff_h_fubini_total_general_column_sum_partial + S (ff_r_fubini_total_general_column_sum) = S ((S (ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_partial. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_partial * S ((S (ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum) + (ff_r_fubini_total_general_column_sum))) /\ ((((exists ff_h_fubini_total_general_column_sum_successor. ff_h_fubini_total_general_column_sum_successor + S (ff_s_fubini_total_general_column_sum) = S ((S (S ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum)) /\ exists ff_q_fubini_total_general_column_sum_successor. ff_u_fubini_total_general_column_sum = ff_q_fubini_total_general_column_sum_successor * S ((S (S ff_i_fubini_total_general_column_sum)) * ff_v_fubini_total_general_column_sum) + (ff_s_fubini_total_general_column_sum))) /\ ff_s_fubini_total_general_column_sum = ff_r_fubini_total_general_column_sum + ff_a_fubini_total_general_column_sum)))))) -> M = T

Structural proof guide

Generated structural guide

Any genuine transposed-column count total equals the swapped semantic row total.

Use the direct prerequisites beta_sum_zero, eisenstein_zero_width_rectangle_sum_zero, eisenstein_successor_rectangle_row_split_prefix_exists, eisenstein_successor_row_split_reduced_rectangle_prefix, beta_sum_exists, eisenstein_successor_row_split_sum_add, eisenstein_fubini_column_count_prefix_succ_restrict, eisenstein_fubini_column_count_prefix_retarget_predecessor, beta_sum_succ_decompose, le_refl, beta_at_unique, eisenstein_successor_terminal_sum_matches_last_column as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (16), intermediate claims (15), equality transport (3).

Referenced ingredients

PA0047 beta_sum_zero PA00ES eisenstein_zero_width_rectangle_sum_zero PA00EY eisenstein_successor_rectangle_row_split_prefix_exists PA00F0 eisenstein_successor_row_split_reduced_rectangle_prefix PA003H beta_sum_exists PA00F2 eisenstein_successor_row_split_sum_add PA00F3 eisenstein_fubini_column_count_prefix_succ_restrict PA00F8 eisenstein_fubini_column_count_prefix_retarget_predecessor PA003Y beta_sum_succ_decompose PA001A le_refl PA002F beta_at_unique PA00FB eisenstein_successor_terminal_sum_matches_last_column

Proof neighborhood

Direct dependencies

Direct dependents

PA00FD eisenstein_constructed_column_total_equals_swapped_total

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.

0001intro h
0002induction h
0003intro p
0004intro q
0005intro k
0006intro bb
0007intro bc
0008intro db
0009intro dc
0010intro T
0011intro M
0012intro houter
0013intro hcolumns
0014intro houtersum
0015intro hcolumnsum
0016have hmzero : M = 0
0017specialize beta_sum_zero db
0018specialize beta_sum_zero dc
0019specialize beta_sum_zero M
0020apply beta_sum_zero
0021exact hcolumnsum
0022have htzero : T = 0
0023specialize eisenstein_zero_width_rectangle_sum_zero q
0024specialize eisenstein_zero_width_rectangle_sum_zero p
0025specialize eisenstein_zero_width_rectangle_sum_zero 0
0026specialize eisenstein_zero_width_rectangle_sum_zero bb
0027specialize eisenstein_zero_width_rectangle_sum_zero bc
0028specialize eisenstein_zero_width_rectangle_sum_zero k
0029specialize eisenstein_zero_width_rectangle_sum_zero T
0030apply eisenstein_zero_width_rectangle_sum_zero
0031refl
0032exact houter
0033exact houtersum
0034trans 0
0035exact hmzero
0036symm
0037exact htzero
0038intro p
0039intro q
0040intro k
0041intro bb
0042intro bc
0043intro db
0044intro dc
0045intro T
0046intro M
0047intro houter
0048intro hcolumns
0049intro houtersum
0050intro hcolumnsum
0051have hsplit_exists : exists rb rc tb tc. (forall efrd_row_index_fubini_total_universal_split_exists. (exists efrd_lt_gap_fubini_total_universal_split_exists_bound. efrd_lt_gap_fubini_total_universal_split_exists_bound + S (efrd_row_index_fubini_total_universal_split_exists) = k) -> exists efrd_count_fubini_total_universal_split_exists efrd_reduced_count_fubini_total_universal_split_exists efrd_terminal_bit_fubini_total_universal_split_exists. (((((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_outer_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_outer_entry + S (efrd_count_fubini_total_universal_split_exists) = S ((S (efrd_row_index_fubini_total_universal_split_exists)) * bc)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_outer_entry. bb = ff_q_efrd_fubini_total_universal_split_exists_entry_outer_entry * S ((S (efrd_row_index_fubini_total_universal_split_exists)) * bc) + (efrd_count_fubini_total_universal_split_exists))) /\ (((exists ff_h_efrd_fubini_total_universal_split_exists_entry_reduced_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_reduced_entry + S (efrd_reduced_count_fubini_total_universal_split_exists) = S ((S (efrd_row_index_fubini_total_universal_split_exists)) * rc)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_reduced_entry. rb = ff_q_efrd_fubini_total_universal_split_exists_entry_reduced_entry * S ((S (efrd_row_index_fubini_total_universal_split_exists)) * rc) + (efrd_reduced_count_fubini_total_universal_split_exists)))) /\ (((exists ff_h_efrd_fubini_total_universal_split_exists_entry_terminal_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_terminal_entry + S (efrd_terminal_bit_fubini_total_universal_split_exists) = S ((S (efrd_row_index_fubini_total_universal_split_exists)) * tc)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_terminal_entry. tb = ff_q_efrd_fubini_total_universal_split_exists_entry_terminal_entry * S ((S (efrd_row_index_fubini_total_universal_split_exists)) * tc) + (efrd_terminal_bit_fubini_total_universal_split_exists)))) /\ (exists efrd_row_code_fubini_total_universal_split_exists_entry_split efrd_row_scale_fubini_total_universal_split_exists_entry_split. (((((forall eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = S h) -> exists eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists))) \/ (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_total_universal_split_exists) = S ((S (S h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_terminal * S ((S (S h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (efrd_count_fubini_total_universal_split_exists))) /\ forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = S h) -> exists ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum) + (ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum = ff_r_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum + ff_a_efrd_fubini_total_universal_split_exists_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits = S h) -> exists ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_total_universal_split_exists_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_eri_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists))) \/ (eri_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_right + S (q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix) = p * S efrd_row_index_fubini_total_universal_split_exists) /\ ~(exists eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix_choice_left + S (p * S efrd_row_index_fubini_total_universal_split_exists) = q * S eri_column_efrd_fubini_total_universal_split_exists_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry. ff_h_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_total_universal_split_exists) = S ((S (h)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (efrd_terminal_bit_fubini_total_universal_split_exists))))) /\ (((((exists ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_total_universal_split_exists) = S ((S (h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_total_universal_split_exists))) /\ forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum = ff_r_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum + ff_a_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split)) /\ exists ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_total_universal_split_exists_entry_split = ff_q_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_total_universal_split_exists_entry_split) + (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_total_universal_split_exists_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_total_universal_split_exists = 0 \/ efrd_terminal_bit_fubini_total_universal_split_exists = 1)) /\ efrd_count_fubini_total_universal_split_exists = efrd_reduced_count_fubini_total_universal_split_exists + efrd_terminal_bit_fubini_total_universal_split_exists)))))))
0052specialize eisenstein_successor_rectangle_row_split_prefix_exists q
0053specialize eisenstein_successor_rectangle_row_split_prefix_exists p
0054specialize eisenstein_successor_rectangle_row_split_prefix_exists h
0055specialize eisenstein_successor_rectangle_row_split_prefix_exists (S h)
0056specialize eisenstein_successor_rectangle_row_split_prefix_exists bb
0057specialize eisenstein_successor_rectangle_row_split_prefix_exists bc
0058specialize eisenstein_successor_rectangle_row_split_prefix_exists k
0059apply eisenstein_successor_rectangle_row_split_prefix_exists
0060refl
0061exact houter
0062cases hsplit_exists
0063cases hsplit_exists_witness
0064cases hsplit_exists_witness_witness
0065cases hsplit_exists_witness_witness_witness
0066have hreduced_outer : forall erc_row_fubini_total_universal_reduced_outer. (exists erc_lt_gap_fubini_total_universal_reduced_outer_bound. erc_lt_gap_fubini_total_universal_reduced_outer_bound + S (erc_row_fubini_total_universal_reduced_outer) = k) -> exists erc_count_fubini_total_universal_reduced_outer. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_decoded. ff_h_erc_fubini_total_universal_reduced_outer_decoded + S (erc_count_fubini_total_universal_reduced_outer) = S ((S (erc_row_fubini_total_universal_reduced_outer)) * x1)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_decoded. x = ff_q_erc_fubini_total_universal_reduced_outer_decoded * S ((S (erc_row_fubini_total_universal_reduced_outer)) * x1) + (erc_count_fubini_total_universal_reduced_outer))) /\ (exists erc_row_code_fubini_total_universal_reduced_outer_witness erc_row_scale_fubini_total_universal_reduced_outer_witness. ((forall eri_column_erc_fubini_total_universal_reduced_outer_witness_row. (exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_bound. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_bound + S (eri_column_erc_fubini_total_universal_reduced_outer_witness_row) = h) -> exists eri_bit_erc_fubini_total_universal_reduced_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_universal_reduced_outer_witness_row) = S ((S (eri_column_erc_fubini_total_universal_reduced_outer_witness_row)) * erc_row_scale_fubini_total_universal_reduced_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded. erc_row_code_fubini_total_universal_reduced_outer_witness = ff_q_eri_erc_fubini_total_universal_reduced_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_universal_reduced_outer_witness_row)) * erc_row_scale_fubini_total_universal_reduced_outer_witness) + (eri_bit_erc_fubini_total_universal_reduced_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_universal_reduced_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_universal_reduced_outer) = q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row) = p * S erc_row_fubini_total_universal_reduced_outer))) \/ (eri_bit_erc_fubini_total_universal_reduced_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row) = p * S erc_row_fubini_total_universal_reduced_outer) /\ ~(exists eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left. eri_gap_erc_fubini_total_universal_reduced_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_universal_reduced_outer) = q * S eri_column_erc_fubini_total_universal_reduced_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_start. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_start. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal + S (erc_count_fubini_total_universal_reduced_outer) = S ((S (h)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (erc_count_fubini_total_universal_reduced_outer))) /\ forall ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum = h) -> exists ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * erc_row_scale_fubini_total_universal_reduced_outer_witness)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand. erc_row_code_fubini_total_universal_reduced_outer_witness = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * erc_row_scale_fubini_total_universal_reduced_outer_witness) + (ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor. ff_u_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_sum)) * ff_v_erc_fubini_total_universal_reduced_outer_witness_count_sum) + (ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_universal_reduced_outer_witness_count_sum = ff_r_erc_fubini_total_universal_reduced_outer_witness_count_sum + ff_a_erc_fubini_total_universal_reduced_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_universal_reduced_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits = h) -> exists ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits)) * erc_row_scale_fubini_total_universal_reduced_outer_witness)) /\ exists ff_q_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded. erc_row_code_fubini_total_universal_reduced_outer_witness = ff_q_erc_fubini_total_universal_reduced_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_universal_reduced_outer_witness_count_bits)) * erc_row_scale_fubini_total_universal_reduced_outer_witness) + (ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_universal_reduced_outer_witness_count_bits = 1))))))))
0067specialize eisenstein_successor_row_split_reduced_rectangle_prefix q
0068specialize eisenstein_successor_row_split_reduced_rectangle_prefix p
0069specialize eisenstein_successor_row_split_reduced_rectangle_prefix h
0070specialize eisenstein_successor_row_split_reduced_rectangle_prefix (S h)
0071specialize eisenstein_successor_row_split_reduced_rectangle_prefix bb
0072specialize eisenstein_successor_row_split_reduced_rectangle_prefix bc
0073specialize eisenstein_successor_row_split_reduced_rectangle_prefix x
0074specialize eisenstein_successor_row_split_reduced_rectangle_prefix x1
0075specialize eisenstein_successor_row_split_reduced_rectangle_prefix x2
0076specialize eisenstein_successor_row_split_reduced_rectangle_prefix x3
0077specialize eisenstein_successor_row_split_reduced_rectangle_prefix k
0078apply eisenstein_successor_row_split_reduced_rectangle_prefix
0079exact hsplit_exists_witness_witness_witness_witness
0080have hreduced_sum : exists R. (exists ff_u_fubini_total_universal_reduced_sum ff_v_fubini_total_universal_reduced_sum. ((((exists ff_h_fubini_total_universal_reduced_sum_start. ff_h_fubini_total_universal_reduced_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_start. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_start * S ((S (0)) * ff_v_fubini_total_universal_reduced_sum) + (0))) /\ ((((exists ff_h_fubini_total_universal_reduced_sum_terminal. ff_h_fubini_total_universal_reduced_sum_terminal + S (R) = S ((S (k)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_terminal. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_terminal * S ((S (k)) * ff_v_fubini_total_universal_reduced_sum) + (R))) /\ forall ff_i_fubini_total_universal_reduced_sum. (exists ff_lt_fubini_total_universal_reduced_sum_bound. ff_lt_fubini_total_universal_reduced_sum_bound + S ff_i_fubini_total_universal_reduced_sum = k) -> exists ff_a_fubini_total_universal_reduced_sum ff_r_fubini_total_universal_reduced_sum ff_s_fubini_total_universal_reduced_sum. ((((exists ff_h_fubini_total_universal_reduced_sum_summand. ff_h_fubini_total_universal_reduced_sum_summand + S (ff_a_fubini_total_universal_reduced_sum) = S ((S (ff_i_fubini_total_universal_reduced_sum)) * x1)) /\ exists ff_q_fubini_total_universal_reduced_sum_summand. x = ff_q_fubini_total_universal_reduced_sum_summand * S ((S (ff_i_fubini_total_universal_reduced_sum)) * x1) + (ff_a_fubini_total_universal_reduced_sum))) /\ ((((exists ff_h_fubini_total_universal_reduced_sum_partial. ff_h_fubini_total_universal_reduced_sum_partial + S (ff_r_fubini_total_universal_reduced_sum) = S ((S (ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_partial. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_partial * S ((S (ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum) + (ff_r_fubini_total_universal_reduced_sum))) /\ ((((exists ff_h_fubini_total_universal_reduced_sum_successor. ff_h_fubini_total_universal_reduced_sum_successor + S (ff_s_fubini_total_universal_reduced_sum) = S ((S (S ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum)) /\ exists ff_q_fubini_total_universal_reduced_sum_successor. ff_u_fubini_total_universal_reduced_sum = ff_q_fubini_total_universal_reduced_sum_successor * S ((S (S ff_i_fubini_total_universal_reduced_sum)) * ff_v_fubini_total_universal_reduced_sum) + (ff_s_fubini_total_universal_reduced_sum))) /\ ff_s_fubini_total_universal_reduced_sum = ff_r_fubini_total_universal_reduced_sum + ff_a_fubini_total_universal_reduced_sum))))))
0081specialize beta_sum_exists x
0082specialize beta_sum_exists x1
0083specialize beta_sum_exists k
0084exact beta_sum_exists
0085cases hreduced_sum
0086have hterminal_sum : exists D. (exists ff_u_fubini_total_universal_terminal_sum ff_v_fubini_total_universal_terminal_sum. ((((exists ff_h_fubini_total_universal_terminal_sum_start. ff_h_fubini_total_universal_terminal_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_start. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_start * S ((S (0)) * ff_v_fubini_total_universal_terminal_sum) + (0))) /\ ((((exists ff_h_fubini_total_universal_terminal_sum_terminal. ff_h_fubini_total_universal_terminal_sum_terminal + S (D) = S ((S (k)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_terminal. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_terminal * S ((S (k)) * ff_v_fubini_total_universal_terminal_sum) + (D))) /\ forall ff_i_fubini_total_universal_terminal_sum. (exists ff_lt_fubini_total_universal_terminal_sum_bound. ff_lt_fubini_total_universal_terminal_sum_bound + S ff_i_fubini_total_universal_terminal_sum = k) -> exists ff_a_fubini_total_universal_terminal_sum ff_r_fubini_total_universal_terminal_sum ff_s_fubini_total_universal_terminal_sum. ((((exists ff_h_fubini_total_universal_terminal_sum_summand. ff_h_fubini_total_universal_terminal_sum_summand + S (ff_a_fubini_total_universal_terminal_sum) = S ((S (ff_i_fubini_total_universal_terminal_sum)) * x3)) /\ exists ff_q_fubini_total_universal_terminal_sum_summand. x2 = ff_q_fubini_total_universal_terminal_sum_summand * S ((S (ff_i_fubini_total_universal_terminal_sum)) * x3) + (ff_a_fubini_total_universal_terminal_sum))) /\ ((((exists ff_h_fubini_total_universal_terminal_sum_partial. ff_h_fubini_total_universal_terminal_sum_partial + S (ff_r_fubini_total_universal_terminal_sum) = S ((S (ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_partial. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_partial * S ((S (ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum) + (ff_r_fubini_total_universal_terminal_sum))) /\ ((((exists ff_h_fubini_total_universal_terminal_sum_successor. ff_h_fubini_total_universal_terminal_sum_successor + S (ff_s_fubini_total_universal_terminal_sum) = S ((S (S ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum)) /\ exists ff_q_fubini_total_universal_terminal_sum_successor. ff_u_fubini_total_universal_terminal_sum = ff_q_fubini_total_universal_terminal_sum_successor * S ((S (S ff_i_fubini_total_universal_terminal_sum)) * ff_v_fubini_total_universal_terminal_sum) + (ff_s_fubini_total_universal_terminal_sum))) /\ ff_s_fubini_total_universal_terminal_sum = ff_r_fubini_total_universal_terminal_sum + ff_a_fubini_total_universal_terminal_sum))))))
0087specialize beta_sum_exists x2
0088specialize beta_sum_exists x3
0089specialize beta_sum_exists k
0090exact beta_sum_exists
0091cases hterminal_sum
0092have hsource_add : x4 + x5 = T
0093specialize eisenstein_successor_row_split_sum_add q
0094specialize eisenstein_successor_row_split_sum_add p
0095specialize eisenstein_successor_row_split_sum_add h
0096specialize eisenstein_successor_row_split_sum_add (S h)
0097specialize eisenstein_successor_row_split_sum_add bb
0098specialize eisenstein_successor_row_split_sum_add bc
0099specialize eisenstein_successor_row_split_sum_add x
0100specialize eisenstein_successor_row_split_sum_add x1
0101specialize eisenstein_successor_row_split_sum_add x2
0102specialize eisenstein_successor_row_split_sum_add x3
0103specialize eisenstein_successor_row_split_sum_add k
0104specialize eisenstein_successor_row_split_sum_add x4
0105specialize eisenstein_successor_row_split_sum_add x5
0106specialize eisenstein_successor_row_split_sum_add T
0107apply eisenstein_successor_row_split_sum_add
0108exact hsplit_exists_witness_witness_witness_witness
0109exact hreduced_sum_witness
0110exact hterminal_sum_witness
0111exact houtersum
0112have hrestricted_columns : forall eft_fixed_index_fubini_total_universal_restricted_columns. (exists edt_lt_gap_eft_fubini_total_universal_restricted_columns_bound. edt_lt_gap_eft_fubini_total_universal_restricted_columns_bound + S (eft_fixed_index_fubini_total_universal_restricted_columns) = h) -> exists eft_count_fubini_total_universal_restricted_columns. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_decoded. ff_h_eft_fubini_total_universal_restricted_columns_decoded + S (eft_count_fubini_total_universal_restricted_columns) = S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * dc)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_decoded. db = ff_q_eft_fubini_total_universal_restricted_columns_decoded * S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * dc) + (eft_count_fubini_total_universal_restricted_columns))) /\ (exists eft_column_code_fubini_total_universal_restricted_columns_witness eft_column_scale_fubini_total_universal_restricted_columns_witness. ((forall etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column. (exists edt_lt_gap_eft_fubini_total_universal_restricted_columns_witness_column_bound. edt_lt_gap_eft_fubini_total_universal_restricted_columns_witness_column_bound + S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) = k) -> exists etc_bit_eft_fubini_total_universal_restricted_columns_witness_column. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded + S (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column) = S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * eft_column_scale_fubini_total_universal_restricted_columns_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded. eft_column_code_fubini_total_universal_restricted_columns_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * eft_column_scale_fubini_total_universal_restricted_columns_witness) + (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column))) /\ (exists etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * bc)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry. bb = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column)) * bc) + (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = S h) -> exists eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_eri_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column))) \/ (eri_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_restricted_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness) = S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_terminal * S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_universal_restricted_columns_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = S h) -> exists ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits = S h) -> exists ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column) = S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_universal_restricted_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_restricted_columns_witness_column_witness_inner_entry * S ((S (eft_fixed_index_fubini_total_universal_restricted_columns)) * etc_row_scale_eft_fubini_total_universal_restricted_columns_witness_column_witness) + (etc_bit_eft_fubini_total_universal_restricted_columns_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_start. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_start. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal + S (eft_count_fubini_total_universal_restricted_columns) = S ((S (k)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (eft_count_fubini_total_universal_restricted_columns))) /\ forall ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum. (exists ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_sum_bound. ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_sum_bound + S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum = k) -> exists ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand + S (ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_restricted_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand. eft_column_code_fubini_total_universal_restricted_columns_witness = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_restricted_columns_witness) + (ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial + S (ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor + S (ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor. ff_u_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_restricted_columns_witness_count_sum) + (ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum))) /\ ff_s_eft_fubini_total_universal_restricted_columns_witness_count_sum = ff_r_eft_fubini_total_universal_restricted_columns_witness_count_sum + ff_a_eft_fubini_total_universal_restricted_columns_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits. (exists ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_bits_bound. ff_lt_eft_fubini_total_universal_restricted_columns_witness_count_bits_bound + S ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits. ((((exists ff_h_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded. ff_h_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits) = S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_restricted_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded. eft_column_code_fubini_total_universal_restricted_columns_witness = ff_q_eft_fubini_total_universal_restricted_columns_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_universal_restricted_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_restricted_columns_witness) + (ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits))) /\ (ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_universal_restricted_columns_witness_count_bits = 1))))))))
0113specialize eisenstein_fubini_column_count_prefix_succ_restrict p
0114specialize eisenstein_fubini_column_count_prefix_succ_restrict q
0115specialize eisenstein_fubini_column_count_prefix_succ_restrict h
0116specialize eisenstein_fubini_column_count_prefix_succ_restrict (S h)
0117specialize eisenstein_fubini_column_count_prefix_succ_restrict bb
0118specialize eisenstein_fubini_column_count_prefix_succ_restrict bc
0119specialize eisenstein_fubini_column_count_prefix_succ_restrict db
0120specialize eisenstein_fubini_column_count_prefix_succ_restrict dc
0121specialize eisenstein_fubini_column_count_prefix_succ_restrict k
0122apply eisenstein_fubini_column_count_prefix_succ_restrict
0123refl
0124exact hcolumns
0125have hreduced_columns : forall eft_fixed_index_fubini_total_universal_reduced_columns. (exists edt_lt_gap_eft_fubini_total_universal_reduced_columns_bound. edt_lt_gap_eft_fubini_total_universal_reduced_columns_bound + S (eft_fixed_index_fubini_total_universal_reduced_columns) = h) -> exists eft_count_fubini_total_universal_reduced_columns. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_decoded. ff_h_eft_fubini_total_universal_reduced_columns_decoded + S (eft_count_fubini_total_universal_reduced_columns) = S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * dc)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_decoded. db = ff_q_eft_fubini_total_universal_reduced_columns_decoded * S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * dc) + (eft_count_fubini_total_universal_reduced_columns))) /\ (exists eft_column_code_fubini_total_universal_reduced_columns_witness eft_column_scale_fubini_total_universal_reduced_columns_witness. ((forall etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column. (exists edt_lt_gap_eft_fubini_total_universal_reduced_columns_witness_column_bound. edt_lt_gap_eft_fubini_total_universal_reduced_columns_witness_column_bound + S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) = k) -> exists etc_bit_eft_fubini_total_universal_reduced_columns_witness_column. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded + S (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column) = S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * eft_column_scale_fubini_total_universal_reduced_columns_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded. eft_column_code_fubini_total_universal_reduced_columns_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * eft_column_scale_fubini_total_universal_reduced_columns_witness) + (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column))) /\ (exists etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * x1)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry. x = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column)) * x1) + (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = h) -> exists eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_eri_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column))) \/ (eri_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_reduced_columns_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness) = S ((S (h)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_universal_reduced_columns_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column) = S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_universal_reduced_columns_witness_column_witness = ff_q_etc_eft_fubini_total_universal_reduced_columns_witness_column_witness_inner_entry * S ((S (eft_fixed_index_fubini_total_universal_reduced_columns)) * etc_row_scale_eft_fubini_total_universal_reduced_columns_witness_column_witness) + (etc_bit_eft_fubini_total_universal_reduced_columns_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_start. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_start. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal + S (eft_count_fubini_total_universal_reduced_columns) = S ((S (k)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (eft_count_fubini_total_universal_reduced_columns))) /\ forall ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum. (exists ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_sum_bound. ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_sum_bound + S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum = k) -> exists ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand + S (ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_reduced_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand. eft_column_code_fubini_total_universal_reduced_columns_witness = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * eft_column_scale_fubini_total_universal_reduced_columns_witness) + (ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial + S (ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor + S (ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor. ff_u_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_sum)) * ff_v_eft_fubini_total_universal_reduced_columns_witness_count_sum) + (ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum))) /\ ff_s_eft_fubini_total_universal_reduced_columns_witness_count_sum = ff_r_eft_fubini_total_universal_reduced_columns_witness_count_sum + ff_a_eft_fubini_total_universal_reduced_columns_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits. (exists ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_bits_bound. ff_lt_eft_fubini_total_universal_reduced_columns_witness_count_bits_bound + S ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits. ((((exists ff_h_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded. ff_h_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits) = S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_reduced_columns_witness)) /\ exists ff_q_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded. eft_column_code_fubini_total_universal_reduced_columns_witness = ff_q_eft_fubini_total_universal_reduced_columns_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_universal_reduced_columns_witness_count_bits)) * eft_column_scale_fubini_total_universal_reduced_columns_witness) + (ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits))) /\ (ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_universal_reduced_columns_witness_count_bits = 1))))))))
0126specialize eisenstein_fubini_column_count_prefix_retarget_predecessor p
0127specialize eisenstein_fubini_column_count_prefix_retarget_predecessor q
0128specialize eisenstein_fubini_column_count_prefix_retarget_predecessor h
0129specialize eisenstein_fubini_column_count_prefix_retarget_predecessor (S h)
0130specialize eisenstein_fubini_column_count_prefix_retarget_predecessor bb
0131specialize eisenstein_fubini_column_count_prefix_retarget_predecessor bc
0132specialize eisenstein_fubini_column_count_prefix_retarget_predecessor x
0133specialize eisenstein_fubini_column_count_prefix_retarget_predecessor x1
0134specialize eisenstein_fubini_column_count_prefix_retarget_predecessor db
0135specialize eisenstein_fubini_column_count_prefix_retarget_predecessor dc
0136specialize eisenstein_fubini_column_count_prefix_retarget_predecessor k
0137apply eisenstein_fubini_column_count_prefix_retarget_predecessor
0138refl
0139exact hreduced_outer
0140exact hrestricted_columns
0141have hsum_decompose : exists a r. ((((exists ff_h_fubini_total_universal_column_last_entry. ff_h_fubini_total_universal_column_last_entry + S (a) = S ((S (h)) * dc)) /\ exists ff_q_fubini_total_universal_column_last_entry. db = ff_q_fubini_total_universal_column_last_entry * S ((S (h)) * dc) + (a))) /\ ((exists ff_u_fubini_total_universal_column_prefix_sum ff_v_fubini_total_universal_column_prefix_sum. ((((exists ff_h_fubini_total_universal_column_prefix_sum_start. ff_h_fubini_total_universal_column_prefix_sum_start + S (0) = S ((S (0)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_start. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_start * S ((S (0)) * ff_v_fubini_total_universal_column_prefix_sum) + (0))) /\ ((((exists ff_h_fubini_total_universal_column_prefix_sum_terminal. ff_h_fubini_total_universal_column_prefix_sum_terminal + S (r) = S ((S (h)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_terminal. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_terminal * S ((S (h)) * ff_v_fubini_total_universal_column_prefix_sum) + (r))) /\ forall ff_i_fubini_total_universal_column_prefix_sum. (exists ff_lt_fubini_total_universal_column_prefix_sum_bound. ff_lt_fubini_total_universal_column_prefix_sum_bound + S ff_i_fubini_total_universal_column_prefix_sum = h) -> exists ff_a_fubini_total_universal_column_prefix_sum ff_r_fubini_total_universal_column_prefix_sum ff_s_fubini_total_universal_column_prefix_sum. ((((exists ff_h_fubini_total_universal_column_prefix_sum_summand. ff_h_fubini_total_universal_column_prefix_sum_summand + S (ff_a_fubini_total_universal_column_prefix_sum) = S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * dc)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_summand. db = ff_q_fubini_total_universal_column_prefix_sum_summand * S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * dc) + (ff_a_fubini_total_universal_column_prefix_sum))) /\ ((((exists ff_h_fubini_total_universal_column_prefix_sum_partial. ff_h_fubini_total_universal_column_prefix_sum_partial + S (ff_r_fubini_total_universal_column_prefix_sum) = S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_partial. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_partial * S ((S (ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum) + (ff_r_fubini_total_universal_column_prefix_sum))) /\ ((((exists ff_h_fubini_total_universal_column_prefix_sum_successor. ff_h_fubini_total_universal_column_prefix_sum_successor + S (ff_s_fubini_total_universal_column_prefix_sum) = S ((S (S ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum)) /\ exists ff_q_fubini_total_universal_column_prefix_sum_successor. ff_u_fubini_total_universal_column_prefix_sum = ff_q_fubini_total_universal_column_prefix_sum_successor * S ((S (S ff_i_fubini_total_universal_column_prefix_sum)) * ff_v_fubini_total_universal_column_prefix_sum) + (ff_s_fubini_total_universal_column_prefix_sum))) /\ ff_s_fubini_total_universal_column_prefix_sum = ff_r_fubini_total_universal_column_prefix_sum + ff_a_fubini_total_universal_column_prefix_sum)))))) /\ M = r + a))
0142specialize beta_sum_succ_decompose db
0143specialize beta_sum_succ_decompose dc
0144specialize beta_sum_succ_decompose h
0145specialize beta_sum_succ_decompose M
0146apply beta_sum_succ_decompose
0147exact hcolumnsum
0148cases hsum_decompose
0149cases hsum_decompose_witness
0150cases hsum_decompose_witness_witness
0151cases hsum_decompose_witness_witness_right
0152have hih : x7 = x4
0153specialize IH p
0154specialize IH q
0155specialize IH k
0156specialize IH x
0157specialize IH x1
0158specialize IH db
0159specialize IH dc
0160specialize IH x4
0161specialize IH x7
0162apply IH
0163exact hreduced_outer
0164exact hreduced_columns
0165exact hreduced_sum_witness
0166exact hsum_decompose_witness_witness_right_left
0167have hlast_stored : exists n. ((((exists ff_h_fubini_total_universal_last_stored_entry. ff_h_fubini_total_universal_last_stored_entry + S (n) = S ((S (h)) * dc)) /\ exists ff_q_fubini_total_universal_last_stored_entry. db = ff_q_fubini_total_universal_last_stored_entry * S ((S (h)) * dc) + (n))) /\ (exists eft_column_code_fubini_total_universal_last_stored_witness eft_column_scale_fubini_total_universal_last_stored_witness. ((forall etc_row_index_eft_fubini_total_universal_last_stored_witness_column. (exists edt_lt_gap_eft_fubini_total_universal_last_stored_witness_column_bound. edt_lt_gap_eft_fubini_total_universal_last_stored_witness_column_bound + S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column) = k) -> exists etc_bit_eft_fubini_total_universal_last_stored_witness_column. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_decoded. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_decoded + S (etc_bit_eft_fubini_total_universal_last_stored_witness_column) = S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * eft_column_scale_fubini_total_universal_last_stored_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_decoded. eft_column_code_fubini_total_universal_last_stored_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_decoded * S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * eft_column_scale_fubini_total_universal_last_stored_witness) + (etc_bit_eft_fubini_total_universal_last_stored_witness_column))) /\ (exists etc_count_eft_fubini_total_universal_last_stored_witness_column_witness etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness. ((((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry + S (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness) = S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * bc)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry. bb = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_universal_last_stored_witness_column)) * bc) + (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row. (exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_bound. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = S h) -> exists eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_eri_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column))) \/ (eri_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row) = p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column) /\ ~(exists eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_universal_last_stored_witness_column) = q * S eri_column_etc_eft_fubini_total_universal_last_stored_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness) = S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_terminal * S ((S (S h)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_universal_last_stored_witness_column_witness))) /\ forall ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = S h) -> exists ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits = S h) -> exists ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_universal_last_stored_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry. ff_h_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry + S (etc_bit_eft_fubini_total_universal_last_stored_witness_column) = S ((S (h)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness)) /\ exists ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry. etc_row_code_eft_fubini_total_universal_last_stored_witness_column_witness = ff_q_etc_eft_fubini_total_universal_last_stored_witness_column_witness_inner_entry * S ((S (h)) * etc_row_scale_eft_fubini_total_universal_last_stored_witness_column_witness) + (etc_bit_eft_fubini_total_universal_last_stored_witness_column))))))) /\ (((exists ff_u_eft_fubini_total_universal_last_stored_witness_count_sum ff_v_eft_fubini_total_universal_last_stored_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_start. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_start. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_terminal. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_terminal + S (n) = S ((S (k)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_terminal. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (n))) /\ forall ff_i_eft_fubini_total_universal_last_stored_witness_count_sum. (exists ff_lt_eft_fubini_total_universal_last_stored_witness_count_sum_bound. ff_lt_eft_fubini_total_universal_last_stored_witness_count_sum_bound + S ff_i_eft_fubini_total_universal_last_stored_witness_count_sum = k) -> exists ff_a_eft_fubini_total_universal_last_stored_witness_count_sum ff_r_eft_fubini_total_universal_last_stored_witness_count_sum ff_s_eft_fubini_total_universal_last_stored_witness_count_sum. ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_summand. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_summand + S (ff_a_eft_fubini_total_universal_last_stored_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * eft_column_scale_fubini_total_universal_last_stored_witness)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_summand. eft_column_code_fubini_total_universal_last_stored_witness = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_summand * S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * eft_column_scale_fubini_total_universal_last_stored_witness) + (ff_a_eft_fubini_total_universal_last_stored_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_partial. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_partial + S (ff_r_eft_fubini_total_universal_last_stored_witness_count_sum) = S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_partial. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_partial * S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (ff_r_eft_fubini_total_universal_last_stored_witness_count_sum))) /\ ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_successor. ff_h_eft_fubini_total_universal_last_stored_witness_count_sum_successor + S (ff_s_eft_fubini_total_universal_last_stored_witness_count_sum) = S ((S (S ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_successor. ff_u_eft_fubini_total_universal_last_stored_witness_count_sum = ff_q_eft_fubini_total_universal_last_stored_witness_count_sum_successor * S ((S (S ff_i_eft_fubini_total_universal_last_stored_witness_count_sum)) * ff_v_eft_fubini_total_universal_last_stored_witness_count_sum) + (ff_s_eft_fubini_total_universal_last_stored_witness_count_sum))) /\ ff_s_eft_fubini_total_universal_last_stored_witness_count_sum = ff_r_eft_fubini_total_universal_last_stored_witness_count_sum + ff_a_eft_fubini_total_universal_last_stored_witness_count_sum)))))) /\ (forall ff_i_eft_fubini_total_universal_last_stored_witness_count_bits. (exists ff_lt_eft_fubini_total_universal_last_stored_witness_count_bits_bound. ff_lt_eft_fubini_total_universal_last_stored_witness_count_bits_bound + S ff_i_eft_fubini_total_universal_last_stored_witness_count_bits = k) -> exists ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits. ((((exists ff_h_eft_fubini_total_universal_last_stored_witness_count_bits_decoded. ff_h_eft_fubini_total_universal_last_stored_witness_count_bits_decoded + S (ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits) = S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_bits)) * eft_column_scale_fubini_total_universal_last_stored_witness)) /\ exists ff_q_eft_fubini_total_universal_last_stored_witness_count_bits_decoded. eft_column_code_fubini_total_universal_last_stored_witness = ff_q_eft_fubini_total_universal_last_stored_witness_count_bits_decoded * S ((S (ff_i_eft_fubini_total_universal_last_stored_witness_count_bits)) * eft_column_scale_fubini_total_universal_last_stored_witness) + (ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits))) /\ (ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits = 0 \/ ff_bit_eft_fubini_total_universal_last_stored_witness_count_bits = 1))))))))
0168specialize hcolumns h
0169apply hcolumns
0170specialize le_refl (S h)
0171exact le_refl
0172cases hlast_stored
0173cases hlast_stored_witness
0174cases hlast_stored_witness_right
0175cases hlast_stored_witness_right_witness
0176cases hlast_stored_witness_right_witness_witness
0177cases hlast_stored_witness_right_witness_witness_right
0178have hcount_eq : x8 = x6
0179specialize beta_at_unique db
0180specialize beta_at_unique dc
0181specialize beta_at_unique h
0182specialize beta_at_unique x8
0183specialize beta_at_unique x6
0184apply beta_at_unique
0185exact hlast_stored_witness_left
0186exact hsum_decompose_witness_witness_left
0187have hterminal_eq : x5 = x8
0188specialize eisenstein_successor_terminal_sum_matches_last_column p
0189specialize eisenstein_successor_terminal_sum_matches_last_column q
0190specialize eisenstein_successor_terminal_sum_matches_last_column h
0191specialize eisenstein_successor_terminal_sum_matches_last_column (S h)
0192specialize eisenstein_successor_terminal_sum_matches_last_column bb
0193specialize eisenstein_successor_terminal_sum_matches_last_column bc
0194specialize eisenstein_successor_terminal_sum_matches_last_column x
0195specialize eisenstein_successor_terminal_sum_matches_last_column x1
0196specialize eisenstein_successor_terminal_sum_matches_last_column x2
0197specialize eisenstein_successor_terminal_sum_matches_last_column x3
0198specialize eisenstein_successor_terminal_sum_matches_last_column x9
0199specialize eisenstein_successor_terminal_sum_matches_last_column x10
0200specialize eisenstein_successor_terminal_sum_matches_last_column k
0201specialize eisenstein_successor_terminal_sum_matches_last_column x5
0202specialize eisenstein_successor_terminal_sum_matches_last_column x8
0203apply eisenstein_successor_terminal_sum_matches_last_column
0204refl
0205exact hsplit_exists_witness_witness_witness_witness
0206exact hlast_stored_witness_right_witness_witness_left
0207exact hterminal_sum_witness
0208exact hlast_stored_witness_right_witness_witness_right_left
0209have htotal : M = x4 + x5
0210rewrite hih at hsum_decompose_witness_witness_right_right
0211rewrite <- hcount_eq at hsum_decompose_witness_witness_right_right
0212rewrite <- hterminal_eq at hsum_decompose_witness_witness_right_right
0213exact hsum_decompose_witness_witness_right_right
0214trans x4 + x5
0215exact htotal
0216exact hsource_add