PA00F1

eisenstein_successor_row_split_decoded_add

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

Every aligned decoded successor count is exactly its decoded reduced count plus terminal bit.

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 i n r a. (forall efrd_row_index_fubini_row_split_semantic_prefix. (exists efrd_lt_gap_fubini_row_split_semantic_prefix_bound. efrd_lt_gap_fubini_row_split_semantic_prefix_bound + S (efrd_row_index_fubini_row_split_semantic_prefix) = l) -> exists efrd_count_fubini_row_split_semantic_prefix efrd_reduced_count_fubini_row_split_semantic_prefix efrd_terminal_bit_fubini_row_split_semantic_prefix. (((((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_outer_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_outer_entry + S (efrd_count_fubini_row_split_semantic_prefix) = S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * bc)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_outer_entry. bb = ff_q_efrd_fubini_row_split_semantic_prefix_entry_outer_entry * S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * bc) + (efrd_count_fubini_row_split_semantic_prefix))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry + S (efrd_reduced_count_fubini_row_split_semantic_prefix) = S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * dc)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry. db = ff_q_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry * S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * dc) + (efrd_reduced_count_fubini_row_split_semantic_prefix)))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry + S (efrd_terminal_bit_fubini_row_split_semantic_prefix) = S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * tc)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry. tb = ff_q_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry * S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * tc) + (efrd_terminal_bit_fubini_row_split_semantic_prefix)))) /\ (exists efrd_row_code_fubini_row_split_semantic_prefix_entry_split efrd_row_scale_fubini_row_split_semantic_prefix_entry_split. (((((forall eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix))) \/ (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_semantic_prefix) = S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (efrd_count_fubini_row_split_semantic_prefix))) /\ forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum + ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix))) \/ (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_semantic_prefix) = S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (efrd_terminal_bit_fubini_row_split_semantic_prefix))))) /\ (((((exists ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_semantic_prefix) = S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_semantic_prefix))) /\ forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum + ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_semantic_prefix = 0 \/ efrd_terminal_bit_fubini_row_split_semantic_prefix = 1)) /\ efrd_count_fubini_row_split_semantic_prefix = efrd_reduced_count_fubini_row_split_semantic_prefix + efrd_terminal_bit_fubini_row_split_semantic_prefix))))))) -> (exists efrd_lt_gap_fubini_row_split_semantic_bound. efrd_lt_gap_fubini_row_split_semantic_bound + S (i) = l) -> (((exists ff_h_fubini_row_split_semantic_source. ff_h_fubini_row_split_semantic_source + S (n) = S ((S (i)) * bc)) /\ exists ff_q_fubini_row_split_semantic_source. bb = ff_q_fubini_row_split_semantic_source * S ((S (i)) * bc) + (n))) -> (((exists ff_h_fubini_row_split_semantic_reduced. ff_h_fubini_row_split_semantic_reduced + S (r) = S ((S (i)) * dc)) /\ exists ff_q_fubini_row_split_semantic_reduced. db = ff_q_fubini_row_split_semantic_reduced * S ((S (i)) * dc) + (r))) -> (((exists ff_h_fubini_row_split_semantic_terminal. ff_h_fubini_row_split_semantic_terminal + S (a) = S ((S (i)) * tc)) /\ exists ff_q_fubini_row_split_semantic_terminal. tb = ff_q_fubini_row_split_semantic_terminal * S ((S (i)) * tc) + (a))) -> n = r + a

Structural proof guide

Generated structural guide

Every aligned decoded successor count is exactly its decoded reduced count plus terminal bit.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (10), intermediate claims (5), equality transport (3).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA00F2 eisenstein_successor_row_split_sum_add

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

67 script commands · 9 reading checkpoints · 5 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.

Named ingredients (1)
beta at unique

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–20

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

  1. L11
    intro l
  2. L12
    intro i
  3. L13
    intro n
  4. L14
    intro r
  5. L15
    intro a
  6. L16
    intro hprefix
  7. L17
    intro hi
  8. L18
    intro hn
  9. L19
    intro hr
  10. L20
    intro ha
03Establish hstoredL21–24

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

  1. L21
    have hstored : ∃ storedn. ∃ storedr. ∃ storeda. BetaAt(bb,bc,i,storedn) ∧ BetaAt(db,dc,i,storedr) ∧ BetaAt(tb,tc,i,storeda) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,sh,storedn) ∧ ((∀ z. Lt(z,h) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BetaAt(x,y,h,storeda)) ∧ (BitCount(x,y,h,storedr) ∧ (storeda = 0 ∨ storeda = 1) ∧ storedn = storedr + storeda))Definitions: LtBetaAtBitCount
  2. L22
    specialize hprefix i
  3. L23
    apply hprefix
  4. L24
    exact hi
04Separate the logical casesL25–30

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

  1. L25
    cases hstored
  2. L26
    cases hstored_witness
  3. L27
    cases hstored_witness_witness
  4. L28
    cases hstored_witness_witness_witness
  5. L29
    cases hstored_witness_witness_witness_left
  6. L30
    cases hstored_witness_witness_witness_left_left
05Establish hsource_eqL31–39

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

  1. L31
    have hsource_eq : x = n
  2. L32
    specialize beta_at_unique bb
  3. L33
    specialize beta_at_unique bc
  4. L34
    specialize beta_at_unique i
  5. L35
    specialize beta_at_unique x
  6. L36
    specialize beta_at_unique n
  7. L37
    apply beta_at_unique
  8. L38
    exact hstored_witness_witness_witness_left_left_left
  9. L39
    exact hn
