PA00F1

eisenstein_successor_row_split_decoded_add

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

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

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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro sh
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro 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