PA00F0

eisenstein_successor_row_split_reduced_rectangle_prefix

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

The reduced-count code in a split prefix is itself a semantic predecessor-width rectangle prefix.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall p q h sh bb bc db dc tb tc l. (forall efrd_row_index_fubini_reduced_projection_split. (exists efrd_lt_gap_fubini_reduced_projection_split_bound. efrd_lt_gap_fubini_reduced_projection_split_bound + S (efrd_row_index_fubini_reduced_projection_split) = l) -> exists efrd_count_fubini_reduced_projection_split efrd_reduced_count_fubini_reduced_projection_split efrd_terminal_bit_fubini_reduced_projection_split. (((((((exists ff_h_efrd_fubini_reduced_projection_split_entry_outer_entry. ff_h_efrd_fubini_reduced_projection_split_entry_outer_entry + S (efrd_count_fubini_reduced_projection_split) = S ((S (efrd_row_index_fubini_reduced_projection_split)) * bc)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_outer_entry. bb = ff_q_efrd_fubini_reduced_projection_split_entry_outer_entry * S ((S (efrd_row_index_fubini_reduced_projection_split)) * bc) + (efrd_count_fubini_reduced_projection_split))) /\ (((exists ff_h_efrd_fubini_reduced_projection_split_entry_reduced_entry. ff_h_efrd_fubini_reduced_projection_split_entry_reduced_entry + S (efrd_reduced_count_fubini_reduced_projection_split) = S ((S (efrd_row_index_fubini_reduced_projection_split)) * dc)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_reduced_entry. db = ff_q_efrd_fubini_reduced_projection_split_entry_reduced_entry * S ((S (efrd_row_index_fubini_reduced_projection_split)) * dc) + (efrd_reduced_count_fubini_reduced_projection_split)))) /\ (((exists ff_h_efrd_fubini_reduced_projection_split_entry_terminal_entry. ff_h_efrd_fubini_reduced_projection_split_entry_terminal_entry + S (efrd_terminal_bit_fubini_reduced_projection_split) = S ((S (efrd_row_index_fubini_reduced_projection_split)) * tc)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_terminal_entry. tb = ff_q_efrd_fubini_reduced_projection_split_entry_terminal_entry * S ((S (efrd_row_index_fubini_reduced_projection_split)) * tc) + (efrd_terminal_bit_fubini_reduced_projection_split)))) /\ (exists efrd_row_code_fubini_reduced_projection_split_entry_split efrd_row_scale_fubini_reduced_projection_split_entry_split. (((((forall eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_reduced_projection_split_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_reduced_projection_split_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_eri_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_decoded. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_eri_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (eri_bit_efrd_fubini_reduced_projection_split_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_reduced_projection_split_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_reduced_projection_split) = p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix) = q * S efrd_row_index_fubini_reduced_projection_split))) \/ (eri_bit_efrd_fubini_reduced_projection_split_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix) = q * S efrd_row_index_fubini_reduced_projection_split) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_split_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_reduced_projection_split) = p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_start. ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_start. ff_u_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_reduced_projection_split) = S ((S (sh)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) + (efrd_count_fubini_reduced_projection_split))) /\ forall ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum ff_r_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum ff_s_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_summand. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (ff_a_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) + (ff_r_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum) + (ff_s_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum = ff_r_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum + ff_a_efrd_fubini_reduced_projection_split_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (ff_bit_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_reduced_projection_split_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_eri_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_eri_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (eri_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_reduced_projection_split) = p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_reduced_projection_split))) \/ (eri_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_reduced_projection_split) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_reduced_projection_split) = p * S eri_column_efrd_fubini_reduced_projection_split_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_terminal_entry. ff_h_efrd_fubini_reduced_projection_split_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_reduced_projection_split) = S ((S (h)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_terminal_entry. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_efrd_fubini_reduced_projection_split_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (efrd_terminal_bit_fubini_reduced_projection_split))))) /\ (((((exists ff_u_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_reduced_projection_split) = S ((S (h)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_reduced_projection_split))) /\ forall ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum ff_r_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum ff_s_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (ff_a_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum = ff_r_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum + ff_a_efrd_fubini_reduced_projection_split_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_reduced_projection_split_entry_split)) /\ exists ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_reduced_projection_split_entry_split = ff_q_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_reduced_projection_split_entry_split) + (ff_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_reduced_projection_split_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_reduced_projection_split = 0 \/ efrd_terminal_bit_fubini_reduced_projection_split = 1)) /\ efrd_count_fubini_reduced_projection_split = efrd_reduced_count_fubini_reduced_projection_split + efrd_terminal_bit_fubini_reduced_projection_split))))))) -> (forall erc_row_fubini_reduced_projection_rectangle. (exists erc_lt_gap_fubini_reduced_projection_rectangle_bound. erc_lt_gap_fubini_reduced_projection_rectangle_bound + S (erc_row_fubini_reduced_projection_rectangle) = l) -> exists erc_count_fubini_reduced_projection_rectangle. ((((exists ff_h_erc_fubini_reduced_projection_rectangle_decoded. ff_h_erc_fubini_reduced_projection_rectangle_decoded + S (erc_count_fubini_reduced_projection_rectangle) = S ((S (erc_row_fubini_reduced_projection_rectangle)) * dc)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_decoded. db = ff_q_erc_fubini_reduced_projection_rectangle_decoded * S ((S (erc_row_fubini_reduced_projection_rectangle)) * dc) + (erc_count_fubini_reduced_projection_rectangle))) /\ (exists erc_row_code_fubini_reduced_projection_rectangle_witness erc_row_scale_fubini_reduced_projection_rectangle_witness. ((forall eri_column_erc_fubini_reduced_projection_rectangle_witness_row. (exists eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_bound. eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_bound + S (eri_column_erc_fubini_reduced_projection_rectangle_witness_row) = h) -> exists eri_bit_erc_fubini_reduced_projection_rectangle_witness_row. ((((exists ff_h_eri_erc_fubini_reduced_projection_rectangle_witness_row_decoded. ff_h_eri_erc_fubini_reduced_projection_rectangle_witness_row_decoded + S (eri_bit_erc_fubini_reduced_projection_rectangle_witness_row) = S ((S (eri_column_erc_fubini_reduced_projection_rectangle_witness_row)) * erc_row_scale_fubini_reduced_projection_rectangle_witness)) /\ exists ff_q_eri_erc_fubini_reduced_projection_rectangle_witness_row_decoded. erc_row_code_fubini_reduced_projection_rectangle_witness = ff_q_eri_erc_fubini_reduced_projection_rectangle_witness_row_decoded * S ((S (eri_column_erc_fubini_reduced_projection_rectangle_witness_row)) * erc_row_scale_fubini_reduced_projection_rectangle_witness) + (eri_bit_erc_fubini_reduced_projection_rectangle_witness_row))) /\ (((eri_bit_erc_fubini_reduced_projection_rectangle_witness_row = 0 /\ ((exists eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_left. eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_left + S (q * S erc_row_fubini_reduced_projection_rectangle) = p * S eri_column_erc_fubini_reduced_projection_rectangle_witness_row) /\ ~(exists eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_right. eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_right + S (p * S eri_column_erc_fubini_reduced_projection_rectangle_witness_row) = q * S erc_row_fubini_reduced_projection_rectangle))) \/ (eri_bit_erc_fubini_reduced_projection_rectangle_witness_row = 1 /\ ((exists eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_right. eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_right + S (p * S eri_column_erc_fubini_reduced_projection_rectangle_witness_row) = q * S erc_row_fubini_reduced_projection_rectangle) /\ ~(exists eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_left. eri_gap_erc_fubini_reduced_projection_rectangle_witness_row_choice_left + S (q * S erc_row_fubini_reduced_projection_rectangle) = p * S eri_column_erc_fubini_reduced_projection_rectangle_witness_row))))))) /\ (((exists ff_u_erc_fubini_reduced_projection_rectangle_witness_count_sum ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum. ((((exists ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_start. ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_start. ff_u_erc_fubini_reduced_projection_rectangle_witness_count_sum = ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_terminal. ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_terminal + S (erc_count_fubini_reduced_projection_rectangle) = S ((S (h)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_terminal. ff_u_erc_fubini_reduced_projection_rectangle_witness_count_sum = ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum) + (erc_count_fubini_reduced_projection_rectangle))) /\ forall ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum. (exists ff_lt_erc_fubini_reduced_projection_rectangle_witness_count_sum_bound. ff_lt_erc_fubini_reduced_projection_rectangle_witness_count_sum_bound + S ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum = h) -> exists ff_a_erc_fubini_reduced_projection_rectangle_witness_count_sum ff_r_erc_fubini_reduced_projection_rectangle_witness_count_sum ff_s_erc_fubini_reduced_projection_rectangle_witness_count_sum. ((((exists ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_summand. ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_summand + S (ff_a_erc_fubini_reduced_projection_rectangle_witness_count_sum) = S ((S (ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum)) * erc_row_scale_fubini_reduced_projection_rectangle_witness)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_summand. erc_row_code_fubini_reduced_projection_rectangle_witness = ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_summand * S ((S (ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum)) * erc_row_scale_fubini_reduced_projection_rectangle_witness) + (ff_a_erc_fubini_reduced_projection_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_partial. ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_partial + S (ff_r_erc_fubini_reduced_projection_rectangle_witness_count_sum) = S ((S (ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_partial. ff_u_erc_fubini_reduced_projection_rectangle_witness_count_sum = ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_partial * S ((S (ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum) + (ff_r_erc_fubini_reduced_projection_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_successor. ff_h_erc_fubini_reduced_projection_rectangle_witness_count_sum_successor + S (ff_s_erc_fubini_reduced_projection_rectangle_witness_count_sum) = S ((S (S ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_successor. ff_u_erc_fubini_reduced_projection_rectangle_witness_count_sum = ff_q_erc_fubini_reduced_projection_rectangle_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_reduced_projection_rectangle_witness_count_sum)) * ff_v_erc_fubini_reduced_projection_rectangle_witness_count_sum) + (ff_s_erc_fubini_reduced_projection_rectangle_witness_count_sum))) /\ ff_s_erc_fubini_reduced_projection_rectangle_witness_count_sum = ff_r_erc_fubini_reduced_projection_rectangle_witness_count_sum + ff_a_erc_fubini_reduced_projection_rectangle_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_reduced_projection_rectangle_witness_count_bits. (exists ff_lt_erc_fubini_reduced_projection_rectangle_witness_count_bits_bound. ff_lt_erc_fubini_reduced_projection_rectangle_witness_count_bits_bound + S ff_i_erc_fubini_reduced_projection_rectangle_witness_count_bits = h) -> exists ff_bit_erc_fubini_reduced_projection_rectangle_witness_count_bits. ((((exists ff_h_erc_fubini_reduced_projection_rectangle_witness_count_bits_decoded. ff_h_erc_fubini_reduced_projection_rectangle_witness_count_bits_decoded + S (ff_bit_erc_fubini_reduced_projection_rectangle_witness_count_bits) = S ((S (ff_i_erc_fubini_reduced_projection_rectangle_witness_count_bits)) * erc_row_scale_fubini_reduced_projection_rectangle_witness)) /\ exists ff_q_erc_fubini_reduced_projection_rectangle_witness_count_bits_decoded. erc_row_code_fubini_reduced_projection_rectangle_witness = ff_q_erc_fubini_reduced_projection_rectangle_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_reduced_projection_rectangle_witness_count_bits)) * erc_row_scale_fubini_reduced_projection_rectangle_witness) + (ff_bit_erc_fubini_reduced_projection_rectangle_witness_count_bits))) /\ (ff_bit_erc_fubini_reduced_projection_rectangle_witness_count_bits = 0 \/ ff_bit_erc_fubini_reduced_projection_rectangle_witness_count_bits = 1)))))))))

Structural proof guide

Generated structural guide

The reduced-count code in a split prefix is itself a semantic predecessor-width rectangle prefix.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (13), intermediate claims (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00FC eisenstein_fubini_universal

Formal native tactic body

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

Read the argument

Proof checkpoints

39 script commands · 11 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro sh
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro db
  8. L8
    intro dc
  9. L9
    intro tb
  10. L10
    intro tc
02Fix variables and assumptionsL11–14

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro l
  2. L12
    intro hsplit
  3. L13
    intro i
  4. L14
    intro hi
03Establish hstoredL15–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsplit.

  1. L15
    have hstored : ∃ n. ∃ r. ∃ a. BetaAt(bb,bc,i,n) ∧ BetaAt(db,dc,i,r) ∧ BetaAt(tb,tc,i,a) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ m = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,sh,n) ∧ ((∀ z. Lt(z,h) → ∃ m. BetaAt(x,y,z,m) ∧ (m = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ m = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BetaAt(x,y,h,a)) ∧ (BitCount(x,y,h,r) ∧ (a = 0 ∨ a = 1) ∧ n = r + a))Definitions: LtBetaAtBitCount
  2. L16
    specialize hsplit i
  3. L17
    apply hsplit
  4. L18
    exact hi
04Separate the logical casesL19–28

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hstored
  2. L20
    cases hstored_witness
  3. L21
    cases hstored_witness_witness
  4. L22
    cases hstored_witness_witness_witness
  5. L23
    cases hstored_witness_witness_witness_left
  6. L24
    cases hstored_witness_witness_witness_left_left
  7. L25
    cases hstored_witness_witness_witness_right
  8. L26
    cases hstored_witness_witness_witness_right_witness
  9. L27
    cases hstored_witness_witness_witness_right_witness_witness
  10. L28
    cases hstored_witness_witness_witness_right_witness_witness_left
05Separate the logical casesL29–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hstored_witness_witness_witness_right_witness_witness_left_right
  2. L30
    cases hstored_witness_witness_witness_right_witness_witness_right
  3. L31
    cases hstored_witness_witness_witness_right_witness_witness_right_left
06Construct an explicit witnessL32–32

Supply the displayed value, then prove that it has the required property.

  1. L32
    exists x1
07Separate the logical casesL33–33

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L33
    split
08Use earlier factsL34–34

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L34
    exact hstored_witness_witness_witness_left_left_right
09Construct an explicit witnessL35–36

Supply the displayed value, then prove that it has the required property.

  1. L35
    exists x3
  2. L36
    exists x4
10Separate the logical casesL37–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L37
    split
11Use earlier factsL38–39

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    exact hstored_witness_witness_witness_right_witness_witness_left_right_left
  2. L39
    exact hstored_witness_witness_witness_right_witness_witness_right_left_left

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro sh
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro db
  8. 0008intro dc
  9. 0009intro tb
  10. 0010intro tc
  11. 0011intro l
  12. 0012intro hsplit
  13. 0013intro i
  14. 0014intro hi
  15. 0015have hstored : exists n r a. (((((((exists ff_h_efrd_fubini_reduced_projection_stored_outer_entry. ff_h_efrd_fubini_reduced_projection_stored_outer_entry + S (n) = S ((S (i)) * bc)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_outer_entry. bb = ff_q_efrd_fubini_reduced_projection_stored_outer_entry * S ((S (i)) * bc) + (n))) /\ (((exists ff_h_efrd_fubini_reduced_projection_stored_reduced_entry. ff_h_efrd_fubini_reduced_projection_stored_reduced_entry + S (r) = S ((S (i)) * dc)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_reduced_entry. db = ff_q_efrd_fubini_reduced_projection_stored_reduced_entry * S ((S (i)) * dc) + (r)))) /\ (((exists ff_h_efrd_fubini_reduced_projection_stored_terminal_entry. ff_h_efrd_fubini_reduced_projection_stored_terminal_entry + S (a) = S ((S (i)) * tc)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_terminal_entry. tb = ff_q_efrd_fubini_reduced_projection_stored_terminal_entry * S ((S (i)) * tc) + (a)))) /\ (exists efrd_row_code_fubini_reduced_projection_stored_split efrd_row_scale_fubini_reduced_projection_stored_split. (((((forall eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix. (exists eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_bound. eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_bound + S (eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_reduced_projection_stored_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_reduced_projection_stored_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_reduced_projection_stored_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_reduced_projection_stored_split_successor_prefix) = S ((S (eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_eri_efrd_fubini_reduced_projection_stored_split_successor_prefix_decoded. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_eri_efrd_fubini_reduced_projection_stored_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (eri_bit_efrd_fubini_reduced_projection_stored_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_reduced_projection_stored_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_reduced_projection_stored_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_stored_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_reduced_projection_stored_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_reduced_projection_stored_split_successor_count_sum ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_start. ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_start. ff_u_efrd_fubini_reduced_projection_stored_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_terminal. ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_terminal + S (n) = S ((S (sh)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_terminal. ff_u_efrd_fubini_reduced_projection_stored_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum) + (n))) /\ forall ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum. (exists ff_lt_efrd_fubini_reduced_projection_stored_split_successor_count_sum_bound. ff_lt_efrd_fubini_reduced_projection_stored_split_successor_count_sum_bound + S ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_reduced_projection_stored_split_successor_count_sum ff_r_efrd_fubini_reduced_projection_stored_split_successor_count_sum ff_s_efrd_fubini_reduced_projection_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_summand. ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_summand + S (ff_a_efrd_fubini_reduced_projection_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_summand. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (ff_a_efrd_fubini_reduced_projection_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_partial. ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_partial + S (ff_r_efrd_fubini_reduced_projection_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_partial. ff_u_efrd_fubini_reduced_projection_stored_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum) + (ff_r_efrd_fubini_reduced_projection_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_successor. ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_sum_successor + S (ff_s_efrd_fubini_reduced_projection_stored_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_successor. ff_u_efrd_fubini_reduced_projection_stored_split_successor_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_successor_count_sum) + (ff_s_efrd_fubini_reduced_projection_stored_split_successor_count_sum))) /\ ff_s_efrd_fubini_reduced_projection_stored_split_successor_count_sum = ff_r_efrd_fubini_reduced_projection_stored_split_successor_count_sum + ff_a_efrd_fubini_reduced_projection_stored_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_bits. (exists ff_lt_efrd_fubini_reduced_projection_stored_split_successor_count_bits_bound. ff_lt_efrd_fubini_reduced_projection_stored_split_successor_count_bits_bound + S ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_reduced_projection_stored_split_successor_count_bits. ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_bits_decoded. ff_h_efrd_fubini_reduced_projection_stored_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_reduced_projection_stored_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_bits)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_bits_decoded. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_efrd_fubini_reduced_projection_stored_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_successor_count_bits)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (ff_bit_efrd_fubini_reduced_projection_stored_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_reduced_projection_stored_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_reduced_projection_stored_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix. (exists eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_bound. eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_bound + S (eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_reduced_projection_stored_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_reduced_projection_stored_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_reduced_projection_stored_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_reduced_projection_stored_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_eri_efrd_fubini_reduced_projection_stored_split_reduced_prefix_decoded. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_eri_efrd_fubini_reduced_projection_stored_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (eri_bit_efrd_fubini_reduced_projection_stored_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_reduced_projection_stored_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_reduced_projection_stored_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_reduced_projection_stored_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_reduced_projection_stored_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_reduced_projection_stored_split_terminal_entry. ff_h_efrd_fubini_reduced_projection_stored_split_terminal_entry + S (a) = S ((S (h)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_terminal_entry. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_efrd_fubini_reduced_projection_stored_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (a))))) /\ (((((exists ff_u_efrd_fubini_reduced_projection_stored_split_reduced_count_sum ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_start. ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_start. ff_u_efrd_fubini_reduced_projection_stored_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_terminal. ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_terminal + S (r) = S ((S (h)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_terminal. ff_u_efrd_fubini_reduced_projection_stored_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) + (r))) /\ forall ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum. (exists ff_lt_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_bound. ff_lt_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_bound + S ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_reduced_projection_stored_split_reduced_count_sum ff_r_efrd_fubini_reduced_projection_stored_split_reduced_count_sum ff_s_efrd_fubini_reduced_projection_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_summand. ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_summand. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (ff_a_efrd_fubini_reduced_projection_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_partial. ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_partial. ff_u_efrd_fubini_reduced_projection_stored_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) + (ff_r_efrd_fubini_reduced_projection_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_successor. ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_successor. ff_u_efrd_fubini_reduced_projection_stored_split_reduced_count_sum = ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_reduced_projection_stored_split_reduced_count_sum) + (ff_s_efrd_fubini_reduced_projection_stored_split_reduced_count_sum))) /\ ff_s_efrd_fubini_reduced_projection_stored_split_reduced_count_sum = ff_r_efrd_fubini_reduced_projection_stored_split_reduced_count_sum + ff_a_efrd_fubini_reduced_projection_stored_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_bits. (exists ff_lt_efrd_fubini_reduced_projection_stored_split_reduced_count_bits_bound. ff_lt_efrd_fubini_reduced_projection_stored_split_reduced_count_bits_bound + S ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_reduced_projection_stored_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_bits_decoded. ff_h_efrd_fubini_reduced_projection_stored_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_reduced_projection_stored_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_reduced_projection_stored_split)) /\ exists ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_bits_decoded. efrd_row_code_fubini_reduced_projection_stored_split = ff_q_efrd_fubini_reduced_projection_stored_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_reduced_projection_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_reduced_projection_stored_split) + (ff_bit_efrd_fubini_reduced_projection_stored_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_reduced_projection_stored_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_reduced_projection_stored_split_reduced_count_bits = 1))))) /\ (a = 0 \/ a = 1)) /\ n = r + a))))))
  16. 0016specialize hsplit i
  17. 0017apply hsplit
  18. 0018exact hi
  19. 0019cases hstored
  20. 0020cases hstored_witness
  21. 0021cases hstored_witness_witness
  22. 0022cases hstored_witness_witness_witness
  23. 0023cases hstored_witness_witness_witness_left
  24. 0024cases hstored_witness_witness_witness_left_left
  25. 0025cases hstored_witness_witness_witness_right
  26. 0026cases hstored_witness_witness_witness_right_witness
  27. 0027cases hstored_witness_witness_witness_right_witness_witness
  28. 0028cases hstored_witness_witness_witness_right_witness_witness_left
  29. 0029cases hstored_witness_witness_witness_right_witness_witness_left_right
  30. 0030cases hstored_witness_witness_witness_right_witness_witness_right
  31. 0031cases hstored_witness_witness_witness_right_witness_witness_right_left
  32. 0032exists x1
  33. 0033split
  34. 0034exact hstored_witness_witness_witness_left_left_right
  35. 0035exists x3
  36. 0036exists x4
  37. 0037split
  38. 0038exact hstored_witness_witness_witness_right_witness_witness_left_right_left
  39. 0039exact hstored_witness_witness_witness_right_witness_witness_right_left_left