06Establish hreduced_eqL40–48

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

  1. L40
    have hreduced_eq : x1 = r
  2. L41
    specialize beta_at_unique db
  3. L42
    specialize beta_at_unique dc
  4. L43
    specialize beta_at_unique i
  5. L44
    specialize beta_at_unique x1
  6. L45
    specialize beta_at_unique r
  7. L46
    apply beta_at_unique
  8. L47
    exact hstored_witness_witness_witness_left_left_right
  9. L48
    exact hr
07Establish hterminal_eqL49–57

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

  1. L49
    have hterminal_eq : x2 = a
  2. L50
    specialize beta_at_unique tb
  3. L51
    specialize beta_at_unique tc
  4. L52
    specialize beta_at_unique i
  5. L53
    specialize beta_at_unique x2
  6. L54
    specialize beta_at_unique a
  7. L55
    apply beta_at_unique
  8. L56
    exact hstored_witness_witness_witness_left_right
  9. L57
    exact ha
08Separate the logical casesL58–61

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

  1. L58
    cases hstored_witness_witness_witness_right
  2. L59
    cases hstored_witness_witness_witness_right_witness
  3. L60
    cases hstored_witness_witness_witness_right_witness_witness
  4. L61
    cases hstored_witness_witness_witness_right_witness_witness_right
09Establish heqL62–67

Establish this local claim before using it. It is not an additional assumption.

  1. L62
    have heq : x = x1 + x2
  2. L63
    exact hstored_witness_witness_witness_right_witness_witness_right_right
  3. L64
    rewrite hsource_eq at heq
  4. L65
    rewrite hreduced_eq at heq
  5. L66
    rewrite hterminal_eq at heq
  6. L67
    exact heq

Library-wide reading audit

Original exact command ledger · 67 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 i
  13. 0013intro n
  14. 0014intro r
  15. 0015intro a
  16. 0016intro hprefix
  17. 0017intro hi
  18. 0018intro hn
  19. 0019intro hr
  20. 0020intro ha
  21. 0021have hstored : exists storedn storedr storeda. (((((((exists ff_h_efrd_fubini_row_split_semantic_stored_outer_entry. ff_h_efrd_fubini_row_split_semantic_stored_outer_entry + S (storedn) = S ((S (i)) * bc)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_outer_entry. bb = ff_q_efrd_fubini_row_split_semantic_stored_outer_entry * S ((S (i)) * bc) + (storedn))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_stored_reduced_entry. ff_h_efrd_fubini_row_split_semantic_stored_reduced_entry + S (storedr) = S ((S (i)) * dc)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_reduced_entry. db = ff_q_efrd_fubini_row_split_semantic_stored_reduced_entry * S ((S (i)) * dc) + (storedr)))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_stored_terminal_entry. ff_h_efrd_fubini_row_split_semantic_stored_terminal_entry + S (storeda) = S ((S (i)) * tc)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_terminal_entry. tb = ff_q_efrd_fubini_row_split_semantic_stored_terminal_entry * S ((S (i)) * tc) + (storeda)))) /\ (exists efrd_row_code_fubini_row_split_semantic_stored_split efrd_row_scale_fubini_row_split_semantic_stored_split. (((((forall eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal + S (storedn) = S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (storedn))) /\ forall ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum + ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_stored_split_terminal_entry. ff_h_efrd_fubini_row_split_semantic_stored_split_terminal_entry + S (storeda) = S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_terminal_entry. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (storeda))))) /\ (((((exists ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal + S (storedr) = S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (storedr))) /\ forall ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum + ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits = 1))))) /\ (storeda = 0 \/ storeda = 1)) /\ storedn = storedr + storeda))))))
  22. 0022specialize hprefix i
  23. 0023apply hprefix
  24. 0024exact hi
  25. 0025cases hstored
  26. 0026cases hstored_witness
  27. 0027cases hstored_witness_witness
  28. 0028cases hstored_witness_witness_witness
  29. 0029cases hstored_witness_witness_witness_left
  30. 0030cases hstored_witness_witness_witness_left_left
  31. 0031have hsource_eq : x = n
  32. 0032specialize beta_at_unique bb
  33. 0033specialize beta_at_unique bc
  34. 0034specialize beta_at_unique i
  35. 0035specialize beta_at_unique x
  36. 0036specialize beta_at_unique n
  37. 0037apply beta_at_unique
  38. 0038exact hstored_witness_witness_witness_left_left_left
  39. 0039exact hn
  40. 0040have hreduced_eq : x1 = r
  41. 0041specialize beta_at_unique db
  42. 0042specialize beta_at_unique dc
  43. 0043specialize beta_at_unique i
  44. 0044specialize beta_at_unique x1
  45. 0045specialize beta_at_unique r
  46. 0046apply beta_at_unique
  47. 0047exact hstored_witness_witness_witness_left_left_right
  48. 0048exact hr
  49. 0049have hterminal_eq : x2 = a
  50. 0050specialize beta_at_unique tb
  51. 0051specialize beta_at_unique tc
  52. 0052specialize beta_at_unique i
  53. 0053specialize beta_at_unique x2
  54. 0054specialize beta_at_unique a
  55. 0055apply beta_at_unique
  56. 0056exact hstored_witness_witness_witness_left_right
  57. 0057exact ha
  58. 0058cases hstored_witness_witness_witness_right
  59. 0059cases hstored_witness_witness_witness_right_witness
  60. 0060cases hstored_witness_witness_witness_right_witness_witness
  61. 0061cases hstored_witness_witness_witness_right_witness_witness_right
  62. 0062have heq : x = x1 + x2
  63. 0063exact hstored_witness_witness_witness_right_witness_witness_right_right
  64. 0064rewrite hsource_eq at heq
  65. 0065rewrite hreduced_eq at heq
  66. 0066rewrite hterminal_eq at heq
  67. 0067exact heq