PA00EV

eisenstein_successor_row_split_choices

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

Every stored successor row constructively chooses an aligned reduced count and terminal bit.

Exact expanded PA statement

forall p q h sh bb bc l. sh = S h -> (forall erc_row_fubini_outer_decompose_prefix. (exists erc_lt_gap_fubini_outer_decompose_prefix_bound. erc_lt_gap_fubini_outer_decompose_prefix_bound + S (erc_row_fubini_outer_decompose_prefix) = l) -> exists erc_count_fubini_outer_decompose_prefix. ((((exists ff_h_erc_fubini_outer_decompose_prefix_decoded. ff_h_erc_fubini_outer_decompose_prefix_decoded + S (erc_count_fubini_outer_decompose_prefix) = S ((S (erc_row_fubini_outer_decompose_prefix)) * bc)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_decoded. bb = ff_q_erc_fubini_outer_decompose_prefix_decoded * S ((S (erc_row_fubini_outer_decompose_prefix)) * bc) + (erc_count_fubini_outer_decompose_prefix))) /\ (exists erc_row_code_fubini_outer_decompose_prefix_witness erc_row_scale_fubini_outer_decompose_prefix_witness. ((forall eri_column_erc_fubini_outer_decompose_prefix_witness_row. (exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_bound. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_bound + S (eri_column_erc_fubini_outer_decompose_prefix_witness_row) = sh) -> exists eri_bit_erc_fubini_outer_decompose_prefix_witness_row. ((((exists ff_h_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded. ff_h_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded + S (eri_bit_erc_fubini_outer_decompose_prefix_witness_row) = S ((S (eri_column_erc_fubini_outer_decompose_prefix_witness_row)) * erc_row_scale_fubini_outer_decompose_prefix_witness)) /\ exists ff_q_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded. erc_row_code_fubini_outer_decompose_prefix_witness = ff_q_eri_erc_fubini_outer_decompose_prefix_witness_row_decoded * S ((S (eri_column_erc_fubini_outer_decompose_prefix_witness_row)) * erc_row_scale_fubini_outer_decompose_prefix_witness) + (eri_bit_erc_fubini_outer_decompose_prefix_witness_row))) /\ (((eri_bit_erc_fubini_outer_decompose_prefix_witness_row = 0 /\ ((exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left + S (q * S erc_row_fubini_outer_decompose_prefix) = p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row) /\ ~(exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row) = q * S erc_row_fubini_outer_decompose_prefix))) \/ (eri_bit_erc_fubini_outer_decompose_prefix_witness_row = 1 /\ ((exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row) = q * S erc_row_fubini_outer_decompose_prefix) /\ ~(exists eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left. eri_gap_erc_fubini_outer_decompose_prefix_witness_row_choice_left + S (q * S erc_row_fubini_outer_decompose_prefix) = p * S eri_column_erc_fubini_outer_decompose_prefix_witness_row))))))) /\ (((exists ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_start. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_start. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal + S (erc_count_fubini_outer_decompose_prefix) = S ((S (sh)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_terminal * S ((S (sh)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (erc_count_fubini_outer_decompose_prefix))) /\ forall ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum. (exists ff_lt_erc_fubini_outer_decompose_prefix_witness_count_sum_bound. ff_lt_erc_fubini_outer_decompose_prefix_witness_count_sum_bound + S ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum = sh) -> exists ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_summand. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_summand + S (ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * erc_row_scale_fubini_outer_decompose_prefix_witness)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_summand. erc_row_code_fubini_outer_decompose_prefix_witness = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_summand * S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * erc_row_scale_fubini_outer_decompose_prefix_witness) + (ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_partial. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_partial + S (ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_partial. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_partial * S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_successor. ff_h_erc_fubini_outer_decompose_prefix_witness_count_sum_successor + S (ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum) = S ((S (S ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_successor. ff_u_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_q_erc_fubini_outer_decompose_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_outer_decompose_prefix_witness_count_sum)) * ff_v_erc_fubini_outer_decompose_prefix_witness_count_sum) + (ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum))) /\ ff_s_erc_fubini_outer_decompose_prefix_witness_count_sum = ff_r_erc_fubini_outer_decompose_prefix_witness_count_sum + ff_a_erc_fubini_outer_decompose_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits. (exists ff_lt_erc_fubini_outer_decompose_prefix_witness_count_bits_bound. ff_lt_erc_fubini_outer_decompose_prefix_witness_count_bits_bound + S ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits = sh) -> exists ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits. ((((exists ff_h_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded. ff_h_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded + S (ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits) = S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits)) * erc_row_scale_fubini_outer_decompose_prefix_witness)) /\ exists ff_q_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded. erc_row_code_fubini_outer_decompose_prefix_witness = ff_q_erc_fubini_outer_decompose_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_outer_decompose_prefix_witness_count_bits)) * erc_row_scale_fubini_outer_decompose_prefix_witness) + (ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits))) /\ (ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits = 0 \/ ff_bit_erc_fubini_outer_decompose_prefix_witness_count_bits = 1))))))))) -> (forall efrd_row_index_fubini_row_split_choices. (exists efrd_lt_gap_fubini_row_split_choices_bound. efrd_lt_gap_fubini_row_split_choices_bound + S (efrd_row_index_fubini_row_split_choices) = l) -> exists efrd_count_fubini_row_split_choices efrd_reduced_count_fubini_row_split_choices efrd_terminal_bit_fubini_row_split_choices. ((((exists ff_h_efrd_fubini_row_split_choices_outer_entry. ff_h_efrd_fubini_row_split_choices_outer_entry + S (efrd_count_fubini_row_split_choices) = S ((S (efrd_row_index_fubini_row_split_choices)) * bc)) /\ exists ff_q_efrd_fubini_row_split_choices_outer_entry. bb = ff_q_efrd_fubini_row_split_choices_outer_entry * S ((S (efrd_row_index_fubini_row_split_choices)) * bc) + (efrd_count_fubini_row_split_choices))) /\ (exists efrd_row_code_fubini_row_split_choices_split efrd_row_scale_fubini_row_split_choices_split. (((((forall eri_column_efrd_fubini_row_split_choices_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_choices_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_eri_efrd_fubini_row_split_choices_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_split) + (eri_bit_efrd_fubini_row_split_choices_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_choices))) \/ (eri_bit_efrd_fubini_row_split_choices_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_choices) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_choices_split_successor_count_sum ff_v_efrd_fubini_row_split_choices_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_choices) = S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (efrd_count_fubini_row_split_choices))) /\ forall ff_i_efrd_fubini_row_split_choices_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_choices_split_successor_count_sum ff_r_efrd_fubini_row_split_choices_split_successor_count_sum ff_s_efrd_fubini_row_split_choices_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_a_efrd_fubini_row_split_choices_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_choices_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_choices_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_choices_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_choices_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_split_successor_count_sum = ff_r_efrd_fubini_row_split_choices_split_successor_count_sum + ff_a_efrd_fubini_row_split_choices_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_choices_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_eri_efrd_fubini_row_split_choices_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_split) + (eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_choices))) \/ (eri_bit_efrd_fubini_row_split_choices_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_choices) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_choices) = p * S eri_column_efrd_fubini_row_split_choices_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_choices_split_terminal_entry. ff_h_efrd_fubini_row_split_choices_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_choices) = S ((S (h)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_terminal_entry. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_choices_split) + (efrd_terminal_bit_fubini_row_split_choices))))) /\ (((((exists ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_choices) = S ((S (h)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_choices))) /\ forall ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_choices_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_split_reduced_count_sum = ff_r_efrd_fubini_row_split_choices_split_reduced_count_sum + ff_a_efrd_fubini_row_split_choices_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_split)) /\ exists ff_q_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_choices_split = ff_q_efrd_fubini_row_split_choices_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_split) + (ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_choices = 0 \/ efrd_terminal_bit_fubini_row_split_choices = 1)) /\ efrd_count_fubini_row_split_choices = efrd_reduced_count_fubini_row_split_choices + efrd_terminal_bit_fubini_row_split_choices))))))

Structural proof guide

Generated structural guide

Every stored successor row constructively chooses an aligned reduced count and terminal bit.

Use the direct prerequisites eisenstein_successor_row_count_decompose as previously established PA formulas.

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

Referenced ingredients

PA00EU eisenstein_successor_row_count_decompose

Proof neighborhood

Direct dependencies

PA00EU eisenstein_successor_row_count_decompose

Direct dependents

PA00EY eisenstein_successor_rectangle_row_split_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro sh
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro l
  8. 0008intro hsh
  9. 0009intro houter
  10. 0010intro i
  11. 0011intro hi
  12. 0012have hstored : exists n. ((((exists ff_h_fubini_row_split_choices_stored_entry. ff_h_fubini_row_split_choices_stored_entry + S (n) = S ((S (i)) * bc)) /\ exists ff_q_fubini_row_split_choices_stored_entry. bb = ff_q_fubini_row_split_choices_stored_entry * S ((S (i)) * bc) + (n))) /\ (exists erc_row_code_fubini_row_split_choices_stored_witness erc_row_scale_fubini_row_split_choices_stored_witness. ((forall eri_column_erc_fubini_row_split_choices_stored_witness_row. (exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_bound. eri_gap_erc_fubini_row_split_choices_stored_witness_row_bound + S (eri_column_erc_fubini_row_split_choices_stored_witness_row) = sh) -> exists eri_bit_erc_fubini_row_split_choices_stored_witness_row. ((((exists ff_h_eri_erc_fubini_row_split_choices_stored_witness_row_decoded. ff_h_eri_erc_fubini_row_split_choices_stored_witness_row_decoded + S (eri_bit_erc_fubini_row_split_choices_stored_witness_row) = S ((S (eri_column_erc_fubini_row_split_choices_stored_witness_row)) * erc_row_scale_fubini_row_split_choices_stored_witness)) /\ exists ff_q_eri_erc_fubini_row_split_choices_stored_witness_row_decoded. erc_row_code_fubini_row_split_choices_stored_witness = ff_q_eri_erc_fubini_row_split_choices_stored_witness_row_decoded * S ((S (eri_column_erc_fubini_row_split_choices_stored_witness_row)) * erc_row_scale_fubini_row_split_choices_stored_witness) + (eri_bit_erc_fubini_row_split_choices_stored_witness_row))) /\ (((eri_bit_erc_fubini_row_split_choices_stored_witness_row = 0 /\ ((exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_row_split_choices_stored_witness_row) /\ ~(exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right + S (p * S eri_column_erc_fubini_row_split_choices_stored_witness_row) = q * S i))) \/ (eri_bit_erc_fubini_row_split_choices_stored_witness_row = 1 /\ ((exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_right + S (p * S eri_column_erc_fubini_row_split_choices_stored_witness_row) = q * S i) /\ ~(exists eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left. eri_gap_erc_fubini_row_split_choices_stored_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_row_split_choices_stored_witness_row))))))) /\ (((exists ff_u_erc_fubini_row_split_choices_stored_witness_count_sum ff_v_erc_fubini_row_split_choices_stored_witness_count_sum. ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_start. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_start. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_terminal. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_terminal + S (n) = S ((S (sh)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_terminal. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_terminal * S ((S (sh)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (n))) /\ forall ff_i_erc_fubini_row_split_choices_stored_witness_count_sum. (exists ff_lt_erc_fubini_row_split_choices_stored_witness_count_sum_bound. ff_lt_erc_fubini_row_split_choices_stored_witness_count_sum_bound + S ff_i_erc_fubini_row_split_choices_stored_witness_count_sum = sh) -> exists ff_a_erc_fubini_row_split_choices_stored_witness_count_sum ff_r_erc_fubini_row_split_choices_stored_witness_count_sum ff_s_erc_fubini_row_split_choices_stored_witness_count_sum. ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_summand. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_summand + S (ff_a_erc_fubini_row_split_choices_stored_witness_count_sum) = S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * erc_row_scale_fubini_row_split_choices_stored_witness)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_summand. erc_row_code_fubini_row_split_choices_stored_witness = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_summand * S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * erc_row_scale_fubini_row_split_choices_stored_witness) + (ff_a_erc_fubini_row_split_choices_stored_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_partial. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_partial + S (ff_r_erc_fubini_row_split_choices_stored_witness_count_sum) = S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_partial. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_partial * S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (ff_r_erc_fubini_row_split_choices_stored_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_successor. ff_h_erc_fubini_row_split_choices_stored_witness_count_sum_successor + S (ff_s_erc_fubini_row_split_choices_stored_witness_count_sum) = S ((S (S ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_successor. ff_u_erc_fubini_row_split_choices_stored_witness_count_sum = ff_q_erc_fubini_row_split_choices_stored_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_row_split_choices_stored_witness_count_sum)) * ff_v_erc_fubini_row_split_choices_stored_witness_count_sum) + (ff_s_erc_fubini_row_split_choices_stored_witness_count_sum))) /\ ff_s_erc_fubini_row_split_choices_stored_witness_count_sum = ff_r_erc_fubini_row_split_choices_stored_witness_count_sum + ff_a_erc_fubini_row_split_choices_stored_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_row_split_choices_stored_witness_count_bits. (exists ff_lt_erc_fubini_row_split_choices_stored_witness_count_bits_bound. ff_lt_erc_fubini_row_split_choices_stored_witness_count_bits_bound + S ff_i_erc_fubini_row_split_choices_stored_witness_count_bits = sh) -> exists ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits. ((((exists ff_h_erc_fubini_row_split_choices_stored_witness_count_bits_decoded. ff_h_erc_fubini_row_split_choices_stored_witness_count_bits_decoded + S (ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits) = S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_bits)) * erc_row_scale_fubini_row_split_choices_stored_witness)) /\ exists ff_q_erc_fubini_row_split_choices_stored_witness_count_bits_decoded. erc_row_code_fubini_row_split_choices_stored_witness = ff_q_erc_fubini_row_split_choices_stored_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_row_split_choices_stored_witness_count_bits)) * erc_row_scale_fubini_row_split_choices_stored_witness) + (ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits))) /\ (ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits = 0 \/ ff_bit_erc_fubini_row_split_choices_stored_witness_count_bits = 1))))))))
  13. 0013specialize houter i
  14. 0014apply houter
  15. 0015exact hi
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018have hsplit : exists efrd_terminal_bit_fubini_row_split_choices_decomposition efrd_reduced_count_fubini_row_split_choices_decomposition. (exists efrd_row_code_fubini_row_split_choices_decomposition_split efrd_row_scale_fubini_row_split_choices_decomposition_split. (((((forall eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_choices_decomposition_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal + S (x) = S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (x))) /\ forall ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum = ff_r_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum + ff_a_efrd_fubini_row_split_choices_decomposition_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_decomposition_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_eri_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_choices_decomposition_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_terminal_entry. ff_h_efrd_fubini_row_split_choices_decomposition_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_choices_decomposition) = S ((S (h)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_terminal_entry. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (efrd_terminal_bit_fubini_row_split_choices_decomposition))))) /\ (((((exists ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_choices_decomposition) = S ((S (h)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_choices_decomposition))) /\ forall ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum = ff_r_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum + ff_a_efrd_fubini_row_split_choices_decomposition_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split)) /\ exists ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_choices_decomposition_split = ff_q_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_choices_decomposition_split) + (ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_choices_decomposition_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_choices_decomposition = 0 \/ efrd_terminal_bit_fubini_row_split_choices_decomposition = 1)) /\ x = efrd_reduced_count_fubini_row_split_choices_decomposition + efrd_terminal_bit_fubini_row_split_choices_decomposition))))
  19. 0019specialize eisenstein_successor_row_count_decompose p
  20. 0020specialize eisenstein_successor_row_count_decompose q
  21. 0021specialize eisenstein_successor_row_count_decompose h
  22. 0022specialize eisenstein_successor_row_count_decompose sh
  23. 0023specialize eisenstein_successor_row_count_decompose i
  24. 0024specialize eisenstein_successor_row_count_decompose x
  25. 0025apply eisenstein_successor_row_count_decompose
  26. 0026exact hsh
  27. 0027exact hstored_witness_right
  28. 0028cases hsplit
  29. 0029cases hsplit_witness
  30. 0030exists x
  31. 0031exists x2
  32. 0032exists x1
  33. 0033split
  34. 0034exact hstored_witness_left
  35. 0035exact hsplit_witness_witness